lean_reference.md

Lean theorem reference

Latest generated audit. Declaration counts and build budgets are injected via [[VAR:lean_*]] tokens from output/data/manuscript_variables.json (regenerated by scripts/manuscript_variables.py). The boundary fragment under ../../lean/ActinfPolicyEntanglement/ remains sorry-free, axiom-free, Mathlib-import-free, and unsafe/partial/noncomputable-free on the stock Lean pin in lean/lean-toolchain.

A per-theorem status table for everything under ../../lean/ActinfPolicyEntanglement/. The status column is one of:

• proved — full proof, no sorry.
• forwarder — proved by forwarding to another theorem.
• boundary — type-checked statement whose closed-form / algebraic content is supplied as a hypothesis or threaded through definitional unfolding; the theorem certifies the boundary identity without any sorry of its own.
• witness — boundary form whose existence claim is supplied by a structure parameter; the theorem certifies the witness without any sorry of its own. Used for theorems whose analytic content (KL chain rule, real-analytic continuity, matrix SVD, tensor-train rank envelopes, measure tightness) is scoped to a separate Mathlib4 analytic-discharge layer. The retired sketch and deferred buckets appear only in revision history. They are no longer legal current statuses in manuscript/refs/labels.yaml; the status-table tests reject them.

The boundary fragment is sorry-free, axiom-free, and unsafe/partial/noncomputable-free. Refresh hygiene with:

uv run python scripts/build_lean.py     # asserts the budget is 0

Witness-contract summary

The boundary fragment exposes analytic content as witness-consuming theorems: the caller supplies a structure-packaged analytic witness, and the boundary theorem certifies it. The witness boundary is the API contract; a separate Mathlib4 discharge layer can construct those witness structures from library lemmas without touching the existing boundary files.

