One Markdown file per major mathematical object — read the section of the manuscript that introduces it, then come here for the unfolded proof, numerical realization, and Lean status.
| File | Manuscript section | Lean module | Python module |
|---|---|---|---|
basic.md |
§3 setup | Basic |
(no separate mirror) |
scalar_typeclass.md |
(Lean infrastructure) | Scalar |
(typeclass; not directly Python-mirrored) |
joint_dist.md |
§3 (setup, joint / mean-field PMFs) | JointDist |
lean/joint_dist |
coupling.md |
§4 (λ-deformation) | Coupling |
lean/coupling |
decomposition_theorem.md |
§5 (decomposition theorem) | Decomposition |
lean/decomposition |
free_energy.md |
§5 / §7 (total-correlation primitives) | FreeEnergy |
lean/free_energy |
convexity.md |
§5.4 / §11.3 (convexity and local-concavity witnesses) | Convexity |
(realized in lean/free_energy and lean/coupling) |
information_geometry.md |
§7 (information geometry) | Geometry |
lean/geometry |
markov_blanket.md |
§19.3 (Markov-blanket separation) | MarkovBlanket |
(realized in lean/free_energy) |
spectral_structure.md |
§8 (spectral / TT structure; factorization forward/converse) | Spectral |
lean/spectral |
spectral_witnesses.md |
§8.1 / §8.3 (rank-continuity and sparsity-rank witness rows) | SpectralWitnesses |
(realized in lean/spectral; multi-K experiments in scripts/simulate_multi_k.py) |
connections_witnesses.md |
§17 (hierarchical AIF and sophisticated-inference witness rows) | ConnectionsWitnesses |
(realized in lean/decomposition; long-horizon experiment in scripts/simulate_long_horizon.py) |
float_real_residual_witness.md |
Float↔ℝ residual scaffold (roadmap row) | FloatRealResidualWitness |
(roadmap row — residual fields sourced from output/reports/float_real_residual.json; residual tracking in tests/test_meta_files_and_float_residual.py) |
heterogeneous_ensembles.md |
§9 (coupling-tax witnesses) | Heterogeneous |
lean/heterogeneous |
bernoulli_toy.md |
§6 (examples), App. C | BernoulliToy |
lean/bernoulli_toy |
monotonicity.md |
(constructive helper) | Monotonicity |
(no Python mirror) |
constructive.md |
§4 (λ-deformation) / §5 baseline (λ = 0) | Constructive |
(realized in lean/decomposition) |
| GNN fifth track (S08) | S08_gnn_generalized_notation_extension.md |
(empirical; no Lean proof row) | src/gnn/AGENTS.md · reference/python_api_gnn.md |