Witness theorem	File	Manuscript ref	Witness structure	Mathlib lemma needed	Numerical companion (Python)
dualFlat_pythagorean_witness	Geometry.lean	Prop 7.5	PythagoreanWitness with tie-ins for klVal, tcVal, and residual plus the analytic identity	Mathlib.InformationTheory.KullbackLeibler.Basic (KL chain rule, when Bregman / KL-decomposition lemmas land)	src/lean/geometry.py::pythagorean_residual
entangledFamily_eGeodesic	Geometry.lean	Thm 7.4	(forwarder; no extra witness)	none — derived from couplingLogWeight_affine_in_lam	src/lean/coupling.py::entangled_log_weight_affine_in_lambda
entanglement_decomposition	Decomposition.lean	Thm 5.1	EntanglementDecomposition (4-term split)	algebraic identity (proven in Constructive.lean for the canonical case)	src/lean/decomposition.py::entanglement_decomposition_rhs
couplingTax_quadratic_bound	Heterogeneous.lean	Thm 9.1	BoundedQuadraticTax {C, C_nonneg, bound}	a Bregman-Taylor library extending Mathlib.Analysis.Convex.SpecificFunctions.Deriv (Bregman divergence is not yet a Mathlib4 file as of v4.29.0)	src/lean/heterogeneous.py::quadratic_bound
couplingTax_small_lambda_tolerance	Heterogeneous.lean	Cor 9.2	SmallLambdaTolerance {lamMax, lamMax_pos, bound}	Mathlib.Analysis.Calculus.ContDiff (real-analytic continuity at λ=0)	src/lean/heterogeneous.py::small_lambda_tolerance
Spectral.factors_isBipartiteMeanField (converse only)	Spectral.lean	Prop 8.1 (full ⇔)	(forward direction proven; converse via Mathlib outer-product rank)	Mathlib.LinearAlgebra.Matrix.Rank + Matrix.rank_one_outer_product	src/lean/spectral.py::schmidt_decomposition
freeEnergy_convex_in_lam_witness (round 2)	Convexity.lean	Thm 5.6	FreeEnergyConvexityWitness {F_curve, convex, F_at_zero}	Bregman / log-partition convexity (Mathlib.Analysis.Convex.Basic + KL-Bregman lemma when it lands)	src/lean/bernoulli_toy.py::ising_free_energy_curve (closed-form convex curve at K=2)
freeEnergy_localConcavity_at_zero_witness (round 2)	Convexity.lean	Prop 11.1	LocalConcavityAtZero {a₀, a₁, a₂, C, eps, a2_nonpos, eps_pos, bound}	Taylor-expansion lemmas around Real.exp (Mathlib.Analysis.Calculus.Taylor)	numerical Taylor fit consumed by tests/test_witness_theorems.py
markovBlanket_separation_identity_witness (round 2)	MarkovBlanket.lean	Prop 19.3	MarkovBlanketSeparationWitness {Hq, sumStreamEntropies, Iq, sep, Hq_pos, Hq_eq, Iq_eq, Iq_nonneg, sep_eq}	algebraic identity plus KL-non-negativity for Iq ≥ 0; the witness ties Hq/Iq to shannonEntropy/totalCorrelation	src/lean/free_energy.py::total_correlation + shannon_entropy
schmidtRank_upperSemicontinuous_witness (NEW, round 3)	SpectralWitnesses.lean	Prop 8.2	UpperSemicontinuousRankWitness {rank_at_zero, usc}	Mathlib.Topology.Semicontinuous + lower-semicontinuity of matrix rank	src/lean/spectral.py::schmidt_rank
sparsityRank_tradeoff_witness (NEW, round 3)	SpectralWitnesses.lean	Thm 8.3	SparsityRankEnvelope {cut_rank, bond_bound, envelope}	Mathlib.LinearAlgebra.TensorProduct + matrix-rank bounds	src/lean/spectral.py::tensor_train_ranks
hierarchicalAIF_lambda_limit_witness (NEW, round 3)	ConnectionsWitnesses.lean	Thm 17.1	HierarchicalConcentrationWitness {concentrate}	Mathlib.MeasureTheory.Measure.Tight (tightness of families of measures) + KL-projection argument	src/lean/decomposition.py::free_energy_against_entangled_prior
sophisticatedInference_embedding_witness (NEW, round 3)	ConnectionsWitnesses.lean	Prop 17.2	SophisticatedInferenceEmbedding {source, siValue, embed, preserveVFE}	recursive Bellman-style update + KL-control identity for sophisticated inference	src/simulation/inference.py (numerical coupled-policy posterior under λ-deformation)
couplingVerdict_correct (NEW, round 3)	Decomposition.lean	Cor 5.2	none — decide_eq_true_iff discharge	none — boundary-fragment Bool/decide identity	src/lean/decomposition.py::coupling_pays_for_itself

How to read this table:

• "Witness structure" — the analytic content consumed at the boundary. A Mathlib4 discharge layer can supply an instance; today, the Python companion supplies a numerical witness verified to floating tolerance by the test suite.
• "Mathlib lemma needed" — the Mathlib4 area a discharge library would use to construct the structure. None of the boundary fragment imports Mathlib; that's the point.
• "Numerical companion" — the Python module that exhibits the witness for a concrete K=2 / Ising / Bernoulli toy, gated by an invariant in src/lean/invariants.py.

For the full per-file theorem inventory (proved / forwarder / witness / deferred status, plus discharge tactic), see the per-file tables below.

Basic.lean

Lean name	Status	Notes
StreamIdx K	abbrev	Fin K
PolicyFactor K	abbrev	StreamIdx K → Type
PolicySpace K Pol	def	∀ k, Pol k
IsPlanningStream	def	0 < horizon
IsReflexiveStream	def	horizon = 0
instDecidableIsPlanningStream	proved	forwarder to Nat.decLt
instDecidableIsReflexiveStream	proved	forwarder to Nat.decEq
stream_classification	proved	cases horizon then Or.inl/inr

Scalar.lean (NEW)

The abstract scalar interface used by the algebraic theorems. Stays Mathlib-free by phrasing each ring law as a typeclass field.

Lean name	Status	Notes
CommScalar α	class	extends Add/Mul/Sub/Neg/Zero/One; 14 ring-law fields
CommScalar.mul_sub	proved	derived from sub_def + mul_add + mul_neg
CommScalar.sub_mul	proved	derived via mul_comm
CommScalar.sub_self	proved	derived from sub_def + add_neg_self
CommScalar.affine_diff	proved	core algebraic identity for couplingLogWeight_affine_in_lam
CommScalar.affine_at_zero	proved	core algebraic identity for couplingLogWeight_at_zero
instance : CommScalar Int	proved	forwarders to Int.add_comm, Int.mul_assoc, etc.

JointDist.lean

Lean name	Status	Notes
JointDist K Pol	abbrev	PolicySpace K Pol → Float
MFDist K Pol	abbrev	∀ k, Pol k → Float
IsNonNeg	def	pointwise 0 ≤ q π
IsPMF	def	exists list-support summing to 1.0
mfProductWeight	def	terminating fold over Fin K
mfToJoint	def	embed mean-field factors into joint
IsMeanField	def	exists factors m s.t. q = mfToJoint m

Coupling.lean

Lean name	Status	Notes
CouplingPotential α K Pol	abbrev	PolicySpace K Pol → α, polymorphic
trivialCoupling	def	fun _ => 0, requires [Zero α]
couplingLogWeight	def	λ·J(π) − γ·λ·K_c(π), requires [Mul α] [Sub α]
entangledPosteriorLogWeight	def	logE − γ·G + couplingLogWeight, requires [Add α] [Mul α] [Sub α]
couplingLogWeight_affine_in_lam	proved	unfold + CommScalar.affine_diff
couplingLogWeight_at_zero	proved	unfold + CommScalar.affine_at_zero

FreeEnergy.lean

Lean name	Status	Notes
supportSum	def	List.foldr reducer (no Finset)
logFloor, safeLog	def	1e-300 floor + Float.log
shannonEntropy, kl, totalCorrelation	def	boundary forms
variationalFreeEnergy, marginalFreeEnergy	def	boundary forms
totalCorrelation_eq_kl_to_mprojection	witness	unfold; exact hWitness (Prop 7.3)

Geometry.lean

Lean name	Status	Notes
mfImage_isMeanField	proved	⟨m, fun π => rfl⟩ (Prop 7.1; round-3 relabel sketch → proved after audit confirmed the existing constructive proof)
supportSum_pointwise_eq (private)	proved	congrArg (supportSum s) (funext h)
mProjection_kl_eq_self_when_meanfield	proved	unfold kl + supportSum_pointwise_eq + rw [← h π] (Prop 7.2 boundary form: kl q (mfToJoint m) = kl q q)
entangledFamily_eGeodesic	forwarder	uses couplingLogWeight_affine_in_lam (Thm 7.4)
dualFlat_pythagorean_witness	witness	extracts a PythagoreanWitness whose fields tie klVal, tcVal, and residual to boundary primitives (Prop 7.5)

Spectral.lean

Lean name	Status	Notes
Bipartite.BipartiteJoint	abbrev	Pol1 → Pol2 → Float
Bipartite.IsBipartiteMeanField	def	exists outer-product factorization
Bipartite.isBipartiteMeanField_factors	proved	forward direction of Prop 8.1 (constructively true)
Bipartite.factors_isBipartiteMeanField	proved	converse direction of Prop 8.1

The full Schmidt-rank-1 ⇔ mean-field characterization requires Mathlib's Matrix.rank_one_outer_product; the boundary fragment ships only the constructively-true factorization witnesses. The upper-semicontinuity claim (Prop 8.2) and the tensor-train sparsity-rank tradeoff (Thm 8.3) are shipped in witness form in the new SpectralWitnesses.lean (round 3); the analytic payload of each witness — semicontinuity bookkeeping for matrix rank, tensor-train rank envelopes — remains for the Mathlib refinement.

Heterogeneous.lean

Lean name	Status	Notes
HorizonProfile K	abbrev	StreamIdx K → Nat
couplingTax	def	taxFunction λ − taxFunction 0
BoundedQuadraticTax	structure	{C, C_nonneg, bound} envelope witness
couplingTax_quadratic_bound (Thm 9.1)	witness	Theorem 9.1; coupling tax bound; witness-form
SmallLambdaTolerance	structure	{lamMax, lamMax_pos, bound} tolerance witness
couplingTax_small_lambda_tolerance (Cor 9.2)	witness	extracts the tolerance from a SmallLambdaTolerance witness

BernoulliToy.lean

All binary types and helpers proved or definitional; closed-form formulas verified to floating tolerance by the Python companion src/lean/bernoulli_toy.py.

Lean name	Status
Action, BinaryMF, BinaryJoint, BinaryCoupling	abbrev
floatExp, floatLog, floatLogistic, floatArctanh	def
alignedIndicator, isingCoupling	def
xLogX, binaryEntropy, isingMutualInformation	def
optimalLambda, isingFreeEnergyCurve	def
lambdaC1, lambdaC2, couplingPhaseAt	def
isingMI_zero_at_zero	proved (⟨..., rfl⟩)
isingFreeEnergyCurve_total	proved (⟨..., rfl⟩)

Decomposition.lean

Theorem 5.1 plus four corollaries (5.2–5.5). Round 3 upgraded Cor 5.2 (couplingVerdict) from sketch to proved by adding the correctness theorem couplingVerdict_correct (boundary identity couplingVerdict gain tax = true ↔ tax < gain) plus two convenience extractors.

Lean name	Status	Notes
couplingExpectationSkeleton	def	threads (J, K_c, γ, λ) through couplingLogWeight integrated against q
entanglement_decomposition (Thm 5.1)	witness	takes the Mathlib-supplied algebraic split, certifies it; every coupling parameter appears in the conclusion
couplingVerdict (Cor 5.2 helper)	def	Boolean verdict via decide (tax < gain)
couplingVerdict_correct (Cor 5.2) (NEW, round 3)	proved	unfold + decide_eq_true_iff: certifies couplingVerdict gain tax = true ↔ tax < gain
couplingVerdict_sound (NEW, round 3)	proved	forward extractor (true → tax < gain)
couplingVerdict_complete (NEW, round 3)	proved	reverse extractor (tax < gain → true)
couplingLogWeight_pointwise_at_zero (Cor 5.3)	proved	forwarder to couplingLogWeight_at_zero
totalCorrelation_def_unfold (Cor 5.4)	boundary	rfl (totalCorrelation = kl q q by definition); the substantive strict-gain claim is a typed boundary witness (cor_4_4 is status: boundary), with strict-negativity the Mathlib extension
freeEnergy_closedForm_witness (Thm 5.5)	boundary	witness-consuming closed-form F[q_λ] = log Z_E − log Z
freeEnergy_closedForm_at_zero (corollary of Thm 5.5)	proved	algebraic skeleton of the λ = 0 collapse to F = -log Z

Monotonicity.lean (constructive sub-fragment)

Constructive lemmas about Nat, Or, And, List, and Fin. Demonstrates that the boundary skeleton supports non-vacuous structural reasoning.

Lean name	Discharge
nat_le_refl, nat_le_trans	Nat.le_refl/Nat.le_trans
nat_succ_pos, nat_zero_le, nat_le_succ, nat_lt_succ_self	Nat.* forwarders
or_self_iff, or_comm_iff, and_self_iff	constructive
list_length_nonneg, list_length_cons	Nat.zero_le _ / rfl
list_length_append	induction + omega
list_append_nil	induction + rw
list_nil_append	rfl
fin_lt_size, fin_zero_lt	k.isLt / rfl

Constructive.lean (CommScalar-polymorphic boundary lemmas)

Substantive = 0 proofs (not vacuous reflexivity) thanks to the CommScalar typeclass.

Lean name	Discharge
entangledPosteriorLogWeight_at_zero	unfold + couplingLogWeight_at_zero + CommScalar.add_zero
couplingLogWeight_trivialCoupling	unfold + CommScalar.mul_zero + CommScalar.sub_self
couplingNormSq_of_trivialCoupling	CommScalar.zero_mul 0
couplingTax_zero_at_zero	rw [h, CommScalar.sub_self]

Convexity.lean (NEW, round 2)

Theorem 5.6 (convexity of F[q_λ] in λ) and Proposition 11.1 (local Taylor-form concavity at λ = 0), both stated in witness-consuming boundary form. Each witness anchors F at λ = 0 via couplingLogWeight_at_zero so that (J, K_c, γ) are genuinely referenced and the boundary statement is non-vacuous.

Lean name	Status	Notes
FreeEnergyConvexityWitness	structure	{F_curve, convex, F_at_zero} — convex curve + λ = 0 anchor value
freeEnergy_convex_in_lam_witness (Thm 5.6)	witness	refine ⟨witness.convex, ?_⟩; intro π; exact couplingLogWeight_at_zero …
LocalConcavityAtZero	structure	{a₀, a₁, a₂, C, eps, a2_nonpos, eps_pos, bound} — Taylor coefficients + cubic remainder envelope + window [0, eps]
freeEnergy_localConcavity_at_zero_witness (Prop 11.1)	witness	extracts (a2_nonpos, eps_pos, bound) from a LocalConcavityAtZero witness plus the λ = 0 anchor

MarkovBlanket.lean (NEW, round 2)

Proposition 19.3 — the Markov-blanket separation identity sep = 1 − I(q) / H(q), stated in witness-consuming boundary form with tie-in equalities that bind Hq and Iq to the boundary-fragment primitives shannonEntropy q s and totalCorrelation q s.

Lean name	Status	Notes
MarkovBlanketSeparationWitness	structure	{Hq, Iq, sep, Hq_pos, Hq_eq, Iq_eq, sep_eq} — entropy positivity + tie-ins + algebraic identity
markovBlanket_separation_identity_witness (Prop 19.3)	witness	one-line proof: ⟨witness.Hq_pos, witness.Hq_eq, witness.Iq_eq, witness.sep_eq⟩

SpectralWitnesses.lean (NEW, round 3)

Proposition 8.2 (Schmidt rank upper-semicontinuous in λ) and Theorem 8.3 (sparsity-rank tradeoff for tensor-train coupling), both stated in witness-consuming boundary form. Each witness packages the analytic / tensor-train content as a structural hypothesis and the boundary fragment certifies the existence claim by extracting fields.

Lean name	Status	Notes
UpperSemicontinuousRankWitness	structure	{rank_at_zero, usc} — mean-field anchor (rankCurve 0 = 1) + tolerance-window upper-semicontinuity
schmidtRank_upperSemicontinuous_witness (Prop 8.2)	witness	one-line extractor: ⟨witness.rank_at_zero, witness.usc⟩
SparsityRankEnvelope	structure	{cut_rank, bond_bound, envelope} — per-cut bond-dimension envelope for K-stream tensor-train coupling
sparsityRank_tradeoff_witness (Thm 8.3)	witness	extractor: witness.envelope
sparsityRank_meanField_at_zero (corollary)	proved	rw + Nat.le_refl 1: mean-field anchor of cut ranks at λ = 0

ConnectionsWitnesses.lean (NEW, round 3)

Theorem 17.1 (hierarchical AIF as the λ → ∞ limit) and Proposition 17.2 (sophisticated-inference embedding), both stated in witness- consuming boundary form. Each witness threads through the boundary- fragment primitives kl and variationalFreeEnergy so the statements are non-vacuous.

Lean name	Status	Notes
HierarchicalConcentrationWitness	structure	{concentrate} — for every ε > 0 there exists λ₀ > 0 such that every λ ≥ λ₀ satisfies kl (qFamily λ) q_infty support ≤ ε
hierarchicalAIF_lambda_limit_witness (Thm 17.1)	witness	extractor: witness.concentrate
hierarchicalAIF_threshold_exists (helper)	proved	one-shot tightness-window extractor for a fixed ε > 0
SophisticatedInferenceEmbedding	structure	{source, siValue, embed, preserveVFE} — opaque sophisticated-inference source type + value function + embedding into JointDist K Pol + VFE tie-in
sophisticatedInference_embedding_witness (Prop 17.2)	witness	extractor: witness.preserveVFE

Hygiene snapshot (current)

File	sorry count	axiom count	unsafe/partial/noncomputable
Basic.lean	0	0	0
Scalar.lean	0	0	0
JointDist.lean	0	0	0
Coupling.lean	0	0	0
FreeEnergy.lean	0	0	0
Geometry.lean	0	0	0
Spectral.lean	0	0	0
SpectralWitnesses.lean (NEW, round 3)	0	0	0
Heterogeneous.lean	0	0	0
BernoulliToy.lean	0	0	0
Decomposition.lean	0	0	0
Monotonicity.lean	0	0	0
Constructive.lean	0	0	0
Convexity.lean	0	0	0
MarkovBlanket.lean	0	0	0
ConnectionsWitnesses.lean	0	0	0
FepSketches/PolicyEntanglementBoundary.lean	0	0	0
total	0	0	0

The CI gate scripts/build_lean.py enforces this on every run; a single regression returns non-zero and fails the pipeline.

What the Mathlib4 discharge layer adds

A separate lean/MathlibProofs/ library now discharges the headline real-valued decomposition through free_energy_decomposition_full and the general-K finite-KL kernel entanglement_decomposition_generalK. It remains separate from the stock-Lean boundary fragment, and row-specific proof slices should import the boundary fragment and discharge the remaining witness payloads there:

• dualFlat_pythagorean_witness's caller can be derived from the KL chain rule over finite probability spaces.
• BoundedQuadraticTax instances can be constructed from Bregman Taylor expansion over real finite-dimensional charts.
• SmallLambdaTolerance instances can be constructed from real-analytic continuity at λ = 0.
• FreeEnergyConvexityWitness instances (Thm 5.6) can be supplied from log-partition convexity once the finite KL / Bregman bridge is in place.
• LocalConcavityAtZero instances (Prop 11.1) can be constructed from Taylor-expansion lemmas.
• MarkovBlanketSeparationWitness (Prop 19.3) is algebraic at the boundary; a Mathlib extension supplies the entropy / total-correlation numerical primitives.
• The Schmidt-rank-1 ⇔ mean-field characterization can be supplied by Mathlib4 matrix-rank and outer-product lemmas.

Critically, this composes on top of the boundary fragment without touching the existing files: the witness boundary form is the API contract.

Deferred theorems remaining

Zero deferred theorems remain. All twenty manuscript theorems now have a live Lean companion in the boundary fragment. The spectral and connections rows ship witness-consuming theorems plus supporting structures in SpectralWitnesses.lean and ConnectionsWitnesses.lean. Mathlib4 discharge still has work to prove the payloads of those witnesses (Schmidt-rank semicontinuity, tensor-train rank envelopes, measure-tightness arguments, recursive Bellman / KL-control identities), but the boundary-fragment statements themselves are now type-checked and reproduce in [[LEAN:label]] tokens at render time.