# Lean 4 Formalization — Quantum Logical Framework

**Build:** `lake build` on Lean 4.30.0-rc2 + Mathlib  
**Status:** CI passing, zero `sorry` blocks across all 211 active modules (registered in [`../lakefile.lean`](../lakefile.lean) roots). This table is the **canonical full per-module index** — [`../CLAUDE.md`](../CLAUDE.md) keeps only a short core-anchor list and points here. The table may trail the roots by a few of the most recent modules.

## What This Formalization Proves

This is not just a type-checked implementation — it is a machine-verified formal proof that:

1. **ZFA is the selection principle for physical reality**: every terminating computation encodes as a ZFA string (`qlf_universality`), and every ZFA string is symmetric (`zfa_implies_critical_line`) — the Church-Turing universe filtered to its ZFA-balanced subset is exactly our physical universe.
2. **Pauli exclusion is a genuine structural constraint**: the matrix commutator of identical ρ-processes is zero (`pauli_exclusion`), and this is non-vacuous — `fermi_nonzero_example` proves [σ_x, σ_z] ≠ 0.
3. **The stable-state count is C(2n, n)**: `find_stable_states_length_even` proves there are exactly C(2n, n) ZFA-stable strings of length 2n — the same combinatorial structure that appears in string mode degeneracy.
4. **Every QLF string has a Hermitian spectral mode**: `toSpectralMode_hermitian` — the physical observables are Hermitian by construction, not postulate.
5. **The Riemann Hypothesis in QLF**: under `spectral_hilbert_polya` (an explicit axiom marking the RCA₀ → WKL₀ boundary), non-trivial zeros lie on the critical line (`riemann_hypothesis_in_qlf`).
6. **Bra-ket notation is RhoQuCalc**: `action f` = ket direction [pos,neg], `lift f` = bra direction [neg,pos], `parallel` = superposition, `sequence` = composition — `bra_ket_always_balanced` proves ZFA balance IS bra-ket well-typedness, machine-verified.

The entire combinatorial core operates strictly within **RCA₀** — the minimum constructive logical subsystem (Harvey Friedman's Reverse Mathematics). No Axiom of Choice, no non-constructive existence, no continuity assumptions. See the [Logical Subsystems](#logical-subsystems-reverse-mathematics) section below.

---

## Active Modules

### Core ZFA Combinatorics

| Module | Description | Key theorems |
|---|---|---|
| [QLF_Axioms.lean](QLF_Axioms.lean) | Types, counting, pruning, ZFA definition | `zfa_implies_critical_line`, `full_prune_invariant`, `single_prune_invariant` |
| [QLF_Combinatorics.lean](QLF_Combinatorics.lean) | Phase-string generation helpers | `expand_generation_list`, `find_stable_states_list` |
| [QLF_QuCalc.lean](QLF_QuCalc.lean) | Phase-generation engine, stable-state filter | `expand_generation`, `find_stable_states`, `qucalc_generates_all_phase_strings` |

### Universality & Computability

| Module | Description | Key theorems |
|---|---|---|
| [QLF_Universality.lean](QLF_Universality.lean) | Every terminating computation IS a ZFA string — Church-Turing completeness in QLF | `encode_is_zfa`, `encode_is_generated`, `qlf_universality`, `encode_is_phase_only` |

### Spectral Structure & Riemann Program

| Module | Description | Key theorems |
|---|---|---|
| [QLF_Critical_Line.lean](QLF_Critical_Line.lean) | ZFA-to-symmetry bridge | `riemann_zfa_critical_line`, `riemann_zfa_critical_line_sym` |
| [QLF_Spectral.lean](QLF_Spectral.lean) | Spectral projector operators; Hermitian structure; Hilbert-Pólya bridge | `toSpectralMode_hermitian`, `spectral_symmetric_eq_scalar_id` |
| [QLF_Riemann.lean](QLF_Riemann.lean) | Riemann hypothesis program | `find_stable_states_iff`, `find_stable_states_length_odd`, `find_stable_states_length_even`, `critical_line_forcing`, `riemann_hypothesis_in_qlf` |

### Physics Layer

| Module | Description | Key theorems |
|---|---|---|
| [SpacetimeDynamics.lean](SpacetimeDynamics.lean) | Pauli-basis Clifford algebra elements; spacetime synthesis | `Form.toMatrix_adjoint`, `Form.equal_and_opposite_self` |
| [RhoQuCalc.lean](RhoQuCalc.lean) | ρ-process algebra; Hermitian structure; ZFA stability; capability-secure concurrency | `parallel_hermitian`, `action_lift_hermitian`, `rho_process_always_zfa`, `rho_process_always_symmetric`, `phase_symmetric_achieves_zfa` |
| [ZFAEventDynamics.lean](ZFAEventDynamics.lean) | ZFA event dynamics; spacetime synthesis; acceleration | `spacetime_from_zfa_preserves_synthesis`, `zfa_dynamics_drive_acceleration` |
| [PauliExclusion.lean](PauliExclusion.lean) | Bosonic vs. fermionic statistics via matrix commutator; Pauli exclusion as genuine constraint | `pauli_exclusion`, `fermi_nonzero_example`, `bosonic_double_occupancy`, `fermi_antisym_action_lift` |
| [BraKetRhoQuCalc.lean](BraKetRhoQuCalc.lean) | Formal correspondence between Dirac bra-ket notation and RhoQuCalc operators in the density-matrix picture; the Σ₈ τ-algebra (`τᵢ=iσᵢ`) and its **weak-isospin su(2)** closure (`[τᵢ,τⱼ]=−2εᵢⱼₖτₖ`, `Q₈⊂SU(2)` — the SU(2) subgroup of the 8-twist algebra, see [Weak_Force.md](../Weak_Force.md)) | `bra_ket_always_balanced`, `pauli_x_sq`, `sigma_comm_xy`, `tau_xy_product`, `tau_comm_xy`, `tau_anticomm_xy`, `weak_isospin_su2`, `trace_preservation_unitary` |
| [QLF_FreeEnergy.lean](QLF_FreeEnergy.lean) | Per-event free-energy decrement at a half-spin ZFA closure (`ΔF = −log 2` nats); MRE saturation bound | `binary_kl_delta_uniform`, `zfa_closure_minimizes_free_energy`, `binary_kl_uniform_lt_log_two` |
| [QLF_Pauli.lean](QLF_Pauli.lean) | The 4-element Pauli scalar group `{+I, −I, +iI, −iI}` (≅ ℤ/4) as the algebraic kernel of the runtime `is_pauli_closed` check: closed under multiplication, associative, with inverses; `pauli_fold` is a multiplicative homomorphism over twist sequences | `PauliScalar.mul_assoc`, `PauliScalar.mul_comm`, `pauli_fold_append`, `pauli_closed_of_admissible_zfa` |
| [QLF_TwistAlphabet.lean](QLF_TwistAlphabet.lean) | The 8-twist alphabet with its explicit σ-matrix mapping (`^v ↔ ±σ_y, <> ↔ ∓σ_x, /\ ↔ ±σ_z, +- ↔ ±I`), bridging the abstract Pauli scalar group to concrete 2×2 matrices. **The keystone: `count_balanced_pauli_closed` — count balance ⟹ Pauli closure for ALL twist histories**, closing the cross-axis-interleaving case (e.g. `^<v>`) that the pair-by-pair theorems left open. Proof spine: the 9 σ-product identities → 16-case `axisMatrix_mul` → `pauliScalarToMatrix_mul`/`psm_comm` → `nf_decomp` (every fold = `phase • axisMatrix(axisProd)`) → the `(ZMod 2)²` axis-parity bridge `axisProd_eq_I_of_countBalanced`. So runtime ZFA (`is_count_balanced ∧ is_pauli_closed`) is Lean-anchored end-to-end | `hermitian_pair_is_pauli_scalar`, `concat_pairs_is_pauli_scalar`, `sigma_xy`, `axisMatrix_mul`, `pauliScalarToMatrix_mul`, `nf_decomp`, `axisProd_eq_I_of_countBalanced`, `count_balanced_pauli_closed` |
| [QLF_AlphabetNecessity.lean](QLF_AlphabetNecessity.lean) | **Why the alphabet has exactly eight twists — the size is quantized, and six is impossible.** [eight-twists-sufficiency.md](../eight-twists-sufficiency.md) argued *sufficiency*; this is the necessity half. The alphabet **is** the signed axis frame: every twist is a sign plus an axis and every sign-axis pair is a twist (`Twist.toSignedAxis`/`ofSignedAxis`, round-tripping both ways), agreeing with the Pauli-closure normal form (`twistNF_eq_signedAxis`), and conjugation is sign flip at fixed axis (`toSignedAxis_conj`) — which is why `F(h)` has four terms. So `|Σ| = 2·|axes|`, and since axes compose, an axis set is closed, hence a **subgroup of the Klein four-group** `Axis ≅ (ZMod 2)²`. `decide`-checked over all 16 candidate axis sets: `frame_axisCount_trichotomy` (1, 2 or 4 axes — Lagrange by exhaustion), `alphabetSize_trichotomy` (`|Σ| ∈ {2,4,8}`), **`no_six_twist_alphabet`** (`3 ∤ 4`: "three spatial axes, no gauge pair" is not an alphabet, and `frame_contains_I` shows the gauge pair `+`/`−` is the identity axis closure *forces*), **`two_spatial_axes_force_three`** (two distinct spatial axes force the third, so the spatial count is 0, 1 or 3 — **never 2**; an independent and stronger route to the substrate's `3` than `6 = 2·3`), and **`noncommuting_iff_eight`** (non-commuting observables occur at `|Σ| = 8` and nowhere else, grounded in the matrices by `sigma_xy_noncomm`: `σxσy = iσz` vs `σyσx = −iσz`) — so uncertainty, SU(2), the double cover and spin exist only at eight, the 4-element alphabet being abelian. Residual posit, named: an elementary distinction *is* a signed frame element of a two-valued system (two-valuedness proved in [QLF_SpinorInformation](QLF_SpinorInformation.lean); for a `d`-valued atom the signed-frame count is `2d²` = `2·dim_ℝ Herm(d)`, though the Klein-group quantization itself is special to `d = 2`). Enumerated independently in [alphabet_necessity.py](../alphabet_necessity.py). No axioms | `Twist.toSignedAxis`, `Twist.ofSignedAxis`, `ofSignedAxis_toSignedAxis`, `toSignedAxis_ofSignedAxis`, `twistNF_eq_signedAxis`, `toSignedAxis_conj`, `IsAxisFrame`, `alphabetSize`, `fullFrame_alphabetSize`, `frame_axisCount_trichotomy`, `alphabetSize_trichotomy`, `no_six_twist_alphabet`, `frame_contains_I`, `two_spatial_axes_force_three`, `alphabet_eight_of_two_spatial_axes`, `noncommuting_iff_eight`, `sigma_xy_noncomm`, `axisMatrix_X_Y_noncomm` |
| [QLF_ElectronClosure.lean](QLF_ElectronClosure.lean) | **The electron as a closed periodic mode, and charge as the residue of non-closure** ([Electron.md](../Electron.md) §1). Settles a standing contradiction: the internal cycle `^<v>` **is** count-balanced and folds to `−I` (`electronCycle_countBalanced`, reusing [interleaved_xlvr_folds_to_negI](QLF_TwistAlphabet.lean)), while what is open is the **gauge** twist — and that unmatched count **is** the charge (`electronCharged_charge = 1`, `electronCharged_not_countBalanced`); the manifest event is the joint closure and it is neutral (`positronium_countBalanced`/`positronium_neutral`). **`hermitian_not_implies_zfa`**: the prefix `^<v` folds to the Hermitian `−σx` (`electronPrefix_fold`, `neg_sigmax_hermitian`) while carrying `F = 1` — self-adjointness is a property of the operator, closure of the history, which is the exact content of *manifest only at full cycles*. **`zfa_closure_is_neutral`**: a ZFA-closed history has zero charge (`chiralCharge_eq_gauge_counts`), so charge is **emergent** — a count of what has not closed, with conservation and integer quantization following from the count. **`no_charge_between_spatial_modes`**: `twistCharge` vanishes on all six spatial twists, so charge is a function of the gauge counts alone (`chiralCharge_determined_by_gauge`) and two modes differing only in spatial content — any spin, any harmonic — carry **exactly zero** charge difference; this derives QED's exact spin-independence of the direct Coulomb term. **`charge_nonzero_not_countBalanced`**: contrapositively, a charged history does *not* close, hence is **not an event**, hence has no effect — nothing is pending, an electron does not "seek" a partner. So what is called Coulomb attraction/repulsion is a **count**: `joint_closure_total_charge_zero` (a joint closure exists only where the charges cancel), `like_charges_do_not_close` (**zero** ways, not a repulsion), `opposite_charges_close` (ways exist), assembled as **`coulomb_is_a_counting_rule`** — no force, no field, no action at a distance. **`joint_closure_allows_unequal_components`**: two unbalanced halves of *different lengths* whose joint history closes — unequal energies in one event are normal, not a counterexample. Coherence layer: `cycleOverlap_distinct`/`harmonics_orthogonal` (a root of unity sums to zero over a full period) + `spin_projectors_orthogonal` give `channelKernel_diagonal` (`Γ = δ_mn δ_ss'`). Scale layer: `rest_period_times_c` (`c·(h/mc²) = h/mc`) and `compton_full_cycle` (`λ_C = 2π·ƛ_C`) — the closure fixes a period, not a radius. Reuses `QLF.Spin`'s `twistCharge`/`chiralCharge`. No axioms | `electronCycle`, `electronPrefix`, `electronCycle_countBalanced`, `electronCycle_folds_negI`, `electronPrefix_not_countBalanced`, `electronPrefix_fold`, `neg_sigmax_hermitian`, `hermitian_not_implies_zfa`, `chiralCharge_eq_gauge_counts`, `zfa_closure_is_neutral`, `twistCharge_eq_zero_of_spatial`, `chiralCharge_append`, `chiralCharge_eq_zero_of_all_zero`, `chiralCharge_determined_by_gauge`, `no_charge_between_spatial_modes`, `electronCharged_charge`, `electronCharged_not_countBalanced`, `positronium_countBalanced`, `positronium_neutral`, `charge_nonzero_not_countBalanced`, `joint_closure_total_charge_zero`, `like_charges_do_not_close`, `positronCharged`, `positronCharged_charge`, `opposite_charges_close`, `coulomb_is_a_counting_rule`, `joint_closure_allows_unequal_components`, `cycleOverlap`, `cycleOverlap_same`, `cycleOverlap_distinct`, `harmonics_orthogonal`, `projUp`, `projDown`, `projUp_eq_half`, `projDown_eq_half`, `spin_projectors_orthogonal`, `projUp_idem`, `spinOverlap_opposite`, `spinOverlap_same`, `channelKernel_diagonal`, `closurePeriod`, `closureWavelength`, `rest_period_times_c`, `compton_full_cycle` |
| [QLF_Handedness.lean](QLF_Handedness.lean) | **Handedness is the primitive; charge is one of its four components.** Answers what [QLF_ElectronClosure](QLF_ElectronClosure.lean) left open — if charge is emergent, what is fundamental. A twist **is** a handedness together with an axis and nothing else (`Twist ≃ Bool × Axis`, [QLF_AlphabetNecessity](QLF_AlphabetNecessity.lean)), so charge is nowhere in the primitives. **`zfa_iff_handedness_balanced`**: **ZFA is exactly zero net handedness on every axis** — count balance was always a statement about handedness, one component per conjugate pair, which is why `F(h)` has four terms. **`chiralCharge_eq_handednessOn_gauge`**: **charge is the gauge component**, one of four — not a substance, not a fifth axis; this *explains* [no_charge_between_spatial_modes](QLF_ElectronClosure.lean) rather than restating it, since spin and energy are the other three components and components do not mix. **`handednessOn_map_conj`**: conjugation negates every component, so charge flips *because* handedness does (`chiralCharge_conj` is its `Axis.I` case). **`electron_neutral_but_handed`** + `handedness_ne_zero`: the primitive never vanishes while the derived quantity does — the electron cycle is neutral *and built entirely of handed twists*, so **neutral means handedness balanced, not handedness-free**. Structural corollary: `C` flips all four components while `P` (`reflect`) flips one, and charge is the gauge component, so **`reflect_preserves_charge`** — parity cannot touch charge by construction, where conjugation negates it; the C/P asymmetry is a fact about how many components each touches ([CP-Violation-and-Chirality.md](../CP-Violation-and-Chirality.md) §1a). Capstone `handedness_is_the_primitive`. Reuses `QLF.Spin`'s `chiralCharge`. No axioms | `handedness`, `twistAxis`, `handedness_ne_zero`, `handedness_conj`, `twistAxis_conj`, `rightTwist`, `leftTwist`, `rightTwist_eq`, `leftTwist_eq`, `handedness_rightTwist`, `handedness_leftTwist`, `handednessOn`, `handednessOn_nil`, `handednessOn_cons`, `handednessOn_append`, `zfa_iff_handedness_balanced`, `chiralCharge_eq_handednessOn_gauge`, `handednessOn_map_conj`, `electron_neutral_but_handed`, `reflect`, `reflect_twistAxis`, `reflect_eq_of_ne`, `handednessOn_map_reflect_other`, `reflect_preserves_charge`, `handedness_is_the_primitive` |
| [QLF_VacuumAlignment.lean](QLF_VacuumAlignment.lean) | Per-event AND trajectory-level Lean anchors for the vacuum-alignment TOE-completing principle ([VacuumEnergy.md §6](../VacuumEnergy.md)): KL saturation against the vacuum's max-entropy prior is equivalent to ZFA-closure delta realisation at every event in the trajectory | `binary_kl_delta_zero_uniform`, `vacuum_alignment_selects_zfa`, `misalignment_strictly_underperforms`, `binary_kl_uniform_le_log_two_endpoint`, `cumulative_kl_le_length_log_two`, `global_alignment_selects_zfa` |
| [QLF_RhoProcessBridge.lean](QLF_RhoProcessBridge.lean) | Third layer of the vacuum-alignment selection rule: every constructible RhoProcess produces an events-trajectory that saturates the cumulative information bound against the vacuum prior, by structural recursion (`action → 1`, `lift → 0`, `parallel`/`sequence` concatenate) | `events`, `events_all_delta`, `events_bounded`, `rho_process_alignment_saturates` |
| [QLF_LocalClock.lean](QLF_LocalClock.lean) | Markov-blanket-local-clock identity ([Kitada_Local_Time_GR.md §3 Gap 1](../Kitada_Local_Time_GR.md), [Frequency_Synchronization.md §1.1](../Frequency_Synchronization.md)): a QLF Markov blanket of depth `R` IS a local clock with period `R` substrate ticks, each contributing `log 2` nats. The QLF realisation of Kitada's local-time framework (gr-qc/9612043) | `local_clock_period`, `markov_blanket_local_clock`, `local_clock_tick_is_log_two` |
| [QLF_EinsteinGeometricFactor.lean](QLF_EinsteinGeometricFactor.lean) | Einstein-field-equation geometric factor `8π = 4π · 2` decomposed structurally ([Kitada_Local_Time_GR.md §5.1](../Kitada_Local_Time_GR.md)): `4π` is the Markov-blanket boundary 2-sphere solid angle; `2` is the Hermitian-pair degeneracy per ZFA event (action vs lift) from `events_all_delta` and `bra_ket_always_balanced`. The factor `½` in the trace-reversed Einstein tensor `G_μν = R_μν − ½ g_μν R` is the inverse of the substrate Hermitian-pair degeneracy | `boundary_solid_angle`, `hermitian_pair_degeneracy`, `einstein_geometric_factor_eight_pi`, `trace_reversed_half_is_inverse_hermitian_degeneracy` |
| [QLF_SubstrateLightSpeed.lean](QLF_SubstrateLightSpeed.lean) | Constancy of `c` from the cosmic-ratio identity ([Kitada_Local_Time_GR.md §5.3](../Kitada_Local_Time_GR.md)): `c = R_cosmic / T_cosmic = (n · L_Planck) / (n · τ_Planck) = L_Planck / τ_Planck`. The cosmic-horizon depth `n` cancels exactly, giving `c` as a substrate property from two independently-derived QLF quantities (apparent universe size + apparent universe age). Generalises to any Markov blanket of depth `ρ`: local `c = c_substrate` by the same ρ-cancellation, structurally grounding local Lorentz invariance in the substrate's irreducible space-time event quantum | `planck_length`, `planck_time`, `substrate_light_speed`, `cosmic_horizon_depth`, `apparent_universe_size`, `apparent_universe_age`, `substrate_light_speed_from_cosmic_ratio`, `local_light_speed_invariant` |
| [QLF_FineStructureSubstrate.lean](QLF_FineStructureSubstrate.lean) | Fine-structure constant α derived from QLF substrate combinatorics, **zero free parameters** ([Magnetism_Spatial_Dynamics.md §6.1](../Magnetism_Spatial_Dynamics.md)): `α_QLF = α_bare / (1 + N · α_bare) = 1/137` exactly, where `α_bare = (1/16) × (1/4) × (1/2) × 1 = 1/128 = 2⁻⁷` from the 8-twist alphabet chain (naive closure rate × gauge selectivity × phase coherence × spatial co-location), and `N = 3² = 9` is the count of independent components of the 3 × 3 directional-coupling tensor (substrate is 3-dimensional, derived in [`Magic_numbers.md`](../Magic_numbers.md) from the 6+2 alphabet split). Matches CODATA `α = 1/137.036` at **0.026% relative error** with no observable input. Counterfactual theorems show 2D substrate → α = 1/132 (3.82% off), 4D → α = 1/144 (4.84% off); only 3D gives α = 1/137. The value is the **q²→0 (Thomson/IR) coupling of fully-rendered 3-D space**; the whole chain reduces to the closed form `α(d) = 1/(128 + d²)`, so α is a function of the rendering dimension **alone** — no time argument — giving the **no-cosmological-time-drift** result `no_cosmological_drift_of_alpha` (canonical doc [Alpha.md](../Alpha.md)) | `naive_closure_rate`, `gauge_selectivity`, `phase_coherence`, `spatial_colocation`, `alpha_bare`, `substrate_spatial_dimension`, `N_directional_modes`, `alpha_QLF`, `alpha_bare_eq`, `N_directional_modes_eq_nine`, `alpha_QLF_eq`, `alpha_QLF_2d_counterfactual`, `alpha_QLF_4d_counterfactual`, `only_3d_substrate_gives_137`, `alpha_at_dim`, `alpha_at_dim_closed_form`, `alpha_at_dim_three`, `alpha_at_dim_eq_alpha_QLF`, `no_cosmological_drift_of_alpha` |
| [QLF_LenzMassRatio.lean](QLF_LenzMassRatio.lean) | Proton-to-electron mass ratio `m_p / m_e = 6π⁵` from QLF substrate ([Proton_Resonance_R_e.md §§5-7](../Proton_Resonance_R_e.md)): the chirality-hiding-resonance reading decomposes the 70-year-old Lenz coincidence as `|S_3| · π⁵`, with `|S_3| = 6` the Bose permutation symmetry of the 3-quark proton Borromean closure and `π⁵` the integration measure over the 5-angle hidden-chirality configuration space (3 Jacobi internal coordinates + 2 chirality-mixing angles per Hermitian-conjugate pair). Matches PDG `m_p/m_e = 1836.152` at **0.002% relative error**. Counterfactual theorems show 2-quark proton → 2π⁵ ≈ 612 (off by 67%); 4-angle space → 6π⁴ ≈ 584 (off by 68%); 6-angle space → 6π⁶ ≈ 5769 (off by 214%). Second Lean-verified fundamental-constant theorem in the QLF tree, sibling to `QLF_FineStructureSubstrate.lean` | `S3_order`, `hidden_chirality_angles`, `lenz_factor`, `mass_ratio_QLF`, `lenz_factor_eq`, `mass_ratio_QLF_eq`, `mass_ratio_2_quark_eq`, `mass_ratio_4_angle_eq`, `mass_ratio_6_angle_eq`, `counterfactual_summary` |
| [QLF_PionMassRatio.lean](QLF_PionMassRatio.lean) | Charged-pion / electron mass ratio `m_π±/m_e = \|S₂\|/α = 2/α` ([Pion_QLF.md](../Pion_QLF.md)): a structural reading of Nambu's `m_π ≈ 2 m_e/α` coincidence, made non-arbitrary by QLF's derived `α = 1/137`. The proton hides chirality (Borromean → geometric `π⁵`, `m_p/m_e=6π⁵`); the pion is a 2-quark pseudoscalar with **exposed** chirality → EM factor `1/α`. So `m_π±/m_e = 2/α = 274` vs measured 273.1 (**0.3%**), the single-quark counterfactual `1/α=137` confirms the 2 = two quarks, and the proton↔pion ratio `6π⁵/(2/α)=3π⁵/137≈6.70` matches 6.72 (0.3%). Honest: `\|S₂\|=2` solid; the `1/α` from exposed chirality is the open mechanism (`pion_mass_ratio_in_progress`), not yet first-principles | `S2_order`, `pion_electron_ratio`, `pion_electron_ratio_eq`, `single_quark_eq`, `proton_pion_ratio_eq`, `pion_mass_ratio_in_progress` |
| [QLF_QuantumBlackHole.lean](QLF_QuantumBlackHole.lean) | **Every hadron (meson + baryon) is a Markov-blanket quantum black hole** ([Hadron_BlackHoles.md](../Hadron_BlackHoles.md)), unifying the [`BLACK-HOLES.md`](../BLACK-HOLES.md) particle↔BH equivalence across composite hadrons. The **Compton–Schwarzschild crossing at the Planck mass** — in Planck units the Compton radius `1/μ` and Schwarzschild radius `2μ` coincide *iff* `μ²=1/2` (`compton_eq_schwarzschild_iff`), and a sub-Planck hadron (`μ²<1/2`) lives on the Compton side (`sub_planck_compton_gt_schwarzschild`), so its horizon is the **Planck-scale Markov blanket**, not a Schwarzschild horizon. Reuses the verified holographic area law `S=4πR²log2` (`hadron_horizon_entropy_eq` from `QLF_GravityFromDelay`) and `baryonNumber` (meson `B=0` `pion_meson_horizon`, baryon `B=1` `proton_baryon_horizon`). Mass `m=1/R` (`mass_depth_product`, `lighter_is_deeper` ⟹ pion = deepest hadronic horizon). Coherence with the mass ratios: hidden-vs-exposed chirality fixes both the mass factor (`π⁵` vs `1/α`) *and* the horizon fate (stable vs decay = Hawking evaporation). Honest scope (`hadron_black_hole_framing_constructive`): a unification + thermodynamic reading, **not** a derivation of hadron masses or the pion `1/α` — `R` per hadron is an input (`pion_mass_ratio_in_progress`) | `compton_radius`, `schwarzschild_radius`, `compton_eq_schwarzschild_iff`, `sub_planck_compton_gt_schwarzschild`, `hadron_horizon_entropy`, `hadron_horizon_entropy_eq`, `mass_from_depth`, `mass_depth_product`, `lighter_is_deeper`, `isMesonHorizon`, `pion_meson_horizon`, `proton_baryon_horizon`, `hadron_black_hole_framing_constructive` |
| [QLF_DarkMatter.lean](QLF_DarkMatter.lean) | **Dark matter as denser logic near masses** — the quantitative skeleton of [DarkMatter.md](../DarkMatter.md). The crossover acceleration `a₀ = cH₀/(2π) = c²/(2π R_H)` sits on the **same Hubble radius `R_H = c/H₀`** that fixes `Ω_Λ = log 2` in `QLF_CosmologicalConstant` (`mond_acceleration_horizon_form`), ≈`1.05×10⁻¹⁰` vs Milgrom's `1.2×10⁻¹⁰ m/s²` (~13%, zero new inputs). Transition radius `σ = √(GM/a₀)` is where Newtonian `GM/r²` equals the floor (`mond_radius_accel`); the **dense/sparse crossover** `a₀ < GM/r² ⟺ r² < GM/a₀` (`newtonian_dominates_iff`) splits the dense interior (Newton + GR — Mercury perihelion, hadron quantum black holes) from the sparse exterior (apparent dark matter). Baryonic Tully–Fisher `v⁴ = GM a₀`, r-independent (`tully_fisher_flat`). The congestion profile is the maximum-relative-entropy (MRE — same `binary_kl` principle as `Ω_Λ`) **Gaussian** bump, densest at the mass (`gaussian_logic_density`, `gaussian_denser_near_center`). Dark matter ↔ dark energy = the expand/contract logical-density gradient on one horizon. **The dense↔sparse interpolation is now derived** — the closure-balance **radial acceleration relation** `g_obs²=g_bar·(g_obs+a₀)` (`radialAccel_self_consistent`; closure needs both the local AND cosmological condition, a ZFA conjunction), with the Newtonian limit (`radialAccel_newtonian`), the geometric-mean/Tully–Fisher deep limit (`radialAccel_ge_geometric_mean`), and `a_cl=g_obs−g_bar≥0` (`radialAccel_ge_baryonic`) all exact. The **blind SPARC benchmark** ([`SPARC.md`](../SPARC.md), #77: 147 curated galaxies, baryonic-only, SHA-256-sealed, zero per-galaxy tuning) reproduces the galactic Radial Acceleration Relation **parameter-free** at the observational floor (`0.133 dex` scatter, zero offset) with the *derived* `a₀=cH₀/2π` — = best-fit MOND, vs Newton (fails ×2.7) and NFW (needs 294 halo params). Honest scope (`dark_matter_from_logic_density_constructive`): the `1/2π` prefactor (the ~13% residual, absorbed at local `H₀`) and the interpolation form being the *unique* forced ν stay open (`dark_matter_acceleration_scale_in_progress`) | `hubble_acceleration`, `mond_acceleration`, `mond_acceleration_horizon_form`, `mond_radius`, `mond_radius_accel`, `newtonian_dominates_iff`, `tully_fisher_flat`, `gaussian_logic_density`, `gaussian_denser_near_center`, `radialAccel`, `radialAccel_self_consistent`, `radialAccel_newtonian`, `radialAccel_ge_baryonic`, `radialAccel_ge_geometric_mean`, `dark_matter_from_logic_density_constructive` |
| [QLF_BorromeanAngles.lean](QLF_BorromeanAngles.lean) | Structural decomposition of the 5-angle count used in `QLF_LenzMassRatio`: `5 = 3 + 2` where `3` is the standard 3-body Jacobi internal DOF (`9 - 3 - 3 = 3`, rigorous group-theoretic reduction) and `2` is the chirality-mixing angles per gauge-fold Hermitian-conjugate pair (structural reading from QLF_Pauli's scalar group `{+I, -I, +iI, -iI}` as a 2-axis sign × phase structure). Bridge theorem `matches_lenz_hidden_chirality_angles : total_angular_DOF = hidden_chirality_angles` connects the structural decomposition to the constant in `QLF_LenzMassRatio`. Counterfactual theorems: 2-quark composite → 2 angular DOF; 4-quark → 8. Only the 3-quark Borromean gives 5. Open sub-target: rigorously derive the chirality-mixing-per-pair = 2 claim from QLF_Pauli's scalar group | `quark_count`, `spatial_dimension`, `total_spatial_DOF`, `cm_translation_DOF`, `overall_rotation_DOF`, `internal_jacobi_DOF`, `chirality_mixing_per_gauge_fold`, `gauge_fold_pair_count`, `chirality_mixing_DOF`, `total_angular_DOF`, `internal_jacobi_DOF_eq_three`, `chirality_mixing_DOF_eq_two`, `total_angular_DOF_eq_five`, `matches_lenz_hidden_chirality_angles`, `total_angular_DOF_2_quark_eq`, `total_angular_DOF_4_quark_eq`, `only_3_quark_gives_five_angles` |
| [QLF_EulerMascheroni.lean](QLF_EulerMascheroni.lean) | Euler-Mascheroni constant γ ≈ 0.5772156649 from QLF substrate ([Experimental_Consistency.md §6.2](../Experimental_Consistency.md)): γ emerges as the harmonic excess `H_N − ln N` of the ordered ZFA-stable closure ensemble in the limit `N → ∞`. Module Lean-anchors the structural form: `harmonic N` (the N-th harmonic sum), `harmonic_excess N` (= H_N − ln N), and `gamma_QLF` (the limit value). Small-N arithmetic proved (`harmonic_one = 1`, `harmonic_excess_one = 1`). Numerical demonstration at 0.017% relative error in `constants_mapper.emerge_gamma()` at N ≈ 5000. Honest scope: structural form Lean-anchored; full convergence proof (Tendsto with monotone-bounded sequence) deferred. Third Lean-anchored fundamental constant in the QLF tree (after α and m_p/m_e) | `harmonic`, `harmonic_excess`, `gamma_QLF`, `harmonic_excess_def`, `harmonic_zero`, `harmonic_one`, `harmonic_excess_one`, `gamma_QLF_value`, `gamma_QLF_structural` |
| [QLF_RiemannZeta.lean](QLF_RiemannZeta.lean) | Substrate-to-ζ bridge ([Riemann-Conjecture-Proof.md](../Riemann-Conjecture-Proof.md), [ReverseMathematics.md §4.9](../ReverseMathematics.md)): identifies γ_QLF from `QLF_EulerMascheroni` with the Laurent constant of the Riemann zeta function at its pole s = 1, by the classical expansion `ζ(s) = 1/(s−1) + γ + O(s−1)`. Lean-anchors the structural identifications: ζ's Laurent constant at s = 1 IS γ_QLF (substrate-to-analytic bridge), and the critical-line real part `Re(s) = 1/2` IS the count-balance ratio (the fixed locus of the functional-equation involution `s ↔ 1−s`, matched by the H ↔ H† adjoint involution on `Σ_sa`). Includes `rh_proof_in_progress : True` as explicit honest scoping: this module does NOT close RH (the spectral-isomorphism bridge to Berry-Keating remains the open piece in `QLF_Riemann.lean`'s axiom inventory); it consolidates the substrate-side γ-Lean work with the existing QLF Riemann program | `zeta_laurent_constant_at_one`, `critical_line_real_part`, `zeta_laurent_constant_eq_gamma_QLF`, `zeta_laurent_constant_value`, `critical_line_real_part_eq`, `functional_equation_fixed_real`, `qlf_zeta_substrate_bridge`, `rh_proof_in_progress` |
| [QLF_RiemannMRE.lean](QLF_RiemannMRE.lean) | **MRE bridge** — a constructive scaffold for the Riemann boundary (ReverseMathematics.md §4). `Z_QLF = (1/(1−5x)+1/(1−3x))/2` is concrete with verified singularities at the substrate axis weights `1/5`, `1/3` (`Z_QLF_pole_fifth`, `Z_QLF_pole_third`). MRE saturation is grounded in `binary_kl`: under the uniform `1/2` prior the per-event info gain `log 2` is saturated only at the half-spin closure (`mre_saturation_only_at_closure`, reusing `binary_kl_delta_uniform` + `binary_kl_uniform_lt_log_two`), and that saturating prior `1/2` IS `critical_line_real_part` (`mre_prior_is_critical_line`). The bare `spectral_hilbert_polya` is refined into the single structurally-motivated axiom `mre_factorization` (over the concrete `Z_QLF`), giving `riemann_hypothesis_in_qlf_via_MRE`; `MRE_bridge` and `zero_is_mellin_singularity` are **theorems** read off it. The boundary's strength is measured, not described: `mellinFactorization_iff_rh` proves the two-leg factorization is equivalent to RH, and `mellinFactorization_independent_of_generator` proves the generating function does no logical work — so the scaffold is motivation. Giving `MellinStructuralSingularity` a concrete definition is a trap that falsifies one leg either way (module section note). Residual Mellin↔ζ correspondence is the WKL₀/continuum boundary (`rh_mre_proof_in_progress`) | `Z_QLF`, `Z_QLF_pole_fifth`, `Z_QLF_pole_third`, `mre_saturation_only_at_closure`, `mre_prior_is_critical_line`, `MellinFactorization`, `mellinFactorization_iff_rh`, `mellinFactorization_independent_of_generator`, `mre_factorization`, `MRE_bridge`, `zero_is_mellin_singularity`, `riemann_hypothesis_in_qlf_via_MRE`, `rh_mre_proof_in_progress` |
| [QLF_DiracCorrection.lean](QLF_DiracCorrection.lean) | Hydrogen fine structure: the relativistic/Dirac α² correction to the Bohr spectrum, decomposed into three substrate mechanisms (kinematic, spin-orbit, Darwin), each carrying one α²; closes the Bohr-model 0.05% residual. Honest scope: per-mechanism Lean chains from `QLF_Pauli`/`QLF_TwistAlphabet` remain doc-anchored (`dirac_correction_proven_constructively`) | `dirac_ground_state`, `dirac_ground_state_substrate`, `dirac_n2_j_half`, `dirac_n2_j_three_half`, `fine_structure_n2_splitting`, `reduced_mass_factor_eq`, `three_mechanisms_alpha_squared`, `hydrogen_spectrum_from_h_and_m_e`, `dirac_correction_proven_constructively` |
| [QLF_LambShift.lean](QLF_LambShift.lean) | Lamb shift: the prefactor `4/(3π n³) = 4·(2/3)·(1/2π)·(1/n³)` — its *entire* π is the single `1/(2π)` loop-phase primitive that g-2 validates (`a_e = α/2π`); the α⁵ scaling and Bethe-log structure are anchored. The Bethe constant `k(n,0)` is a principled continuum-sector boundary, not closed by counting (`lamb_shift_proven_constructively`) | `lamb_alpha_scaling_eq`, `lamb_prefactor_loop_phase`, `lamb_shift_expansion`, `alpha_five_decomposition`, `substrate_bethe_log_ground_state`, `substrate_bethe_log_n2`, `lamb_shift_substrate_summary`, `lamb_shift_proven_constructively` |
| [QLF_GMinusTwo.lean](QLF_GMinusTwo.lean) | Electron anomalous magnetic moment at leading order: `a_e = α/(2π)` (Schwinger), `g = 2(1 + α/2π)` — the `1/(2π)` is the substrate loop-phase primitive. Matches CODATA at 0.2% (one-loop); higher-loop QED is `g_minus_2_proven_constructively` | `a_e_QLF_eq_schwinger`, `a_e_QLF_substrate`, `g_factor_QLF_eq`, `schwinger_two_factor_decomposition`, `a_e_substrate_summary`, `g_minus_2_proven_constructively` |
| [QLF_GravityFromDelay.lean](QLF_GravityFromDelay.lean) | Newton's law from holographic constructing-delay: inverse-square only in 3D (`newton_exponent_only_3d_matches`: 2D→1, 4D→3), with `G = L_P²c³/ℏ`. Emergent (Jacobson/Verlinde) gravity; the SI calibration residual is `gravity_from_delay_proven_constructively` | `holographic_entropy_eq`, `newton_exponent_3d`, `newton_exponent_2d`, `newton_exponent_4d`, `newton_exponent_only_3d_matches`, `G_value_eq`, `gravity_substrate_summary`, `gravity_from_delay_proven_constructively` |
| [QLF_PlanckScale.lean](QLF_PlanckScale.lean) | **The Planck length is the closure floor *by construction*, not a posited input** ([Planck_Scale.md](../Planck_Scale.md)). The substrate granularity follows from QLF's own structure, via the Compton–Schwarzschild crossing in [QLF_QuantumBlackHole.lean](QLF_QuantumBlackHole.lean). **`coherent_iff_subplanck`** — a closure stays coherent (its confinement-energy horizon does not engulf its Compton extent) **iff** sub-Planck `μ²<1/2` (`←` reuses `sub_planck_compton_gt_schwarzschild`). **`planck_length_floor`** — every coherent closure has Compton length `>√2` (Planck units): there is **no coherent closure below the Planck length** — confine tighter and the horizon exceeds the blanket, so it cannot close. **`planck_self_dual`** — the floor is the unique self-dual point `μ²=1/2` where Compton = Schwarzschild (reuses `compton_eq_schwarzschild_iff`). So given QLF's own emergent gravity + blanket closure, the substrate granularity *is* the Planck scale by construction. Scope (`planck_scale_by_construction`): the Planck *scale* (dimensionless `μ²=1/2`) follows by construction; the SI value in metres is a unit convention (not a physics question); matter-depth-above-floor = the `14π` hierarchy (`QLF_AlphaS`), tracked separately | `coherent_iff_subplanck`, `planck_length_floor`, `planck_self_dual`, `planck_scale_by_construction` |
| [QLF_LoopQuantumGravity.lean](QLF_LoopQuantumGravity.lean) | **QLF's substrate is a spin network of half-spin (j=½) ZFA closures** — the Loop Quantum Gravity correspondence ([LQG_QLF.md](../LQG_QLF.md)). Builds on [QLF_GravityFromDelay.lean](QLF_GravityFromDelay.lean)'s holographic entropy and [QLF_Spin.lean](QLF_Spin.lean)'s `su(2)` closure. **`puncture_is_log_two`** — a horizon puncture (one half-spin closure) carries `log 2` = `per_event_entropy` (the MRE quantum, same `log 2` as `gaugeMassGap`): QLF's per-Planck-patch quantum *is* the LQG j=½ puncture entropy. **`horizonEntropy_eq`** — `n` punctures carry `n·log 2` (the LQG black-hole entropy count with dominant j=½ punctures). **`lqg_horizon_is_holographic`** — QLF's holographic entropy `S(R)=4πR²log2` *is* the puncture sum over its `N(R)=4πR²` half-spin punctures, so the LQG state count and the QLF holographic count are one object; the **Barbero–Immirzi parameter is fixed by construction** by the `log 2`-per-half-spin-puncture (no free `γ`). Background independence by construction (synthesized spacetime, [QLF_ReachableEvent.lean](QLF_ReachableEvent.lean) causal set) — and the synthesized time `f=1/t` **supplies the arrow that canonical / Wheeler–DeWitt LQG's frozen `H=0` "problem of time" lacks** (the reversibility/energy audit, [Reversibility.md](../Reversibility.md) §6); note QLF's holographic entropy is the **de Sitter / ZFA-closure** boundary (positive `Λ=log 2`, the created future-energy of [Conservation.md](../Conservation.md) §2b), **not** AdS/CFT's static negative-Λ unitary frame. Honest scope (`lqg_correspondence_in_progress`): anchors the entropy-count correspondence, **not** the general `√(j(j+1))` area-operator spectrum or the LQG Hamiltonian/spin-foam dynamics | `punctureEntropy`, `puncture_is_log_two`, `punctureEntropy_pos`, `horizonEntropy_eq`, `lqg_horizon_is_holographic`, `lqg_correspondence_in_progress` |
| [QLF_MercuryPerihelion.lean](QLF_MercuryPerihelion.lean) | GR's first triumph from the substrate: Mercury's perihelion advance = 42.99″/century vs measured 42.98″ (0.03%), via the Schwarzschild radius extracted from `Form` equivalence; `G` and `c` substrate-derived | `schwarzschild_radius_eq`, `perihelion_advance_form_equivalence`, `perihelion_advance_extracts_R_s`, `perihelion_advance_per_century_eq`, `mercury_perihelion_substrate_summary`, `mercury_perihelion_proven_constructively` |
| [QLF_CosmologicalConstant.lean](QLF_CosmologicalConstant.lean) | Cosmological constant: `Ω_Λ = log 2 ≈ 0.693` vs observed 0.685 (1.2%) — the gauge-axis fraction (2 of the 8 twists) sets the vacuum prefactor, closing the 10¹²² vacuum catastrophe structurally. Counterfactuals: 4-gauge → 2 log 2, 0-gauge → 0 (`only_2_gauge_matches_observed_Omega_Lambda`) | `gauge_axis_fraction_eq`, `vacuum_energy_prefactor_friedmann_form`, `vacuum_energy_prefactor_decomposition`, `Omega_Lambda_4_gauge_eq`, `Omega_Lambda_0_gauge_eq`, `only_2_gauge_matches_observed_Omega_Lambda`, `cosmological_constant_substrate_summary`, `cosmological_constant_proven_constructively` |
| [QLF_PrimordialMarkovBlanket.lean](QLF_PrimordialMarkovBlanket.lean) | Markov blankets as Fuller geodesic spheres: the icosahedral base closure (Euler characteristic, 12 pentamons, hexamon count, holographic event count, information capacity) and its binary-icosahedral group `2I` → `E₈` via the McKay correspondence (`E8_dimension_eq` = 248, `mckay_2I_E8_anchor`) | `base_icosahedron`, `primordial_blanket_euler`, `pentamons_invariant`, `primordial_blanket_hexamon_count_eq`, `holographic_event_count_blanket_eq`, `primordial_blanket_information_capacity_eq`, `binary_icosahedral_order_eq`, `E8_dimension_eq`, `mckay_2I_E8_anchor`, `primordial_markov_blanket_substrate_summary`, `primordial_markov_blanket_proven_constructively` |
| [QLF_Koide.lean](QLF_Koide.lean) | Koide relation `Q = (Σmℓ)/(Σ√mℓ)² = 2/3` as the three charged leptons being three 120°-phases of one gauge-fold closure; `koide_two_thirds` proves it follows by construction from `N=3` (axes) ∧ `A²=2` (transverse axes) ⇒ predicts `m_τ` from `m_e,m_μ` to 0.006%. Scale + Koide angle remain inputs ([Weak_Force.md](../Weak_Force.md) §5) | `koide_three_phase`, `koide_two_thirds`, `koide_phase_witness` |
| [QLF_Generations.lean](QLF_Generations.lean) | **Why exactly three fermion generations** — a generation is a balanced phase of a gauge-fold closure about the spatial axes, so the count equals `substrate_spatial_dimension = 3` (`num_generations_eq_three`). The non-trivial content: **one substrate integer `3`** underlies four independent facts — generations, Koide's `N=3` phases (`QLF_Koide`), colour `SU(3)` (`QLF_StrongAlgebra`), and `α` via `N=9=3²` (`QLF_FineStructureSubstrate`) — packaged in `three_axis_signature`. The three generations are realized concretely as Koide's three cube-root-of-unity phases `(1,−½,−½)`, which satisfy `Σc=0, Σc²=3/2` and hence `Q=2/3` (`three_generations_satisfy_koide`, reusing `koide_two_thirds`). Counterfactuals `only_3d_gives_three_generations` (2D→2, 4D→4). Honest scope (`generations_from_three_axes_constructive`): this **reduces "why 3 generations" to "why 3 spatial dimensions"** — the 3D-ness is the input, argued elsewhere (Newton `1/r²`, magic numbers, the α tensor), not derived from nothing | `num_generations`, `num_generations_eq_three`, `generations_in_dim`, `only_3d_gives_three_generations`, `three_generations_satisfy_koide`, `three_axis_signature`, `generations_from_three_axes_constructive` |
| [QLF_HorizonTemperature.lean](QLF_HorizonTemperature.lean) | **Unruh, Hawking, and de Sitter temperatures from one substrate relation** ([Gravity_From_Delay.md §5.1](../Gravity_From_Delay.md)). Every horizon temperature is the Unruh master `T = ℏa/(2πck_B)` (`unruh_temperature`) at the appropriate acceleration, with the universal `2π` identified as QLF's **loop phase** (same `2π` as `g−2 = α/2π`). **Hawking**: at surface gravity `κ = c⁴/(4GM)` ⟹ canonical `T = ℏc³/(8πGMk_B)` (`hawking_temperature_eq`) — the `8π` is the loop `2π` times the `4` in `κ`, the same `8π` as Einstein's `8π=4π·2`. **de Sitter**: at `cH₀` ⟹ `T = ℏH₀/(2πk_B)` (`desitter_temperature_eq`). Both are literally the master relation (`hawking_is_unruh`, `desitter_is_unruh`). **Dark-sector closure**: the de Sitter acceleration `cH₀` is `QLF_DarkMatter`'s `hubble_acceleration`, and `a₀ = cH₀/(2π) = a_dS/(2π)` (`mond_accel_is_hubble_over_loop`) — `Ω_Λ = log 2`, the horizon temperature, and the dark-matter scale all hang on one Hubble horizon and one `2π`. Honest scope (`horizon_temperature_constructive`): the algebraic unification + loop-phase identification, **not** a from-scratch QFT-in-curved-spacetime derivation; distinct from the equipartition shell temperature `T∝M/r²` of §5 | `unruh_temperature`, `surface_gravity`, `hawking_temperature`, `hawking_is_unruh`, `hawking_temperature_eq`, `desitter_temperature`, `desitter_is_unruh`, `desitter_temperature_eq`, `mond_accel_is_hubble_over_loop`, `horizon_temperature_constructive` |
 | [QLF_MondScale.lean](QLF_MondScale.lean) | **The `2π` in `a₀ = cH₀/(2π)` derived — the ZFA closure-loop period** ([DarkMatter.md](../DarkMatter.md) §5). The MOND `1/2π` is the period of **one ZFA closure loop**, not a fit: `a₀ = cH₀/τ_ZFA` is the Hubble acceleration delivered per closure loop (`a0_is_hubble_per_closure_loop`); `H₀` is the cosmic horizon's *angular* rate (the de Sitter temperature `T=ℏH₀/(2πk_B)` is `T=ℏω/(2πk_B)` with `ω=H₀`), so `a₀ = c·` the cyclic closure rate `H₀/τ_ZFA` (`a0_eq_c_times_cyclic_rate`); and `τ_ZFA = 2·π_QLF` (`loop_period_is_two_pi_QLF`) with `π_QLF` census-derived (`QLF_PhysicalPi`). So the `2π` is the substrate closure-loop period grounded in counting, the same loop behind `g−2=α/2π` and the horizon temperatures. **Honest scope:** the premise is `H₀` = the cosmic closure's angular rate; SPARC confirms `1/2π` at the local `H₀`. No new axioms | `cyclicClosureRate`, `a0_is_hubble_per_closure_loop`, `a0_eq_c_times_cyclic_rate`, `loop_period_is_two_pi_QLF`, `mond_scale_two_pi_derived` |
 | [QLF_MondNu.lean](QLF_MondNu.lean) | **The MOND interpolation function `ν` is the *unique* closure-balance form** ([DarkMatter.md](../DarkMatter.md) §7.5). The closure-balance RAR `g_obs²=g_bar·(g_obs+a₀)` is a ZFA conjunction (squared round-trip closure × local source × additive de Sitter floor). `radialAccel_unique`: for `g_bar,a₀>0` it has a **unique** non-negative solution (the other root is negative) — the interpolation function is fixed by the principle with no freedom, not a choice among the MOND family. `radialAccel_eq_nu`: `g_obs = ν(g_bar/a₀)·g_bar` with explicit `ν(y)=(1+√(1+4/y))/2`, exact Newton + Tully–Fisher limits. **Honest scope:** the uniqueness given the conjunction is proven; the structural reading itself is **derived** in `QLF_RarBalance`. No new axioms | `radialAccel_unique`, `nu`, `radialAccel_eq_nu`, `mond_nu_unique` |
 | [QLF_RarBalance.lean](QLF_RarBalance.lean) | **The structural reading of the closure-balance conjunction, derived** ([DarkMatter.md](../DarkMatter.md) §7.5). The squared/multiplicative form of `g_obs²=g_bar·(g_obs+a₀)` is forced by the **logarithmic free energy** (`QLF_FreeEnergy`, `ΔF=−log 2`): a closure rate `g` has free energy `F(g)=−log g`, ZFA balance puts the observed closure at the **average** of its two conjoined conditions' free energies, and since `F=−log` an average of logs is a geometric mean = the squared form. `log_geometric_mean_balance` (`2 log g = log A + log B ⟺ g²=A·B`), `closure_balance_iff_free_energy_balance`, `rar_is_free_energy_balance` (the RAR *is* the free-energy midpoint). Squared = geometric mean; multiplicative = conjunction (logs add); additive floor = accelerations add. **Honest scope:** the geometric-mean consequence + log free energy proven; acceleration-as-closure-rate (`F=−log g`) and balance-as-average are the QLF reading. No new axioms | `freeEnergy`, `log_geometric_mean_balance`, `closure_balance_iff_free_energy_balance`, `rar_is_free_energy_balance` |
 | [QLF_AlgebraEmergence.lean](QLF_AlgebraEmergence.lean) | **A group emerges from the substrate as a genuine Mathlib structure** ([Mathematics_From_QLF.md](../Mathematics_From_QLF.md)). The closure-fold group (`PauliScalar`, reached by every balanced closure via `count_balanced_pauli_closed`) is exhibited as the cyclic group `ℤ/4` = `μ₄=(ℤ[i])ˣ`, derived not imported. `toZMod_hom`: the closure-fold **multiplication IS `ℤ/4` addition**; `toZMod_injective`: faithful ⟹ `PauliScalar ≅ ℤ/4`. Anchors the bootstrapping resolution — the algebraic structure is *generated* by the substrate (counting + the two folds), so using Mathlib's algebra to verify QLF is not circular. No new axioms | `toZMod`, `toZMod_hom`, `toZMod_injective`, `pauli_fold_group_is_cyclic_four` |
| [QLF_WeinbergAngle.lean](QLF_WeinbergAngle.lean) | **Weak mixing angle from the 6+2 alphabet** ([Weak_Force.md §2](../Weak_Force.md)). At the unification scale `sin²θ_W = (spatial axes)/(alphabet) = 3/8` (`sin2_weinberg_substrate_eq`) — *exactly* the SU(5) Georgi–Glashow GUT normalization, the **third** electroweak/cosmological constant from the same `6 spatial + 2 gauge = 8` split as `α` (`N=3²`) and `Ω_Λ` (gauge `2/8`), packaged in `electroweak_substrate_signature`. Tree-level mass relations Lean-anchored: custodial `ρ=1` (`rho_one_of_mass_relation`) and on-shell `cos²θ_W = (M_W/M_Z)²` (`onshell_weinberg`). **Honest scope** (`weinberg_running_in_progress`): `3/8 = 0.375` is the *unification* value, **not** the measured `sin²θ_W(M_Z) ≈ 0.231` — the RG running is the open renormalization sector (a genuine GUT group-theoretic value, not a fit to data, contrast the `δ = 2/9` Koide-phase *candidate*, [Weak_Force.md §5c](../Weak_Force.md)); the absolute `W/Z` masses and `G_F` need the Higgs VEV | `sin2_weinberg_substrate`, `sin2_weinberg_substrate_eq`, `rho_parameter`, `rho_one_of_mass_relation`, `onshell_weinberg`, `electroweak_substrate_signature`, `weinberg_running_in_progress` |
| [QLF_RunningCouplings.lean](QLF_RunningCouplings.lean) | **One-loop RG structure + the substrate has no UV catastrophe** ([TheContinuum.md §3.1](../TheContinuum.md)). The inverse coupling runs logarithmically `1/α(t) = 1/α₀ + (b/2π)·t` (`inv_coupling`), the `2π` being the substrate **loop phase** (same as `g−2 = α/2π`, the horizon temperature). `asymptotic_freedom` (`b>0`, non-abelian/QCD: `1/α` grows ⇒ coupling vanishes at high energy), `infrared_growth` (`b<0`, abelian/QED screening), `landau_pole_location` (`1/α = 0` at the finite `t* = −(1/α₀)·2π/b`). The continuum theory hits the pole (a real divergence over infinitely divisible momentum space); QLF's **discrete substrate has a hard UV cutoff** at the Planck event scale, so the pole is never reached and every coupling stays finite — *no UV catastrophe*, the same thesis as the Millennium program. Honest scope (`running_couplings_structural`): anchors the RG **structure** + UV-finiteness, **not** the β-coefficients `b_i` (need the full SU(3)×SU(2)×U(1) matter content) or the GUT scale, so the `sin²θ_W = 3/8 → 0.231` running is consistent-with but not derived | `inv_coupling`, `asymptotic_freedom`, `infrared_growth`, `landau_pole_location`, `inv_coupling_at_zero`, `running_couplings_structural` |
| [QLF_GravitationalWaves.lean](QLF_GravitationalWaves.lean) | **What the substrate fixes about gravitational waves** ([GR_Schwarzschild.md](../GR_Schwarzschild.md)). A GW is a massless (gauge-fold-free, `R=0`) transverse ripple of synthesized spacetime, so it propagates at the substrate light speed `c = L_Planck/τ_Planck` (`gw_speed_eq_planck_ratio`, reusing `QLF_SubstrateLightSpeed` / `local_light_speed_invariant`) — the GW170817 result `|v_GW − c|/c < 10⁻¹⁵`. The **graviton is spin-2**, a composite of four half-spins = two photon-worths (`graviton_integer_spin`, reusing `boson_even_pairs` / `photon_integer_spin` from `QLF_Spin`), with **2 transverse-traceless polarizations** (the `±2` helicities, not `2J+1=5`) from masslessness, exactly like the photon's 2 (`massless_two_polarizations`). **The linearized wave equation is now anchored via the density-perturbation route:** a GW is a propagating modulation `δρ` of the closure-density field around the SOC equilibrium `ρ*` (`QLF_SteadyStateDensity`), and the discrete d'Alembertian `boxD = ∂_t² − ∂_x²` annihilates *every* traveling-wave profile — `boxD_rightMover`, `boxD_leftMover`, and the general d'Alembert solution `boxD_dAlembert` — so `□_d δρ = 0` at one Planck length per Planck tick `= c`, with the metric perturbation `h ∝ δρ/ρ*` obeying the same equation (`boxD_metricPerturbation`); continuum limit `□h_μν = 0`. The **quadrupole is the leading radiative multipole** (`quadrupole_is_leading_radiative`): mass–energy and momentum conservation force the monopole (`monopole_no_radiation`) and dipole (`dipole_no_radiation`) to be non-radiative (`ddt2 = 0`), the quadrupole not (`quadrupole_radiates`, `= 2`). Numerical companion [`gw_density_wave.py`](../gw_density_wave.py). Honest scope (`gravitational_waves_in_progress`), localized to the dynamical-metric step: deriving `boxD` from the SOC binding+continuity rate equations (`QLF_ClosureAttraction`/`QLF_SteadyStateDensity`) in the continuum limit, and the quadrupole luminosity *coefficient* `G/(5c⁵)` (with substrate `G = L_P²c³/ℏ` and `8π = 4π·2`) | `gw_speed`, `gw_speed_eq_c`, `gw_speed_eq_planck_ratio`, `graviton_integer_spin`, `photon_spin`, `graviton_spin`, `graviton_spin_two_photons`, `photon_polarizations`, `graviton_polarizations`, `massless_two_polarizations`, `LatticeField`, `d2t`, `d2x`, `boxD`, `rightMover`, `leftMover`, `boxD_rightMover`, `boxD_leftMover`, `dAlembert`, `boxD_dAlembert`, `metricPerturbation`, `boxD_metricPerturbation`, `TimeSeries`, `ddt2`, `monopole_no_radiation`, `dipole_no_radiation`, `quadrupole_radiates`, `quadrupole_is_leading_radiative`, `gravitational_wave_substrate_summary`, `gravitational_waves_in_progress` |
| [QLF_FlavorMixing.lean](QLF_FlavorMixing.lean) | **CKM/PMNS parameter count + the Kobayashi–Maskawa CP condition** ([Standard_Model.md §4.2](../Standard_Model.md)). An `N×N` unitary mixing matrix has `N(N−1)/2` physical mixing angles (`mixing_angles`) and `(N−1)(N−2)/2` CP-violating phases (`cp_phases`); QLF's **exactly three generations** (`num_generations = 3`, `QLF_Generations`) give exactly **3 angles + 1 CP phase** (`substrate_mixing_parameters`) — the CKM/PMNS content (θ₁₂, θ₂₃, θ₁₃ + δ). **Kobayashi–Maskawa**: a physical CP phase needs `N ≥ 3` — `0` for one or two generations (the Cabibbo case has one angle, no CP), `1` for three (`cp_requires_three_generations`); so the substrate's three-ness — the same `3` behind Koide, colour SU(3), and `α`'s `N=3²` — is why CP violation is possible. Honest scope (`flavor_mixing_in_progress`): anchors the **counting** + KM condition (both exact), **not** the angle values (the Yukawa/mass-matrix sector, open like the Koide δ); the quark-small (hidden chirality) vs lepton-large (exposed, near tri-bimaximal) contrast is a structural reading on the same hidden/exposed-chirality axis as the pion/black-hole work | `mixing_angles`, `cp_phases`, `three_generation_mixing_angles`, `three_generation_cp_phase`, `two_generation_one_angle_no_cp`, `one_generation_no_mixing`, `cp_requires_three_generations`, `substrate_mixing_parameters`, `flavor_mixing_in_progress` |
| [QLF_CondensedMatter.lean](QLF_CondensedMatter.lean) | **The quantum Hall resistance from α, and Cooper pairs as bosons** ([Electricity.md §6–§7](../Electricity.md)). The **von Klitzing constant** `R_K = h/e² = Z₀/(2α)` (`von_klitzing`, `Z₀` = vacuum impedance) — and because QLF *derives* `α = 1/137` (`alpha_QLF_eq`), it is fixed by the substrate: `R_K = Z₀·137/2 ≈ 25806 Ω` vs measured `25812.807 Ω`, the **0.026%** that is exactly the α error (`von_klitzing_substrate`). The integer-quantum-Hall plateaus `R_xy = R_K/ν` (`hall_resistance`) are the substrate's α made macroscopically visible — the most precisely measured resistance in metrology reading back the 8-twist combinatorial constant. A **Cooper pair** is two half-spin closures = an even pair count folding to `+I` = an integer-spin **boson** (`cooper_pair_boson`, reusing `boson_even_pairs` from `QLF_Spin`), so it condenses into the coherent supercurrent channel. Honest scope (`condensed_matter_in_progress`): anchors `R_K`, the integer-QHE quantization, and Cooper-pair-is-a-boson; **not** the BCS gap equation, the *fractional* QHE / anyons (2D braiding), or topological band structure | `von_klitzing`, `von_klitzing_substrate`, `hall_resistance`, `hall_plateau_one`, `conductance_quantum`, `cooper_pair_boson`, `condensed_matter_in_progress` |
| [QLF_CosmicInflation.lean](QLF_CosmicInflation.lean) | **Inflation (past) and gravity (present) as one event duality** ([Curvature.md §8](../Curvature.md)). Each ZFA event expands the future and contracts locally — two faces of one per-event quantum, oppositely signed (`event_duality_balanced`). The reusable core: a static event-synthesis field has equation of state `w = −1` (`zfa_dynamics_drive_acceleration`, `ZFAEventDynamics`), so **inflation and dark energy are the same `w = −1` field at two energy scales** (`inflation_and_dark_energy_same_field`) — high `V` early (inflation), low `V` now (dark energy): **inflation without an inflaton** (the "inflaton" is QLF's event-synthesis field). Friedmann `H ∝ √V` (`higher_energy_faster_expansion`) makes the early high-energy epoch inflate faster than today. Temporal vantage (`temporal_vantage_summary`): past = high-`V` expansion (inflation), present-local = contraction (gravity), future = residual `w=−1` (dark energy, `Ω_Λ=log2`). Honest scope (`cosmic_inflation_in_progress`): anchors the duality, the `√V`-monotonicity, and the shared-`w=−1` unification; **not** the inflation observables (e-folds ~60, `n_s≈0.965`, `r`, reheating) or the vacuum-frequency evolution `f(t)` | `future_expansion`, `local_contraction`, `event_duality_balanced`, `expansion_rate`, `higher_energy_faster_expansion`, `inflation_and_dark_energy_same_field`, `temporal_vantage_summary`, `cosmic_inflation_in_progress` |
| [QLF_StrongCP.lean](QLF_StrongCP.lean) | **`θ̄ = 0` without an axion** ([CP-Violation-and-Chirality.md §4a](../CP-Violation-and-Chirality.md)). The strong-CP `θ`-term is a CP-odd topological winding (a signed count flipping under charge conjugation). QLF proves *every* CP-odd (annihilation-odd) signed count is **exactly zero on every ZFA closure** (`cp_odd_winding_zero_on_closure`, the general statement; `theta_zero_on_closure` for the canonical CP-odd weight `chargeWeight`) — reusing `wcount_zero_on_ZFA` + `chargeWeight_annihilationOdd` from `QLF_BMinusL`, the same mechanism as charge neutrality and the `B−L` obstruction. So `θ̄ = 0` holds on every physical (ZFA-closed) state with **no axion and no fine-tuning** — ZFA closure does the Peccei–Quinn symmetry's job. Honest scope (`strong_cp_in_progress`): the identification of the QCD `θ`-vacuum / gluonic `G·G̃` with a QLF CP-odd signed winding is structural; the instanton θ-vacuum is not field-theoretically constructed | `cp_odd_winding_zero_on_closure`, `theta_charge`, `theta_zero_on_closure`, `strong_cp_in_progress` |
| [QLF_Baryogenesis.lean](QLF_Baryogenesis.lean) | **The three Sakharov conditions are met ⟹ a matter excess is generic** ([CP-Violation-and-Chirality.md §4b](../CP-Violation-and-Chirality.md)). Matter and antimatter carry *opposite* baryon winding — `B(antiparticle ts) = −B(ts)` for every history (`matter_antimatter_opposite`, reusing `baryon_dagger_odd`) — so they are distinguishable and B is not conjugation-invariant (proton `B=+1`, antiproton `B=−1`; `proton_antiproton_asymmetric`, `baryon_not_conjugation_invariant`). The Sakharov conditions all hold structurally: **(1) B-violation** (winding, not a conserved count; `B−L` violated via `neutrino_majorana`), **(2) C/CP violation** (the chirality engine + `QLF_StrongCP`), **(3) departure from equilibrium** (the inflating early universe, `QLF_CosmicInflation`). Honest scope (`baryogenesis_in_progress`): anchors the distinguishability / B-violation handle and that all three conditions hold (⟹ asymmetry generic); **not** the *magnitude* `η_B ≈ 6×10⁻¹⁰`, which is open in QLF exactly as in the Standard Model | `matter_antimatter_opposite`, `proton_antiproton_asymmetric`, `baryon_not_conjugation_invariant`, `baryogenesis_in_progress` |
| [QLF_Nucleosynthesis.lean](QLF_Nucleosynthesis.lean) | **The primordial helium fraction from the n/p ratio** ([Fusion.md §7a](../Fusion.md)). Every surviving neutron is swept into the deepest light closure, **⁴He** (doubly-magic `Z=N=2`, [`Magic_numbers.md`](../Magic_numbers.md)), so the helium mass fraction is `Y_p = 2n/(n+p) = 2r/(1+r)` with `r=n/p` (`helium_fraction`). The standard freeze-out `r ≈ 1/7` gives `Y_p = 1/4` (`helium_fraction_one_seventh`), matching observed `Y_p ≈ 0.247`; the counterfactual `r=1` (equal n,p) gives `Y_p = 1` — all helium (`helium_fraction_equal_np`) — so the quarter-helium universe requires the small freeze-out `r`. Honest scope (`nucleosynthesis_in_progress`): anchors the `Y_p = 2r/(1+r)` funnel and `r≈1/7 ⟹ Y_p≈1/4`; **not** `r` itself (the n–p mass difference + weak rates `G_F`, open), the D/⁷Li abundances, or the CMB power spectrum | `helium_fraction`, `helium_fraction_one_seventh`, `helium_fraction_equal_np`, `nucleosynthesis_in_progress` |
| [QLF_MassSpectrum.lean](QLF_MassSpectrum.lean) | **The absolute mass spectrum is one scale, exponentially generated** ([Per_Qubit_Mass_Quantum.md §3.3a](../Per_Qubit_Mass_Quantum.md)) — a serious run at the hardest open problem. **(1) One parameter.** Every QLF mass *ratio* is a verified dimensionless number (`m_p/m_e=6π⁵`, `m_p/m_π=3π⁵/137`, Koide, depth ratios), so every mass = the single proton scale `m_p` × a verified ratio (`spectrum_one_scale`; `m_e=m_p/6π⁵`, `electron_mass_from_proton_eq`, reusing `mass_ratio_QLF` + `proton_pion_ratio_eq`) — the Standard Model's ~13 independent mass parameters collapse to **one** absolute input. **(2) Dimensional transmutation.** Why is that scale `R_p≈10¹⁹` so huge? Not tuning: the strong coupling runs logarithmically (asymptotic freedom, `QLF_RunningCouplings`), reaching confinement after a depth `exp(2π/(b·α))` — `ln R = 2π/(b·α)` (`log_transmuted_hierarchy`), linear in `1/α`. With the QCD `b=7` and a moderate `α_s≈0.02`, `ln R ≈ 44.9 ≈ ln(M_Planck/m_p)=44.0`: the 10¹⁹ hierarchy from a moderate input, exponentially amplified, no fine-tuning (`weaker_coupling_larger_hierarchy` = the AF amplification). Honest scope (`mass_spectrum_in_progress`): reduces the spectrum to one scale and shows it exponentially *natural*; does **not** derive the value — the β-coefficient `b`, the substrate `α_s`, and the Planck→SI calibration (the combinatorial `R_e≈2.4×10²²` count) remain open | `electron_mass_from_proton`, `electron_mass_from_proton_eq`, `spectrum_one_scale`, `transmuted_hierarchy`, `log_transmuted_hierarchy`, `weaker_coupling_larger_hierarchy`, `mass_spectrum_in_progress` |
| [QLF_BetaFunction.lean](QLF_BetaFunction.lean) | **The QCD asymptotic-freedom coefficient `b₀ = 7` from the substrate** ([TheContinuum.md §3.1](../TheContinuum.md)) — completing the transmutation. The one-loop `b₀ = 11 N_c/3 − 2 n_f/3` with `N_c = color_count = substrate_spatial_dimension = 3` (the three spatial axes / SU(3) of `QLF_StrongAlgebra`) and `n_f = flavor_count = 2·num_generations = 6` (two flavours per generation × the three generations, `QLF_Generations`) gives `b₀ = 11·3/3 − 2·6/3 = 7` (`beta_coefficient_eq_seven`, `substrate_qcd_counts`). Gluon antiscreening `11 > 4` quark screening ⟹ `b₀ > 0` = **asymptotic freedom** (`asymptotic_freedom_from_substrate`), which feeds the hierarchy `ln R_p = 2π/(7 α_s)` (`QLF_MassSpectrum`). Honest scope (`beta_function_in_progress`): QLF fixes the *counts* `N_c=3`, `n_f=6`; the `11/3`,`2/3` one-loop coefficient *structure* is standard β-function group theory (input), and `α_s` + calibration + the electroweak coefficients remain open | `color_count`, `flavor_count`, `substrate_qcd_counts`, `beta_coefficient`, `beta_coefficient_eq_seven`, `asymptotic_freedom_from_substrate`, `beta_function_in_progress` |
| [QLF_Anyons.lean](QLF_Anyons.lean) | **Fractional statistics from a 2D braiding phase** ([Electricity.md §6–§7](../Electricity.md)) — completing the condensed-matter sector. In 3D, exchanging two identical particles squares to `1`, so only `±1` is allowed — bosons/fermions, *which are* the two elements `{+I,−I}` of the SU(2)→SO(3) double-cover kernel (`QLF_Spin`). In **2D** the exchange braids, so the phase is a continuous `e^{iθ}` (`exchange_phase`): **anyons** — `boson_phase` (θ=0 ⟹ `+1`), `fermion_phase` (θ=π ⟹ `−1`, via `Complex.exp_pi_mul_I`), the double-braid `(e^{iθ})²=e^{2iθ}` (`double_braid`) generally `≠1` where the 3D one is necessarily trivial (`fermion_double_trivial`). Semion (`θ=π/2`) and Laughlin `ν=1/m` (`θ=π/m`) phases. Honest scope (`anyons_in_progress`): anchors the braiding algebra + boson/fermion/anyon phases + the 3D-vs-2D contrast; **not** the FQHE filling fractions `ν` or the Laughlin many-body wavefunction | `exchange_phase`, `boson_phase`, `fermion_phase`, `double_braid`, `fermion_double_trivial`, `semion_phase`, `laughlin_phase`, `anyons_in_progress` |
| [QLF_MuonG2.lean](QLF_MuonG2.lean) | **Placing the muon `g−2` honestly** ([g_minus_2.md §4a](../g_minus_2.md)). The famous ~5σ *data-driven* muon-`g−2` discrepancy, placed without overclaiming. **Leading term is universal:** the one-loop QED vertex is mass-independent, so `a_μ = α/(2π) = a_e` (`a_mu_leading_eq_a_e`, reusing `a_e_QLF_eq_schwinger`) to the same ~0.6%. **Why the muon is the probe:** its sensitivity to hadronic vacuum-polarization loops is amplified by `(m_μ/m_e)² ≈ 42753` (`hadronic_sensitivity_value`) — so a hadronic-sector discrepancy is a *muon* effect, invisible in the electron; the dominant hadronic contribution is the `ππ`/`ρ` channel = the pion (the deepest hadronic horizon, `QLF_QuantumBlackHole`). **Honest status:** the residual is the hadronic-vacuum-polarization sector — (a) QLF's open hadronic quantitative frontier (no quark masses/`f_π`) and (b) experimentally **unsettled** (data-driven ~5σ vs lattice BMW + CMD-3 ~1σ). QLF claims **no** new-physics anomaly (`muon_g2_in_progress`) | `a_mu_leading`, `a_mu_leading_eq_a_e`, `muon_electron_ratio`, `hadronic_sensitivity`, `hadronic_sensitivity_value`, `muon_g2_in_progress` |
| [QLF_AlphaS.lean](QLF_AlphaS.lean) | **The substrate strong coupling, and the hierarchy from one integer** ([Per_Qubit_Mass_Quantum.md §3.3b](../Per_Qubit_Mass_Quantum.md)) — closing `QLF_MassSpectrum`'s last input. Posit `α_s(substrate) = 1/b₀²` (`substrate_alpha_s`), *consistent with the measured running* (`1/α_s(M_Planck) ≈ 52 ≈ b₀² = 49`, ~7%). Then the dimensional-transmutation hierarchy **collapses to a pure integer**: `ln R_p = 2π/(b₀·α_s) = 2π·b₀` (`log_hierarchy_pure_integer`, `log_transmuted_hierarchy_integer` reusing `QLF_MassSpectrum`). With the substrate `b₀ = 7` (`N_c=3`, `n_f=6`, `QLF_BetaFunction`): `ln R_p = 14π ≈ 43.98` vs measured `ln(M_Planck/m_p) ≈ 44.01` — **0.07%** (`hierarchy_log_eq_fourteen_pi`). So `R_p = e^{2π b₀} = e^{14π}`, and the entire absolute mass spectrum follows from the **single integer `7`**. Honest scope (`alpha_s_substrate_in_progress`): `α_s=1/b₀²` is a running-consistent *posit*, not a derivation; the value-level match is ~3% (`e^{14π}=1.26×10¹⁹` vs `1.30×10¹⁹` — the Planck-mass/SI calibration), the log match 0.07% | `substrate_alpha_s`, `log_hierarchy_pure_integer`, `log_transmuted_hierarchy_integer`, `hierarchy_log_eq_fourteen_pi`, `alpha_s_substrate_in_progress` |
| [QLF_EinsteinEquations.lean](QLF_EinsteinEquations.lean) | **The Einstein equations as the substrate's equation of state** ([Einstein_Equations.md](../Einstein_Equations.md), [Kitada_Local_Time_GR.md §5.2](../Kitada_Local_Time_GR.md), [GR_Schwarzschild.md](../GR_Schwarzschild.md)). Following **Jacobson (1995)**, the full field equations `G_μν = 8πG T_μν` are the **equation of state** of horizon thermodynamics — the Clausius relation `δQ = T δS` on every local Rindler horizon — not a fundamental dynamical law. QLF supplies *both* of Jacobson's inputs from its own substrate: the area law `S = 4πR² log 2` (`QLF_GravityFromDelay`, entropy density `η = 1/4G`) and the Unruh temperature (`QLF_HorizonTemperature`). These force the coefficient to be the **Unruh `2π` over the entropy density**: `8πG = 2π/η` (`einstein_coupling_from_thermodynamics`), the same `8π = 4π·2` (boundary solid angle × Hermitian-pair degeneracy) as `QLF_EinsteinGeometricFactor` (`einstein_coupling_geometric`); the integration constant is the cosmological constant `Λ = Ω_Λ = log 2` (`QLF_CosmologicalConstant`). **Kitada local-time tie:** Jacobson's derivation is *local* — `δQ=TδS` at each local Rindler horizon — and that horizon **is** the QLF Markov blanket = Kitada local clock (`markov_blanket_local_clock`, `QLF_LocalClock`); so the Einstein equation of state is the Clausius relation evaluated at each local clock, global GR is the local-clock network in simultaneous local equilibrium, and `Λ = log 2` is the local clock's own tick (`local_clock_tick_is_log_two`). Honest scope (`einstein_equations_in_progress`): anchors the **coefficient + thermodynamic skeleton**, *not* the full tensor derivation — the local Rindler construction, Raychaudhuri focusing, and general covariance need differential-geometry machinery QLF's Lean core lacks (the same dynamical-metric step still open for the Schwarzschild metric and gravitational waves) | `entropy_density`, `einstein_coupling`, `einstein_coupling_from_thermodynamics`, `einstein_coupling_geometric`, `einstein_equations_in_progress` |
| [QLF_Fusion.lean](QLF_Fusion.lean) | **The β⁺ keystone — joining two Markov blankets needs distinguishability** ([Fusion.md](../Fusion.md) §3a, [SEX.md](../SEX.md), [Beta_Decay_Neutrino_Nature.md](../Beta_Decay_Neutrino_Nature.md)). The pp-chain's first step `p+p→²H+e⁺+ν` is *simultaneously* a fusion (two blankets join) and a β⁺ decay (one proton→neutron), and the **insulator proof** says why it must be both. Two *identical* proton blankets have **no** bound fermionic channel — `fermi_antisym p p = 0` (`diproton_pauli_blocked`, reusing **`pauli_exclusion`**) — so there is no diproton (²He unbound) and the §2 merger pathway is *Pauli-insulated*. A *distinguishable* `p+n` Hermitian-pair channel, by contrast, **closes** to identity (`deuteron_channel_closes`, reusing `QLF.Spin.opposite_spin_singlet_closes`). Packaged as **`pp_join_requires_distinguishability`** (the conjunction of the two): the first Markov-blanket join therefore requires a β⁺ `u→d` step to make the two protons distinguishable — **the weak force is the precondition for fusion**, and its weak-mediated rarity is why the Sun burns over billions of years rather than detonating (`no β⁺ → no deuteron → no chain`, feeding the quarter-helium universe of `QLF_Nucleosynthesis`). Honest scope (`fusion_weak_rate_in_progress`): the **necessity** is owned (binds two already-verified theorems, no new axioms); the β⁺ **rate** — the cross-section / weak coupling `G_F` that sets how slow the pp-chain is — stays the open weak-rate sector | `diproton_pauli_blocked`, `deuteron_channel_closes`, `pp_join_requires_distinguishability`, `fusion_weak_rate_in_progress` |
| [QLF_InfoSynthesis.lean](QLF_InfoSynthesis.lean) | **Information synthesis as disjunctive (OR) closure** ([MRE.md](../MRE.md), [Active_Inference_Mathematics.md](../Active_Inference_Mathematics.md), [P_vs_NP_QLF.md](../P_vs_NP_QLF.md)). A ZFA closure takes the **random signal** of the possibility stream — every admissible history, generated unbiased (`expand_generation`) — and **closes on an OR condition**: `List.any verify` is the Boolean OR-fold `⋁_{s ∈ generated} verify s`. **`disjunctive_closure`**: `(expand_generation (2n)).any verify = true ↔ ∃ s ∈ generated, verify s` — closing on the OR *is* the existential (the synthesis step that turns noise into a definite closure). **`disjunct_count_eq_central_binomial`**: the OR has exactly `C(2n,n)` satisfying disjuncts (the verify-filter length, reusing `realized_count_eq_central_binomial` from `QLF_PvsNP`) — massively degenerate, the boundary is the OR over `~4ⁿ/√(πn)` interior histories (holographic screening). **`closure_always_fires`**: `C(2n,n) ≥ 1`, so the disjunction is always satisfiable — a random signal always closes, synthesis never stalls. The realized closure synthesizes one bit `ΔF = −log 2` (`QLF_FreeEnergy`). Honest scope (`info_synthesis_disjunctive`): the disjunctive **structure** is anchored (no new axioms); the log-2 synthesis (`QLF_FreeEnergy`) and the OR-looks-lossy-vs-unitarity tension — resolved holographically as a **screened boundary-OR** (which-disjunct-fired coarse-grained out of the exterior, bulk retains it via QEC) — stay prose | `disjunctive_closure`, `disjunct_count_eq_central_binomial`, `closure_always_fires`, `info_synthesis_disjunctive` |
| [QLF_MuonCatalysis.lean](QLF_MuonCatalysis.lean) | **Lepton-catalyzed fusion is QLF cold fusion — rate, not necessity** ([Fusion.md](../Fusion.md) §3b). **Muon-catalyzed fusion** (μCF) is the *legitimate* cold fusion — fusion at room temperature, Frank/Sakharov/Alvarez 1956, **distinct** from the discredited Fleischmann–Pons claim — reproduced **in agreement with the Standard Model**. A μ⁻ (≈207× the electron mass) shrinks the muonic molecule ≈207×, collapsing the Coulomb barrier and boosting the overlap `|ψ(0)|²`. QLF reading: "cold" = crossing the [Fusion.md](../Fusion.md) §2 critical-density threshold by **generation-depth** (a deeper-generation completer `e⁻/μ⁻/τ⁻` shrinks the blanket, raising `ρ`) rather than temperature; **α-sticking** = the muon blanket captured into the deep doubly-magic ⁴He closure (a deeper attractor). The structural claim QLF owns: **catalysis touches rate, not necessity** — `catalysis_preserves_necessity` (the identical-pair Pauli block `fermi_antisym p p = 0` is *catalyst-independent*: no completer makes two identical protons distinguishable, only a real `u→d` β⁺ does) and `catalyzed_join_still_requires_beta` (the full §3a keystone `pp_join_requires_distinguishability` holds with any catalyst present). Honest scope (`muon_catalysis_in_progress`): **D-T not p-p** (catalysis boosts the overlap prefactor, not the weak `G_F²` vertex, so p-p stays Sun-slow); the **τ⁻ is too short-lived** to catalyze (0.29 ps ≪ molecular-formation time — the generation depth↔lifetime trade-off); and the **muon economy** (~2× energy-negative: ≈5 GeV/muon vs ≈150 cycles × 17.6 MeV, capped by α-sticking + the 2.2 µs lifetime) is SM/engineering, not a QLF gap | `catalysis_preserves_necessity`, `catalyzed_join_still_requires_beta`, `muon_catalysis_in_progress` |
| [QLF_LoopClosure.lean](QLF_LoopClosure.lean) | **The closure machine vs the `2π` rendering — the dependency direction** ([TheContinuum.md](../TheContinuum.md), [Continuum_Choice_Fallacy.md](../Continuum_Choice_Fallacy.md); issues #59/#71/#73). Answers the recurring π/closure critique: when QLF writes `2π`, is it *the machine* or *the display of a finite closure*? Separates Allen's three objects. The **closure operation** is `phase k N = k % N` — finite, decidable, RCA₀, **no `Real.pi`** (`phase_full_cycle`: advancing a whole cycle returns the same phase; `phase_lt`: a phase is a finite-alphabet residue `< N`). The **continuum `2π`** enters only in `renderAngle k N = 2π·k/N` and is *recovered* as the rendered full cycle (`render_full_cycle`: `renderAngle (k+N) N = renderAngle k N + 2π`; `render_one_cycle`), never imported as the source of closure; `τ_ZFA = 2·π_QLF` named (`tau_is_two_pi_QLF`). So the machine is `% N`; `2π` is the display. **Key reframing (per Jim):** `π` is a *computable* real (RCA₀) — precision was never the issue (the #37 audit shows ≤15 digits suffice); only the dependency direction needed tidying, and it is explicit. Open: which physical `N` a given loop closes on (`loop_closure_value_in_progress`) | `cycleTicks`, `phase`, `phase_full_cycle`, `phase_lt`, `renderAngle`, `render_full_cycle`, `render_one_cycle`, `tau_ZFA`, `pi_QLF`, `tau_is_two_pi_QLF`, `loop_closure_value_in_progress` |
| [QLF_ReachableEvent.lean](QLF_ReachableEvent.lean) | **Closure-reachability as a pre-geometric Lean object** ([SpaceTime.md](../SpaceTime.md), [TheContinuum.md](../TheContinuum.md); issues #63, #72). Supplies the substrate "reachable-event" object of the #46 stack with no spacetime primitive. An `Event α = List α` is a finite ZFA history (no coordinates, no manifold); **`reachable A B := A <+: B`** — `B`'s history extends `A`'s (`A` in `B`'s past) — is defined purely by history-extension. It is a **partial order / causal set** (Bombelli–Sorkin): `reachable_refl`, `reachable_trans`, `reachable_antisymm`. The future of `A` is `futureCone A = {B | reachable A B}` — the set the continuum **light cone / causal diamond renders** (`futureCone_subset`: cones nest along reachability). **Answers #72** ("what drives closure succession *before* time?"): the history-extension partial order is the pre-temporal succession driver — it exists with *no time coordinate*; time is its rendered total-order read-out (the "everything is a clock" picture). Honest scope (`light_cone_rendering_in_progress`): does not reconstruct the continuum light-cone *metric* from the discrete order (the Causal-Set order→metric step, the continuum boundary) nor bind `reachable` to the full `full_zeno_prune` dynamics. No new axioms | `Event`, `reachable`, `reachable_refl`, `reachable_trans`, `reachable_antisymm`, `futureCone`, `mem_futureCone_self`, `futureCone_subset`, `light_cone_rendering_in_progress` |
| [QLF_SU5.lean](QLF_SU5.lean) | **The `5̄⊕10` generation as the antisymmetric tensor content of QLF's `3⊕2`** ([Forces_From_Three_Axes.md](../Forces_From_Three_Axes.md) §5a, [Weak_Force.md](../Weak_Force.md) §2). Follow-on to `QLF_WeinbergAngle`'s `sin²θ_W=3/8`: checks SU(5)'s one-generation fermion content against the substrate. The `15` Weyl fermions of a generation = `5̄ ⊕ 10` = the **rank-≤2 antisymmetric tensors over the fundamental `5`** (rank 1 → `5̄`, rank 2 → `Λ²(5) = C(5,2) = 10`), and QLF *identifies* `5 = colour(3) ⊕ weak(2)` — the same `3+2` behind `α` (N=9=3²), `Ω_Λ` (2/8), `sin²θ_W` (3/8). Decomposition: `5̄ = 3̄⊕2` (`d^c` ⊕ lepton doublet, `3+2=5`); `10 = Λ²3 ⊕ (3⊗2) ⊕ Λ²2 = u^c ⊕ Q ⊕ e^c = 3+6+1` (`ten_decomposition`, `ten_pieces`); `generation_eq_fifteen`. The antisymmetry of the `10` **is the Pauli/fermionic wedge**; the count is **15, not SO(10)'s 16** (`so10_eq_sixteen`), matching QLF's Majorana neutrino (no independent light Dirac `ν_R`). Honest scope (`su5_generation_content_in_progress`): anchors the **counting + group-theoretic decomposition under the `5=3⊕2` identification** — `5̄⊕10 = Λ^{≤2}(5)` is standard SU(5) rep theory, QLF's content is the substrate identification — **not** the hypercharges, the chirality, or the per-field twist-closure map. Part of QLF's SU(5) relationship: reproduces the parameter-free wins (`3/8`, the 15, charge quantization) + explains no-proton-decay (baryon winding), without a GUT embedding | `colour`, `weak`, `fundamental`, `fundamental_eq_five`, `antisym2`, `antisym2_eq_ten`, `generation`, `generation_eq_fifteen`, `ten_decomposition`, `ten_pieces`, `fivebar_decomposition`, `so10_generation`, `so10_eq_sixteen`, `su5_generation_content_in_progress` |
| [QLF_CausalInterval.lean](QLF_CausalInterval.lean) | **Number↔volume — the curvature side of the Einstein equations begins** ([Einstein_Equations.md](../Einstein_Equations.md) §6a, [TheContinuum.md](../TheContinuum.md)). `QLF_EinsteinEquations` anchored the Einstein *equation of state* (coefficient `8πG=2π/η`, `Λ=log2`); this advances the open *tensor/curvature* side, which is **not** generic missing differential geometry but the **causal-set order→metric program** (Sorkin / Benincasa–Dowker) on QLF's causal set (`QLF_ReachableEvent`). First rung: the **causal (Alexandrov) interval** `causalInterval A B = {C \| reachable A C ∧ reachable C B}` (the events causally between `A` and `B`, from order alone), and CST's **number↔volume** principle as `intervalVolume A B = \|B\|−\|A\|+1` — the Markov-blanket **depth difference** = the **Kitada local-clock tick count** between the two events. Theorems: `left_mem_interval`/`right_mem_interval` (endpoints in the interval), `intervalVolume_self` (one tick), **`intervalVolume_additive`** (proper time is additive along a causal chain `A≤B≤C`, sharing the endpoint — the discrete seed of the line element), `reachable_length_mono`; **`causalInterval_eq`** (the interval is exactly the prefixes of `B` no shorter than `A`) and **`interval_isChain`** (every prefix-order interval is *totally ordered* — a single history line is **flat**). The chain result is a *sharpening*: a flat chain has no curvature, so the Ricci scalar must come from the **branching** of the closure graph (incomparable histories / antichains, the `expand_generation` QuCalc tree) — exactly where the Benincasa–Dowker d'Alembertian samples it. **`layer x k`** = the BD causal layer `{y ≤ x : volume[y,x]=k}` (the d'Alembertian's input), and **`layer_unique`** proves that in the single-history substrate every layer is a **singleton**. **The Benincasa–Dowker curvature operator is anchored at its flat baseline:** **`bdCoeff`** is the `+1,−2,+1` second-difference stencil, **`bdCoeff_sum_zero`** proves its coefficients are balanced (sum to zero — the property that makes it read the *second difference* of layer occupations, i.e. curvature, not a bare count), **`layerCard`/`layerCard_chain`** give the layer cardinalities (a chain's in-range layers have cardinality 1), **`bdCurvature`** is the BD reading (the balanced alternating sum of the first three layer cardinalities), and **`bdCurvature_chain_zero`** proves a single history of depth ≥2 reads `R=0` — the reading collapses to `+1−2+1=0`, the 1-D discrete second difference annihilating a constant. So the `R=0` baseline is anchored in the *actual* curvature operator; the spatial dimensions *and* the curvature are both the *growth* of `|L_k|` once the graph branches (dovetailing with the 3D graph-rendering of `SpaceTime.md` §3a). Reuses `QLF_ReachableEvent`, no new axioms. Honest scope (`einstein_curvature_in_progress`): `|L_k|` on the branching graph through the BD sum → the **Ricci scalar**, and the **continuum limit** to `G_μν = 8πG T_μν`, stay the named open step — a concrete CST program | `causalInterval`, `intervalVolume`, `reachable_length_mono`, `left_mem_interval`, `right_mem_interval`, `intervalVolume_self`, `intervalVolume_additive`, `causalInterval_eq`, `interval_isChain`, `layer`, `layer_unique`, `layerCard`, `layerCard_chain`, `bdCoeff`, `bdCoeff_sum_zero`, `bdCurvature`, `bdCurvature_chain_zero`, `einstein_curvature_in_progress` |
| [QLF_CausalDimension.lean](QLF_CausalDimension.lean) | **Dimension from combining histories — number↔volume reads the dimension** ([Einstein_Equations.md](../Einstein_Equations.md) §6a, [SpaceTime.md](../SpaceTime.md) §3a). A *single* QLF history is a 1-D **chain**; combining two by the **product order** gives a 2-D causal diamond = `1+1` Minkowski in light-cone coordinates (the two null directions are two histories / local clocks). The Myrheim–Meyer principle (event count `~ (proper time)^d`) appears as a **multiplicity** fingerprint: `chainVolume d = d+1` is **injective** (`chainVolume_injective` — one interval per volume = singleton layers, the 1-D / flat signature), whereas `diamondVolume m n = (m+1)(n+1)` is the **product** of the chain volumes (`diamond_eq_product`) and **many-to-one** (`diamondVolume_collision`: `1×1`, `0×3`, `3×0` all have volume `4` = layer multiplicity / growth). So **adding a causal direction multiplies the count and makes volumes collide** — combining histories raises the dimension, and that growth of the Benincasa–Dowker layers is the same phenomenon as curvature; it is also the same branching that `SpaceTime.md` §3a renders into three spatial dimensions. **The branching layer-growth is computed directly on the product order:** `prodIntervalVolume i j m n = (m−i+1)(n−j+1)` (number↔volume on the combined grid), `prodLayer`/`prodLayerCard` (the BD layer and its cardinality), and the growth itself — `prodLayerCard_chain_link` (one history → singleton volume-2 layer, `|L₂|=1`), `prodLayerCard_diamond_link` (two histories combined → the apex's two immediate predecessors `(0,1)`,`(1,0)` = the two null directions, `|L₂|=2`), `prodLayerCard_link_stable` (size-independent: `=2` for diamonds, `=1` for 1-D strips — a dimension fingerprint), and `layer_growth_from_branching` (the `1→2` growth past the `bdCurvature_chain_zero` flat baseline). Reuses `QLF_CausalInterval`, no new axioms. Honest scope (`causal_dimension_in_progress`): the layer *growth* (the BD input departing from flat) is computed; the **Ricci scalar** is this growth read in the **statistical continuum limit** (sprinkling average), not the finite count of a small diamond — that, with general `d ≥ 3` and the Myrheim–Meyer continuum limit, stays open | `chainVolume`, `diamondVolume`, `diamond_eq_product`, `chainVolume_injective`, `diamondVolume_collision`, `prodIntervalVolume`, `prodLayer`, `prodLayerCard`, `prodLayerCard_chain_link`, `prodLayerCard_diamond_link`, `prodLayerCard_link_stable`, `layer_growth_from_branching`, `causal_dimension_in_progress` |
| [QLF_CausalContinuum.lean](QLF_CausalContinuum.lean) | **The statistical continuum limit of the Benincasa–Dowker curvature operator** ([Einstein_Equations.md](../Einstein_Equations.md) §6a) — the Einstein curvature side in the Millennium pattern (verified discrete core + one named continuum bridge). The discrete rungs (`bdCurvature_chain_zero` flat `R=0`; `layer_growth_from_branching` `\|L_k\|: 1→2` under branching) pass to the smooth Ricci scalar **statistically**: Benincasa–Dowker (2010) sprinkle points by a Poisson process of intensity `ρ` into a Lorentzian region and take the `ρ→∞` *expectation*. **Proven (the statistical kernel):** `poissonOccupation lam k = e^{−lam} lam^k / k!` — the expected BD layer occupation under a sprinkling of (intensity × volume) `lam` (`poissonOccupation_nonneg`); and the **Poisson layer recurrence** `poissonOccupation_succ` (`⟨N_{k+1}⟩(k+1) = ⟨N_k⟩ lam`), the bridge carrying the verified discrete `\|L_k\|` counts into the sprinkling expectations. **Bridge axiom `benincasa_dowker_limit`** (with opaque `bdMeanOnConstant`): the `ρ→∞` mean of the BD operator on a constant → `−R/2` — the curved convergence, settled CST Poisson + Lorentzian-volume machinery Mathlib lacks assembled, the `RCA₀→analytic` boundary parallel to `yang_mills_gap` / `continuum_vorticity_planck_capped`. **Derived:** `flat_curvature_zero_in_mean` — flat space (`R=0`) reads `0` in the mean, the statistical survival of `bdCurvature_chain_zero`. So the Einstein curvature side has the Millennium shape: a verified discrete core plus one continuum bridge, like Riemann / Yang–Mills / Navier–Stokes | `poissonOccupation`, `poissonOccupation_nonneg`, `poissonOccupation_succ`, `bdMeanOnConstant`, `benincasa_dowker_limit`, `flat_curvature_zero_in_mean`, `bd_continuum_limit_summary` |
| [QLF_OrderMetric.lean](QLF_OrderMetric.lean) | **The order → metric reconstruction — *Order + Number = Geometry*** ([Order_Metric_QLF.md](../Order_Metric_QLF.md)) — the named frontier of QLF's synthesized-spacetime program, in the Millennium pattern (verified discrete core + one named continuum bridge). Sorkin's decomposition of the metric: **`conformal_structure_is_the_order`** — *Malament's theorem* (1977: the causal order fixes the metric up to a conformal factor); on the substrate that order is `reachable`, a verified **partial order** (reusing `reachable_refl`/`trans`/`antisymm`), so the substrate already carries the conformal/light-cone structure — the **"Order"** half. **`properTime A B = \|B\|−\|A\|`** = `intervalVolume − 1` (`properTime_succ_eq_volume`), **additive along the order** (`properTime_additive`) — the discrete timelike line element / conformal factor from the count, the **"Number"** half. Dimension ([`QLF_CausalDimension`](QLF_CausalDimension.lean)) and curvature ([`QLF_CausalContinuum`](QLF_CausalContinuum.lean), `benincasa_dowker_limit`) complete the metric data. **Bridge axiom `order_metric_continuum_limit`** (opaque `continuumProperTime` / `reconstructedProperTime`): as the sprinkling intensity `ρ→∞`, the Causal-Set reconstruction of the line element from order + number converges to the continuum Lorentzian value — settled CST mathematics (Malament + Bombelli–Henson–Sorkin sprinkling + Myrheim–Meyer dimension), the explicit `RCA₀→analytic` boundary parallel to `benincasa_dowker_limit` / `yang_mills_gap` / `continuum_vorticity_planck_capped`. **Reduces** the formerly-opaque `light_cone_rendering_in_progress` to a verified discrete core plus one named bridge. Reuses `QLF_CausalInterval`; no new axioms beyond the bridge | `properTime`, `properTime_self`, `properTime_succ_eq_volume`, `properTime_additive`, `conformal_structure_is_the_order`, `continuumProperTime`, `reconstructedProperTime`, `order_metric_continuum_limit`, `order_metric_reconstruction_summary` |
| [QLF_HorizonClosure.lean](QLF_HorizonClosure.lean) | **Closure is horizon-relative; observation is bounded closure** (issue #104, `Open_Problems.md`). QLF's absolute closure is `achieves_ZFA s ⟺ full_zeno_prune s = []` (prune the phase string to the empty closure *at fixpoint*). This adds the **bounded** notion: a finite-resolution horizon `boundedPrune R` applies the one-pass cancellation `zeno_prune` only `R` times, and `closedAtHorizon R s := boundedPrune R s = []` is closure *as a usable receipt at resolution `R`*. **`horizon_relative`** — the nested singlet `[+,+,−,−]` is **not** closed at horizon 1 (one pass leaves `[+,−]`) but **is** at horizon 2: the same history reads *open* to a shallow observer and *closed* to a deeper one, so open/closed is not a primitive yes/no. **`closedAtHorizon_succ`/`closedAtHorizon_mono`** — closure is stable as the horizon widens (once a receipt within a horizon, a receipt within every larger one). **`nestedSinglet_zfa`** — the witness that is closed at horizon 2 is also **absolutely** closed (`achieves_ZFA`), so the deep-horizon reading is the genuine receipt and absolute closure is the asymptotic ideal the finite horizons approach (the witness exhibits open@1, closed@2, absolutely-closed). The **observer** is a local finite-capacity information horizon (a finite-information region, `QLF_Realizability.no_continuum_in_finite_region`) reading `closedAtHorizon` at its own resolution — "observation is bounded closure, not eyeballs," never owning the unbounded absolute horizon. Reuses `QLF_Axioms`, no new axioms | `boundedPrune`, `closedAtHorizon`, `closedAtHorizon_succ`, `closedAtHorizon_mono`, `nestedSinglet`, `horizon_relative`, `nestedSinglet_zfa`, `horizon_closure_summary` |
| [QLF_MaxwellCurl.lean](QLF_MaxwellCurl.lean) | **The Maxwell curl laws as a flux-conservation closure over the event sequence** (issue #93; [Maxwell.md](../Maxwell.md)). The divergence laws are already substrate-anchored (`∇·B=0` = `no_magnetic_monopoles`, `ZFAEventDynamics`); the *curl* laws (`∇×E=−∂B/∂t`, `∇×B=μ₀J+μ₀ε₀∂E/∂t`) needed a **time-indexed event sequence** — now the causal order, whose depth = the Kitada local-clock tick. The substrate `B`-field through a loop is a census of spatial twist threads, `flux : ℕ → ℝ` of the event step. **`emf`/`faraday_local`** — Faraday's local/curl form `emf t = −(flux(t+1)−flux t)` (the `−1` = Hermitian-conjugate orientation reversal). **`faraday_integral`** — the EMF over `[0,n]` **telescopes** to `−(flux n − flux 0)`, the Stokes/integral form: the boundary circulation *closes on* the net flux through the loop (the closure process behind the Heaviside curl form). **`faraday_closed_cycle`** — `flux n = flux 0` (a closed `B`-cycle) ⟹ zero net EMF (Faraday as a ZFA closure: the circulation vanishes iff the flux is closed). **`mmf`/`ampere_integral`** — Ampère–Maxwell as the dual telescoping with an enclosed source current + displacement current. So with `∇·B=0`, all four Maxwell equations are substrate-anchored at the conservation level. Honest scope: the structural conservation content is proven; the full 3-D vector `∇×` (Stokes on the synthesized metric) is the continuum rendering. No new axioms | `emf`, `faraday_local`, `faraday_integral`, `faraday_closed_cycle`, `mmf`, `ampere_integral`, `maxwell_curl_summary` |
| [QLF_Consciousness.lean](QLF_Consciousness.lean) | **The frequency-hierarchy of resonant closures — a QLF model of consciousness** ([Consciousness.md](../Consciousness.md); structural skeleton). Self-awareness = a Markov blanket modeling self/environment/interaction ([TheBigProblem.md](../TheBigProblem.md)), realized as closures at a spectrum of frequencies — each a local clock of period `R` (its `local_clock_period`, `QLF_LocalClock`), closure frequency `f = 1/R` ([Philosophy.md](../Philosophy.md) §2). **`freq R = 1/R`** + **`freq_lt_of_lt`** (a shorter period is a higher frequency). **`bind`/`freq_bind_ge_left`/`freq_bind_ge_right`** — binding two phase-locked sub-closures into a closure-of-closures (the `disjunctive_closure` OR-fold of `QLF_InfoSynthesis`) closes at the faster rate, so its frequency is ≥ each constituent's: **the graduation** (integration shows up as a higher closure rate — the gamma-band / global-workspace ignition reading). **`consciousPeriod`** = the highest-frequency available closure (what graduates to the top of the hierarchy = conscious thought): **`conscious_internal`** (fast internal binding is conscious by default) vs **`conscious_external`**/**`quieting_shifts_to_external`** (quiet the internal closures and the conscious content shifts to the **low-frequency external joint closure** — the cosmic/meditative *receiver* regime, coupling to the de Sitter horizon / collective joint closures). Honest scope: the **functional architecture** (which closure is conscious, why tuning/binding selects it); the **hard problem (qualia) is bracketed**, a stance offered not a proof. Reuses the `f=1/R` identity of `QLF_LocalClock`; no new axioms | `freq`, `freq_lt_of_lt`, `bind`, `freq_bind_ge_left`, `freq_bind_ge_right`, `consciousPeriod`, `conscious_internal`, `conscious_external`, `quieting_shifts_to_external`, `consciousness_frequency_hierarchy_summary` |
| [QLF_PrimeResonance.lean](QLF_PrimeResonance.lean) | **Prime frequencies are the irreducible modes; the half-spin prime-3 keystone** ([Geometry_Of_Space.md](../Geometry_Of_Space.md)) — the **first Lean anchor for prime topology stability** ([Prime_Topology_Stability.md](../Prime_Topology_Stability.md), until now prose). **`prime_freq_irreducible`** — a closure of prime period `R` has no nontrivial sub-closure repeat (only `1`,`R` divide it, via `Nat.Prime.eq_one_or_self_of_dvd`), so the vacuum's Zeno-pruning can't factor it into a repeat of a shorter stable closure: the proton `n=3` topological lock. **`composite_freq_factors`** (`4=2·2`, not prime — decomposable/prunable). **`higher_freq_dominates`** — the shorter-period (higher-frequency) closure dominates the rendering (reuses `QLF_Consciousness.freq_lt_of_lt`); the dominant is the highest-frequency, *prime* mode (conscious content inner, finest structure outer). **The half-spin keystone (Jim's "balanced and prime"):** the fermion closes only at 720° (`rotation_720_eq_id`); reading each 360° turn as **3 steps of 120°** (Koide three-phase / 3 axes / `S₃`), the half-spin is **3 forward + 3 back** (`half_spin_balanced_steps` = 6 = the double-cover return) — **balanced** (forward + Hermitian-conjugate/dagger reverse) **and prime** (`half_spin_prime` = `Nat.Prime 3`; `half_spin_irreducible` = the same lock as the proton `n=3`, at the fundamental fermion). So prime-3 is the keystone of all stable matter. **The general ladder ([Geometry_Of_Space.md](../Geometry_Of_Space.md) §3c):** orthogonality is the **one-bit** resolution of the rendered 3-D perspective (`orthogonal_distinction_is_one_bit` = `log 2`, reusing `zfa_closure_minimizes_free_energy`; the 3 orthogonal axes = 3 one-bit distinctions), and the **prime arrangements** are the irreducible structure — `small_primes_prime` (`2,3,5,7` prime), **2** the bit/spin, **3** axes/proton, **5** the icosahedral lock (`prime_five_irreducible` reusing `prime_freq_irreducible`; `five_divides_icosahedral`, `5∣\|2I\|=120`; the d-subshell `ℓ=2` is `A₅`'s 5-dim irrep, cited group theory), **7** the *derived count* QCD `b₀` (`prime_seven_is_qcd_b0` reusing `beta_coefficient_eq_seven`) **not a 7-fold symmetry**. **Sector pairing + apex:** `5 & 13` icosahedral (`centered_icosahedron_is_thirteen` = `1+12`), `7 & 11` QCD-coupling (`gluon_antiscreening_is_eleven`), apex **`31`** = E₈'s size prime (`e8_dimension_factors`: `248 = 8·31`; `e8_size_prime_31`; `e8_dim_rank_coxeter_succ`: `31 = 1 + h(E₈)`), the exceptional group the icosahedral closure maps to (McKay). **`17/19` have NO substrate lock** (number-theoretic resonances, named as the gap). Honest scope: the `Nat.Prime` + one-bit + `b₀=7` + `248=8·31` facts are exact; 2/3/5/13 are geometric prime symmetries, 7/11/31 counting/structural primes (not n-fold symmetries); the vacuum-prune gloss, the d-orbital ↔ 5-dim-irrep link (a shared representation, **not** a derivation of atomic structure), and the 3-axis/120° cut are the QLF readings (the verified `fold_electron`, `QLF_Spin`, is the 4-twist 2-D cut). Reuses `QLF_Consciousness` + `QLF_FreeEnergy` + `QLF_PrimordialMarkovBlanket` + `QLF_BetaFunction` + Mathlib `Nat.Prime`; no new axioms | `prime_freq_irreducible`, `composite_freq_factors`, `higher_freq_dominates`, `halfSpinSteps`, `half_spin_prime`, `half_spin_balanced_steps`, `half_spin_irreducible`, `orthogonal_distinction_is_one_bit`, `small_primes_prime`, `prime_five_irreducible`, `five_divides_icosahedral`, `prime_seven_is_qcd_b0`, `centered_icosahedron_is_thirteen`, `thirteen_irreducible`, `gluon_antiscreening_is_eleven`, `eleven_thirteen_prime`, `e8_size_prime_31`, `e8_dimension_factors`, `e8_dim_rank_coxeter_succ`, `prime_ladder_summary` |
| [QLF_AtomicStructure.lean](QLF_AtomicStructure.lean) | **What the substrate geometry says about atomic structure** ([Atomic_Structure_QLF.md](../Atomic_Structure_QLF.md)) — origins, not quantum chemistry. **`shells_from_pauli_exclusion`** (reuse `pauli_exclusion`): shells exist because identical closures are excluded — the periodic table's foundation (the same no-free-copy as the no-diproton / no-cloning). **`orbitalDim`** (`2ℓ+1` = `s,p,d,f,g = 1,3,5,7,9`); the orbital ladder is the 3-axis / 3-D-oscillator rendering ([Magic_numbers.md](../Magic_numbers.md)). **The icosahedral signature** — the closure symmetry is `I ≅ A₅` (irreps `1,3,3,4,5`, dims `{1,3,4,5}`): **`spd_icosahedral_sized`** — `s,p,d` dims (`1,3,5`) are each an icosahedral irrep dimension (the arithmetic shadow of the cited fact that `s,p,d` stay **unsplit** — icosahedral is the unique point group where the d-orbitals don't split); **`d_orbital_is_five`** (the 5-dim `H` irrep = the icosahedral 5-fold, cf. `QLF_PrimeResonance.five_divides_icosahedral`); **`f_orbital_breaks_icosahedral`** — `f` (`ℓ=3`, dim 7) is the **first** orbital dimension with no icosahedral irrep, the `ℓ≤2/ℓ≥3` boundary of `Magic_numbers.md`. Honest scope: the orbital-dim arithmetic is exact; the unsplit-ness and the `A₅` irreps are **cited group theory** (a shared-representation resonance `2I/A₅ → SO(3)`), **not** a derivation of the periodic table (the atom is `SO(3)`-symmetric, not icosahedral); α/scale are cited from `QLF_FineStructureSubstrate` etc. Reuses `PauliExclusion`; no new axioms | `orbitalDim`, `icosahedralIrrepDims`, `spd_icosahedral_sized`, `d_orbital_is_five`, `f_orbital_breaks_icosahedral`, `shells_from_pauli_exclusion`, `atomic_structure_summary` |
| [QLF_AngularMomentum.lean](QLF_AngularMomentum.lean) | **Angular momentum as circulation; the Navier–Stokes geometry and no-blow-up** ([Navier_Stokes_Geometry.md](../Navier_Stokes_Geometry.md)). The rotational dynamics of the geometry, and the mechanism behind `QLF_NavierStokes`'s no-blow-up. `baryonNumber` (`QLF_BaryonWinding`) is a sliding-window sum of `signTriple` — the oriented all-three-axes sign (the discrete **Levi-Civita curl**), so: **`circulation := baryonNumber`** = angular momentum (the signed 3-axis winding = Kelvin circulation, the `su(2)` Noether charge; proton `+1`, antiproton `−1`, meson `0`). **`circulation_reverses_under_time_reversal`** — angular momentum is a **pseudovector**, `L → −L` under T/parity (`antiparticle` = conjugate-and-reverse; reuses `baryon_dagger_odd`). **`vorticity a b c := signTriple (axOf a)(axOf b)(axOf c)`** = the local discrete curl; **`vorticity_antisymmetric`** — orientation-odd (`signTriple_rev`). **`signTriple_quantized`/`vorticity_quantized`** — `\|ω\| ≤ 1` per cell (`signTriple ∈ {−1,0,1}`): vorticity **cannot diverge**, so the Beale–Kato–Majda vorticity-blow-up criterion is unsatisfiable on the discrete geometry — *the* mechanism by which QLF avoids the Navier–Stokes finite-time singularity. **`circulation_bounded`** — `\|L\| ≤ n` (finite angular momentum in a finite region). **`continuum_vorticity_unrealizable`** — a continuum `ℝ`-valued vorticity (`Infinite ℝ`) has no faithful realization in a finite cell (`Finite R`), reusing `QLF_Realizability.no_continuum_in_finite_region`. The **correction is the quantization/discreteness** — the same cutoff as the UV / `10¹²²` vacuum catastrophes — giving `realized_flow_is_stable` its geometric mechanism. Honest scope: the discrete mechanism is proven; the continuum-PDE inheritance stays the named boundary `continuum_vorticity_planck_capped` (`QLF_NavierStokesBKM`). Reuses `QLF_BaryonWinding` + `QLF_Realizability`; no new axioms | `circulation`, `circulation_reverses_under_time_reversal`, `vorticity`, `vorticity_antisymmetric`, `signTriple_quantized`, `vorticity_quantized`, `circulation_bounded`, `continuum_vorticity_unrealizable`, `angular_momentum_navier_stokes_summary` |
| [QLF_NavierStokesBKM.lean](QLF_NavierStokesBKM.lean) | **Carrying the Navier–Stokes boundary via the Planck vorticity cap + Beale–Kato–Majda** ([Navier_Stokes_Geometry.md](../Navier_Stokes_Geometry.md)) — a run at *deriving* the Navier–Stokes no-blow-up. The opaque "the continuum inherits the substrate's no-blow-up" is unbundled into three transparent pieces: **(1) proven** — **`planck_caps_vorticity`**: physical vorticity = circulation quantum / cell area `≤ 1/L_P²` (the quantum `≤ 1` from `circulation_quantum_le_one`/`vorticity_quantized`; the cell area `≥ L_P²` from the Planck floor, `QLF_PlanckScale`), a *uniform* cap — **no `ω→∞` on the substrate**, pure substrate arithmetic; **(2) cited** — **`beale_kato_majda`**: a uniform vorticity bound ⟹ no finite-time singularity (the real BKM 1984 theorem, the continuum-analysis input Lean lacks — cited like Wallis/Stirling for π); **(3) the sharp bridge** — **`continuum_vorticity_planck_capped`**: the continuum solution's vorticity *is* the Planck-capped substrate vorticity (rendering faithfulness), **replacing** the opaque axiom. From these **`navier_stokes_no_blowup` is a theorem**. Honest scope: a *reduction* — the mechanism is explicit (vorticity capped at `1/L_P²`), BKM is cited not posited, and the residual gap is localized to the vorticity-rendering faithfulness (sharp & small); **not** a Clay proof. Answers "is the semi-fractal geometry sufficient?": **yes at the fixed Planck floor** (the cap *is* the floor); the Clay `v→∞` limit is the rendering step (3). Reuses `QLF_AngularMomentum` | `circulation_quantum_le_one`, `planck_caps_vorticity`, `GloballySmooth`, `beale_kato_majda`, `continuum_vorticity_planck_capped`, `navier_stokes_no_blowup`, `navier_stokes_bkm_reduction` |
| [QLF_Turbulence.lean](QLF_Turbulence.lean) | **Turbulence as a quantized-vortex tangle; the cascade as a frequency hierarchy** ([Navier_Stokes_Geometry.md](../Navier_Stokes_Geometry.md)). The vorticity-quantization finding applied to turbulence. **`vortex_quantum`** — a vortex line is one circulation quantum (`\|ω\| ≤ 1`, reuses `vorticity_quantized`). **`circulation_integer_quantized`** — total circulation is an integer count of net quanta (`circulation = baryonNumber ∈ ℤ`, bounded by the cells it threads): **Onsager–Feynman quantization derived from the substrate**, so turbulent vorticity is a discrete *quantized-vortex tangle*, not a continuum field — and **classical turbulence is the coarse-grained limit of quantum turbulence** (why superfluid/BEC turbulence reproduces the classical Kolmogorov `k^{−5/3}` cascade). **`cascade_frequency_increases`** — the cascade is a **frequency hierarchy**: a smaller eddy (shorter period `R`) has higher frequency `f=1/R` (reuses `QLF_Consciousness.freq_lt_of_lt`), so the inertial range runs from low-frequency large eddies to high-frequency small eddies. **`cascade_capped`** — a top frequency / dissipation floor (Kolmogorov, ultimately the Planck floor): the cascade is bounded above, no infinite cascade; dissipation is vortex **reconnection** (a ZFA closure) at the floor — the same vorticity cap that removes the Navier–Stokes blow-up. **It is all Navier–Stokes, two distinct questions:** the Clay **regularity** (no blow-up — reduced in `QLF_NavierStokesBKM`) and the **statistics** (the `−5/3` Kolmogorov spectrum / intermittency — a distinct, also-open question, not the Clay one). Honest scope: structural/foundational; the spectrum and intermittency statistics are **not** derived. Reuses `QLF_AngularMomentum` + `QLF_Consciousness`; no new axioms | `vortex_quantum`, `circulation_integer_quantized`, `cascade_frequency_increases`, `cascade_capped`, `turbulence_summary` |
| [QLF_NoFreeDuplication.lean](QLF_NoFreeDuplication.lean) | **The substrate forbids free Banach–Tarski duplication** ([Banach_Tarski_QLF.md](../Banach_Tarski_QLF.md)). Banach–Tarski (1924) uses the Axiom of Choice to duplicate a ball for free; the QLF substrate admits no such free copy — every real duplication **buys distinguishability and pays in information**. A *reuse-corollary* module (no new axioms, no `sorry`; Banach–Tarski itself is **not** formalized — its non-measurable pieces are non-realizable, not inconsistent: the claim is **consistency ≠ realizability**). **`identical_copy_pauli_blocked`** — two *identical* offspring closures have no bound fermionic channel (`fermi_antisym p p = 0`), the substrate's no-cloning (reuses `QLF.Fusion.diproton_pauli_blocked` = `pauli_exclusion`; genuine because `fermi_antisym` is not identically zero, `fermi_nonzero_example`). **`realizable_duplication_needs_distinguishability`** — a viable one-becomes-two needs a *distinguishable* channel (reuses the β⁺ keystone `pp_join_requires_distinguishability`). **`duplication_pays_log_two`** — minting the one distinguishing bit is a half-spin ZFA closure costing `ΔF = −log 2` (Landauer; reuses `zfa_closure_minimizes_free_energy`). One principle across four scales: no-cloning ↔ no-diproton ↔ no-free-mitosis ↔ no-Banach–Tarski — *all real duplication buys distinguishability and pays in energy/time/information*. Honest scope: substrate/nuclear core verified by reuse; the cellular/mitosis reading is a structural analogy. Reuses `QLF_Fusion` + `QLF_FreeEnergy`; no new axioms | `identical_copy_pauli_blocked`, `realizable_duplication_needs_distinguishability`, `duplication_pays_log_two`, `no_free_duplication_summary` |
| [QLF_Firebreak.lean](QLF_Firebreak.lean) | **ZFA closure as the firebreak on path-integral possibility-space** (issue #103; [P_vs_NP_QLF.md](../P_vs_NP_QLF.md)). The quantum path integral's "many kinematic paths exist but they do not all become physical receipts" as **generate-then-close**: the QuCalc tree generates every path (`expand_generation`, branching ×2 via `branch_state`), and ZFA closure is the firebreak (the substrate form of phase/projectors/exclusion preventing runaway occupation of possibility-space). **`expand_states_length`** (each step doubles) ⟹ **`expand_generation_length`** (`2^n`) ⟹ **`generated_count`** (`\|expand_generation 2n\| = 4^n`, every kinematic path of length `2n`). **`realized_le_generated`** — the realized receipts are the `verify` (closure) filter, a sub-list, of size `C(2n,n)` (`realized_count_eq_central_binomial`, reusing `QLF_PvsNP`). **`firebreakCount`/`firebreakCount_eq`** — the firebreak = `4^n − C(2n,n)` (generated minus closing). **`not_all_paths_close`** (`verify [+,+] = false`) + **`firebreak_nonempty`** (`C(2,1)=2 < 4^1=4`) — a generated path that does not close, so possibility-space is **not greedily filled**. Asymptotically the realized fraction `C(2n,n)/4^n → 0` (Wallis/Stirling, the `QLF_PhysicalPi` census), so the firebreak is **all** of possibility-space — surviving amplitude receipts are sparse. Honest scope: the structural/combinatorial firebreak + sparsity; the literal `e^{iS/ℏ}` phase cancellation is the continuum rendering. Reuses `QLF_PvsNP`/`QLF_QuCalc`; no new axioms | `expand_states_length`, `expand_generation_length`, `generated_count`, `realized_le_generated`, `firebreakCount`, `firebreakCount_eq`, `not_all_paths_close`, `firebreak_nonempty`, `firebreak_summary` |
| [QLF_GaugeUnification.lean](QLF_GaugeUnification.lean) | **One force, three projections — EM is the abelian limit** ([Forces_From_Three_Axes.md](../Forces_From_Three_Axes.md) §3a, [Higgs.md](../Higgs.md)). Completes the "weak/strong are EM seen from different 3-axis projections" reading with its crisp algebraic form. **`em_gauge_abelian`** — the gauge-fold (Pauli scalar) group *commutes* (reusing `QLF.PauliScalar.mul_comm`): EM is the **abelian** sector, the unbroken `U(1)`, the *massless, long-range photon*. **`strong_nonabelian`** — the gluon directional couplings do **not** commute (`gluon_commutator_nonzero`), and likewise weak isospin (`weak_isospin_su2`, `[τᵢ,τⱼ]=−2εᵢⱼₖτₖ ≠ 0`): the weak and strong forces are **non-abelian** projections of the same three axes — self-interacting, short-range, confined/massive. **`gauge_unification_signature`** packages the two: the abelian/non-abelian split *is* the massless-photon-vs-massive-`W`/`Z` split. Electroweak breaking is read as the **logical-density threshold** below which the Markov-blanket structure (the constructive Higgs = gauge-fold delay) confines the non-abelian projections and gives them mass (`m=1/R`), while the abelian trace (photon) stays free; the projection ratio is `sin²θ_W = 3/8`. Reuses `QLF_Pauli` + `QLF_StrongAlgebra`; no new axioms. Honest scope (`gauge_unification_in_progress`): the couplings, the `W`/`Z` mass values (Higgs VEV), the RG running, and the symmetry-breaking dynamics as a field theory stay open | `em_gauge_abelian`, `strong_nonabelian`, `gauge_unification_signature`, `gauge_unification_in_progress` |
| [QLF_GaugeHolonomy.lean](QLF_GaugeHolonomy.lean) | **The gauge *force* is the holonomy of the closure connection** ([Forces_From_Three_Axes.md](../Forces_From_Three_Axes.md) §3a) — the *dynamics* on top of `QLF_GaugeUnification`'s *algebras*. A gauge force's field strength is the **Wilson-loop plaquette** `A·B·A⁻¹·B⁻¹` (transport around the smallest loop). **`em_plaquette_trivial`** — in the commuting Pauli-scalar (EM) group the plaquette is `1`: flat `U(1)`, the photon's field strength carries no self-interaction (massless, long-range). Reuses `PauliScalar.mul_comm` (= `em_gauge_abelian`). **`nonabelian_plaquette`** — with `σ` self-inverse, the elementary non-abelian plaquette `σx σy σx⁻¹ σy⁻¹ = σx σy σx σy = -(1:M)`; **`nonabelian_plaquette_ne_one`** (`≠ 1`, reusing `spin_double_cover_nontrivial`) = curved `SU(2)`/`SU(3)`, the gluon/W field strength self-interacts (short-range, confining/massive). So flat-abelian vs curved-non-abelian Wilson loop **is** the massless-photon vs massive/confined split — the internal-gauge analogue of spacetime curvature, the same holonomy object as the LQG/lattice picture ([QLF_LoopQuantumGravity.lean](QLF_LoopQuantumGravity.lean)). Honest scope (`gauge_holonomy_in_progress`): the full Yang–Mills action `∫tr F∧⋆F`, the matter covariant derivative, and the couplings `g₁,g₂,g₃` stay open | `em_plaquette_trivial`, `nonabelian_plaquette`, `nonabelian_plaquette_ne_one`, `gauge_holonomy_in_progress` |
| [QLF_WeakChirality.lean](QLF_WeakChirality.lean) | **The weak force is chiral; only the left-handed neutrino enters the Markov blanket** ([CP-Violation-and-Chirality.md](../CP-Violation-and-Chirality.md), [Beta_Decay_Neutrino_Nature.md](../Beta_Decay_Neutrino_Nature.md)). **`weak_charge_parity_odd`** — under view-from-behind (the antiparticle map) the weak/chiral charge is **odd**: both `perpChirality` and `chiralCharge` negate (`perpChirality_conj` + `chiralCharge_conj`). A parity-symmetric force would treat a history and its mirror identically; the weak (chiral) charge does not — **parity violation by construction** (the V−A signature). **`neutrino_no_perp_chirality`** — the Majorana neutrino (`neutrino_majorana`) has **zero perpendicular chirality**: self-conjugacy + parity-odd chirality give `perpChirality ν = −perpChirality ν = 0`, so its only handedness is **helical** (the flat `σy` spin vs motion). Jim's blanket admissibility (read with `weak_isospin_su2`, the spatial weak `su(2)`): a pure-gauge right-handed / sterile neutrino carries no spatial isospin — a weak singlet outside the charged-current blanket — so only the spatially-twisted left-handed neutrino is admitted. Honest scope (`weak_chirality_in_progress`): the V−A projector `P_L=(1−γ₅)/2` and the helicity-vs-motion operator that would make "only-left-closes" a theorem stay open | `weak_charge_parity_odd`, `neutrino_no_perp_chirality`, `weak_chirality_in_progress` |
| [QLF_Confinement.lean](QLF_Confinement.lean) | **Color confinement = the singlet-closure obstruction** ([Forces_From_Three_Axes.md](../Forces_From_Three_Axes.md)). Reuses the verified `wcount_zero_on_ZFA` ([QLF_BMinusL.lean](QLF_BMinusL.lean)): every annihilation-odd signed charge is zero on every ZFA closure (a closure prunes to the empty string). Electric charge is the canonical instance; **color is the strong instance**. **`charged_not_closed`** — the contrapositive: a state carrying a net charge of this kind is **not** a ZFA closure. For color this is confinement — a lone quark carries net color, so it cannot close; only color-neutral combinations are physical. **`singlet_closure`** — every ZFA closure has zero net (charge/color) count: only singlets close. Structural reading: the flux-tube linear potential `V(r)∝r` is the constructing delay growing with separation (color = the 3-axis Borromean instance; a baryon needs one charge per spatial axis). Pairs with the curved non-abelian Wilson loop of [QLF_GaugeHolonomy.lean](QLF_GaugeHolonomy.lean). Honest scope (`confinement_in_progress`): the string-tension value and the asymptotic-freedom→confinement RG flow stay open | `charged_not_closed`, `singlet_closure`, `confinement_in_progress` |
| [QLF_HiggsMechanism.lean](QLF_HiggsMechanism.lean) | **Mass is the gauge-fold delay — the constructive Higgs** ([Higgs.md](../Higgs.md)). No fundamental scalar: mass is the constructing delay of a gauge fold. **`mass_is_gauge_fold_delay`** — a fold of depth `R` carries `m = 1/R` (reuses `mass_from_depth`). **`weak_boson_mass_pos`** — a fold (`R>0`) makes mass `m=1/R>0`: the non-abelian `W`/`Z` are massive, while the abelian fold-free photon is massless (the curved-vs-flat Wilson loop of [QLF_GaugeHolonomy.lean](QLF_GaugeHolonomy.lean)). **`heavier_is_shallower`** — masses are blanket depths (`m=1/R` monotone, reuses `lighter_is_deeper`). **`custodial_rho_one`** — tree-level custodial `ρ = M_W²/(M_Z²cos²θ_W) = 1` when `M_W²=M_Z²cos²θ_W` (reuses `rho_one_of_mass_relation` from [QLF_WeinbergAngle.lean](QLF_WeinbergAngle.lean)), `cos²θ_W=1−sin²θ_W`, unification `sin²θ_W=3/8`. Electroweak breaking = the logical-density threshold. Honest scope (`higgs_mechanism_in_progress`): the VEV `v≈246 GeV`, the `125 GeV` Higgs mass, and the absolute `W`/`Z` masses stay open | `mass_is_gauge_fold_delay`, `weak_boson_mass_pos`, `heavier_is_shallower`, `custodial_rho_one`, `higgs_mechanism_in_progress` |
| [QLF_CKM.lean](QLF_CKM.lean) | **Flavor mixing is a unitary rotation — unitarity = closure** ([Standard_Model.md](../Standard_Model.md) §4.2). Strengthens [QLF_FlavorMixing.lean](QLF_FlavorMixing.lean)'s *counting* with the dynamical constraint it presupposes: the CKM matrix is **unitary**, and in QLF unitarity *is* closure — mixing rotates flavor without creating/destroying it (the ZFA-balanced total is conserved). For the Cabibbo block (`V_ud=cos θ_C`, `V_us=sin θ_C`): **`cabibbo_row_unitarity`** (`|V_ud|²+|V_us|²=cos²θ_C+sin²θ_C=1` — the mixing row is a unit vector, each up-type's branching across down-types sums to 1); **`cabibbo_rows_orthogonal`** (the two generation rows are orthogonal ⟹ full `V Vᵀ=I`, the closing unitarity triangle, geometric home of the Jarlskog CP area); **`ckm_parameter_count`** (re-anchors 3 angles + 1 CP phase). Honest scope (`ckm_in_progress`): the angle *values* (Cabibbo angle, Wolfenstein `λ`,`λ²`,`λ³`) and the CP phase `δ` are the Yukawa sector, open like the quark masses | `cabibbo_row_unitarity`, `cabibbo_rows_orthogonal`, `ckm_parameter_count`, `ckm_in_progress` |
| [QLF_QuarkMass.lean](QLF_QuarkMass.lean) | **Quark masses are not closure observables; hadron masses are** ([Weak_Force.md](../Weak_Force.md) §5d–§5f) — the category correction sharpened by confinement. **`quark_not_closed`** — a lone net-charged/coloured twist is **not** a ZFA closure (the canonical charge instance witnessing the colour obstruction, reusing `charged_not_closed` from [QLF_Confinement.lean](QLF_Confinement.lean)): a quark cannot be isolated, so its mass is not a closure observable. **`hadron_mass_eq_depth`** — the observable hadron mass is the colour-singlet closure depth `m=1/R` (`mass_from_depth`), set by the QCD binding; quark "masses" enter only as the small isospin splitting. So the right target is the hadron mass *splittings* — `m_n−m_p = (m_d−m_u) − ΔE_EM`, two opposite-pushing gauge pieces, the strong `d↔u` step winning (proton lighter/stable ⟹ hydrogen exists) — **not** a quark-mass Koide (QLF's own confinement forbids it). `u,d` are the weak `SU(2)` doublet (`weak_isospin_su2`). Honest scope (`quark_mass_in_progress`): the bare quark masses, the `d↔u` flavour step, and the sub-MeV `m_n−m_p` cancellation (needed lattice QCD+QED) stay open; the deuteron's existence/uniqueness is a positive QLF result (Pauli + `d↔u` distinguishability) | `quark_not_closed`, `hadron_mass_eq_depth`, `quark_mass_in_progress` |
| [QLF_QuarkStructure.lean](QLF_QuarkStructure.lean) | **The Borromean three-colour necessity, proven** ([Quarks.md](../Quarks.md), [Atomic_Structure_QLF.md](../Atomic_Structure_QLF.md) §7) — reuse-only, no new axioms. Generalises `baryon_zero_of_noZ` from the `z` axis to *every* axis. **`signTriple_missing`** — a 3-window missing any one axis cannot span all three, so its oriented linking sign is `0`. **`baryon_zero_of_missing`** — a history in which some colour axis never appears has `baryonNumber = 0`. **`baryon_needs_all_three_axes`** (the keystone) — `B ≠ 0` requires a twist on **every** colour axis `x,y,z`; remove any one colour and `B = 0`. This is **confinement as a Borromean necessity**: the three quarks are the three axes, all three required to close — no one- or two-colour baryon (reuses `baryonNumber`/`signTriple`/`axOf` from [QLF_BaryonWinding.lean](QLF_BaryonWinding.lean), and pairs with `charged_not_closed` from [QLF_Confinement.lean](QLF_Confinement.lean)). **`minimal_baryon_one_per_axis`** — the minimal baryon `>^/` carries exactly one twist on each axis. **`single_colour_not_baryon`** — a history on a single colour axis has `B=0` (a lone quark's colour content is not a baryon — confinement). **Charge thirds from colour:** **`charge_quantum_from_colours`** — tracelessness `n·q + L = 0` ⟹ `q = −L/n`, so the charge quantum is `1/n_colours`; **`down_quark_charge_third`** — the SU(5) `5̄` (3 colour copies + lepton net `−1`) gives `q = 1/3`, so the down quark is `−1/3` (the thirds forced by the three colours). The per-flavour u/d twist signature and quark masses stay open | `signTriple_missing`, `baryon_zero_of_missing`, `baryon_needs_all_three_axes`, `minimal_baryon_one_per_axis`, `single_colour_not_baryon`, `charge_quantum_from_colours`, `down_quark_charge_third` |
| [QLF_NeutrinoMass.lean](QLF_NeutrinoMass.lean) | **The neutrino mass is Majorana; only the self-conjugate fermion can be** ([Beta_Decay_Neutrino_Nature.md](../Beta_Decay_Neutrino_Nature.md), [Beyond_Standard_Model.md](../Beyond_Standard_Model.md) §3). Mass type is fixed by self-conjugacy (reusing the verified `QLF_Majorana` tests). **`neutrino_mass_majorana`** — the neutrino `^v` is its own antiparticle, so a Majorana mass `m ν ν` is allowed. **`electron_mass_dirac`** — `^<v>` is not self-conjugate, so the charged lepton is Dirac (needs a distinct partner). **`majorana_mass_only_neutrino`** — a lepton-number-violating Majorana mass, and hence `0νββ` (`ΔL=2`), is available to the neutrino and *only* the neutrino (the unique self-conjugate fermion). The smallness is the seesaw reading (the active left neutrino mixes with a heavy sterile = pure-gauge right-handed partner, [QLF_WeakChirality.lean](QLF_WeakChirality.lean); `m_ν~m_D²/M_R`). Honest scope (`neutrino_mass_in_progress`): the absolute mass scale, `M_R`, the ordering, and `Σm_ν` stay open | `neutrino_mass_majorana`, `electron_mass_dirac`, `majorana_mass_only_neutrino`, `neutrino_mass_in_progress` |
| [QLF_PMNS.lean](QLF_PMNS.lean) | **Lepton mixing is unitary, with extra Majorana phases** ([Standard_Model.md](../Standard_Model.md) §4.2). The PMNS analogue of [QLF_CKM.lean](QLF_CKM.lean): also a unitary rotation (`pmns_row_unitarity` — `|U_e1|²+|U_e2|²=cos²+sin²=1`, lepton flavour rotated not lost = closure), but because the neutrino is **Majorana** ([QLF_NeutrinoMass.lean](QLF_NeutrinoMass.lean)) it carries `N−1` **extra** phases CKM lacks: **`majorana_phases`** (`N−1`), **`three_gen_majorana_phases`** (`=2`), **`pmns_total_cp_phases`** (`1 Dirac + 2 Majorana = 3` total, vs CKM's lone Dirac phase — the extra two physical only in lepton-number-violating `0νββ`). Structural reading: quarks mix small/hierarchically (hidden chirality), leptons mix large (near tri-bimaximal, exposed chirality). Honest scope (`pmns_in_progress`): the angle values (tri-bimaximal / `θ₁₃`), the Dirac phase `δ_CP`, and the Majorana phase values stay open | `pmns_row_unitarity`, `majorana_phases`, `three_gen_majorana_phases`, `pmns_total_cp_phases`, `pmns_in_progress` |
| [QLF_Supersymmetry.lean](QLF_Supersymmetry.lean) | **The supercharge is the half-spin shift; `{Q,Q†}=2P` is two half-spins closing a spacetime event** ([SUSY_QLF.md](../SUSY_QLF.md)) — relates QLF to **supersymmetry**, the third quantum-gravity TOE pillar alongside [StringTheory.md](../StringTheory.md) and [LQG_QLF.md](../LQG_QLF.md). Statistics is the **parity of the half-spin count** (`QLF_Spin`): boson = even pairs → `+I` (`boson_even_pairs`), fermion = odd → `−I` (`fermion_odd_pairs`). So the **supercharge `Q` = adjoin one half-spin pair**. **`supercharge_flips_statistics`** — it flips `Even ↔ Odd` (boson ↔ fermion). **`supercharge_boson_to_fermion`** — a boson (`+I`) plus one pair is a fermion (`−I`). **`two_supercharges_close_event`** (= `rotation_720_eq_id`) — two half-spin pairs (720° double cover) fold to `+I`, and that `+I` is **one closed ZFA event** = one `log 2` = one Planck-tick translation: `{Q,Q†}=2P`, the half-spin as the **square root of the spacetime event** (the `2` = the Hermitian-pair factor). **Punchline:** SUSY's boson–fermion symmetry is the even/odd parity of closures, realized **without a doubled spectrum** — `Q` shifts the same closure, it does not create a superpartner *particle*; so there are no squarks/sleptons and QLF *predicts* the LHC null result (same move as the composite graviton and the fold-Higgs). Reuses `QLF_Spin`; no new axioms. Honest scope (`supersymmetry_in_progress`): the full graded super-Poincaré algebra, superspace, and MSSM dynamics stay open — QLF argues the doubled MSSM spectrum is *not* a prediction | `supercharge_flips_statistics`, `supercharge_boson_to_fermion`, `two_supercharges_close_event`, `boson_is_even`, `fermion_is_odd`, `supersymmetry_in_progress` |
| [QLF_AlphaBound.lean](QLF_AlphaBound.lean) | **What the substrate FORCES about α — short of deriving the value** ([Alpha.md](../Alpha.md); companion to `QLF_FineStructureSubstrate`). Leading combinatorial value `α⁻¹ = 128 + d² = 137`; the measured `137.035999` (q²→0 Thomson) is the open residual (`alpha_exact_value_in_progress`). Machine-checked **bounds, not the value**: **`alpha_inv_gt_137`** — abelian EM (`em_gauge_abelian`, U(1), no self-interaction) ⟹ higher closures *screen* (positive corrections) ⟹ `α⁻¹ > 137`, an unconditional falsifiable before-data inequality CODATA satisfies. **`codata_in_exact_census_band`** — under one `α_bare` per closure order the residual is bracketed by the irreducible-leading term `1/64` and the **exact total-census upper limit** `(217+512√62)/31 ≈ 137.04813` (the tail `∑ C(2n,n)·α_bare^(n−1)` summed via the central-binomial generating function `(1−4x)^(−1/2)`); the measured `0.035999` lies strictly inside, ~0.012 below the cap. **`steep_map_excludes_codata`** — a steeper `α_bare²`-per-order map caps the residual below the measured value, so the data *requires* the shallow map; the length→order rule is the named open piece. **Not** a derivation of `137.036` — the resummation/curvature rule stays open (candidate routes: a curvature correction to `N=d²` via `QLF_CausalDimension`, or the irreducible-closure generating function `1−√(1−4x)`). Census counts explicit (`C(2n,n)=2,6,20,70`; irreducible `2·Catalan(n−1)=2,2,4,10`). The **exact `√62` cap is formalized with zero axioms**: `censusTail` is the constructive tsum over the central-binomial census counts; `central_binom_genfun` is now a **theorem** — the generating function `∑ C(2n,n)xⁿ=(1−4x)^(−1/2)` at `x=1/128`, derived from Mathlib's `(1+x)^a` binomial series (`Real.one_add_rpow_hasFPowerSeriesOnBall_zero`, `a=−1/2`, `x=−1/32`) via the coefficient identity `qlf_choose_neg_half` (`4ⁿ·choose(−1/2) n=(−1)ⁿ·C(2n,n)`, by induction) and the recurrence `qlf_ring_choose_succ` (from `descPochhammer`); `censusTail_eq` is a theorem derived from it; and `codata_below_alphaInvCap` *proves* `137.035999 < (217+512√62)/31 ≈ 137.04813`. The GF analysis-boundary axiom is **discharged**. The bracket is now **two-sided and exact**: the irreducible (prime-closure) lower cap `137 + irreducibleTail = 263 − 16√62 ≈ 137.01587` (`irreducibleCap_eq`; count `2·Catalan(n−1) = 4·C(2n−2,n−1) − C(2n,n)` per `irrCoeff_matches`, so `irreducibleTail = 4·(G−1) − censusTail`, no new axiom), with the Dyson/1PI resummation `G·(1−I) = 1` (`census_irreducible_resummation`) — total census = geometric resummation of the prime closures. The only open piece is the physics residual `+0.036` (which partial resummation between the two caps; both pure-geometry/gauge shortcuts eliminated, see `Alpha_Residual.md`) | `alpha_inv_gt_137`, `leadInv_eq`, `residLowerTerm_eq`, `censusUpperLimit`, `codata_below_census_upper_limit`, `codata_in_exact_census_band`, `steep_map_excludes_codata`, `censusTail`, `qlf_ring_choose_succ`, `qlf_choose_neg_half`, `central_binom_genfun`, `censusTail_eq`, `irreducibleTail`, `irreducibleTail_eq`, `irreducibleCap_eq`, `irrCoeff_matches`, `census_irreducible_resummation`, `alphaInvCap`, `alphaInvCap_eq`, `sqrt62_gt`, `codata_below_alphaInvCap`, `alpha_bound_forced` |
| [QLF_PhysicalPi.lean](QLF_PhysicalPi.lean) | **π derived by construction from the closure census** (Allen's [#86](https://github.com/jimscarver/quantum-logical-framework/issues/86)/[#89](https://github.com/jimscarver/quantum-logical-framework/issues/89)/[#90](https://github.com/jimscarver/quantum-logical-framework/issues/90), [Physical_Pi.md](../Physical_Pi.md)). The substrate's *own* closure walk constructs π. **`closure_census`** *(theorem)* — the census of ZFA-balanced stable closures of length `2n` is the central binomial `C(2n,n)` (reusing `find_stable_states_length_even`), the *return count* of the walk. **`returnDensity`** / **`returnDensity_eq_census`** *(theorem)* — the 2-D return density `P₂ₙ(0) = (C(2n,n)/4ⁿ)²` is a finite computable **rational** (no `Real.pi`) built from that count; since `C(2n,n) ~ 4ⁿ/√(πn)` (Wallis/Stirling, settled mathematics), `π = lim 1/(n·returnDensity n)` — π from intrinsic substrate counting, no circle. Same `C(2n,n)` as Born stats / P-vs-NP verify-filter / Riemann gap-zero density. Imports `QLF_Riemann`; no new axioms. **Narrow residuals (don't undermine the construction):** *formalizing* the (settled) convergence in-module is housekeeping (`physical_pi_in_progress`); the 2-D **squaring** wants a ZFA-derived random-walk probability space; gauge-increment caveats (`4π` = spin-½ *representation* period; `2π/3` = `SU(3)` *center* increment, ×3 to close); the Riemann/GUE tie is a *shared object*, not a proof. **Separate (Allen [#90](https://github.com/jimscarver/quantum-logical-framework/issues/90)):** the *effective-limit* geometry recovery (`C/2r→π`, `A/r²→π`) is the emergent-spacetime burden QLF carries (it uses `Real.pi` in α, GR). **Declined only:** the continuum as *fundamental substrate*; `2π` is *inserted* in `renderAngle`, not recovered | `closure_census`, `returnDensity`, `returnDensity_eq_census`, `physical_pi_in_progress` |
| [QLF_StrongAlgebra.lean](QLF_StrongAlgebra.lean) | Strong `SU(3)` as the **traceless** part of the 3×3 directional-coupling tensor of the three spatial axes (8 = 3²−1 gluons): `trace_commutator_zero` (every commutator is traceless ⇒ closed under the bracket), `gluon_commutator_nonzero` (non-abelian). Algebra-level; the gauge *dynamics* are in [QLF_GaugeHolonomy.lean](QLF_GaugeHolonomy.lean) (the curved non-abelian Wilson loop) and **confinement** in [QLF_Confinement.lean](QLF_Confinement.lean) (the singlet-closure obstruction); only the couplings / string-tension *value* stay open ([Forces_From_Three_Axes.md](../Forces_From_Three_Axes.md)) | `trace_commutator_zero`, `g1_traceless`, `g3_traceless`, `gluon_commutator_nonzero`, `strong_su3_summary` |
| [QLF_BMinusL.lean](QLF_BMinusL.lean) | Electric charge as an exactly-conserved signed twist count: any annihilation-odd weight is additive under concatenation and invariant under the ZFA pruning dynamics (`signed_count_conserved`). **Obstruction** `wcount_zero_on_ZFA`: every conserved signed count is zero on every ZFA closure — so `B−L` (nonzero on the deuteron) is NOT a weight dictionary but a winding invariant. `chargeWeight` recovers `count_pos − count_neg` | `wcount_append`, `wcount_zeno_prune`, `wcount_full_zeno_prune`, `signed_count_conserved`, `no_spontaneous`, `zfa_prune_nil`, `wcount_zero_on_ZFA`, `chargeWeight_annihilationOdd`, `wcount_chargeWeight` |
| [QLF_Majorana.lean](QLF_Majorana.lean) | The neutrino is **Majorana**: in QLF the antiparticle is the Hermitian conjugate (conjugate each twist **and** reverse the order, `(A·B·C)†=C†·B†·A†`), so "its own antiparticle" is the decidable property *the twist string is a fixed point of conjugate-and-reverse*. The neutrino loop `^v` IS a fixed point (`neutrino_majorana`); the electron `^<v>` is NOT (`electron_not_majorana` ⇒ Dirac). Predicts 0νββ ([Beta_Decay_Neutrino_Nature.md](../Beta_Decay_Neutrino_Nature.md)) | `neutrino_majorana`, `electron_not_majorana`, `antiparticle_involutive`, `Twist.conj_conj` |
| [QLF_BaryonWinding.lean](QLF_BaryonWinding.lean) | Baryon number = a signed 3-axis **linking (winding)** number: slide a 3-window, `+1` cyclic `(x,y,z)` / `−1` anticyclic / `0` else. Proton `>^/` = +1, antiproton = −1, leptons & meson = 0; `baryon_zero_of_noZ` proves the whole z-free lepton/EM sector is baryon-neutral; **`baryon_dagger_odd`** proves `B(ts†) = −B(ts)` for all histories (baryon/antibaryon = ±B, fully general). The concrete realisation of "baryon number = topological winding" | `baryon_proton`, `baryon_antiproton`, `baryon_electron`, `baryon_neutrino`, `baryon_meson`, `signTriple_noZ`, `baryon_zero_of_noZ`, `axOf_conj`, `signTriple_rev`, `baryon_eq_bnA`, `endWindowA_append_two`, `endWindowA_cons3`, `bnA_snoc`, `bnA_reverse`, `baryon_dagger_odd` |
| [QLF_Spin.lean](QLF_Spin.lean) | **Spin demystified — spin IS the twists** (`Twist.toMatrix`: ^=σy, v=−σy, <=−σx, >=σx, /=σz, \=−σz, +=I, −=−I). Worked qucalc folds: `^v`=σy·(−σy)=−I (`fold_up_down`), `^v^v`=+I (`fold_up_down_twice`, the 720° return), `^>`=−iσz (`fold_up_right`, cross-axis), `+−`=−I (`fold_plus_minus`, charge pair). **SU(2)/SO(3) double cover**: 360°→−I (`rotation_360_eq_negI`), 720°→+I (`rotation_720_eq_id`); the three twist axes close su(2) (`su2_comm_xy/yz/zx`, `[σi,σj]=2iεσk`); the cover is genuine `−I≠+I` (`spin_double_cover_nontrivial`). **Charge conjugation = view-from-behind**: under `antiparticle` (conjugate-and-reverse) charge and perpendicular-chirality co-negate (`C_eq_motional_reversal`, reusing `baryon_dagger_odd`) — a positron from behind reads as an electron. **Neutrino**: self-conjugate ⟹ neutral (`majorana_is_neutral`, `neutrino_neutral`). **Integer spin = composite of half-spins**: `boson_even_pairs`/`fermion_odd_pairs`, photon = ½+½=1 (`photon_integer_spin`). Exclusion (`like_spin_excludes` = `pauli_exclusion`); opposite-spin singlet `(−I)(−I)=+I` (`opposite_spin_singlet_closes`). Magnetism = flat axis, motion-independent (`magneticMoment`, `flat_independent_of_motion`). See [Spin_QLF.md](../Spin_QLF.md) | `fold_up_down`, `fold_up_down_twice`, `fold_up_right`, `fold_plus_minus`, `rotation_360_eq_negI`, `rotation_720_eq_id`, `su2_comm_xy`, `spin_double_cover_nontrivial`, `perpChirality_conj`, `chiralCharge_conj`, `C_eq_motional_reversal`, `majorana_is_neutral`, `neutrino_neutral`, `photon_integer_spin`, `like_spin_excludes`, `opposite_spin_singlet_closes`, `flat_independent_of_motion` |
| [QLF_MassGap.lean](QLF_MassGap.lean) | **Yang–Mills mass gap** (Millennium Prize) from the substrate: gauge excitations are non-abelian ZFA closures (SU(2)/SU(3) verified elsewhere), the vacuum is the ℒ=0 identity closure, and the lightest non-vacuum closure carries exactly one `log 2` quantum — so the spectrum has a positive gap `gaugeMassGap = log 2`. The continuum-QFT existence is the explicit boundary axiom `yang_mills_continuum_gap` (à la `spectral_hilbert_polya`); status `mass_gap_proven_constructively`. See [YangMills_MassGap_QLF.md](../YangMills_MassGap_QLF.md) | `gaugeMassGap`, `mass_gap_quantum_pos`, `lightest_closure_is_gap_quantum`, `yang_mills_mass_gap_in_qlf`, `mass_gap_proven_constructively` |
| [QLF_BSD.lean](QLF_BSD.lean) | **Birch–Swinnerton-Dyer** (Millennium Prize) via the Langlands hook: the L(E,s) central point `s=1` is the self-dual fixed point of `s↦2−s` (`bsd_central_point_self_dual`), grounded in the *same* `H↔H†` involution as Riemann — both central loci are `a/2` midpoints of an `s↦a−s` reflection (`reflection_fixed_iff`, `bsd_central_point_eq_midpoint`, `bsd_riemann_shared_involution` reusing `functional_equation_fixed_real`). **Proven (substrate):** the self-dual central point, `reflection_fixed_iff`, and the *computed* closure encoding (Frobenius traces). **The gap is faithfulness:** `rank = ord` (`bsd_rank_equals_order`) and `bsd_in_qlf` follow from the bridge `modularity_mirror_invariant` (mirror-invariance of the central multiplicity at the self-dual fixed point), which on BSD has the conjecture's full strength. `Perspective` (galois/automorphic), the `modularityMirror` involution, `centralMultiplicity` on the two sides. *(Contrast: the classical BSD conjecture is not proved here.)* **`EllipticCurveQLF` is concrete** (integral Weierstrass `y²=x³+ax+b`) with its closure encoding *computed* — `affinePointCount`/`frobeniusTrace` (= `a_p = p − #E(𝔽_p)`) over `ZMod p`, worked curve `Ecn1` with `Ecn1_smooth` and verified `Ecn1_frobenius_two` (`a₂=0`); `centralMultiplicity`/ranks stay abstract (uncomputable in general — BSD's content). Status `bsd_proof_in_progress`. See [BSD_QLF.md](../BSD_QLF.md) | `bsd_central_point_self_dual`, `bsd_riemann_shared_involution`, `EllipticCurveQLF`, `affinePointCount`, `frobeniusTrace`, `Ecn1_frobenius_two`, `modularityMirror`, `centralMultiplicity`, `modularity_mirror_invariant`, `bsd_rank_equals_order`, `bsd_in_qlf`, `bsd_proof_in_progress` |
| [QLF_Hodge.lean](QLF_Hodge.lean) | **Hodge conjecture** (Millennium Prize) as the cohomological face of ZFA selection: the Hodge conjugation `H^{p,q}↔H^{q,p}` IS the QLF adjoint involution H↔H† (`conj_involutive`), and Hodge classes are exactly its balanced self-dual fixed points — the `(p,p)` diagonal (`conj_fixed_of_isHodge`, `isHodge_of_conj_fixed`). A `(p,q)` class encodes (`CohClass.encode`) to a twist history count-balanced iff `p=q` (`encode_countBalanced`), and count-balanced ⟹ Pauli-closed (`count_balanced_pauli_closed`) — so **proven (no axiom): Hodge classes are exactly the substrate-realized closures** (`hodge_realized_on_substrate`). **The gap is faithfulness:** `substrate_realization_is_algebraic`, the bridge from a realized closure to a *classical* algebraic cycle (`CohClass.isAlgebraic` abstract; on Hodge classes it has the conjecture's full strength) — located precisely by the faithfulness swings (`QLF_HodgeExpSequence`, `QLF_HodgeIrreducible`) as a cycle-faithful encoding, every other piece in hand. *(Contrast: the **classical** Hodge conjecture — finite ℚ-linear algebra, not independence — is not proved here; reformulation + faithfulness would give it.)* **The standard conjectures (B/C/D) reduce to the *same* one bridge** (`standard_conjectures_on_substrate`) — mirroring that they are one coupled package: **C (Künneth)** — each diagonal component is a `(d,d)` Hodge class on `X×X` (`diagonalComponent_isHodge`, `kunneth_diagonal_components_algebraic`); **D (numerical ≡ homological)** — the intersection pairing's non-degeneracy is the substrate's `(d,d)`-realization (`pairing_realizes`, every in-range class pairs with its Poincaré dual `poincareDual_pairs`), so `conjecture_D_numerical_eq_homological`; **B (Lefschetz)** — `L`/`Λ` preserve the Hodge balance (`lefschetzPow_isHodge`) so their `(D,D)` correspondence is algebraic (`conjecture_B_lefschetz_algebraic`). The substrate foundation of Grothendieck's **motives** ([Grothendieck_QLF.md](../Grothendieck_QLF.md)). Status `hodge_proof_in_progress`. See [Hodge_QLF.md](../Hodge_QLF.md) | `conj_involutive`, `conj_fixed_of_isHodge`, `isHodge_of_conj_fixed`, `CohClass.encode`, `encode_countBalanced`, `hodge_pattern_substrate_witness`, `hodge_realized_on_substrate`, `substrate_realization_is_algebraic`, `hodge_class_is_algebraic`, `non_algebraic_not_hodge`, `diagonalComponent_isHodge`, `kunneth_component_algebraic`, `kunneth_diagonal_components_algebraic`, `poincareDual_pairs`, `pairing_realizes`, `conjecture_D_numerical_eq_homological`, `lefschetzPow_isHodge`, `conjecture_B_lefschetz_algebraic`, `standard_conjectures_on_substrate`, `hodge_proof_in_progress` |
| [QLF_PvsNP.lean](QLF_PvsNP.lean) | **P vs NP** (Millennium Prize): the generate/verify asymmetry Lean-anchored on real theorems. The realized (verifiable) set IS the O(n) verify-filter of the generated candidates (`realized_is_verify_filter`, `rfl`), and its cardinality is the genuine `C(2n,n)` (`realized_count_eq_central_binomial`, reusing `find_stable_states_length_even`). The formal separation is the single boundary axiom `generate_not_reducible_to_verify` over an abstract `PTime`/`search` cost model; status `p_vs_np_proof_in_progress`. See [P_vs_NP_QLF.md](../P_vs_NP_QLF.md) | `verify`, `realizedSet`, `realized_is_verify_filter`, `realized_count_eq_central_binomial`, `verify_is_ptime`, `generate_not_reducible_to_verify`, `p_vs_np_in_qlf`, `p_vs_np_proof_in_progress` |
| [QLF_NavierStokes.lean](QLF_NavierStokes.lean) | **Navier–Stokes smoothness** (Millennium Prize): realized flows achieve ZFA (`realized_flow_achieves_zfa`, reusing `encode_is_zfa`) and are stable closures (`realized_flow_is_stable`, reusing `qlf_universality`) — no realized history blows up, since blow-up is a non-terminating history pruned by `full_zeno_prune`. Continuum-PDE inheritance is the single boundary `continuum_vorticity_planck_capped`, in `QLF_NavierStokesBKM` — this module's own opaque pair was **removed** (measured, it was satisfied by `⟨True, trivial⟩`; `continuumClaim_nonempty` records why). Status `navier_stokes_proof_in_progress`. See [NavierStokes_QLF.md](../NavierStokes_QLF.md) | `realized_flow_achieves_zfa`, `realized_flow_is_stable`, `continuumClaim_nonempty`, `navier_stokes_proof_in_progress` |
 | [QLF_SpanningMap.lean](QLF_SpanningMap.lean) | **The spanning question on the cycle ring — the genuine Hodge content** ([Hodge_QLF.md](../Hodge_QLF.md); the honest floor of the Hodge thread). **`decomposes_into_primes`** *(real theorem)* — the cycle ring is **free on the prime generators**: every `CycleClass` factors as the product of `primeOf` over its components, so the algebraic classes are exactly the ℚ-combinations of products of irreducible cycle classes (the cycle class map's image). `divisor_eq_primeOf_one` (divisor = codim-1 prime), `primeOf_codim`/`primeOf_irreducible`. This states Hodge precisely as **spanning**: *the prime cycle classes span the Hodge classes in each degree* — codim 1 = Lefschetz `(1,1)` (classical input), codim `p≥2` = the open spanning, which **is** the Hodge conjecture itself, on the right object. The remaining foundational piece is the class map into a *real* cohomology (the substrate has none yet). **Not a proof** — the located floor | `primeOf`, `primeOf_codim`, `primeOf_irreducible`, `unitCycle`, `divisor_eq_primeOf_one`, `decomposes_into_primes`, `spanning_is_the_hodge_content` |
 | [QLF_CycleEncoding.lean](QLF_CycleEncoding.lean) | **Going for the gap — a cycle-faithful representation where irreducibility *bites*** ([Hodge_QLF.md](../Hodge_QLF.md)). First genuine step on the one Hodge gap. The toy `encode` collapses cycle structure (every `(p,p)` ↦ a nested prime), so irreducibility is invisible and the closure fold is multiplicative. **`CycleClass`** retains the prime decomposition — a cycle by its list of irreducible components, each a codim. **`irreducible_not_preserved_under_product`** — the invariant now *bites*: a product of two irreducibles is **not** irreducible, so the representation distinguishes a single cycle from a product (the multiplicative fold could not). `divisor` = irreducible codim-1 (the `Pic` generator); `codim_tensor` (codim additive). **The gap MOVED (honestly):** from "encoding is bidegree-coarse" to "does the prime-generated cycle structure *span* the `(p,p)` Hodge classes" — the genuine Hodge content (codim 1 ✓ = divisors/Lefschetz; codim `p≥2` = the open spanning question), now on the right object. Not a proof; the next genuine rung | `CycleClass`, `CycleClass.codim`, `CycleClass.isIrreducible`, `CycleClass.tensor`, `codim_tensor`, `divisor`, `divisor_irreducible`, `irreducible_not_preserved_under_product`, `cycle_encoding_skeleton` |
 | [QLF_GradedCohomology.lean](QLF_GradedCohomology.lean) | **Starting the cohomology object — the cycle class map + spanning made concrete** ([Hodge_QLF.md](../Hodge_QLF.md)). Reaches the foundational piece `QLF_SpanningMap` named: the class map `cl : CycleClass → cohomology` into a real graded ℚ-cohomology. **Proven:** `cl` **respects the grading** — codim-`p` cycle ↦ degree `2p` (`cohDegree`), cup/intersection product **adds degrees** (`cohDegree_cup`) = the ring-hom/subalgebra property; divisor ↦ deg 2 (`divisor_cohDegree`), codim-`p` prime ↦ deg `2p` (`primeOf_cohDegree`); the algebraic classes are a **subalgebra** (`algebraic_closed_under_cup`). **`HodgeDatum V`** (a ℚ-space slot of `H^{2p}`) carries the `algebraic` + `hodge` subspaces with the **easy direction `algebraic ≤ hodge` proven**; **spanning** is the reverse `hodge ≤ algebraic` (`isSpanned`), equal to equality (`spanned_iff_eq`), with the settled Lefschetz shape realized (`trivialDatum_spanned`). **Honest scope:** which subspace is *Hodge* / which data are *geometric* is kept abstract (a real cohomology theory must supply it); `isSpanned` is per-datum, never a faked global proof — codim 1 = Lefschetz, codim `p≥2` = the open conjecture, on the right object (`cohomology_build_in_progress`). **Not a proof** — the next genuine rung | `cohDegree`, `cohDegree_cup`, `divisor_cohDegree`, `primeOf_cohDegree`, `algebraic_closed_under_cup`, `HodgeDatum`, `HodgeDatum.isSpanned`, `HodgeDatum.spanned_iff_eq`, `trivialDatum`, `trivialDatum_spanned`, `cohomology_build_in_progress` |
 | [QLF_CohomologyRing.lean](QLF_CohomologyRing.lean) | **The cohomology ring + the cycle class map as a graded homomorphism** ([Hodge_QLF.md](../Hodge_QLF.md)). Builds the ring `QLF_GradedCohomology` only gestured at: the **free graded-commutative algebra on prime cycle classes** `Coh = Multiset ℕ`, cup product = union, `degree = 2·sum`. **Proven:** ring laws (`cup_comm`/`cup_assoc`/`cup_zero`); the grading is a **ring grading** (`degree_cup`); and `cl : CycleClass → Coh` is a genuine **graded homomorphism** — `cl_tensor` (intersection → cup), `cl_unit` (→ ring unit `0`), `cl_graded` (respects degree), `cl_divisor`/`cl_primeOf` (single degree-`2n` generators). So the algebraic classes are *literally* the image submonoid of a graded ring hom into a concrete ring. **Honest scope:** the transcendental Hodge decomposition (which classes are *Hodge*) is the analytic input the substrate doesn't yet supply, where the codim `p≥2` spanning lives (`cohomology_ring_built`). **Not a proof** — a genuine rung | `Coh`, `cup`, `cup_comm`, `cup_assoc`, `cup_zero`, `degree`, `degree_cup`, `cl`, `cl_tensor`, `cl_unit`, `cl_sum`, `cl_graded`, `cl_divisor`, `cl_primeOf`, `cohomology_ring_built` |
 | [QLF_CohomologyLinear.lean](QLF_CohomologyLinear.lean) | **The ℚ-linear cohomology + the algebraic classes as a concrete `Submodule ℚ`** ([Hodge_QLF.md](../Hodge_QLF.md)). Hodge is about ℚ-linear structure; this adds it. `CohQ = Coh →₀ ℚ` (the free ℚ-space on cohomology monomials = `AddMonoidAlgebra ℚ Coh`); the ℚ-linear class map `clQ c = single (cl c) 1`; and **`algebraic = span_ℚ (range clQ)`** is a real `Submodule ℚ CohQ` — *exactly* the object the Hodge conjecture concerns. **Proven:** every cycle class, the divisor (Lefschetz `(1,1)`), and the primes are algebraic (`clQ_mem_algebraic`, `divisor_algebraic`, `primeOf_algebraic`); closed under ℚ-scaling + addition (`smul_algebraic`, `add_algebraic`). **Honest scope:** the **Hodge** subspace (transcendental `(p,p)` decomposition) is the open input; the conjecture is `hodge ≤ algebraic`, codim `p≥2` open (`cohomology_linear_built`). The algebraic half made fully concrete. **Not a proof** — a genuine rung | `CohQ`, `clQ`, `algebraic`, `clQ_mem_algebraic`, `divisor_algebraic`, `primeOf_algebraic`, `smul_algebraic`, `add_algebraic`, `cohomology_linear_built` |
 | [QLF_CohomologyAlgebra.lean](QLF_CohomologyAlgebra.lean) | **`cl` as a ℚ-algebra homomorphism; the algebraic classes a `Subalgebra ℚ`** ([Hodge_QLF.md](../Hodge_QLF.md); the algebraic side completed). Cohomology as a ℚ-algebra is the monoid algebra `CohA = AddMonoidAlgebra ℚ Coh` (mul = convolution = cup product). **`cl` is a ℚ-algebra homomorphism:** `clA_mul` (intersection → cup, via `AddMonoidAlgebra.single_mul_single`), `clA_one` (unit cycle → ring unit `1`) — so `cl` respects addition, the grading, AND multiplication. The algebraic classes **`algebraicA = Algebra.adjoin ℚ (range clA)`** are a genuine **`Subalgebra ℚ`**, closed under cup product (`mul_mem_algebraicA`, `tensor_mem_algebraicA`) *because it is a subalgebra*. So the algebraic side is **complete** — the algebraic classes are the image ℚ-subalgebra of a ℚ-algebra hom from the cycle ring, graded and cup-closed. **Honest scope:** the lone remaining gap is the transcendental **Hodge** subspace (`hodge ≤ algebraic`, codim `p≥2`), the analytic input the substrate doesn't yet supply (`cohomology_algebra_built`). **Not a proof** — the algebraic half finished | `CohA`, `clA`, `clA_mul`, `clA_one`, `algebraicA`, `clA_mem_algebraicA`, `mul_mem_algebraicA`, `tensor_mem_algebraicA`, `cohomology_algebra_built` |
 | [QLF_HodgeStructure.lean](QLF_HodgeStructure.lean) | **The transcendental `(p,q)` Hodge structure** ([Hodge_QLF.md](../Hodge_QLF.md); the transcendental side, built honestly). A pure Hodge structure is *definable* mathematics (Deligne), NOT the open part: **`PureHodgeStructure`** carries the weight, the bigraded Hodge numbers `h^{p,q}`, the **real-structure symmetry** `h^{p,q}=h^{q,p}` (`conj_symm`/`hodge_number_symmetric` — **the substrate `H↔H†` adjoint**, cf. `QLF_Hodge.conj_involutive`; `bidegree_conj_involutive`), and purity. **Proven:** Tate twists `H(n)` (weight `w−2n`, functorial — `tate_weight`, `tate_hodgeNumber`, `tate_tate_weight`, `tate_tate_hodgeNumber`); the Tate/Lefschetz objects (`tateObject n` = the 1-dim `(n,n)` class of weight `2n`; `lefschetzObject` = the `(1,1)` divisor class), each with exactly one Hodge class (`tateObject_hodgeClassDim`, `lefschetz_hodgeClassDim`); Hodge classes `hodgeClassDim` with **odd-weight vanishing** (`oddWeight_no_hodge_classes` — odd cohomology has no Hodge classes). **Honest scope:** the lone open input is **geometricity/polarization** — *which* Hodge structure the cohomology carries (its periods) — named, not asserted (`hodge_structure_built`); the conjecture is a *geometric* weight-`2p` structure's `hodgeClassDim` being spanned by `QLF_CohomologyAlgebra`'s algebraic subalgebra. **Not a proof** — the transcendental side built | `PureHodgeStructure`, `hodge_number_symmetric`, `bidegree_conj_involutive`, `PureHodgeStructure.tate`, `tate_weight`, `tate_hodgeNumber`, `tate_tate_weight`, `tate_tate_hodgeNumber`, `tateObject`, `tateObject_weight`, `PureHodgeStructure.hodgeClassDim`, `oddWeight_no_hodge_classes`, `tateObject_hodgeClassDim`, `lefschetzObject`, `lefschetz_hodgeClassDim`, `hodge_structure_built` |
 | [QLF_PhaseInformation.lean](QLF_PhaseInformation.lean) | **Shannon (count) is not sufficient — phase is independent information** ([Shannon_And_Phase.md](../Shannon_And_Phase.md)). Answers "is Shannon enough, or does the Fourier/phase domain add info for spacetime & matter?" — **no**. Shannon entropy is the permutation-invariant *count* (multiplicity); the physics rides on the *order* (phase) it discards. **`count_does_not_determine_phase`** — two histories with the **identical twist multiset** (same per-symbol counts ⟹ identical Shannon content), both `countBalanced`, fold to **opposite** Pauli scalars: `^v<>` = `[up,down,left,right]` → `+I` (`fold_udlr`, boson/720°) vs `^<v>` = `[up,left,down,right]` → `−I` (`fold_uldr`, reusing `QLF_Spin.fold_electron`, the 360° fermion sign). The count can't tell them apart; the phase can — and here the difference **is** spin (boson vs fermion). The same non-count structure carries time (`f=1/t`) and mass (`m=ℏf/R`) as frequency. Reuses `twistMatrixFold`/`countBalanced` (`QLF_TwistAlphabet`) + `fold_electron`/`spin_double_cover_nontrivial` (`QLF_Spin`); no new axioms | `fold_udlr`, `fold_uldr`, `count_does_not_determine_phase`, `shannon_necessary_not_sufficient` |
 | [QLF_Realizability.lean](QLF_Realizability.lean) | **Consistency ≠ realizability — the Bekenstein obstruction** ([TheContinuum.md](../TheContinuum.md) §3). A structure can be *consistent* (an abstract model exists) yet *physically unrealizable*. **Premise (Bekenstein, not proven here):** a bounded region holds finite information ⟹ finitely many distinguishable states (`Finite R`). **Modeling:** a faithful realization is an injection. **Theorem `no_continuum_in_finite_region`:** `[Infinite S] [Finite R]` ⟹ no injective `S → R` — uses only the continuum's *infinitude*, never that `ℝ` is inconsistent. With `realized_state_space_is_finite` (realizability ⟹ finiteness) and `real_continuum_not_realizable` (`ℝ ↛ Fin (2^bits)`). So "the continuum is consistent but physically unrealizable" is machine-checked: finite-information physics forbids a physical continuum. No new axioms | `no_continuum_in_finite_region`, `realized_state_space_is_finite`, `real_continuum_not_realizable`, `continuum_consistent_but_unrealizable` |
 | [QLF_Uncertainty.lean](QLF_Uncertainty.lean) | **The `ħ/2` quantum, machine-checked** ([UncertaintyPrinciple.md](../UncertaintyPrinciple.md) §2). The substrate origin of the uncertainty bound: observables are integer counts of twists (action in `ħ`), so mapping a continuum value onto its nearest integer count leaves an irreducible spread — one bin's half-width, `ħ/2`. **`binning_halfwidth_le`** (`\|x − round x\| ≤ 1/2`, via Mathlib `abs_sub_round`) + **`binning_halfwidth_tight`** (`= 1/2` attained) ⟹ the discretization spread is *exactly* `ħ/2` (`uncertainty_quantum_eq_half`). **Honest scope:** the conjugate-pair *product* `Δx·Δp ≥ ħ/2` rests on the non-commuting Fourier-dual axes (`QLF_Spin.su2_comm_xy`); the sharp Shannon form is the entropic uncertainty relation (Beckner; §3a). No new axioms | `binning_halfwidth_le`, `binning_halfwidth_tight`, `uncertainty_quantum_eq_half`, `uncertainty_bound_anchored` |
 | [QLF_StateSpace.lean](QLF_StateSpace.lean) | **The space QLF lives in — a Gaussian-integer lattice, not Hilbert space** ([The_QLF_State_Space.md](../The_QLF_State_Space.md)). Hilbert space `ℂ^∞` is *too general* (continuum cardinality, continuous `U(1)` phases, infinite dimension — none realized, `QLF_Realizability`); QLF's state space is the discrete computable substructure it is the *completion* of: a finite-rank free module over the Gaussian integers `ℤ[i]` with phases in `μ₄={±1,±i}` and rational Born probabilities. Machine-checks that the QLF phase group (`PauliScalar`, the scalars `{+I,−I,+iI,−iI}` every balanced closure folds to via `count_balanced_pauli_closed`) is exactly `μ₄=(ℤ[i])ˣ`: every phase a 4th root of unity, generated by `i`, embedding into `ℂ`'s 4th roots of unity. Since `σx,σy,σz ∈ M₂(ℤ[i])`, amplitudes live over `ℤ[i]` (the stabilizer/Clifford = computable fragment); Hilbert space = the continuum completion. **`ℤ[i]` vs `ℤ[ζ₈]` resolved → `ℤ[i]`:** the Hadamard `√2` is a global, projectively-inert normalization (`bornProb_global_scale`, `hadamard_born_half`); a relative `ζ₈` needs the non-Clifford `T`-gate (magic/continuum), so the boundary is Clifford↔`T` = computable↔universal. No new axioms | `pauliScalar_pow_four_eq_one`, `pauliScalar_i_order_four`, `toComplex_pow_four`, `bornProb_global_scale`, `hadamard_born_half`, `qlf_phase_group_is_mu4` |
 | [QLF_Minkowski.lean](QLF_Minkowski.lean) | **The QLF state IS Minkowski space; its determinant is the spacetime interval** ([The_QLF_State_Space.md](../The_QLF_State_Space.md) §7). The 2×2 Hermitian `Form` `!![t+z,x−iy;x+iy,t−z]` is a point of Minkowski `ℝ^{1,3}` (1 trace = time + 3 traceless Pauli = space). `det_toMatrix_eq_interval`: `det = t²−x²−y²−z²`, the Minkowski interval — the metric IS the determinant. `pure_qubit_null`: pure qubits are null (Bloch = celestial sphere). Lorentz invariance: `lorentz_preserves_interval` (`SL(2,ℂ)` congruence preserves the interval ⟹ `SL(2,ℂ)→SO⁺(1,3)`, twists as 2-spinors). Dynamics too: `det_congruence` (`X↦AXA†` scales by `\|det A\|²`) + `interval_preserved_of_unit_det` (every twist has `\|det\|=1` ⟹ preserved). Over `ℤ[i]` the interval is integer-valued (discrete causal order); continuum Minkowski is its rendering. **Honest scope:** kinematic core + per-event dynamical preservation proven; double-cover surjectivity machine-checked in `QLF_LorentzCover`; macroscopic frame-independence = uniform-ether. No new axioms | `det_toMatrix_eq_interval`, `pure_qubit_null`, `lorentz_preserves_interval`, `det_congruence`, `interval_preserved_of_unit_det`, `qlf_state_is_minkowski` |
 | [QLF_EnergyMomentum.lean](QLF_EnergyMomentum.lean) | **The relativistic `E² = p² + m²` off the Minkowski interval** ([The_QLF_State_Space.md](../The_QLF_State_Space.md) §7). Read the Minkowski `Form` `(t,x,y,z)` as a **4-momentum** `(E,p_x,p_y,p_z)` (`c=1`): its interval `E²−\|p\|²` **is** the invariant mass². **`energy_momentum_relation`** — `(energy p)² = momentumSq p + invariantMassSq p`, i.e. `E² = p² + m²`, read straight off `Form.interval` (not a postulate — the relation IS the interval). **`massSq_eq_det`** — `m² = det(4-momentum)`, the same `Herm₂(ℂ) ≅ ℝ^{1,3}` identity (reuses `det_toMatrix_eq_interval`). **`mass_lorentz_invariant`** — the `SL(2,ℂ)` congruence `X↦AXA†` (`\|det A\|=1`) preserves the determinant `= m²` (reuses `interval_preserved_of_unit_det`): all observers agree on the invariant mass (E and p transform, m² does not). **`rest_energy_sq`** — `p=0 ⟹ E²=m²` (rest energy `E=mc²`). **`massless_null`** — `m²=0 ⟹ E²=p²` (the photon: a null/light-like 4-momentum on the light cone, the `pure_qubit_null` condition). So momentum enters QLF through the verified Lorentzian geometry, not as a bare additive count (the `Conservation.md` Noether entry). Reuses `QLF_Minkowski`; no new axioms | `energy`, `momentumSq`, `invariantMassSq`, `energy_momentum_relation`, `massSq_eq_det`, `mass_lorentz_invariant`, `rest_energy_sq`, `massless_null`, `energy_momentum_summary` |
 | [QLF_LorentzCover.lean](QLF_LorentzCover.lean) | **The `SL(2,ℂ) → SO⁺(1,3)` double cover, machine-checked** ([The_QLF_State_Space.md](../The_QLF_State_Space.md) §7). The double-cover structure of `QLF_Minkowski`'s spinor action `X↦AXA†`: `spinor_hom` (homomorphism); `boostZ_action` (`diag(a,b)`, `ab=1`, is a Lorentz boost — null coords `u↦a²u`, `v↦b²v`); `rotZ_action` (`diag(w,w̄)`, `\|w\|=1`, is a spatial rotation — `x−iy↦w²(x−iy)`); **`spinor_kernel`** (the only `A∈SL(2,ℂ)` acting trivially is `±I` — the 2-to-1); **`spinor_surjective`** (every proper orthochronous Lorentz transformation has an `SL(2,ℂ)` preimage). **Honest scope:** homomorphism + explicit generators + kernel `{±I}` fully proven; surjectivity rests on the one bridge axiom `lorentz_generated_by_boosts_rotations` (boosts+rotations generate `SO⁺(1,3)`; the generators it composes are proven in the image) | `spinor_hom`, `boostZ_action`, `rotZ_action`, `spinor_kernel`, `spinor_surjective`, `det_congruence` |
 | [QLF_HodgeIrreducible.lean](QLF_HodgeIrreducible.lean) | **The Hodge faithfulness swing series converges — the irreducibility invariant exists; the encoding is the floor** ([Hodge_QLF.md](../Hodge_QLF.md)). The non-multiplicative invariant `QLF_HodgeExpSequence` named missing was **already in the codebase**, from the α census: the prime/irreducible closures `2·Catalan(n−1)` + the **Dyson resummation** `G·(1−I)=1` (**`irreducibility_invariant_is_dyson`** = `census_irreducible_resummation`, [QLF_AlphaBound](QLF_AlphaBound.lean)) — total *multiplicative* census = geometric resummation of the irreducible primitives ⟹ a product of primes is composite ⟹ genuinely non-multiplicative. **But the bottleneck is the encoding:** the toy `encode⟨p,p⟩=upᵖdownᵖ` is the nested staircase, *prime for every `p`*, so the invariant is still `p`-uniform through it. **The floor:** all structural pieces (exp sequence + Chern/winding, balance/`(p,p)`, irreducibility/primes) are in hand; the whole faithfulness gap reduces to **one** thing — a *cycle-faithful encoding* of cohomology as closures (= build algebraic geometry in the substrate). **Not a proof** — the precisely-located floor; `substrate_realization_is_algebraic` stays the axiom | `irreducibility_invariant_is_dyson`, `hodge_faithfulness_floor` |
 | [QLF_HodgeExpSequence.lean](QLF_HodgeExpSequence.lean) | **The substrate exponential-sequence analog — the Hodge `(1,1)` faithfulness swing** ([Hodge_QLF.md](../Hodge_QLF.md)). Can the substrate make codim-1 *forced* like Lefschetz `(1,1)`? **Transfers (real):** the phase wrap `% N` ([QLF_LoopClosure](QLF_LoopClosure.lean)) **is** the substrate `0→ℤ→𝒪→𝒪*→0` — kernel = the integer winding `Nℤ` (**`substrate_exp_kernel`**, via `ZMod.intCast_zmod_eq_zero_iff_dvd`); a single winding = an elementary closure (**`codim_one_closes`** = `hermitian_pair_is_pauli_scalar`), the substrate's `Pic =` line bundles. **The finding (honest, one level finer than `realization_blind_to_codimension`):** realization is **multiplicative** — concatenated windings also close (**`codim_p_also_closes`** = `concat_pairs_is_pauli_scalar`) — so the substrate can't separate an *irreducible single cycle* from a *product*; that multiplicativity **is** the `p`-uniformity. Classical `(1,1)` cracks open because `H¹(𝒪*)=Pic` is *line bundles* (irreducible, no multiplicative collapse). **Sharpened target:** a **non-multiplicative irreducibility invariant** on closures. **Not a proof** — the located wall, named finer; `substrate_realization_is_algebraic` stays the axiom | `substrate_exp_kernel`, `codim_one_closes`, `codim_p_also_closes`, `hodge_exp_sequence_finding` |
 | [QLF_EtalePi1.lean](QLF_EtalePi1.lean) | **The profinite étale `π₁` — the first non-abelian layer** (the deepening past the order-2 `H↔H†` mirror; [Grothendieck_QLF.md](../Grothendieck_QLF.md) §2). Profinite by construction: the finite/RCA₀ substrate makes `π₁` an inverse limit of *finite* covers (no continuum imported). **`AxisDeck = Equiv.Perm (Fin 3) = S₃`** — the permutation group of QLF's three spatial axes, the *same* `S₃` (order 6, **`axisDeck_card`**) behind `m_p/m_e=6π⁵` (`QLF_LenzMassRatio`), colour SU(3), and the three generations. **`etale_pi1_nonabelian`** — non-abelian (two axis transpositions don't commute) ⟹ strictly richer than the abelian `Z/2` mirror. **`etale_pi1_mirror_quotient`** — the sign `S₃→Z/2` is non-trivial, so the motivic-Galois order-2 mirror `weightConjAut` is exactly the **abelian (sign) quotient** through which the non-abelian étale `π₁` factors: a genuine non-abelian Galois quotient above the `Z/2` of `QLF_AnabelianGalois`. **Open:** the full inverse-limit `Profinite` object + binding the axis-deck action to `closurePi1` cover-by-cover (`etale_pi1_profinite_in_progress`). No QLF axioms | `AxisDeck`, `axisDeck_card`, `etale_pi1_nonabelian`, `etale_pi1_mirror_quotient`, `etale_pi1_profinite_in_progress` |
 | [QLF_AnabelianGalois.lean](QLF_AnabelianGalois.lean) | **Closes the anabelian exact sequence on the substrate** — ties [QLF_Anabelian](QLF_Anabelian.lean) (geometric `π₁`) to [QLF_MotivicGalois](QLF_MotivicGalois.lean) (arithmetic Galois). A `Motive`'s closure *is* an anabelian `Event` (both `List Twist`), so the motivic Galois group acts on the anabelian objects. `weightConjAut` moves the **weight** (arithmetic enrichment) while fixing the **closure** (geometric `π₁`) — `1→π₁ᵍᵉᵒᵐ→π₁ᵃʳⁱᵗʰ→Gal→1` on the substrate: **`motive_closure_galois_invariant`** (Galois fixes the geometric closure), **`anabelian_galois_equivariant`** (`closurePi1` Galois-invariant ⟹ geometric `π₁` = kernel), **`galois_acts_on_weight`** (arithmetic side moves), **`galois_fixed_iff_hodge`** (the Galois-fixed locus = Hodge/Tate diagonal = the **Riemann critical line** = the **BSD central point** — the three Millennium self-dual loci are *one* verified motivic-Galois involution). Grounding + unification of the Millennium `H↔H†` spine; no new axioms. **`millennium_involution_unified`** packages it across modules: the **BSD** central point `s=1=2/2`, the **Riemann** functional-equation reflection, and the motivic-Galois `H↔H†` fixed locus (= the **Hodge**/Tate diagonal) are *one* `s↦a−s` self-duality. See [Grothendieck_QLF.md](../Grothendieck_QLF.md) §2/§5 | `motive_closure_galois_invariant`, `anabelian_galois_equivariant`, `galois_acts_on_weight`, `galois_fixed_iff_hodge`, `millennium_involution_unified`, `anabelian_galois_sequence` |
 | [QLF_AperyPeriod.lean](QLF_AperyPeriod.lean) | **ζ(3) (Apéry's constant) from the *same* closure census as π** — the period rung of Grothendieck's dream ([Grothendieck_QLF.md](../Grothendieck_QLF.md) §3). Apéry's series `ζ(3) = (5/2)·Σ(-1)ⁿ⁻¹/(n³·C(2n,n))` runs on the central binomial `C(2n,n)` = the substrate closure census. No new axioms: **`aperyTerm`/`aperySum`** = the finite, `Real.pi`-free **rational** partial sum; **`apery_summand_census`** (each term's `C(2(k+1),k+1)` *is* the closure count, reusing `closure_census` from [QLF_PhysicalPi](QLF_PhysicalPi.lean)); **`aperyTerm_one`** (`k=1` term `=1/2` ⟹ `5/4≈1.25`, near `ζ(3)≈1.2021`). The bridge `ζ(3)=(5/2)·lim aperySum` is Apéry's settled identity; by the substrate's **scale-free** consistency the convergence is structural (foundation-up, not borrowed) — `apery_period_in_progress`. The *same* census yields both `π` and `ζ(3)` ⟹ periods are combinatorial substrate facts | `aperyTerm`, `aperySum`, `apery_summand_census`, `aperyTerm_one`, `apery_period_in_progress` |
 | [QLF_Anabelian.lean](QLF_Anabelian.lean) | **The anabelian `π₁`↔closure functor** — geometry recovered from the combinatorial skeleton ([Grothendieck_QLF.md](../Grothendieck_QLF.md) §2). On [QLF_ReachableEvent](QLF_ReachableEvent.lean)'s causal set, no new axioms: **`closurePi1`** = the future-cone functor (the thin causal groupoid of closure paths); **`closure_groupoid_thin`** (no non-trivial loops ⟹ topological `π₁` trivial, the anabelian content is the causal *order* — Malament); **`closurePi1_injective`** (the geometry determines the closure — reconstruction on objects); **`reachable_iff_pi1_subset`** (the combinatorial order **is** the geometric inclusion — full faithfulness on morphisms); **`anabelian_fully_faithful`** (the functor is fully faithful ⟹ **geometry is recovered from the combinatorial closure** — Grothendieck's anabelian principle as a theorem). Arithmetic enrichment = the motivic Galois group (`QLF_MotivicGalois`). **Open:** the continuum order→metric step + a profinite étale `π₁` with a non-trivial Galois quotient | `closurePi1`, `closure_groupoid_thin`, `closurePi1_injective`, `reachable_iff_pi1_subset`, `anabelian_fully_faithful`, `anabelian_pi1_closure_functor` |
 | [QLF_MotivicGalois.lean](QLF_MotivicGalois.lean) | **The motivic Galois group** — the crown of Grothendieck's dream ([Grothendieck_QLF.md](../Grothendieck_QLF.md) §5). With the standard conjectures *reformulated* + the motive object built, the (conjectural) Tannakian category of pure motives has a **motivic Galois group** = the automorphism group of the fiber functor — built here as a genuine group. Concrete, no new axioms: a **`MotiveAut`** is a tensor-preserving, rank-preserving, invertible automorphism of motives; they form a **group** — `MotiveAut.comp`/`MotiveAut.id`/`MotiveAut.symm` with `comp_assoc`, `id_comp`/`comp_id` and the inverse laws `symm_comp`/`comp_symm` all machine-checked (`MotiveAut.ext`). **Non-trivial**: `weightConjAut` (the `H↔H†` weight conjugation) is an order-2 element (`weightConjAut_involutive`, reusing `conj_involutive`). The **`unitMotive`** (Tate motive) is the trivial representation (`galois_fixes_unit_rank`, `weightConjAut_fixes_unit`). **Open (next rungs):** the anabelian `π₁`↔closure functor, a second period | `MotiveAut`, `MotiveAut.ext`, `MotiveAut.id`, `MotiveAut.comp`, `MotiveAut.symm`, `comp_assoc`, `id_comp`, `comp_id`, `symm_comp`, `comp_symm`, `weightConjAut`, `weightConjAut_involutive`, `unitMotive`, `unitMotive_rank`, `galois_fixes_unit_rank`, `weightConjAut_fixes_unit`, `motivic_galois_group_on_substrate` |
 | [QLF_Motives.lean](QLF_Motives.lean) | **The motive object — the substrate closure as the universal cohomology** ([Grothendieck_QLF.md](../Grothendieck_QLF.md) §5, the mission). Built on the substrate *reformulation* of the standard conjectures (`standard_conjectures_on_substrate`; the bridge is conjectural), no new axioms beyond it. A pure **`Motive`** *is* a ZFA closure (count-balanced twist history) carrying a weight; **`Motive.realized`** reuses `count_balanced_pauli_closed` (a genuine closure, not a formal symbol). **`comparison_isomorphism`** *(theorem)* — all faithful Weil **`Realization`s** assign the same rank (the universal property; Betti numbers independent of the cohomology theory) because they render the one substrate object. Motives **tensor** (`Motive.tensor` = concat closures + add weights, via `countBalanced_append`; `tensor_realized`); the `H↔H†` **motivic-Galois duality** `Motive.dual` is an involution (`dual_involutive`, reusing `conj_involutive`) whose self-dual locus is the Hodge/Tate weights (`weight_selfDual_iff_hodge`, reusing the `QLF_Hodge` involution equivalence). `CohClass.toMotive`: every Hodge class has a motive. **Open (the next rung):** the motivic Galois *group* (Tannakian automorphisms) + cohomological-degree functoriality | `Motive`, `Motive.ext`, `countBalanced_append`, `countBalanced_reverse`, `Motive.realized`, `CohClass.toMotive`, `Motive.intrinsicRank`, `Realization`, `comparison_isomorphism`, `Motive.tensor`, `Motive.tensor_realized`, `Motive.dual`, `Motive.dual_involutive`, `Motive.weight_selfDual_iff_hodge`, `motive_object_on_substrate` |
 | [QLF_Reversibility.lean](QLF_Reversibility.lean) | **The reversibility capstone** (formal anchor of [Reversibility.md](../Reversibility.md)). Time-reversal **is** the Hermitian conjugate, and it is an *involution* — `antiparticle (antiparticle ts) = ts` (`antiparticle_involutive`, a bijection ⟹ reversible laws); while the forward ZFA closure is *many-to-one* — `C(2n,n) ≥ 2` satisfying histories collapse to one closed outcome for every `n≥1` (`two_le_central_binom` via `Nat.choose_le_middle`, with `disjunct_count_eq_central_binomial`) ⟹ non-injective ⟹ irreversible process. **`time_reverse_involutive_but_closure_degenerate`** packages both clauses. Reversible *logic*, irreversible *process*; the arrow of time is the non-injectivity of the forward map, not any failure of the reverse to exist (the synthesized-time "nowhere to run the reverse" framing is prose, grounded in `ZFAEventDynamics`). No new axioms — both halves reuse verified theorems. See [Reversibility.md](../Reversibility.md), [Conservation.md](../Conservation.md) §2b | `two_le_central_binom`, `time_reverse_involutive_but_closure_degenerate`, `reversibility_capstone_established` |

### Physical Theories

| Module | Description | Key theorems |
|---|---|---|
| [StringTheoryQLF.lean](StringTheoryQLF.lean) | String theory via gauge-fold depth; closed string excitation tower; C(2n,n) mode degeneracy | `string_mass_spectrum`, `string_mode_count`, `landscape_zfa_stable` |
| [MTheoryQLF.lean](MTheoryQLF.lean) | M-theory via gauge-fold stacks; M2/M5-branes; S/T-duality; 11D compactification | `mbrane2_hermitian`, `m2_mass_spectrum`, `s_dual_involution`, `m11d_zfa_stable` |

### Speculative Extensions

| Module | Description | Key theorems |
|---|---|---|
| [AgeOfUniverse.lean](AgeOfUniverse.lean) | Cosmological age from ZFA event rate | `age_is_finite_and_positive` |
| [ER_EPR_QLF.lean](ER_EPR_QLF.lean) | Entanglement-geometry axioms (ER=EPR) | philosophical axioms — explicitly speculative |


### Additional Modules (build order)

Modules registered in `lakefile.lean` after the thematic groups above, in build order. Descriptions carry the honest-scope framing; the full narrative for each lives in the per-topic `../*.md` doc it cites. The Key-theorems column lists each module’s own declarations.

| Module | Description | Key theorems |
|---|---|---|
| [QLF_Kolmogorov.lean](QLF_Kolmogorov.lean) | **The flux-invariance lemma + the forced `−5/3` exponent** (`Navier_Stokes_Geometry.md` §6a, issue #110). `flux_scale_invariant` (per-closure energy = octave-independent `log 2` quantum, reuses `binary_kl_delta_uniform` — K41's inertial-range premise); `octave_frequency_ladder` (= `cascade_frequency_increases`); `kolmogorov_exponents` (`(a,b)=(2/3,−5/3)` the unique solution of the dimensional constraints — a genuine `linarith` theorem). Intermittency: `velocity_holder_exponents`/`she_leveque_beta`/`she_leveque_codimension` (`C₀=d−1=2` the sole `d`-input; `β=2/3` from dimension-independent Hölder `h=1/3`). **Honest scope:** anchors the scaling argument, NOT a derivation of turbulence. No new axioms. See `Navier_Stokes_Geometry.md` §6a | `flux_scale_invariant`, `octave_frequency_ladder`, `kolmogorov_exponents`, `velocity_holder_exponents`, `she_leveque_beta`, `she_leveque_codimension` |
| [QLF_PiRational.lean](QLF_PiRational.lean) | **The substrate π-approximant is rational; the interface is `Real`-free** (`Completeness_Evidence.md` §2a, issue #113). The rendering obligation is substrate → ℚ-with-intervals, not → ℝ. `returnDensity n : ℚ` (`QLF_PhysicalPi`) is rational at every finite `n`: `returnDensity_one` (`1/4`), `returnDensity_two` (`9/64`), `returnDensity_three` (`25/256`), `returnDensity_isRational`. The `(rational)·π` physics bounds via Mathlib `Real.pi_gt_d6`/`_lt_d6`: `hierarchy_rational_interval` (`43.982<14π<43.983`), `eight_pi_rational_interval`, `two_pi_rational_interval`, `pi_rational_interval`. Reuses `QLF_PhysicalPi`; no new axioms. See `Completeness_Evidence.md` §2a | `returnDensity_one`, `returnDensity_two`, `returnDensity_three`, `returnDensity_isRational`, `hierarchy_rational_interval`, `eight_pi_rational_interval`, `two_pi_rational_interval`, `pi_rational_interval` |
| [QLF_ShannonOverfit.lean](QLF_ShannonOverfit.lean) | **The reals over-parameterize physics — non-identifiability, a Shannon proof** (`Shannon_Overfit.md`). `no_real_received` (Thm A — no injection `ℝ → Fin (2^C)` into a capacity-`C` channel, reusing `real_continuum_not_realizable`, so no measurement identifies a real); `tail_unconstrained` (Thm B — every finite `n`-bit dataset leaves an `Infinite` consistency fiber via `tailWitness`). Thm C (finite physical capacity — Shannon–Hartley/Landauer/Bekenstein) is the named empirical premise. **Honest scope:** A/B finite combinatorics; C empirical, not "ℝ inconsistent" (consistency ≠ realizability). Reuses `QLF_Realizability`; no new axioms. See `Shannon_Overfit.md` | `no_real_received`, `tail_unconstrained`, `tailWitness` |
| [QLF_FQHE.lean](QLF_FQHE.lean) | **The fractional-quantum-Hall stability ordering, made rigorous** (`Electricity.md` §7a, issue #111). The composite-fermion tower is closures-within-closures; stability ordering IS closure-depth ordering. `jainDenom s p σ = 2sp+σ` (the depth/denominator); `jainDenom_odd` (depth odd — the odd-denominator rule); `jainDenom_depth_mono` (deeper=less stable, the `1/3>2/5>3/7>4/9` order); `particle_hole_same_depth` (the `2/3~1/3` degeneracy). **Honest scope:** ordering structure proven; deeper=smaller-gap premise + absolute gap scale + odd-denominator origin are residuals. Mathlib only; no new axioms. See `Electricity.md` §7a | `jainDenom_odd`, `jainDenom_depth_mono`, `particle_hole_same_depth` |
| [QLF_ContradictionReceipt.lean](QLF_ContradictionReceipt.lean) | **A contradiction receives no receipt** (`Philosophy.md` §9, `Related_Frameworks.md` Part II §5, issue #115 item 4). Realized information is receipt-counted, and a **contradiction** — an unbalanced ledger (`count_pos ≠ count_neg`) — admits no ZFA closure, hence carries **zero** realized information. **`contradiction_no_receipt`** (unbalanced ⟹ ¬`achieves_ZFA`, the contrapositive of `zfa_implies_critical_line`) + **`receipt_is_balanced`** (every receipt is balanced). Proves the **anti-dialetheist thesis** (contradiction never realized, only cancelled) and dissolves the **Bar-Hillel–Carnap paradox** (a contradiction carries *no* realized information, not maximal — one theorem, two docs). Reuses `QLF_Axioms`; no new axioms. See `Philosophy.md` §9 | `contradiction_no_receipt`, `receipt_is_balanced` |
| [QLF_EntropyUniqueness.lean](QLF_EntropyUniqueness.lean) | **The closure measure is forced, not chosen** (`Completeness_Evidence.md` §6, issue #115 item 6). The information-theoretic wing of the reconstruction program — the finite/additive uniqueness (avoids Gleason's analysis). A *consistent information measure* is additive on independent ledgers (`IsAdditive`: `H(a++b)=H a+H b`). Then **`additive_nil`** (`H[]=0` forced), **`additive_uniform_eq_length_mul`** (`H s = \|s\|·c` — counting is *forced* by additivity + one anchor `H[x]=c`; with `c=log 2` = Shannon on the census), **`additive_unique`** (two measures agreeing on generators agree everywhere ⟹ uniqueness). The Baez–Fritz–Leinster / Knuth *structure-forces-the-measure* move on QLF's own structure. **Honest scope:** the *counting* wing; the full distributional `−Σ p log p` (Faddeev / Cauchy-equation over arbitrary weights) is the analytic residual (#115). Mathlib only; no axioms. See `Completeness_Evidence.md` §6 | `IsAdditive`, `additive_nil`, `additive_uniform_eq_length_mul`, `additive_unique` |
| [QLF_Identifiability.lean](QLF_Identifiability.lean) | **Capacity bounds distinguishability; the unconstrained tail** (`Shannon_Overfit.md`, issue #115 item 2; complements `QLF_ShannonOverfit`). `capacity_bound` (Thm A — a `C`-bit record distinguishes ≤ `2^C` states, via `transcript_card = 2^C`); `consistent_set_infinite`/`consistent_set_continuum` (Thm B — any positive-width record leaves a consistent set of cardinality continuum, `Cardinal.mk_Icc_real`); `Identifiable x` := ∃ computable `f:ℕ→ℚ` with `\|x−f n\|≤(1/2)^n`, `identifiable_rat`, `identifiable_of_modulus`. **Honest scope:** the K-graded tier boundary needs Kolmogorov-complexity machinery Mathlib lacks (#115). Mathlib only; no axioms. See `Shannon_Overfit.md` | `capacity_bound`, `consistent_set_infinite`, `consistent_set_continuum`, `identifiable_rat`, `identifiable_of_modulus` |
| [QLF_CensusShannon.lean](QLF_CensusShannon.lean) | **Information composes as counts multiply** (`Shannon_Overfit.md`, issue #115 item 1). The multiplicative half of *census = Shannon*, on ℕ with no log/`Real`. `independent_join_multiplies` (`card (α×β) = card α · card β`, Boltzmann `W₁·W₂`), `trivial_multiplicity` (1), `bit_multiplicity` (2), `nbit_multiplicity` (`2^n`), `multiplicity_composes` (`2^{m+n}=2^m·2^n`). Complements `QLF_EntropyUniqueness` (additive dual). **Honest scope:** stock finite combinatorics; the closure census `C(2n,n)` itself adds not multiplies, so the honest law is configuration-count multiplicativity; Faddeev uniqueness is the residual (#115). No `Real`, no axioms. See `Shannon_Overfit.md` | `independent_join_multiplies`, `trivial_multiplicity`, `bit_multiplicity`, `nbit_multiplicity`, `multiplicity_composes` |
| [QLF_BornProbability.lean](QLF_BornProbability.lean) | **Count-ratio Born probabilities satisfy the probability axioms** (the #65 keystone, issue #115 item 5). The substrate Born probabilities are **integer path-count ratios** (`bornProb v k = ‖aₖ‖²/Σⱼ‖aⱼ‖²` over the Gaussian integers, `QLF_StateSpace`) and form a genuine probability measure **from counting, no primitive real**: **`bornProb_nonneg`** (Gaussian norms `≥0`), **`bornProb_sum_eq_one`** (normalization, via `Finset.sum_div`+`div_self`), **`eventProb`** + **`eventProb_disjoint_union`** (finite Kolmogorov additivity `P(S⊔T)=P(S)+P(T)`, via `Finset.sum_union`), **`eventProb_univ`**. So logits/amplitudes are a **reporting layer over closure counts**. **Honest scope:** this proves the *measure axioms* for the count-ratio rule QLF uses; the *uniqueness* of the `\|a\|²` form (Gleason) is the separate reconstruction target (`Completeness_Evidence.md` §6). Exact `ℚ` arithmetic; no `Real`, no axioms. See `Shannon_Overfit.md` | `bornProb_nonneg`, `bornProb_sum_eq_one`, `eventProb`, `eventProb_disjoint_union`, `eventProb_univ` |
| [QLF_AlphaRigidity.lean](QLF_AlphaRigidity.lean) | **The elementarity spine of α-rigidity** (`Alpha.md` §6a, issue #116) — toward *137 is the only reachable value*. Spine: `prime_implies_atomic` (I2 — prime ⟹ no factorization), `realization` (P1 — the single physical axiom: every factorization of a ZFE-closed count is realized as independent sub-receipts), `elementary_iff_prime` (I3, from I2+P1), `dyadic_closed` (I1). Cross-sector joint: `d` is substrate-derived (6+2 split → 3 axis-pairs #42), so `α⁻¹ = 128 + d²` is the meeting of two sectors. `alpha_unique` (`128+d²=137 ⟺ d=3`, zero slack), `rival_excluded` (4D→144), `inverseAlpha_three_prime`/`_elementary` (137 prime), `alpha_counts_dimension`, `dimension_136_unreachable` (136 dies twice). **Honest scope:** `d=3` forced at the counting layer; the mechanism-layer #62 swap-graph check pending; the census `N(d)` residual (#116). No new axioms beyond P1. See `Alpha.md` §6a–§6b | `prime_implies_atomic`, `elementary_iff_prime`, `dyadic_closed`, `alpha_unique`, `rival_excluded`, `inverseAlpha_three_prime`, `alpha_counts_dimension`, `dimension_136_unreachable` |
| [QLF_Reconstruction.lean](QLF_Reconstruction.lean) | **The reconstruction theorem's entropy-uniqueness wing (finite lattice)** (`Completeness_Evidence.md` §6, issue #118). The reconstruction theorem (ZFA-free postulates ⟹ isomorphic to ZFA over the 8-twist alphabet) is the converse to `qlf_universality`. Lands the entropy-uniqueness wing: `IsMeasure` (additive over orthogonal events), `measure_eq_sum_atoms` (Gleason-style, finite — atom-determined `μ s = Σ μ{a}`), `measure_unique` (agree on atoms ⟹ unique). Lattice counterpart of `QLF_EntropyUniqueness`. **Honest scope:** orthogonality = the finite Boolean shadow of Gleason; the non-distributive Gleason + postulates→ZFA isomorphism (#118) remain open. Mathlib only; no axioms. See `Completeness_Evidence.md` §6 | `IsMeasure`, `measure_eq_sum_atoms`, `measure_unique` |
| [QLF_EmergenceChain.lean](QLF_EmergenceChain.lean) | **The emergence forcing chain, assembled (reuse-only)** (`Completeness_Evidence.md` §6a). Chains proven links from the bare premise toward ZFA: Link 1 discreteness forced (`realized_realm_discrete`, reusing `no_continuum_in_finite_region`); Link 2 balanced closure folds to the algebra (`closure_folds_to_scalar`, reusing `count_balanced_pauli_closed`); Link 3 fold-target IS `μ₄ = ℤ/4` (`foldTarget_is_mu4`, reusing `toZMod_hom`/`toZMod_injective`); `emergence_chain` bundles Links 2–4. Forces the closure invariant, NOT that the 8-twist machine is unique (`comparison_isomorphism`). **Honest scope:** necessary-condition spine proven; open — why this alphabet (#116) + postulates→ZFA uniqueness (#118). No new axioms. See `Completeness_Evidence.md` §6a | `realized_realm_discrete`, `closure_folds_to_scalar`, `foldTarget_is_mu4`, `emergence_chain` |
| [QLF_PostulateReduction.lean](QLF_PostulateReduction.lean) | **The five reconstruction postulates collapse into one-and-a-half** (`Completeness_Evidence.md` §6b, issue #118). Read against the one postulate (reality = the finite self-closing subset of possibility), four reduce: finite capacity = the "finite" clause (`finite_capacity_forces_discreteness`, reusing `no_continuum_in_finite_region`); closure-as-receipt = the selection clause; reversible-logic/irreversible-realization = DERIVED (`reversible_logic_irreversible_realization`, reusing `time_reverse_involutive_but_closure_degenerate`); no-disconnection = plausibly derivable (doc); orthomodularity = the residue (only the orthomodular law Gleason-hard). Target: one postulate + orthomodular law ⟹ ZFA. **Honest scope:** a reduction, not closure. Reuse-only; no new axioms. See `Completeness_Evidence.md` §6b | `finite_capacity_forces_discreteness`, `reversible_logic_irreversible_realization` |
| [QLF_ProperInvolution.lean](QLF_ProperInvolution.lean) | **The substrate dagger is a proper involution — the (a1) rung of the orthomodular reduction** (`Completeness_Evidence.md` §6c, issue #118). The reconstruction residue narrows to *"proper involution + projection-lattice bridge"*; this lands the proven half: **`substrate_dagger_proper`** (`Mᴴ * M = 0 ⟹ M = 0` on the substrate complex matrices, via Mathlib's `conjTranspose_mul_self_eq_zero` under `open scoped ComplexOrder`) = positive-definiteness of the inner product, with the `Form` corollary **`form_dagger_proper`**. Given the projection-lattice bridge (Baer-`*`-ring→orthomodular, Kaplansky/Berberian — the settled-math step Mathlib lacks assembled), the orthomodular law follows on the non-distributive (rendered) layer. Reuse-only; no new axioms. See `Completeness_Evidence.md` §6c | `substrate_dagger_proper`, `form_dagger_proper` |
| [QLF_StabilizerZi.lean](QLF_StabilizerZi.lean) | **Stabilizer / Clifford evolution never leaves ℤ[i]** (issue #115 item 3). Gottesman–Knill = the *computable* fragment of QM, and QLF's reading is it lives exactly over the **Gaussian integers** (`QLF_StateSpace`). Makes "the integer skeleton is load-bearing" concrete: the Clifford generators are represented over `ℤ[i]` (`GaussianInt`) — **`pauliX`/`pauliY`/`pauliZ`/`sGate`/`sqrt2H`** — with genuine defining relations proven as exact `ℤ[i]` computations (not numerical over ℂ): `gI_sq` (`i²=−1`), `pauliX_sq`/`pauliY_sq`/`pauliZ_sq` (`=I`), **`sGate_sq`** (`S²=Z`), **`sqrt2H_sq`** (`(√2·H)²=2I`), **`hadamard_conjugates_X_to_Z`** (`HXH=Z`, up to the global `2`). Since `ℤ[i]` is a `CommRing` closed under conjugation, every product/adjoint stays in `ℤ[i]` — no continuum entry; the `1/√2` of Hadamard is a global projective normalization (`bornProb_global_scale`). Reuse-only; no new axioms. See `The_QLF_State_Space.md` | `pauliX`, `pauliY`, `pauliZ`, `sGate`, `sqrt2H`, `gI_sq`, `pauliX_sq`, `pauliY_sq`, `pauliZ_sq`, `sGate_sq` |
| [QLF_CensusWalk.lean](QLF_CensusWalk.lean) | **Lean-anchors genesis.py §2 (the `−p/2` spectral exponent) at low orders** (`Genesis.md`, `Physical_Pi.md`). `sumChooseSq_eq_central` (Vandermonde `Σ C(m,k)² = C(2m,m)`, so `c_pair(2,m)=C(2m,m)`); `census_p2` (`realized(2,m)=C(2m,m)²`); `census_p2_is_return_density` (the p=2 return prob IS `returnDensity`, so the p=2 exponent `−1` is the census→π density); `census_p1` (reuse `closure_census`). **Honest scope:** only p=1,2 anchored; general-`p` + the `−p/2` asymptotic stay the settled-analysis residual. No new axioms. See `Genesis.md` | `sumChooseSq_eq_central`, `census_p2`, `census_p2_is_return_density`, `census_p1` |
| [QLF_HarmonicClosure.lean](QLF_HarmonicClosure.lean) | **Reality & constructable truth as the closing spectrum of frequency-component closures** (`Frequency_Synchronization.md` §0, `Philosophy.md`). Each frequency component IS one ZFA closure = a quantum-logical computation (a set of Feynman diagrams); reality = the closing subset of the spectrum. Reuse-only: `component_freq` (`freq R = 1/R`), `higher_freq_dominates` (reuse `freq_lt_of_lt`), `binding_raises_harmonic` (`freq_bind_ge_left`), `irreducible_mode` (`prime_freq_irreducible`), `path_integral_generates` (`4ⁿ` histories, reuse `generated_count`; closure = the firebreak, `not_all_paths_close`; `qlf_universality`). **Honest scope:** structural framing; the QFT `e^{iS/ℏ}` diagrammatics = continuum rendering; no new axioms. See `Frequency_Synchronization.md` §0 | `component_freq`, `higher_freq_dominates`, `binding_raises_harmonic`, `irreducible_mode`, `path_integral_generates` |
| [QLF_DynamicalDarkEnergy.lean](QLF_DynamicalDarkEnergy.lean) | **`ρ_Λ ∝ H²` ⟹ QLF's dark energy is dynamical, not a constant Λ** (`DarkMatter.md` §5a — the Hubble-tension stance). Substituting the Hubble radius `R_H = c/H` into QLF's vacuum density (`vacuum_energy_density_QLF`, `QLF_CosmologicalConstant`) gives **`rhoLambda_prop_Hsq`** (`ρ_Λ = (prefactor·c²/G)·H²`, via `field_simp`), with `rhoLambdaCoeff_pos` (`prefactor = 3 log2/8π > 0`). Hence **`rhoLambda_past_denser`** (strictly increasing in `H` ⟹ **denser in the past** = early-dark-energy character) and **`rhoLambda_not_constant`** (`ρ_Λ` varies with `H`, unlike ΛCDM's static Λ). This is the property placing QLF's cosmology in the *resolution-favorable* class of the Hubble tension. **Honest scope:** anchors the proportionality + monotonicity (reuse-only); does NOT derive absolute `H₀` or resolve the tension numerically. No new axioms. See `DarkMatter.md` §5a | `rhoLambda_prop_Hsq`, `rhoLambdaCoeff_pos`, `rhoLambda_past_denser`, `rhoLambda_not_constant` |
| [QLF_CurvatureLie.lean](QLF_CurvatureLie.lean) | **Curvature from one-bit orthogonality IS the su(2) Lie bracket** (`Curvature.md` §1a, `Mathematics_From_QLF.md` Rung 8). Reuse-only: `orthogonality_one_bit` (a Hermitian-pair distinction = `log 2`, reuse `orthogonal_distinction_is_one_bit`); `orthogonal_axes_close_su2` (`[σx,σy]=2iσz`, reuse `su2_comm_xy`); `curvature_nonabelian`/`curvature_nontrivial` (curvature = non-abelian Wilson-loop `σxσyσxσy=−1`, reuse `QLF_GaugeHolonomy`) vs `flat_when_abelian` (`em_plaquette_trivial`). So `εᵢⱼₖ` = field strength; abelian flat (photon) / non-abelian curved (gluon-W). **Honest scope:** structural reading; the diff-geo tensor step open. No new axioms. See `Curvature.md` §1a | `curvature_is_lie_bracket` |
| [QLF_KnotInvariant.lean](QLF_KnotInvariant.lean) | **Embedded ZFA closures are knots/links — the Kauffman-lineage reading** (`Knot_Theory_QLF.md`, `HALF-SPIN-ZFA-EMBEDDING.md` §3b). Reuse-only, re-reading `QLF_BaryonWinding`/`QLF_QuarkStructure` under knot names: `linkingNumber = baryonNumber`; `linking_orientation_odd` (reuse `signTriple_rev`); `mirror_reverses_linking` (`L↦−L` under conjugation, reuse `baryon_dagger_odd`); `borromean_remove_one_unlinks` + `brunnian_needs_all_three` (baryon = a Borromean 3-link, reuse `baryon_zero_of_missing`/`baryon_needs_all_three_axes`); `single_component_unlinked`, `meson_zero_linking`, `proton_link`. Lineage Jones 1984 → Kauffman 1987 → Witten 1988. **Honest scope:** linking/Borromean core proven; full Reidemeister + the Chern–Simons TQFT rendering stay structural (`knot_invariant_in_progress`). See `Knot_Theory_QLF.md` | `linking_orientation_odd`, `mirror_reverses_linking`, `borromean_remove_one_unlinks`, `brunnian_needs_all_three`, `single_component_unlinked`, `meson_zero_linking`, `proton_link`, `knot_invariant_in_progress` |
| [QLF_ReidemeisterLinking.lean](QLF_ReidemeisterLinking.lean) | **The crossing-sign Levi-Civita algebra + the Reidemeister invariances of the linking number** (`Knot_Theory_QLF.md` §3). Genuine proof that `signTriple` is the oriented Levi-Civita symbol. Crossing algebra (`decide`): `crossing_cyclic`, `crossing_transpose` (`ε a b c = −ε b a c`), `crossing_self_zero` (R1: self-crossing doesn't link), `crossing_R2_cancel` (R2: opposite crossings cancel). Linking invariances: `linking_mirror_odd` (reuse `bnA_reverse`); `linking_missing_axis_zero` (R1, reuse `baryon_zero_of_missing`); `linking_gauge_prepend`/`linking_gauge_append` (gauge kink preserves linking, new `bnA_cons_none`/`endWindowA_none`/`bnA_snoc_none`). **Honest scope:** crossing algebra + R1 + mirror-oddness proven; full R2/R3 over an encoded diagram is `QLF_LinkDiagram`. No new axioms. See `Knot_Theory_QLF.md` | `crossing_cyclic`, `crossing_transpose`, `crossing_self_zero`, `crossing_R2_cancel`, `linking_mirror_odd`, `linking_missing_axis_zero`, `linking_gauge_prepend`, `linking_gauge_append`, `bnA_cons_none`, `endWindowA_none` |
| [QLF_LinkDiagram.lean](QLF_LinkDiagram.lean) | **A Gauss-code link diagram + full R1/R2/R3 invariance of the linking number** (`Knot_Theory_QLF.md` §3, §4a). Encodes a diagram at Gauss-code level (`Crossing` = tags `c1`,`c2` + oriented `sign`; `LinkDiagram = List Crossing`), linking number `crossingSum a b D` (= `2·lk`). All three moves invariant: `linking_r1_invariant` (self-crossing), `linking_r2_invariant` (opposite-sign pair cancels), `linking_r3_invariant` (slide = permutation, `List.Perm.sum_eq`). Calibration: Hopf `crossingSum=2`, unlink `0`. **Honest scope:** full R1/R2/R3 at the Gauss-code level; Reidemeister's 1927 theorem + planar↔crossing-data faithfulness cited. Rides Witten 1988 → Reshetikhin–Turaev (the Chern–Simons bridge already discharged by RT). No new axioms. See `Knot_Theory_QLF.md` §5 | `linking_r1_invariant`, `linking_r2_invariant`, `linking_r3_invariant` |
| [QLF_KauffmanBracket.lean](QLF_KauffmanBracket.lean) | **The Kauffman bracket as a firebreak state-sum — the bridge's discrete side, built** (`Knot_Theory_QLF.md` §4). Defines the bracket as a generate-then-close state-sum (`bracket` = sum over `resolutions n`, `resolutions_length`, weighted `A^#A·Ai^#B·δ^(loops−1)`, `δ=−A²−Ai²`) satisfying the Kauffman defining relations: `bracket_unknot` (`⟨○⟩=1`), `bracket_skein` (`⟨D⟩ = A⟨D_A⟩ + Ai⟨D_B⟩`, via `sum_map_mul_left`/`weight_true_cons`/`weight_false_cons`), `bracket_disjoint_circle` (`δ·⟨D⟩`), `bracket_one_crossing`. Fully general (`R` any `CommRing`). **Honest scope:** state-sum↔bracket built; R2/R3 = cited Reidemeister input, the Chern–Simons leg RT-discharged. So `firebreak_bracket_bridge`'s discrete side is verified. No new axioms. See `Knot_Theory_QLF.md` §4 | `bracket`, `resolutions_length`, `bracket_unknot`, `bracket_skein`, `sum_map_mul_left`, `weight_true_cons`, `weight_false_cons`, `bracket_disjoint_circle`, `bracket_one_crossing` |
| [QLF_TorusBracket.lean](QLF_TorusBracket.lean) | **A concrete planar loop-count — `bracket` computes named knots** (`Knot_Theory_QLF.md` §4). A computed loop-count for the 2-strand torus links `T(2,n)` via Temperley–Lieb: `tlReduce` + Markov closure = `torusLoops` (loop lemmas `tl_*` by `decide`). Feeding `QLF_KauffmanBracket.bracket` computes the actual bracket: `bracket_unknot_kink` (`T(2,1)=−A³`), `bracket_hopf` (`−A⁴−A⁻⁴`), `bracket_trefoil` (`−A⁵−A⁻³+A⁻⁷`) — all matching the literature. **Honest scope:** the 2-strand torus family; a general planar diagram needs the 4-valent-graph/rotation-system model. No new axioms. See `Knot_Theory_QLF.md` §4 | `tlReduce`, `torusLoops`, `bracket_unknot_kink`, `bracket_hopf`, `bracket_trefoil` |
| [QLF_PlanarBracket.lean](QLF_PlanarBracket.lean) | **The general planar loop-tracer — `bracket` computes any knot from its arc code** (`Knot_Theory_QLF.md` §4, §6a). Completes `QLF_TorusBracket`: a diagram as an arc matching `arc : ℕ → ℕ` on `4n` corners; smoothing `smoothPerm` an involution; `planarLoops arc m s = cycleCount (arc ∘ smoothPerm s) m / 2` (`cycleCount` via `orbitList`). Validated on named knots: `bracket_hopf'` (`−A⁴−A⁻⁴`), `bracket_trefoil'` (`−A⁵−A⁻³+A⁻⁷`) — matching the literature and `QLF_TorusBracket` (cross-validation), loop counts by `native_decide`. **Honest scope:** fully general tracer; R2/R3 + Chern–Simons rendering cited. No new axioms. See `Knot_Theory_QLF.md` §4 | `smoothPerm`, `cycleCount`, `orbitList`, `bracket_hopf'`, `bracket_trefoil'` |
| [QLF_CensusBrownian.lean](QLF_CensusBrownian.lean) | **The closure census is a random walk — the Riemann GMC bridge, discrete side** (`Riemann-Conjecture-Proof.md`). Attaches the critical line to settled math (Gaussian multiplicative chaos), the Lever-3 move. A ZFA-balanced string of length `2n` is a closed `±1` random walk (balance = returns to origin), census `= C(2n,n)` = closed-walk count (`census_is_closed_walk_count`); `returnProb1D = C(2n,n)/4ⁿ`; 2-D density = two independent 1-D returns (`returnDensity_eq_sq_1d`). Balance=walk-closure IS the critical-line condition (`zfa_implies_critical_line`); scale-indexed Brownian phases = a log-correlated field (GMC describing `ζ` on the line; Planck floor = GMC UV cutoff). **Honest scope:** Brownian structure proven; the GMC↔`ζ` correspondence is the bridge candidate, does not prove RH (`spectral_hilbert_polya`/`MRE_bridge` stay Class-A). See `Riemann-Conjecture-Proof.md` | `census_is_closed_walk_count`, `returnDensity_eq_sq_1d` |
| [QLF_LorentzGeneration.lean](QLF_LorentzGeneration.lean) | **The round-trip lemmas + the spinor-image submonoid — the genuine reduction of the Lorentz-cover axiom** (`Millennium.md`, `QLF_NavierStokesBKM`-style). Both `Form↔Matrix` round-trips proven (`fromMatrix_toMatrix`, `toMatrix_fromMatrix`, `spinorAct_isHermitian`); the spinor image is a submonoid (`realizes_one`+`realizes_mul`); all generators realized (`boost_realized`, `rot_realized`, `rotY_realized`, `so3_euler_realized`, `kak_realized`) + forward inclusion (`boostMatrix_preserves_metric`/`rotMatrix_preserves_metric`/`rotYMatrix_preserves_metric`). The axiom reduces to the single real-matrix reverse inclusion. Reconstruction: `exists_boost_params`, `su2_realized`/`su2_action`, `su2Matrix_recovery`, `recovered_quaternion_norm` (norm `4(1+tr)`, division-free). Remaining: the 9 entry identities + `cof R=R` + KAK extraction. No new axioms. See `The_QLF_State_Space.md`, `UniversalRelativity.md` | `fromMatrix_toMatrix`, `toMatrix_fromMatrix`, `spinorAct_isHermitian`, `realizes_one`, `realizes_mul`, `boost_realized`, `rot_realized`, `rotY_realized`, `so3_euler_realized`, `kak_realized` |
| [QLF_QuantumTurbulence.lean](QLF_QuantumTurbulence.lean) | **The superfluid/quantum-turbulence dynamical picture, proven** (`Turbulence.md` §5/§8, issue #120). Onsager–Feynman: `vortex_is_one_quantum`, `circulation_is_integer_quantized`. Phase alphabet `μ₄={±1,±i}=(ℤ[i])ˣ`, a primitive quarter-turn (`phase_quantum_is_quarter_turn`, `quarter_turn_primitive`). **A closed ZFA loop folds to real `{±I}`, never `±iI`** — `balanced_closure_folds_real` (even Pauli count `balanced_pauli_count_even`/`countP_isPauli_eq` ⟹ fold det `+1`, `det_twistMatrixFold`/`det_twistMatrix`); the `±i` is an open forward strand closed by its dagger (`dagger_doubles_pauli_count`; `dagger_closes`, `dagger_closure_folds_real`). Plus `highest_frequency_resolves_first`, `cascade_has_floor`, `prime_closure_irreducible`, `half_spin_is_prime_agent`. **Honest scope:** structural core proven; NOT the `−5/3` spectrum. Reuses `QLF_Turbulence`/`QLF_StateSpace`/`QLF_PrimeResonance`/`QLF_TwistAlphabet`. See `Turbulence.md` | `vortex_is_one_quantum`, `circulation_is_integer_quantized`, `phase_quantum_is_quarter_turn`, `quarter_turn_primitive`, `balanced_closure_folds_real`, `balanced_pauli_count_even`, `countP_isPauli_eq`, `det_twistMatrixFold`, `det_twistMatrix`, `dagger_doubles_pauli_count` |
| [QLF_HiggsTurbulence.lean](QLF_HiggsTurbulence.lean) | **The Higgs as the radial mode of a quantum-turbulent gauge-fold vacuum** (`Higgs.md` §5a) — reuse-only, supplying the dynamical origin of `R_stable`. `R_stable` = the mean vortex-tangle depth of the steady-state cascade (a dynamical output). `gauge_fold_is_quantized_defect` (the fold's `μ₄` phase = an Onsager–Feynman vortex); `vacuum_circulation_is_quantized_tangle`; `ew_vacuum_is_closed_real_fold` (stable vacuum = a closed loop folding to real `±I`); `higgs_depth_cascade_floored` + `hierarchy_mass_bounded_by_floor` (Planck floor caps `m=1/R` — hierarchy problem absent, full treatment `Higgs.md` §5b); `ew_phase_nucleated_by_prime_closure`; `higgs_mass_is_stable_depth_inverse` (`M_H=1/R_stable`). Phase directions = eaten Goldstones, fold-depth = Higgs. **Honest scope:** identifications anchored; `R_stable` value + `M_H/v≈0.51` open (`higgs_turbulence_in_progress`). Reuses `QLF_QuantumTurbulence`+`QLF_HiggsMechanism`. See `Higgs.md` §5a | `gauge_fold_is_quantized_defect`, `vacuum_circulation_is_quantized_tangle`, `ew_vacuum_is_closed_real_fold`, `higgs_depth_cascade_floored`, `hierarchy_mass_bounded_by_floor`, `ew_phase_nucleated_by_prime_closure`, `higgs_mass_is_stable_depth_inverse`, `higgs_turbulence_in_progress` |
| [QLF_TopYukawaRunning.lean](QLF_TopYukawaRunning.lean) | **The top-Yukawa running sector of the Higgs quartic** (`Higgs.md` §5a). `λ(v)≈0.13` from the SOC boundary `λ=β_λ=0` at the substrate UV floor (Shaposhnikov–Wetterich; floor by construction, `cascade_has_floor`/`QLF_PlanckScale`) run down with SM RGEs. `higgs_v_ratio_sq` (`(M_H/v)²=2λ`), `top_mass_sq_from_yukawa`, `beta_lambda_top_drives_down` (top term `−6y_t⁴<0`), `soc_balances_top_and_gauge`; `top_mass_sq_at_yukawa_one` (`y_t≈1⟹m_t=v/√2≈174 GeV`) via QCD IR fixed point `qcd_fixed_point_balances`; `higgs_eq_four_lam_top` (`M_H²=4λ·m_t²`). EW sector = one scale `v` (top `⟨t̄t⟩` condensate → composite Higgs, ⟺ no hierarchy problem). `higgs_running_demo.py` confirms near-criticality. **Honest scope:** discharged to {SOC boundary + `m_t` + two-loop}; RGE run is the demo, not Lean (`top_yukawa_running_in_progress`). Reuses `QLF_RunningCouplings`. See `Higgs.md` §5a | `higgs_v_ratio_sq`, `top_mass_sq_from_yukawa`, `beta_lambda_top_drives_down`, `soc_balances_top_and_gauge`, `top_mass_sq_at_yukawa_one`, `qcd_fixed_point_balances`, `higgs_eq_four_lam_top`, `top_yukawa_running_in_progress` |
| [QLF_ClosureBinding.lean](QLF_ClosureBinding.lean) | **How closures bind — the structure of the substrate four-fermion interaction** (`Higgs.md` §5a). Two closures bind = their joint history is a shared closure. Reuse-only: `antiparticle_channel_binds` (fermion–antifermion always binds, `dagger_closes` — the `t̄t` channel); `condensate_is_scalar` (folds to real `{±I}` = the scalar `⟨t̄t⟩` composite Higgs, `dagger_closure_folds_real`); `identical_channel_blocked` (like-charge `tt` Pauli-blocked, `diproton_pauli_blocked`); `distinguishable_channel_binds` (`opposite_spin_singlet_closes`); `binding_quantum` (each binding costs `log 2`, `binary_kl_delta_uniform`). Channel, sign, quantum are substrate facts. **Honest scope:** structure formalized; the coupling magnitude `g` (NJL critical `g_crit=1`) is the residual (`higgs_turbulence_in_progress`). Reuses `QLF_QuantumTurbulence`+`QLF_Fusion`+`QLF_FreeEnergy`+`PauliExclusion`. See `Higgs.md` §5a | `antiparticle_channel_binds`, `condensate_is_scalar`, `identical_channel_blocked`, `distinguishable_channel_binds`, `binding_quantum` |
| [QLF_PrimeCascadeDecay.lean](QLF_PrimeCascadeDecay.lean) | **Turbulence forces decay — the prime phase-slip + the cascade dump** (`Decay.md`, `Turbulence.md`). Reuse-only skeleton. `prime_slip_is_quarter_turn`/`prime_slip_irreducible` (the `±i` phase-slip agent); decay condition `slip_out_of_balance_ends_closure` (unbalancing slip = a contradiction with no receipt, `contradiction_no_receipt` ⟹ decays) + `stable_structure_is_balanced` (`receipt_is_balanced`); `unlock_releases_log_two`, `collective_dump_positive`; `cascade_bath_highest_first`/`cascade_bath_floored`. **Decay is deterministic, not random** (§1a): the exponential law = ensemble statistics of the prime bath (`QLF_BornProbability`), not local hidden variables. **Honest scope:** structure anchored; dynamics = the demo `prime_cascade_decay.py`; NOT a claim about lab muonium/supernovae. Reuses `QLF_QuantumTurbulence`+`QLF_ContradictionReceipt`+`QLF_FreeEnergy`. See `Decay.md` | `prime_slip_is_quarter_turn`, `prime_slip_irreducible`, `slip_out_of_balance_ends_closure`, `stable_structure_is_balanced`, `unlock_releases_log_two`, `collective_dump_positive`, `cascade_bath_highest_first`, `cascade_bath_floored` |
| [QLF_NeutrinoOscillation.lean](QLF_NeutrinoOscillation.lean) | **Flavor oscillation as a norm-preserving closure precession** (`Beta_Decay_Neutrino_Nature.md` §3, verifies `Decay.md` §2.1). Oscillation = slow phase evolution of the three-axis Majorana closure; flavor eigenstates mixed unitarily (`QLF_PMNS`). `flavor_precession_conserves_number` (`dP/dt = Ω×P` a rotation, `P·(Ω×P)=0` via `dot_cross_self` ⟹ `‖P‖²` conserved); `prime_kick_conserves_number` (the turbulent kick adds to the axis ⟹ conserves neutrino number); `two_flavor_unitarity`/`two_flavor_prob_bounds` (rooted in PMNS `mixing_unitary`); `deltaMSq`/`no_oscillation_iff_degenerate` (`Δm²=1/R_i²−1/R_j²` ⟹ requires nonzero Majorana masses). **Honest scope:** structure verified; angles/absolute `Δm²` (`pmns_in_progress`) + conversion rate open. Reuses `QLF_PMNS`+`QLF_QuantumBlackHole`. See `Beta_Decay_Neutrino_Nature.md` §3, `Decay.md` §2.1 | `flavor_precession_conserves_number`, `dot_cross_self`, `prime_kick_conserves_number`, `two_flavor_unitarity`, `two_flavor_prob_bounds`, `mixing_unitary`, `deltaMSq`, `no_oscillation_iff_degenerate` |
| [QLF_LogicalBang.lean](QLF_LogicalBang.lean) | **The logical bang + nested phases (drawn from the inside)** (`Creation.md` §8a) — a logical origin, time local and multi-directional. Reuse-only: `first_distinction_closes` (the bang = the minimal closure `[+,−]`, `conjugate_pair_closes`); `causal_order_refl/trans/antisymm` (phases = a causal partial order); `causal_order_not_total` (spacelike events exist ⟹ no global time line, black-hole-interior-as-cosmology); `phase_is_future_cone`; `fast_resolves_before_slow`; `cascade_floored_at_every_scale` (fractal emergence). **No heat death** (§8c): `no_terminal_phase` (`w++[+,−]` always deeper), `future_cone_never_empty`, `order_at_every_scale` — entropy is local. **Honest scope:** structural; order→metric stays `order_metric_continuum_limit`. Reuses `ER_EPR_QLF`+`QLF_ReachableEvent`+`QLF_QuantumTurbulence`. See `Creation.md` §8a, [`diagrams/logical_bang.svg`](../diagrams/logical_bang.svg) | `first_distinction_closes`, `causal_order_not_total`, `phase_is_future_cone`, `fast_resolves_before_slow`, `cascade_floored_at_every_scale`, `no_terminal_phase`, `future_cone_never_empty`, `order_at_every_scale` |
| [QLF_QuantumLogic.lean](QLF_QuantumLogic.lean) | **The substrate realizes the minimal quantum logic `MO2` — orthomodular, non-distributive, no bridge axiom** (`Quantum_Logic_Foundations.md` §2). `MO2` (the height-2 lattice `0<{x,x⊥,z,z⊥}<1`) is the smallest genuinely-quantum orthomodular lattice, built concretely and `decide`-verified (6-element `QL`). Atoms `ax`/`az` = x-/z-spin closures, incompatible because their Paulis don't commute (`incompatibility_source` = `su2_comm_zx`). `le_refl/trans/antisymm`; `compl_involutive`, `inf_compl_bot`, `sup_compl_top` (orthocomplemented by the Hermitian conjugate); `orthomodular` (`a≤b ⟹ b=a∨(a⊥∧b)`); `not_distributive` (genuinely quantum). Realized, not analogized. **Honest scope:** minimal `MO2` axiom-free; the general orthomodular≅Hilbert-projection representation (Piron/Solèr) is the Gleason-hard bridge (`QLF_ProperInvolution`+`QLF_Reconstruction`). Reuses `QLF_Spin`. See `Quantum_Logic_Foundations.md` §2 | `incompatibility_source`, `compl_involutive`, `inf_compl_bot`, `sup_compl_top`, `orthomodular`, `not_distributive` |
| [QLF_Casimir.lean](QLF_Casimir.lean) | **The Casimir effect — finite census, `1/a⁴` scaling, accelerated-boundary Unruh tie** (`VacuumEnergy.md` §4.0, `QFT_QLF.md`). Force as a finite difference of closed-mode censuses, not a subtracted infinity. `casimir_vacuum_quantum` (per-mode quantum = finite `log 2`, `binary_kl_delta_uniform`, no divergent `Σ½ℏω`); `casimir_scaling` (`1/a⁴` forced by dimensional analysis — only `ℏ,c,a` available ⟹ pressure exponent `−4`); `accelerated_boundary_is_unruh` — **`rfl`, and labelled so**: `unruh_temperature` *is* that expression and no boundary appears in the statement, so it records the identification and is not evidence for it (the honest label `hawking_is_unruh` carries upstream). The statements that are **not** `rfl`: **`boundary_unruh_zero_iff_inertial`** (a boundary reads a thermal vacuum *exactly when it accelerates*, at no constant velocity however large — Galileo's ship, and the isotropy premise [Inertia.md](../Inertia.md) needs), **`boundary_unruh_linear_in_acceleration`** (exactly linear in `a`, as inertia is), **`static_boundary_no_unruh`** (a static boundary has no bath, so the *static* Casimir force is not thermal in origin — the finite-census argument carries it). `casimir_summary` is now the conjunction of what is proved, not `True := trivial`. (dynamical Casimir on Unruh `T=ℏa/(2πck_B)`, `unruh_temperature`, same `2π` loop phase). **Honest scope:** exact `−π²/240` coefficient + pair-creation rate are named continuum-QFT pieces. Reuses `QLF_HorizonTemperature`+`QLF_FreeEnergy`. See `VacuumEnergy.md` §4.0 | `casimir_vacuum_quantum`, `casimir_scaling`, `accelerated_boundary_is_unruh` |
| [QLF_CondensateGap.lean](QLF_CondensateGap.lean) | **The interacting closure-binding condenses — an NJL gap equation with the census as the loop** (issue #121, `closure_binding.py`). NJL condensation `1 = g·(loop)` with loop = the closure census `gapSum N = Σ_{m=1}^N C(2m,m)/4ᵐ` (`censusWeight` = `returnProb1D`), `condenses g N := 1 ≤ g·gapSum N`. Proven (reuse `QLF_CensusBrownian`): `censusWeight_pos`, `gapSum_strictMono`, `condenses_iff_ge_critical` (`⟺ g ≥ criticalCoupling N = 1/gapSum N`), `criticalCoupling_antitone`, `condenses_mono`. Since `gapSum` diverges (`~2√(N/π)`), `g_crit→0` at the floor ⟹ **condensation is generic** (`v≪M_Pl` by discreteness, matching `QLF_AlphaS`). **Honest scope:** settles *does it condense?* (yes); the open number (#121) is now one coupling `g = log2 × channel × packing factor` (packing not derived). Reuses `QLF_CensusBrownian`. See `Higgs.md` §5a, issue #121 | `censusWeight`, `censusWeight_pos`, `gapSum_strictMono`, `condenses_iff_ge_critical`, `criticalCoupling_antitone`, `condenses_mono`, `gapSum` |
| [QLF_HolographicDensity.lean](QLF_HolographicDensity.lean) | **Naming η and quantifying the Bekenstein–Hawking residual exactly** (`Gravity_From_Delay.md` §9). Reconciles `S_QLF = 4πR² log 2` vs. the Jacobson/BH `η = 1/4G`, `S_BH = N/4`. `bekensteinHawkingEntropy`; `holographic_bh_ratio` (`S_QLF/S_BH = 4·log 2 ≈ 2.7726` exactly); `residual_is_quarter_times_quantum` (`4 log 2 = 4 × per_event_entropy`, not free); `eta_eq_quarter_inv_G`. The `1/r²` law + structural `G` are residual-independent. **`no_rational_packing_factor`** — the **packing branch is closed**: a correlation factor making a fraction `p/q` of patches independent would force `log 2 = q/(4p)`, i.e. rational, and the required `1/(4 log 2) ≈ 0.360674` is irrational (near misses bracket without touching — `C(2n,n)/4ⁿ` gives `0.375` at `n=2` and `0.3125` at `n=3`; `1/e` is 2.0% off). **`suppression_cancels_the_quantum`** — `(N log 2)·(1/(4 log 2)) = N/4` contains **no `log 2` at all**, so the realized horizon entropy is not (a count) × (the per-event quantum), which puts the remaining weight on the **area-element** reading rather than a discrete-floor deviation. **Honest scope:** open — why realized entropy is `N/4` not `N log 2` (now a *two-way* classification, not three), + absolute SI `G`. Reuses `QLF_GravityFromDelay`+`QLF_EinsteinEquations`. See `Gravity_From_Delay.md` §9 | `bekensteinHawkingEntropy`, `holographic_bh_ratio`, `residual_is_quarter_times_quantum`, `eta_eq_quarter_inv_G`, `no_rational_packing_factor`, `suppression_cancels_the_quantum`, `holographic_density_summary` |
| [QLF_GravitationalCoupling.lean](QLF_GravitationalCoupling.lean) | **The strength of gravity `α_G = exp(−28π)` from the `14π` hierarchy** (`Gravity_From_Delay.md`). The dimensionless coupling `α_G = G m_p²/ℏc = (m_p/M_Pl)² ≈ 5.9×10⁻³⁹`; since `ln(M_Pl/m_p)=14π` (`QLF_AlphaS`, from `b₀=7`), `α_G = exp(−28π)`. `alpha_G_is_ratio_sq`, `alpha_G_eq_exp_neg_28pi`, `substrate_gravitational_coupling`; `exp(−28π)` vs measured `5.91×10⁻³⁹` = 0.068% on the log. `alpha_G_bracket`; `em_gravity_coupling_ratio` (`α/α_G = exp(28π)/137`). **Honest scope:** dimensionless coupling derived; absolute SI `G` needs `m_p`'s kg value. Reuses `QLF_AlphaS`. See `Gravity_From_Delay.md` | `alpha_G_is_ratio_sq`, `alpha_G_eq_exp_neg_28pi`, `substrate_gravitational_coupling`, `alpha_G_bracket`, `em_gravity_coupling_ratio` |
| [QLF_VacuumPolarization.lean](QLF_VacuumPolarization.lean) | **The one-loop QED running coefficient `2/(3π)` from the census** (#117). Two-vertex split census `Σ k(n−k)=C(n+1,3)` (`census_split`) → `1/6` (`splitRiemannSum_eq`, exact `=1/6−1/(6n²)`; `splitRiemannSum_tendsto`), Wallis `1/π`, `qedVacPolCoeff=2/(3π)` (`qedVacPolCoeff_eq`), `b=−4/3` (`qed_beta_coeff_per_fermion`). Value-free, committed before comparison. Reuses `QLF_PhysicalPi`+`QLF_RunningCouplings`. See `Alpha.md` §4a | `census_split`, `splitRiemannSum_eq`, `splitRiemannSum_tendsto`, `qedVacPolCoeff_eq`, `qed_beta_coeff_per_fermion` |
| [QLF_VacuumPolarizationTower.lean](QLF_VacuumPolarizationTower.lean) | **The horizon→scale tower — the running *function* from the census** (#117). `perOctaveIncrement` (`perOctave_is_flux`), horizon map `Q(R)=Q₀·2^R` ⟹ the QED logarithm IS the census octave count. Extends `QLF_VacuumPolarization`. See `Alpha.md` §4a | `perOctaveIncrement`, `perOctave_is_flux` |
| [QLF_ChargeCensus.lean](QLF_ChargeCensus.lean) | **The charge census `Σ Nᶜ Q_f² = 8 = 2³`** (#117). `censusWeight`, `leptonCensus=1`/`upCensus=4/3`/`downCensus=1/3`, `totalChargeCensus_eq_eight`/`_two_cubed`, leptonic 3 + hadronic 5 (`leptonicCensus_eq_three`/`hadronicCensus_eq_five`) — the running weight = the 8-twist alphabet size. See `Alpha.md` §4a | `censusWeight`, `totalChargeCensus_eq_eight`, `leptonicCensus_eq_three`, `hadronicCensus_eq_five` |
| [QLF_ChargeBalance.lean](QLF_ChargeBalance.lean) | **Anomaly cancellation as a ZFA charge-balance `Σ Q = 0` per generation.** `gen_electric_neutral`, `genPositiveCharge_eq_two`, `genNegativeCharge_eq_neg_two`, `gen_charge_balanced` — the signed sum complementing `QLF_ChargeCensus`. See `Standard_Model.md` | `gen_electric_neutral`, `genPositiveCharge_eq_two`, `genNegativeCharge_eq_neg_two`, `gen_charge_balanced` Also carries **electron capture** ([Quarks.md](../Quarks.md) §4a, [Weak_Force.md](../Weak_Force.md) §4b): `up_to_down_one_charge_unit` (`q_d − q_u = −1`, exactly the electron's — but *not* uniqueness, which is why muon capture is the same vertex), `local_capture_charge_conserved` (the vertex, `−1/3` both sides) beside `electron_capture_charge_balanced` (the global reaction, `0` both sides, each side separately neutral), `capture_flips_exactly_one` (one edge moves, not two), and `capture_changes_exactly_one_slot` over three colour slots `Ax → Flavour` — where every axis staying occupied is true *by construction of the representation*, and what is proved is that the flip moves one slot and leaves the other two literally equal. Plus `electron_capture_factors_through_wminus`: there is **exactly one** mediator charge making both vertices work, computed independently from each side and agreeing at `−1`, which is the `W`-as-operation/`W`-as-particle resolution of [Weak_Force.md](../Weak_Force.md) §4c. These establish capture is **allowed by the invariants**; they say nothing about the rate |
| [QLF_AnomalyCancellation.lean](QLF_AnomalyCancellation.lean) | **Gauge consistency as a ZFA ledger-balance — every anomaly cancels.** Hypercharges from `Q=T₃+Y` (`Y_Q_from_Q_T3`, `Y_L_from_Q_T3`); `grav_anomaly_zero`, `cubic_anomaly_zero` — the SM anomaly miracle as charge-balance. See `Standard_Model.md` | `Y_Q_from_Q_T3`, `Y_L_from_Q_T3`, `grav_anomaly_zero`, `cubic_anomaly_zero` |
| [QLF_ElectroweakBeta.lean](QLF_ElectroweakBeta.lean) | **The three one-loop β-coefficients from the substrate counts.** Extends `QLF_BetaFunction`'s `b₀=7` to the full SM: `b3_eq`, `b2_eq`, `b1_eq` (hypercharge `weylY2_eq`, `hyperSqPerGen_eq`). See `Standard_Model.md` | `b3_eq`, `b2_eq`, `b1_eq`, `weylY2_eq`, `hyperSqPerGen_eq` |
| [QLF_GUTScale.lean](QLF_GUTScale.lean) | **The unification scale — structure derived, absolute value scale-bound.** With the three β's (`QLF_ElectroweakBeta`) + `sin²θ_W=3/8` (`QLF_WeinbergAngle`): `couplings_meet_at`, `b1_minus_b2_val`, `b1_gt_b2`, `gut_scale_from_gap`. Absolute `M_GUT` scale-bound. See `Standard_Model.md` | `couplings_meet_at`, `b1_minus_b2_val`, `b1_gt_b2`, `gut_scale_from_gap` |
| [QLF_BindingStrength.lean](QLF_BindingStrength.lean) | **The gravitational floor + the `g`-decomposition, localizing frontier #1** (#121). `g=(log2)·channel·packing`; `gravBinding_kibble_sciama`, `gravBinding_subcritical` (gravity `g≈0.1–0.4`), `binding_quantum_is_log_two`, `binding_must_supply_rest`. See `Higgs.md` §5a | `gravBinding_kibble_sciama`, `gravBinding_subcritical`, `binding_quantum_is_log_two`, `binding_must_supply_rest` |
| [QLF_PackingFactor.lean](QLF_PackingFactor.lean) | **Modeling the packing factor from the 8-twist combinatorics (the diagnostic, #121).** `bare_packing_subcritical`, `condensationDepth_pos`/`_antitone`; the irreducible piece of `g`, not derived (`packing_factor_in_progress`). See `Higgs.md` §5a | `bare_packing_subcritical`, `condensationDepth_pos`, `packing_factor_in_progress` |
| [QLF_ClosureAttraction.lean](QLF_ClosureAttraction.lean) | **"Gauge folds attract" as a theorem — binding reduces free action** (frontier #1, #121). `count_pos_append`/`count_neg_append`/`netGauge_append`, `freeAction_nonneg` — the shared-closure / free-action-reduction binding rule. See `Higgs.md` §5a | `count_pos_append`, `count_neg_append`, `netGauge_append`, `freeAction_nonneg` |
| [QLF_SteadyStateDensity.lean](QLF_SteadyStateDensity.lean) | **The equilibrium defect density `ρ*` — the interaction supplies the restoring force** (frontier #1, #121). `no_steady_without_binding`, `steady_is_fixed_point`, `steady_pos`, `netRate_strictly_decreasing` — the rate-equation fixed point setting the electroweak scale. See `Higgs.md` §5a | `no_steady_without_binding`, `steady_is_fixed_point`, `steady_pos`, `netRate_strictly_decreasing` |
| [QLF_MO2.lean](QLF_MO2.lean) | **The minimal quantum logic `MO2`, self-contained** (Mathlib-only) — a standalone audit of `QLF_QuantumLogic`'s signature result: `le_refl`/`le_trans`/`le_antisymm`, `compl_involutive`, orthomodular, non-distributive. See `Quantum_Logic_Foundations.md` §2 | `le_refl`, `le_trans`, `le_antisymm`, `compl_involutive` |
| [QLF_ElectroweakScale.lean](QLF_ElectroweakScale.lean) | **Closing the loop `ρ* → packing → g → R_stable`** (frontier #1, #121). `g_eq_binding_quantum`, `RStable_eq`, `RStable_pos`; reduces the EW scale to one SOC observable `ρ*` (`electroweak_scale_in_progress`). See `Higgs.md` §5a | `g_eq_binding_quantum`, `RStable_eq`, `RStable_pos`, `electroweak_scale_in_progress` |
| [QLF_FractalDiagram.lean](QLF_FractalDiagram.lean) | **Closure-as-Feynman-diagram — the inductive correspondence, formalized** (#138). `IsDiagram : TopoString → ℕ → Prop` (base/binding/nesting); `diagram_is_closure` (every diagram is a genuine ZFA closure); **C1** `order_zero_iff_closure` (order-0 diagrams = the closure census, the `α⁻¹` leading structure); **C2** `orderOneWeight_eq` (order-1 weight IS the `2/(3π)` one-loop coefficient) + `orderOne_tower_slope` (`16/(3π)` charge-census slope). The depth-≥3 tail (the `0.036`) stays the frontier-#1 + SM-hadronic residual. Reuses `QLF_VacuumPolarization`+`QLF_ChargeCensus`. See `Frequency_Synchronization.md` §0a | `diagram_is_closure`, `order_zero_iff_closure`, `orderOneWeight_eq`, `orderOne_tower_slope` |
| [QLF_MassGapDispersion.lean](QLF_MassGapDispersion.lean) | **The Yang–Mills mass gap as the dispersion gap of the propagation operator** — bridges `QLF_GravitationalWaves`+`QLF_MassGap`. Discrete Klein–Gordon `boxKG = □_d + m²`: massless (m=0) = `boxD` (`massless_gapless`); massive leaves `m²δρ` (`massive_residual`). Dispersion `ω²=k²+m²` ⟹ rest gap = m at k=0; gauge fold `m = gaugeMassGap = log 2 > 0` (`mass_gap_is_dispersion_gap`). **Honest scope:** a bridge/reframing, not a Clay advance (`yang_mills_continuum_gap` unchanged). No new axioms. See `YangMills_MassGap_QLF.md` | `massless_gapless`, `massive_residual`, `mass_gap_is_dispersion_gap` |
| [QLF_SpinorInformation.lean](QLF_SpinorInformation.lean) | **Spin-½ is the atom of information (after Cartan 1913)** — bridges `QLF_Spin`+`QLF_FreeEnergy` ([Mathematics_From_QLF.md](../Mathematics_From_QLF.md) §Rung 5a). Reading **information = log(number of distinguishable fold outcomes)**: the two-valued **spinor** fold-alphabet `{+I,−I}` (both realized: `spinor_fold_negI`, `vector_fold_id`; distinct by `spin_double_cover_nontrivial`) carries **one bit** — `binary_kl 1 (1/2) = log 2` (`two_valued_one_bit`); a single-valued **vector** alphabet `{+I}` carries **zero** — `binary_kl 1 1 = 0` (`single_valued_zero_information`, the formal content of "one-valued objects can't express information"). **`spin_half_is_information_atom`**: `0 < log 2`, so the jump from no-information to one bit happens exactly when the `−I` double-cover sign (Cartan's double-valued spinor element) is admitted. **Cited classical foundation:** Cartan (1913), *Les groupes projectifs…* — spinor irreps are the non-tensorial ones; the vector rep factors through `SO(3)` and is blind to `π₁(SO(3))=ℤ₂`. **§3 reproves the double-valuedness from explicit rotation matrices** (not cited): a `2π` turn is `+I` on the vector `SO(3)` rep (`vectorRotZ_two_pi = I₃`, via `Real.cos_two_pi`) but `−I` on the spin-½ `SU(2)` rep (`spinorRotZ_two_pi = −I`, via `Complex.exp_pi_mul_I`) — `spinor_double_valued_vector_blind`. **Honest scope:** QLF realizes the concrete `su(2)` instance + the double-cover + the information content; Cartan retained only for the *general* classification (all non-tensorial irreps). No new axioms | `spinor_fold_negI`, `vector_fold_id`, `fold_alphabet_two_valued`, `single_valued_zero_information`, `two_valued_one_bit`, `spin_half_is_information_atom`, `spinorRotZ`, `vectorRotZ`, `spinorRotZ_two_pi`, `vectorRotZ_two_pi`, `spinor_double_valued_vector_blind` |
| [QLF_CensusCurvature.lean](QLF_CensusCurvature.lean) | **The possibility graph is triangle-free, hence nowhere positively curved** — the structural reason behind the *measured* hyperbolicity of the census graph ([Curvature.md](../Curvature.md) §1c; `lepton_blind_classifier.py` §K, every one of 162 interior edges `κ < 0`), valid at **every** length where the measurement is bounded by truncation. Proven with no axiom: the causal parent relation deletes exactly two twists (`isParent_length`), so adjacency changes the length by exactly 2 (`adj_length`), so the graph is **layered** — `length % 4` flips across every edge (`census_bipartite`) — and irreflexive (`adj_irrefl`); hence **no triangles** (`census_triangle_free`), since three mutual neighbours would need three lengths pairwise differing by 2 and no three naturals do. Also proven: the parent relation **preserves count balance** (`countBalanced_of_isParent`, via `isParent_count` + the 64-case `conj_pair_counts`), so the census really is a graph *on* ZFA closures. **One cited bridge** (`jost_liu_triangle_free`, Jost & Liu 2014 — triangle-free ⟹ `κ ≤ 0`; named because Mathlib carries no discrete optimal transport, `ollivierRicci` opaque) turns that into **`census_nowhere_positively_curved`**, a theorem. **Honest scope:** strict negativity does *not* follow from triangle-freeness and stays numerical | `IsParent`, `isParent_length`, `isParent_count`, `conj_pair_counts`, `countBalanced_of_isParent`, `Adj`, `adj_length`, `census_bipartite`, `adj_irrefl`, `census_triangle_free`, `census_no_triangles`, `census_nowhere_positively_curved`, `census_curvature_summary` |
| [QLF_NullTensorReconstruction.lean](QLF_NullTensorReconstruction.lean) | **Nine integer null probes reconstruct the metric multiple** — the algebraic rung of Jacobson (1995) eqs. (5)→(6) toward the full field equations ([Einstein_Equations.md](../Einstein_Equations.md) §6b). Jacobson's horizon relation gives `S_ab k^a k^b = 0` for null `k` (`S := R_ab − κT_ab`); the textbook step to `S_ab = f g_ab` quantifies over the **continuum** of null directions. QLF needs **nine**, and all nine are **integer points of the substrate Hermitian lattice** (`QLF_Minkowski`, `det X ∈ ℤ`): `(1,±1,0,0)`, `(1,0,±1,0)`, `(1,0,0,±1)`, `(5,3,4,0)`, `(5,3,0,4)`, `(5,0,3,4)` — null because `1²=1²` and `5²=3²+4²`, so no square root and no completed continuum is needed to name them (the *unneeded* strike of [TheContinuum.md](../TheContinuum.md) §2). **`finite_null_probes_force_metric`**: the six axis probes kill the time–space components and pin the spatial diagonal to `−S.tt`; the three `3-4-5` probes collapse (`25−9−16=0`) to `24 S.xy = 0`, killing the spatial off-diagonals ⟹ `S = S.tt·diag(1,−1,−1,−1)`. **`contract_metricMultiple`** gives the converse (`contract = f · interval`, so a metric multiple annihilates the *whole* cone), and the two assemble into **`null_annihilator_iff_metric_multiple`** — the null-cone annihilators are **exactly** the metric multiples (one-dimensional, spanned by `g`), membership decided by nine lattice points. **`axis_probes_insufficient`** proves the nine are sharp (the pure-`xy` witness passes all six axis probes and is no metric multiple). No new axioms. **Honest scope:** this is the algebraic rung only — `SymTensor4` is ten reals, nothing ties them to a curvature tensor; the arrow *in* (local Rindler + Raychaudhuri focusing) and *out* (contracted Bianchi ⟹ `f = −R/2 + Λ`) remain `einstein_equations_in_progress` | `SymTensor4`, `contract`, `IsNull`, `metricMultiple`, `finite_null_probes_force_metric`, `contract_metricMultiple`, `metricMultiple_annihilates_null`, `null_annihilator_iff_metric_multiple`, `all_null_projections_force_metric`, `axis_probes_insufficient`, `null_tensor_reconstruction_complete` |
| [QLF_BianchiClosure.lean](QLF_BianchiClosure.lean) | **The third Jacobson arrow: contracted Bianchi closes the field equations** ([Einstein_Equations.md](../Einstein_Equations.md) §6c). From the metric form `R_ab = κT_ab + f g_ab` (delivered by [QLF_NullTensorReconstruction](QLF_NullTensorReconstruction.lean), chained here by **`metric_form_from_null_probes`**), taking the divergence kills the matter term by conservation, metric compatibility gives `∇^a(f g_ab) = ∂_b f`, and contracted Bianchi `∇^a R_ab = ½∂_b R` forces `∂_b(f − R/2) = 0` — so **`scalar_multiple_is_curvature`**: `f = R/2 − Λ` with `Λ` a **constant** (connectedness), and **`einstein_field_equations`**: `G_ab + Λ g_ab = κ T_ab`, with `κ = 8πG` from `einstein_coupling_from_thermodynamics` and `Λ = Ω_Λ = log 2` fixed independently. **Zero new axioms** — the differential-geometry boundary is the **`DivergenceCalculus` structure** (div/grad plus additivity, homogeneity, metric compatibility, gradient linearity, and vanishing-gradient ⟹ constant), taken as a hypothesis in every signature, so a future construction discharges it by *building an instance* rather than deleting an axiom; the two physics inputs (contracted Bianchi, conservation) are likewise explicit hypotheses. Also supplies the componentwise `SymTensor4` algebra (add/neg/sub/smul + 40 projection simp lemmas) and `trace`/`einsteinTensor`. **Honest scope:** the calculus is an interface, not a construction, so the equations are conditional on it; and the **first** arrow (`δQ = TδS ⟹ S_ab k^a k^b = 0`, local Rindler + Raychaudhuri) is untouched and now the single remaining substrate question | `DivergenceCalculus`, `trace`, `trace_metricMultiple`, `metricMultiple_add`, `metricMultiple_neg`, `scalarCurv`, `einsteinTensor`, `scalar_multiple_is_curvature`, `einstein_field_equations`, `metric_form_from_null_probes`, `bianchi_closure_complete` |
| [QLF_ClosureDepth.lean](QLF_ClosureDepth.lean) | **How many ways a history closes at each depth — and `log 2` counted rather than defined** ([Entropy.md](../Entropy.md) §1b, [Philosophy.md](../Philosophy.md) §3a). Grades the census by pruning depth (`QLF_HorizonClosure`'s `boundedPrune`) and **counts the ways at each grade**, the method's rule that an existence witness is only a lower bound on multiplicity. **Depth-1 stratum:** `zeno_prune s = [] ↔ s` is a concatenation of adjacent opposite pairs (**`onePass_closed_iff_pairMatching`**, both directions, no axiom; forward by structural recursion — anything else leaves its head behind), so **`onePass_ways_iff`** identifies the one-pass closures of length `2n` with the boolean words of length `n`: **`2ⁿ` ways, two per pair, independently**, distinct by **`pairMatching_injective`**. Hence **`onePass_entropy`**: `log(2ⁿ) = n·log 2` — **`log 2` per closure pair because a pair closes in exactly two ways**, the one route where the framework's `log 2` quantum is *counted* rather than posited (contrast `ΔF = −log 2`, `Ω_Λ = log 2`, the area law, Immirzi — all re-exports of the same atom). **Deepest stratum:** `poss`/`negs` blocks with **`prune_negs`** (a like-phase block is prune-fixed) and **`prune_wedge`** (one pass peels exactly one shell off `[+^{a+1}−^{b+1}]`) give **`zeno_prune_nested`**, **`boundedPrune_nested`** (`boundedPrune k [+^d−^d] = [+^{d−k}−^{d−k}]`), hence **`nested_closed_at_d`** and **`nested_not_closed_before`** — the depth-`d` fold needs exactly `d` passes, generalizing `horizon_relative` from `d=2` to all `d`, and only two histories reach that depth. **Also defines** the phase walk `imb`/`exc`/`maxExcursion` with **`maxExcursion_pairMatching`** (pair matchings have maximum excess exactly 1). **The closed-form depth law is now proven** in [QLF_ClosureDepthLaw](QLF_ClosureDepthLaw.lean) (`closure_depth_law_proven` points there): `closureDepth = maxExcursion`, the maximum excess of the phase walk — so a capacity-`R` horizon closes exactly the histories staying within `R` of balance, and census depth is the maximum of a `±1` bridge (`E ~ √(πn/2)`), i.e. capacity `R` closes length `~R²`, polynomial rather than exponential. The `d=1` case (`maxExcursion_pairMatching`) is proven here; the per-pass lemma that discharges the general case is `per_pass` there. The exhaustive check (0 counterexamples over all 66,196 balanced histories of length ≤ 18) is now a theorem | `imb`, `exc`, `maxExcursion`, `pairOf`, `pairMatching`, `pairMatching_closes`, `exists_pairMatching_of_closes`, `onePass_closed_iff_pairMatching`, `pairMatching_length`, `pairMatching_injective`, `onePass_ways_iff`, `ways_card`, `onePass_entropy`, `maxExcursion_pairMatching`, `poss`, `negs`, `nested`, `zeno_prune_nested`, `boundedPrune_nested`, `nested_closed_at_d`, `nested_not_closed_before`, `closure_depth_law_proven` |
| [QLF_LawOfExceptions.lean](QLF_LawOfExceptions.lean) | **The Law of Exceptions, proven: a system with more states can always break a finite closure** ([Law_Of_Exceptions.md](../Law_Of_Exceptions.md); [Philosophy.md](../Philosophy.md) §3b). *"There is an exception to every restrictive law except this law"* — the aphorism is late-16th-century folklore; the theorem is not, and self-reference supplies no proof (consistency of "every law but me has an exception" entails nothing about any particular law, and the set version `A_L ⊊ H ⟹ ∃h ∉ A_L` is a tautology, hence bookkeeping by §3a rule 3). Modelling a restrictive law as what it is on the substrate — a **finite closure** `closedAtHorizon R` ([QLF_HorizonClosure](QLF_HorizonClosure.lean)), the observer as a finite-information region ([QLF_Realizability](QLF_Realizability.lean)) — the missing premise is proven with **no axiom**: **`law_of_exceptions`** gives every capacity `R` a **constructed** exception `[+^{R+1} −^{R+1}]`, not admitted at `R` (**`exceptionTo_not_closed`**) yet **genuinely closing at `R+1`** (**`exceptionTo_is_real`** — the load-bearing half: the exception is real, merely deeper than the law can see); **`closure_hierarchy_strict`** shows more capacity admits strictly more, so **`no_final_closure`** — no finite closure is final; **`no_finite_closure_is_exceptionless`** is the sharp kill condition; and **`no_exception_to_unbounded_closure`** shows every such exception is admitted at *some* capacity, so nothing is an exception to ZFA itself — ZFA bounds no capacity (selection, not restriction), which is why it is the one exceptionless law. Reuses `nested_closed_at_d` / `nested_not_closed_before` from [QLF_ClosureDepth](QLF_ClosureDepth.lean). **Why laws look exceptionless:** exceptions are the least-multiplicity histories (2 ways at maximal depth against `2ⁿ` at depth 1), so the most ways happen first and the exception happens last. **Honest scope:** the modelling step — that a restrictive law *is* a finite closure — is the formulation, not a further theorem; the methodological corollary is that **construction proves possibility, not uniqueness** | `exceptionTo`, `exceptionTo_not_closed`, `exceptionTo_is_real`, `law_of_exceptions`, `closure_hierarchy_strict`, `no_final_closure`, `no_exception_to_unbounded_closure`, `no_finite_closure_is_exceptionless`, `law_of_exceptions_summary` |
| [QLF_ClosureDepthLaw.lean](QLF_ClosureDepthLaw.lean) | **The depth law, closed: closure depth IS the maximum phase excess.** Proves the step [QLF_ClosureDepth](QLF_ClosureDepth.lean) left open, giving **`closedAtHorizon_iff_maxExcursion_le`** — for a gauge-free count-balanced history, `boundedPrune R s = []` **iff** `maxExcursion s ≤ R`: a finite-capacity horizon closes exactly the histories whose phase walk **never strays further than `R` from balance**, so **capacity bounds excursion, not length** (capacity `R` buys length `~R²`, a balanced walk's mean maximum being `√(πn/2)` — polynomial, not exponential). **Why generalization was required:** the naive per-pass claim fails over an accumulator (the max can sit at the boundary — `exc 5 [−,+] = 5 = exc 5 []`) and is false outright with gauge elements (`[+, gauge, −]` is prune-fixed, since `zeno_prune` cancels only *adjacent* opposite phases), so both `NoGauge` and `level s = 0` are necessary. What generalizes is the **signed** height with an arbitrary accumulator, **`hmax_zeno_prune`**: `hmax c (zeno_prune s) = max (hmax c s − 1) (max c (c + level s))` — valid for **unbalanced** `s` too, exactly what the emit step needs since it hands the recursion an unbalanced tail; the boundary term is what the naive statement was missing. Mathematically it encodes that greedy leftmost cancellation removes **every** attainment of the extreme level (an attainment at `M` is a peak `(+,−)` that could only be skipped by being the second element of an earlier pair, forcing level `M+1`). Then **`zeno_prune_flip`** (pruning commutes with `+↔−`, so the negative extreme needs no separate argument), **`exc_eq_hmax`** (the `|walk|`-max splits into the two signed heights), **`per_pass`** (one pass drops the excess by exactly one), **`maxExcursion_boundedPrune`**, and **`closureDepth_eq_maxExcursion`** (the exact pass count). **`maxExcursion_nested`** now *derives* the nested-fold witnesses of [QLF_ClosureDepth](QLF_ClosureDepth.lean) / [QLF_LawOfExceptions](QLF_LawOfExceptions.lean). No axioms — the 0/66,196 exhaustive check is now a theorem | `level`, `hmax`, `flipEl`, `flip`, `NoGauge`, `hmax_ge`, `hmax_pos_cons`, `hmax_zeno_prune`, `level_flip`, `noGauge_flip`, `zeno_prune_flip`, `exc_eq_hmax`, `maxExcursion_eq_hmax`, `level_zeno_prune`, `noGauge_zeno_prune`, `level_boundedPrune`, `noGauge_boundedPrune`, `maxExcursion_pos`, `per_pass`, `maxExcursion_boundedPrune`, `closedAtHorizon_iff_maxExcursion_le`, `closureDepth_eq_maxExcursion`, `maxExcursion_nested`, `closure_depth_law_complete` |
| [QLF_LineSpectra.lean](QLF_LineSpectra.lean) | **In what sense line spectra are multiplicity spectra** — proves the provable part of the claim in [Law_Of_Exceptions.md](../Law_Of_Exceptions.md) §4c and refuses the rest. **(1) Why there are lines at all, and it is *capacity* that does it:** integer periods alone give no discrete spectrum (over an unbounded census the differences `1/a − 1/b` accumulate arbitrarily finely), but a finite capacity admits only periods `≤ R` ([QLF_ClosureDepthLaw](QLF_ClosureDepthLaw.lean)), hence a finite line list — **`lines_card_le`** (`≤ R²`) — which **grows with capacity** (**`lines_mono`**), the spectroscopic face of the capacity ladder; plus **`freq_injective`** (distinct periods ⟹ distinct frequencies, so the spectrum labels the closures) and **`lineFreq_pos`**. **(2) Level weights are genuine counts:** **`orientations_card`** proves the statistical weight is the *cardinality* of the orientation set `{−ℓ … ℓ}`, `= orbitalDim ℓ = 2ℓ+1` — a multiplicity, not an arithmetic formula that happens to match one. **(3) Summed intensities stand in the ratio of those counts:** the **Burger–Dorgelo–Ornstein sum rules** (1924–25; Condon & Shortley) enter as an **`IntensityModel` interface** rather than an axiom (the `DivergenceCalculus` discipline — an *observed* regularity, visible in every signature that uses it), and from it **`intensity_ratio_is_multiplicity_ratio`** / **`intensity_ratio_eq_weight_ratio`** follow with the proportionality constant cancelling, plus **`intensity_pos`**. **Honest scope:** individual line strengths are **not** way-counts here — oscillator strengths and dipole matrix elements are not derived, and the sum rules constrain only sums over a common level; the stronger reading needs the multiplicity ↔ Born-norm bridge listed open in [Information_Physics.md](../Information_Physics.md) §6. No axioms | `periods`, `lines`, `lineFreq`, `lines_card_le`, `lines_mono`, `freq_injective`, `lineFreq_pos`, `orientations`, `orientations_card`, `IntensityModel`, `intensity_ratio_is_multiplicity_ratio`, `intensity_ratio_eq_weight_ratio`, `intensity_pos`, `line_spectra_multiplicity_summary` |
| [QLF_BornCounting.lean](QLF_BornCounting.lean) | **Reducing the multiplicity ↔ Born-norm bridge** ([Born_Rule.md](../Born_Rule.md) §4, [Information_Physics.md](../Information_Physics.md) §6) — two halves, unequally hard. **Half one, CLOSED — why the square.** A realized event is a *closed Hermitian pair*, ket **and** bra (`bra_ket_always_balanced`), both required and independently chosen, so its way-count is the **product** of the legs'; the bra being the dagger of the ket, the factors are `a` and `star a` — **`pairCount_eq_leg_times_dagger`**, exactly the norm `bornProb` uses (**`pairCount_eq_norm`**), hence **`born_is_pair_count_ratio`**: the Born measure *is* the normalized count of ways the event closes. The exponent counts the two legs rather than being postulated. **Independently:** a count is a cardinality and `|1+i| = √2` is irrational (**`modulus_not_a_count`**, via `irrational_sqrt_two`) while `pairCount (1+i) = 2` — in `ℤ[i]` the norm is the only integer invariant, so integrality alone forces the square. **Existence is all-or-nothing:** `pairCount` is a whole number of ways (**`pairCount_is_a_whole_count`**), so a single realization gets `1` when the branch takes every way (**`bornProb_eq_one_iff`**) and `0` when it takes none (**`bornProb_eq_zero_iff`**) — every intermediate value is a *ratio of counts of binary events*, never partial existence. **Half two, REDUCED not closed:** both counts are multiplicative (**`pairCount_mul`**, Brahmagupta–Fibonacci; `independent_join_multiplies`), so **`count_determined_by_generators`** localizes the open step to **agreement on the primitive closures** — a finite check per generator, the same shape as completely-additive functions being free on the primes. **Untouched:** uniqueness of the norm-square form against Gleason / envariance / decision-theoretic derivations. **The Born rule is not derived here.** No axioms | `pairCount`, `pairCount_eq_norm`, `pairCount_eq_leg_times_dagger`, `pairCount_nonneg`, `pairCount_mul`, `pairCount_one`, `onePlusI`, `pairCount_onePlusI`, `modulus_not_a_count`, `born_is_pair_count_ratio`, `bornProb_eq_zero_iff`, `bornProb_eq_one_iff`, `pairCount_is_a_whole_count`, `count_determined_by_generators`, `born_counting_summary` |
| [QLF_Degeneracy.lean](QLF_Degeneracy.lean) | **What fixes the degeneracy decomposition: one μ₄ phase per way** — closes the residue [QLF_BornCounting](QLF_BornCounting.lean) left, and does it by showing the naive identification was the wrong statement rather than by patching it. Every closed history folds to a **Pauli scalar in `μ₄ = {±1, ±i}`** ([QLF_Pauli](QLF_Pauli.lean), reachable from count balance via `count_balanced_pauli_closed`), so a way is not a bare tally mark: it carries a **unit amplitude with a μ₄ phase** (**`mu4_pairCount_one`**). That fixes the decomposition completely — one unit-norm component per closure, nothing free — so a branch amplitude is the **sum** over its ways (**`branchAmp`**) and its weight that sum's pair count (**`branchWeight`**). Hence **`weight_is_always_a_norm`**: a sum of Gaussian integers is a Gaussian integer, so every branch weight is automatically a `ℤ[i]` norm and the obstruction found by [born_generator_check.py](../born_generator_check.py) (counts such as `3, 38, 70` are not sums of two squares; no two Gaussian integers have norm ratio `3:1`) **never arises — counts are not weights**. The gap between count and weight is exactly **interference**: orthogonal phases give weight = count (**`orthogonal_two_ways`**, `\|1+i\|² = 2` — precisely why the pair generator matched, its two ways being the orderings `+−`/`−+`, and `pair_generator_squared` at `n=2`), aligned phases give `n²` (**`aligned_weight`**, **`three_aligned_ways`**: three ways weigh `9`, not the impossible `3`), opposed phases give `0` (**`cancelling_two_ways`**). **Honest scope:** *which* phase a given way carries is **not** settled here — that is the `pauli_fold` of the specific history, i.e. the interference calculation itself; and Gleason-style uniqueness is untouched. No axioms | `mu4`, `mu4_pairCount_one`, `branchAmp`, `branchWeight`, `weight_is_always_a_norm`, `branchWeight_nonneg`, `orthogonal_two_ways`, `aligned_two_ways`, `cancelling_two_ways`, `aligned_weight`, `three_aligned_ways`, `pair_generator_squared`, `degeneracy_summary` |
| [QLF_PhaseAssignment.lean](QLF_PhaseAssignment.lean) | **Which phase a way carries — and two corrections recorded in place.** The phase is not free: it is the history's `pauli_fold`. **Proven:** both orderings of a conjugate pair fold to `−I` (**`pair_orderings_aligned`**, **`pair_reversed_folds_to_negI`**, via **`conj_conj`** on top of the pre-existing [hermitian_pair_folds_to_negI](QLF_TwistAlphabet.lean)), so within a pair sector the ways are **aligned**; hence a branch of `k` such ways weighs `k²` (**`aligned_ways_weigh_square`**) and the gauge-pair stratum weighs `4ⁿ`, not `2ⁿ` (**`stratum_weight`**). **Correction 1:** [QLF_Degeneracy](QLF_Degeneracy.lean)'s gloss that those two ways are *orthogonal* (`1` and `i`) is false — its arithmetic stands, the identification does not — so the "agreement on the pair generator" in [born_generator_check.py](../born_generator_check.py) compares a **count** with a **norm**, a coincidence rather than evidence about the amplitude. **Correction 2**, on the principle that things happen *every* way: alignment is a **sector** property, not a census property — counting all balanced histories with their folds shows both phases occurring (length 6: `1 488` at `+1`, `3 632` at `−1`, amplitude `−2 144`), so a census-spanning branch is **mixed**, its amplitude the *signed* sum and its weight far below `count²`. Reasoning from two hand-picked ways was the error in both directions. **Verified not proven:** the two-factor phase rule `(−1)^{#neg} · sign(axis permutation)` (0 counterexamples over all 5,296 balanced histories of length ≤ 6). No axioms | `conj_conj`, `pair_orderings_aligned`, `pair_reversed_folds_to_negI`, `aligned_ways_weigh_square`, `stratum_weight`, `phase_assignment_summary` |
| [QLF_BalancedPhaseReal.lean](QLF_BalancedPhaseReal.lean) | **Balance forces a *real* phase: closures fold to `±I`, never `±iI`** — so the phase group on closures is `μ₂`, not the `μ₄` that [count_balanced_pauli_closed](QLF_TwistAlphabet.lean) allows, and the empirical finding (0 imaginary phases across all 5,296 balanced histories ≤ 6 and 80,000 samples at 8–14) becomes **`balanced_phase_is_real`**. **The proof is one determinant computation, and it is order-blind:** every Pauli matrix has `det = −1` and every gauge matrix `det = +1` (**`det_toMatrix`**; in `2×2` negation leaves `det` alone), `det` is multiplicative so `det(fold) = (−1)^{axisLen}` (**`det_fold`**), count balance makes that exponent even — `2(#^ + #> + #/)` — (**`axisLen_even_of_balanced`**, via **`axisLen_eq_counts`**), giving `det(fold) = 1` (**`det_fold_balanced`**), while `±iI` have `det = −1` (**`det_pauliScalar`**). Because `det` cannot see order, one computation settles **every interleaving at once** — no case analysis, no appeal to the normal form. Presented as *a* proof, not *the* proof ([Law_Of_Exceptions.md](../Law_Of_Exceptions.md) §7). **And the law has its exception, exactly outside its hypothesis:** the *unbalanced* `^ > /` folds to `−iI` (**`unbalanced_can_be_imaginary`**, with **`unbalanced_witness_not_balanced`**; 48 such histories at length 3), so balance is load-bearing and the scope is sharp from both sides. **Consequence:** branch amplitudes over the balanced census are signed **integers**, not Gaussian integers — the `μ₄` freedom [QLF_Degeneracy](QLF_Degeneracy.lean) allowed is never exercised on closures, so every branch weight is a perfect square. No axioms | `isAxis`, `axisLen`, `det_toMatrix`, `det_fold`, `axisLen_eq_counts`, `axisLen_even_of_balanced`, `det_fold_balanced`, `det_pauliScalar`, `balanced_phase_is_real`, `unbalanced_can_be_imaginary`, `unbalanced_witness_not_balanced`, `balanced_phase_real_summary` |
| [QLF_PhaseRule.lean](QLF_PhaseRule.lean) | **Which phase a way carries, computed from the word alone — the census's two-factor rule, proven.** `φ(h) = (−1)^{#neg twists} · (−1)^{inversions of the axis word}` was the repo's flagship *verified-but-not-proven* finding (0 counterexamples across **8,134,416** balanced histories, [Experimental_Consistency.md](../Experimental_Consistency.md)), proven previously only in the pair sector where the axis word is constant ([QLF_PhaseAssignment](QLF_PhaseAssignment.lean)). Now a theorem — **`phase_rule`** — and in a **stronger unrestricted form** that needs no balance hypothesis: **`twist_fold_phase_normal_form`** gives, for *every* history, `fold h = (−1)^{#neg + inv} • σx^{#X}σy^{#Y}σz^{#Z}`. **The two factors separate because they are independent:** signs pull out of a product regardless of order (**`twistMatrixFold_eq`**), while distinct Pauli matrices anticommute (**`anti_yx`**, **`anti_zx`**, **`anti_zy`**), so sorting the axis word costs one `−1` per **inversion** and nothing else (**`axisFold_eq_canon`**, by induction pushing one letter into the sorted product at a time — **`canon_cons_X/Y/Z`** — at a cost equal to the number of smaller letters already there, **`countP_invPair_Y/Z`**). Equal letters commute with themselves, which is exactly why the inversion count and not the count of all distinct-letter pairs is the right statistic. Balance makes each axis multiplicity even, so `σ²=I` kills the sorted remainder (**`canon_axisWord_balanced`**) — a **second, independent route** to [balanced_phase_is_real](QLF_BalancedPhaseReal.lean) (**`phase_rule_real`**), the determinant argument not being the only one. **Consequence:** the phase is a computable **integer** read off the word (**`predictedPhase`**, certified against the matrix product by **`fold_eq_predictedPhase`**) — the signed-census → amplitude bridge no longer needs one `2×2` product per history. Cross-check: the interleaved `^<v>` is settled by *counting* (two negative twists, three inversions, odd ⟹ `−I`; **`phase_of_interleaved_xlvr`**), agreeing with the entrywise [interleaved_xlvr_folds_to_negI](QLF_TwistAlphabet.lean). No axioms | `anti_yx`, `anti_zx`, `anti_zy`, `invPair`, `invCount`, `countP_invPair_Y`, `countP_invPair_Z`, `canonPow_X`, `canonPow_Y`, `canonPow_Z`, `axisFold_eq_canon`, `twistMatrixFold_eq`, `twist_fold_phase_normal_form`, `canon_axisWord_balanced`, `phase_rule`, `predictedPhase`, `fold_eq_predictedPhase`, `phase_rule_real`, `phase_rule_even`, `phase_rule_odd`, `phase_of_interleaved_xlvr`, `phase_rule_summary` |
| [QLF_BasisIndependence.lean](QLF_BasisIndependence.lean) | **The census is basis-independent — *the basis belongs to the question, not to reality*.** [census_inventory.py](../census_inventory.py) writes every way in one chart (`{>,<}↦X`, `{^,v}↦Y`, `{/,\}↦Z`, axis order `X<Y<Z` for the inversion count); this proves that chart is a coordinate convention and never was a preferred physical frame. **Every count-balanced history folds to the same Pauli scalar** after any axis transposition (**`fold_invariant_swapXY`**, **`fold_invariant_swapYZ`**, composite **`fold_invariant_swapXZ`** = `(XY)(YZ)(XY)`), any axis reversal (**`fold_invariant_flipX`**, and **`fold_invariant_flipY`** as the conjugate `(XY)∘flipX∘(XY)`), and the gauge swap (**`fold_invariant_swapGauge`**) — so the whole signed-permutation group of the three axes plus the gauge swap. Mechanism, entirely combinatorial once [phase_rule](QLF_PhaseRule.lean) is in hand: relabeling moves the sign count by an axis multiplicity and the inversion count by a **product** of two axis multiplicities (**`invCount_map_swapAxXY`** `= n_X·n_Y`, **`invCount_map_swapAxYZ`** `= n_Y·n_Z`, proven for *all* words), and count balance makes every axis multiplicity even (**`axisWord_count_X_even`** …), so every correction is even. **Balance is load-bearing** — outside it the corrections are real. **The sharp consequence is negative, and is why it was worth proving:** a relabeling is an involution on the census (**`map_swapXY_involutive`**) preserving each way's phase, so it *permutes* ways without mixing them, and therefore **cannot** produce the Hadamard mixing `(A₊,A₋) ↦ (A₊+A₋, A₊−A₋)` of a quantum basis change — a permutation never sums two amplitude classes into one. The quantum change of basis is not the substrate relabeling; all contextual content sits in how a context **partitions** the ways, and that map must be *derived* (joint closure with the apparatus, [ER_EPR_QLF](ER_EPR_QLF.lean)'s `SharedClosure`) rather than chosen to fit. No axioms | `swapAxXY`, `swapAxYZ`, `swapXY`, `swapYZ`, `flipX`, `swapGauge`, `map_swapXY_involutive`, `countBalanced_map_swapXY`, `invCount_map_swapAxXY`, `invCount_map_swapAxYZ`, `negCount_map_flipX`, `axisWord_count_X_even`, `fold_invariant_swapXY`, `fold_invariant_swapYZ`, `fold_invariant_flipX`, `fold_invariant_swapGauge`, `fold_invariant_swapXZ`, `fold_invariant_flipY`, `basis_independence_summary` |
| [QLF_IndexedFactors.lean](QLF_IndexedFactors.lean) | **Many bodies need *indexed copies* of the eight twists, not more twists — and the sector indexing cannot reach.** A many-body token is `(factor, twist) ∈ ℕ × Σ₈` (**`IndexedTwist`**), an indexed *use* of the same eight, never a new kind of `^` (**`twistOf_mem_alphabet`**) — `N` bodies need `N` labels, not `2ᴺ` primitives, which is [eight-twists-sufficiency.md](../eight-twists-sufficiency.md) made a type. **What indexing changes is the algebra:** independent bodies act as `A⊗I` and `I⊗B` and **commute** (**`indexed_factors_commute`**, via `Matrix.mul_kronecker_mul`), where a flat word puts them in one Pauli algebra and makes distinct axes **anticommute** (**`not_all_flat_pairs_commute`**, with `^` and `>`). **The two models are two sectors, not rivals.** A Kronecker product is scalar exactly when both factors are, so an independent-factor joint closure needs *each* factor closed; in the flat model a factor may stay **open**, balanced by the other — precisely `SharedClosure` ([ER_EPR_QLF](ER_EPR_QLF.lean)), entanglement. **Product sector** (both close alone): phases simply multiply, in **`μ₄` not `μ₂`** — an open factor is not count-balanced so [balanced_phase_is_real](QLF_BalancedPhaseReal.lean) does not apply and its scalar may be `±i` (**`fold_scalar_factorizes`**, **`product_sector_order_free`**, via **`twistMatrixFold_append`**). **Coupled sector** (neither closes alone, the pair does): **`shared_closure_not_factorizable`** — the primordial `^ \| v` is jointly balanced while **neither** side folds to a scalar (**`up_fold_not_scalar`**, **`down_fold_not_scalar`**), so no assignment to independent indexed bodies reproduces it. The gauge pair falls the other way (**`gauge_pair_is_product_sector`**), so the boundary is sharp from both sides. Measured: the coupled sector is the **majority**, settling near four fifths (`0.750`, `0.791`, `0.804`, `0.803` at lengths 2–8, [census_inventory.py](../census_inventory.py) factor census). **Consequence:** index the inventory, but binding two bodies takes a genuine Pauli **string** `σ⊗σ`, not a product of single-factor operations. No axioms | `IndexedTwist`, `twistOf_mem_alphabet`, `onFirst`, `onSecond`, `indexed_factors_commute`, `not_all_flat_pairs_commute`, `twistMatrixFold_append`, `fold_scalar_factorizes`, `product_sector_order_free`, `up_fold_not_scalar`, `shared_closure_not_factorizable`, `gauge_pair_is_product_sector`, `indexed_factors_summary` |
| [QLF_Mpemba.lean](QLF_Mpemba.lean) | **Anomalous relaxation: what the substrate forbids, permits, and does not deliver** ([Mpemba.md](../Mpemba.md)). Relaxation to equilibrium *is* closure and its time *is* the maximum excursion ([closedAtHorizon_iff_maxExcursion_le](QLF_ClosureDepthLaw.lean)), making three statements decidable — and they do not all point the same way. **A no-go:** **`relaxation_ge_distance`** (`|level s| ≤ maxExcursion s`, via **`level_le_hmax`**) — if distance from equilibrium means the history's imbalance, relaxation is bounded **below** by it, so a farther state can *never* relax faster and the effect is **impossible** for that measure; any Mpemba claim must name another distance. **An enabler:** **`equal_length_unequal_relaxation`** / **`nested_relaxes_slower`** — at one length `2n` with identical zero imbalance, the pair matching closes in **one** pass while the nested singlet needs **`n`**, so no scalar macrostate variable determines relaxation, which is exactly the room an anomalous ordering needs. **A translation:** **`strong_mpemba`** — if every history of `H` stays within excursion `R` while some history of `C` exceeds it, then at capacity `R` the `H` preparation has fully closed and `C` has not, so the spectral "slow mode has zero amplitude" becomes the census condition `W_H(deep sector) = 0` with no appeal to eigenmodes. **Honest scope:** the effect itself is **not** derived — the blind test ([mpemba_census.py](../mpemba_census.py)) finds relaxation **monotone** in length with **no** crossing from uniform balanced preparations; the anomalous ordering needs a preparation biased toward the shallow tail, which is the substrate translation of "suppressed slow mode" rather than an independent prediction of it. No axioms | `level_le_hmax`, `relaxation_ge_distance`, `equal_length_unequal_relaxation`, `nested_relaxes_slower`, `strong_mpemba`, `mpemba_summary` |
| [QLF_HorizonBasis.lean](QLF_HorizonBasis.lean) | **A horizon rebasing is an automorphism of the closed causal substrate** ([BLACK-HOLES.md](../BLACK-HOLES.md) §4a). Makes precise the claim that the closures inside a horizon are the closures outside in a different basis — and separates the mathematics from the physics, which had been running together. A `HorizonRebasis` is an invertible relabeling of the twist alphabet preserving balance and, on balanced histories, the fold; every one is then an isomorphism of the whole closed causal structure. **The find is that order preservation is a theorem, not a fourth assumption:** reachability in [QLF_ReachableEvent](QLF_ReachableEvent.lean) is list-prefix and `List.map` distributes over append, so `reachable_map` needs no invertibility and `reachable_rebased_iff` follows from the inverse relabeling — a basis change cannot destroy substrate succession (`rebasis_preserves_causal_chain`). **Read `rebasis_nonempty_trivially` before citing it** (R6a): the interface is satisfied by the identity, so inhabitation is not evidence; the evidence is the non-identity instances `swapXYRebasis`/`swapGaugeRebasis`, which exist because [QLF_BasisIndependence](QLF_BasisIndependence.lean) proved balance and fold survive those relabelings. And in `horizon_rebasis_is_closure_order_iso` two of three conjuncts are the structure's own fields projected — what the theorem adds is that order preservation comes free with them. **Deliberately absent:** no `axiom blackHoleHorizonRebasis` (that renames the hypothesis rather than establishing it) and no `True` summary. Open, and dynamics rather than basis algebra: horizon realization and interior persistence. No axioms | `HorizonRebasis`, `mapHistory_bijective`, `closed_iff_rebased`, `fold_rebased`, `reachable_map`, `reachable_rebased_iff`, `CausalChain`, `rebasis_preserves_causal_chain`, `rebasis_nonempty_trivially`, `swapXYRebasis`, `swapGaugeRebasis`, `horizon_rebasis_is_closure_order_iso` |
| [QLF_Fredkin.lean](QLF_Fredkin.lean) | **Fredkin's conservation law IS ZFA count balance** ([Fredkin_QLF.md](../Fredkin_QLF.md), [fredkin_qlf.py](../fredkin_qlf.py), [fredkin_machine.html](../fredkin_machine.html)). Fredkin & Toffoli (1982) built computation out of a conservation law — the gate `CSWAP(c;a,b)` is its own inverse and *conservative*, its outputs a permutation of its inputs, realized physically as billiard balls whose logical 1s are conserved because balls are. QLF's admissibility is a conservation law too, and under the encoding they are the same one. A ball is the closed plaquette `[up,left,down,right]`, a line carries one or nothing, a register is the concatenation of its three lines — right-nested so the two swapped lines sit in a single sub-append. Then **`encode_fredkin_perm`**: the output history is a *permutation* of the input, by `List.perm_append_comm` on that sub-append and `refl` on the untouched branch. Counts follow from the permutation (**`fredkin_preserves_counts`**), count balance from the counts (**`fredkin_preserves_countBalanced`**, with **`encode_countBalanced`** showing the hypothesis is never in doubt), and the keystone `count_balanced_pauli_closed` hands over the order-sensitive conjunct — so **`fredkin_preserves_zfa`** needs no argument of its own. Admissibility is not something a conservative gate must be checked against; it is the law the gate was built to obey. Read structurally, the gate is an **automorphism of the admissible closure space** — the emergence ladder's first rung that is a *map* on the structure rather than more of it ([Mathematics_From_QLF.md](../Mathematics_From_QLF.md) Rung 5b) — and informationally a **bijection**, so information moves without being forgotten ([Information_Physics.md](../Information_Physics.md) §5a). Also **`fredkin_involutive`**, **`fredkin_conserves_weight`** (the ball count), and **`fredkin_bijective`** — the free-energy ledger's premise where it can be checked: the gate maps its state space onto itself one-to-one, so nothing merges, there is no many-to-one closure to receipt, and an instantaneous zero-free-action closure costs **nothing**. The bill is only the garbage you decline to keep, which is Landauer/Bennett derived from the one closure quantum rather than assumed beside it ([Reversibility.md](../Reversibility.md) §7). Helium is the billiard ball *because* valence 0 means no shared closure hence no bond ([Chemistry.md](../Chemistry.md)). No axioms | `fredkin_involutive`, `fredkin_bijective`, `fredkin_conserves_weight`, `encode_fredkin_perm`, `fredkin_preserves_counts`, `encode_countBalanced`, `fredkin_preserves_countBalanced`, `fredkin_preserves_zfa` |
| [QLF_Folding.lean](QLF_Folding.lean) | **A polymer conformation IS a twist history, and a contact IS a ZFA closure** ([Protein_Folding.md](../Protein_Folding.md), [protein_census.py](../protein_census.py)). [Chemistry.md](../Chemistry.md) gets molecules from one rule — a bond is a shared closure — and stops at stoichiometry, because a small molecule has no shape. A polymer does, and the step needed to talk about shape was already in the alphabet: a backbone on the cubic lattice moves by one of six signed axis displacements, and the 8-twist alphabet **is** the signed axis frame ([QLF_AlphabetNecessity](QLF_AlphabetNecessity.lean)), the gauge pair `±` carrying phase and no displacement (`count_encode_plus`/`count_encode_minus`). So `Step.toTwist` is an identification, not an encoding. Then a **contact** — residues whose connecting segment displaces by exactly one lattice step — closes a loop with zero net displacement, hence **`closedLoop_countBalanced`**, hence Pauli-closed by the keystone `count_balanced_pauli_closed`: **`contact_is_closure`** delivers both ZFA conjuncts and the second needs no argument of its own, the same move [QLF_Fredkin](QLF_Fredkin.lean) makes for a conservative gate (and the minimal contact `minimal_loop_closed` is literally Fredkin's billiard-ball plaquette). Four consequences, each a corollary rather than a modelling choice: **`contact_separation_odd`** — contacts occur only at **odd** sequence separation, the lattice-protein parity rule, off `closedLoop_even_length`; **`closedLoop_append`** — closures **compose**, so a fold's contacts add rather than forming a joint condition to be searched for, which is the substrate reply to Levinthal; **`map_mirror_bijective`** — a **no-go**: mirroring is a length- and closure-preserving involution, so the two handednesses are in bijection and **counting cannot prefer one**, which locates homochirality upstream in [QLF_Handedness](QLF_Handedness.lean) rather than in any fold census; and **`foldFreeEnergy`** — one `log 2` per closure ([QLF_FreeEnergy](QLF_FreeEnergy.lean)), strictly decreasing (`foldFreeEnergy_lt`), so the lattice contact energy is **derived, not fitted**. Non-vacuity is checked both ways (`open_chain_not_closed`, `minimal_loop_closed`). **Deliberately absent:** self-avoidance, positions, and the census itself — those need an embedding rather than an algebra and live in [protein_census.py](../protein_census.py), which re-runs every contact loop through the runtime `twist_core.is_zfa`. No axioms | `count_encode`, `closedLoop_iff_net_zero`, `closedLoop_nil`, `closedLoop_append`, `open_chain_not_closed`, `minimal_loop_closed`, `closedLoop_countBalanced`, `closedLoop_pauli_closed`, `contact_loop_closed`, `contact_is_closure`, `length_eq_counts`, `closedLoop_even_length`, `contact_separation_odd`, `map_mirror_involutive`, `mirror_closedLoop`, `map_mirror_bijective`, `foldFreeEnergy_succ`, `foldFreeEnergy_lt` |
| [QLF_Unsaturation.lean](QLF_Unsaturation.lean) | **"Degree of unsaturation" IS the closure count of a molecule** ([Chemistry.md](../Chemistry.md) §10, [hydrocarbon_census.py](../hydrocarbon_census.py)). Organic chemistry teaches `DoU = (2C + 2 + N − H − X)/2` as a formula to memorise, with oxygen and sulphur left out and no reason given. Read the molecule as a graph whose vertex degrees are the **valences** and the handshake lemma `2E = Σ vᵢ` makes it the cycle rank: `b₁ = E − V + 1 = Σ(vᵢ − 2)/2 + 1`, so each element's coefficient is **`(valence − 2)/2`** — carbon `+1`, nitrogen `+½`, hydrogen and halogen `−½`, and **oxygen `0`, which is why it was missing.** Not a convention, a cancellation: **`divalent_neutral`** — a divalent atom adds one vertex and one edge, so it cannot change a cycle rank. Everything is the master lemma **`doubledClosures_cons`** (an atom contributes `valence − 2`) counted up: **`dou_hydrocarbon`** / **`dou_chno`** recover the textbook formula with no `O` on the right-hand side, and **`saturated_iff_alkane`** makes *saturated* mean **zero closures**, so `CₙH₂ₙ₊₂` follows rather than being stipulated. The content is the **identification**, not the arithmetic, which is easy: `b₁` counts *independent closures*, and a cycle in a molecular graph is the same object as a contact loop in [QLF_Folding](QLF_Folding.lean) — so **a double bond and a ring are one phenomenon**, and `C₆H₁₂` is a single census class holding cyclohexane and every hexene (**`c6h12_one_closure`**; **`benzene_four_closures`** counts three double bonds and the ring without caring which is which). Third corollary: **valence 2 is the neutral element of closure counting** (**`divalent_chain_neutral`**), which is *why* a divalent monomer polymerises into a **chain** — the backbone carries no closure of its own, so every closure a polymer has is a contact, which is exactly what [QLF_Folding](QLF_Folding.lean) assumes. [hydrocarbon_census.py](../hydrocarbon_census.py) checks it: growing skeletons with max degree 4 as the only rule reproduces the alkane series (OEIS A000602) through C₁₄, and the merged closure class gives C₄H₈ → 5, C₅H₁₀ → 10, C₆H₁₂ → 25, each the textbook constitutional-isomer total. Fourth, and the reaction layer: a balanced reaction pins the atom inventory, so `V` and `E` are both fixed and for a mixture of `k` molecules `b₁ = E − V + k` leaves **only `k`** free — **`reaction_delta`** proves the change in closure count *is* the change in molecule count, so organic chemistry's taxonomy is that one number (addition `2→1`, `Δ=−1`; elimination `1→2`, `Δ=+1`; substitution/condensation `2→2`, `Δ=0`, the class fixing the sign and the piece-count the magnitude). **`equal_molecule_count_preserves_closures`** names the neutral class, which is where the **peptide bond** sits — so a polypeptide backbone carries no closure of its own and every closure a folded chain has is a contact. **Honest scope:** exact arithmetic over the valence bookkeeping — the graph is not formalised, so `b₁` enters as the definition `E − V + 1`, not as a proved property of a cycle space; and the closure *count* is derived while its *placement* (resonance, regiochemistry) is not. No axioms | `doubledClosures_cons`, `doubledClosures_append`, `doubledClosures_replicate`, `divalent_neutral`, `divalent_chain_neutral`, `monovalent_caps`, `dou_hydrocarbon`, `dou_chno`, `saturated_iff_alkane`, `benzene_four_closures`, `c6h12_one_closure`, `mixtureClosures_eq`, `reaction_delta`, `equal_molecule_count_preserves_closures` |
| [QLF_Inertia.lean](QLF_Inertia.lean) | **Route A: an accelerated null circulation weighs exactly `E/c²`** ([Inertia.md](../Inertia.md) §4a). Every substrate step runs at `c` (one Planck length per Planck tick, held at every depth by the ρ-cancellation), so a *massive* particle cannot be something moving slower — it must be a **closed circulation of light-speed steps**, and *"the light-speed energy in every direction sums to zero"* is the signed action vector vanishing, i.e. **ZFA count balance itself**. This does the minimal case, a two-leg Einstein light clock, and computes what accelerating it costs. **`netForce_eq`** — `netForce = −E·δ/L`, so the circulation **speed cancels out of the force entirely**; only the shift per unit length survives. **`inertial_reaction`** — feed the equivalence-principle shift `δ = aL/c²` and `netForce = −(E/c²)·a`, with **`L` cancelling too**, hence **`independent_of_circulation_size`**: it does not matter how the mass is built. **`inertial_reaction_mass`** gives `F = −ma`; **`no_force_without_acceleration`** gives Galileo's ship (uniform motion free at any speed); **`legs_balanced_iff_no_shift`** says the legs are equal exactly when `δ=0`, which is what rest *is*. The keystone is **`force_scales_with_shift`** — the force is exactly proportional to `δ`, so a redshift law scaled by `k` yields an inertia scaled by `k`: **the shift law is forced, not fitted**, and a different redshift would make the same energy weigh a different amount. That is the demystification — inertia is not an extra property of matter but what a balanced null circulation costs to unbalance. **Honest scope:** `δ = aL/c²` is *input* (the repo's existing redshift account, `GR_Schwarzschild.md` §2a — not established here); what is derived is that this shift and no other gives `F = −ma` with `c` and `L` both cancelling — a computation that could have failed. **Not established:** that the circulation giving `m = 1/R` is the same object as the gauge-fold depth `Higgs.md` calls inertial mass (kill condition 3, open), the *counting* version of the imbalance (rule 4 wanted a signed integer, this is continuum algebra), or the rotational sector. `route_A_established` is a conjunction, not a `True` summary. No axioms | `legs_balanced_iff_no_shift`, `netForce_eq`, `inertial_reaction`, `inertial_reaction_mass`, `independent_of_circulation_size`, `no_force_without_acceleration`, `force_scales_with_shift`, `route_A_established` |
| [QLF_KraftMeasure.lean](QLF_KraftMeasure.lean) | **The closure-depth measure is counted, not chosen** ([Born_Rule.md](../Born_Rule.md) §8, [contextual_census.py](../contextual_census.py) `--first-closure`). A closure **is** an event, so a run that has closed is not continued, and the first-closure histories of one experiment are therefore **prefix-free**. That single structural fact fixes how a closure at depth `d` weighs against one at depth `d'`, with no room to fit anything: **`kraft_count`** — for prefix-free `F` with every word no longer than `D`, `∑ b^(D−|h|) ≤ b^D` — is the multiplicity reading itself, since a first closure `h` is the prefix of exactly `b^(D−|h|)` complete length-`D` histories (*everything after a closed event can still happen every way*), prefix-freeness makes those completion sets disjoint, and they all sit inside the `b^D` histories of that length. **`kraft_measure`** states it as a mass, `∑ (1/b)^|h| ≤ 1`, and **`twist_kraft`** instantiates it at the 8-twist alphabet. The physical content is the leftover `1 − ∑ b^{−|h|}`: the runs that never close here, so **capacity causes leakage, never renormalisation** — it removes cylinders, it does not reweigh the survivors. Settles the measure, not the Born rule: with it the multiplicity reading converges while the phase-weighted ones diverge (`|A(d)|` grows `3.91^d`–`4.56^d` against the `√8^d = 2.828^d` the measure allows). **And the same counting kills the Born reading.** With the measure fixed, the census weighs an event class of `W` ways carrying signed total `A` as `B = (W/b^d)·(A/W)²` — multiplicity mass times squared mean phase — which is summable for free (`normalized_le_mass`, `normalized_event_mass_le_one`: `|A| ≤ W` puts it under the Kraft bound whatever the phases do). But **merging two families of ways into one event can only lower the weight** (`merge_le_sum`, Cauchy–Schwarz in Engel form via the exact identity `merge_gap`: the gap is `(aq−bp)²/(pq(p+q))`), with equality exactly at equal mean phase (`merge_eq_sum_iff`). So **`no_constructive_interference`** — `B(A ∪ B) ≤ B(A) + B(B)`, always — where QM needs a factor `2` for two coherent equal-amplitude paths. Measured to match in [contextual_census.py](../contextual_census.py) `--two-path`: matched pair ratio `1.000000`, unequal `0.999288`, destructive `0`. **The inequality that bought summability forbids the enhancement**, but only where that normalisation is needed. Some preparation–apparatus pairs carry a convergent amplitude *without* it: the transverse geometry grows `2.24^d` and the ZX/ZY mixes `2.65^d`, under the forced `√8^d` threshold (one way must weigh its own cylinder mass, so amplitude ∝ `√μ`), and there the unnormalized weight is an exact rational — aligned `1`, transverse `1/2`, the mixes `196/197` at amplitude ratio `−1/14` — with interference in both directions (`2.0000` constructive, `0.0000` destructive). This is **geometry-dependent, not capacity-dependent**: the absorbing operator's radius is `3.99`/`4.38` at capacity 2/3, both above threshold, so those cases are subdominant modes. Whether the convergent geometries form a structured class is open. Supporting: `words`, `card_words`, `completions`, `PrefixFree`. No axioms | `kraft_count`, `kraft_measure`, `twist_kraft`, `merge_gap`, `merge_le_sum`, `no_constructive_interference`, `merge_eq_sum_iff`, `normalized_le_mass`, `normalized_event_mass_le_one`, `card_words`, `completions_disjoint`, `card_twist` |

---

## Axiom Inventory

All axioms are isolated and explicit. The combinatorial core is axiom-free beyond standard Lean/Mathlib. The only axioms are in `QLF_Riemann` and `ER_EPR_QLF`, marking exact logical boundaries.

| Axiom | Location | Meaning | Logical role |
|---|---|---|---|
| `spectral_hilbert_polya` | `QLF_Riemann` | Scalar spectral mode requires a non-trivial zero on the critical line | Marks the RCA₀ → WKL₀ boundary; the QLF form of the Hilbert-Pólya conjecture |
| `resonant_computation_for` | `QLF_Riemann` | Associates a TerminatingComputation to each candidate zero | Bridge from combinatorics to the Dirichlet series world |

`critical_line_forcing` is **derived** from `spectral_hilbert_polya` via `spectral_symmetric_eq_scalar_id` — it is a theorem, not an axiom.

`NonTrivialZero` was formerly listed here as a third axiom. It is now a **definition** over Mathlib's `riemannZeta` — `riemannZeta ρ = 0 ∧ 0 < ρ.re < 1` — with `not_nonTrivialZero_of_re_nonpos` and `trivial_zero_not_nonTrivial` proved from it. It was never a bridge: naming ζ's zeros is vocabulary, and leaving the name opaque made the bridge above assert nothing, since the interpretation where no complex number is a non-trivial zero satisfied it. Two axioms remain.

`ER_EPR_QLF.lean` contains philosophical axioms explicitly marked as speculative; they are not used by any other module.

---

## Key Proof Chains

### Riemann Hypothesis in QLF

```
encode_is_phase_only            : encodeComputation c is pure-phase              [RCA₀]
encode_is_zfa                   : encodeComputation c achieves ZFA               [RCA₀]
zfa_implies_critical_line       : ZFA ⟹ is_symmetric                            [RCA₀]
spectral_symmetric_eq_scalar_id : is_symmetric ⟹ toSpectralMode s = c • I       [RCA₀]
spectral_hilbert_polya          : (axiom) scalar mode ⟹ ρ.re = 1/2             [WKL₀ boundary]
─────────────────────────────────────────────────────────────────────────────────
riemann_hypothesis_in_qlf       : NonTrivialZero ρ ⟹ ρ.re = 1/2
```

### Universality (Church-Turing in QLF)

```
encode_is_phase_only  : every terminating computation maps to a pure-phase string
encode_is_generated   : the encoded string is produced by expand_generation
encode_is_zfa         : the encoded string achieves ZFA balance
─────────────────────────────────────────────────────────────────────────────
qlf_universality      : every terminating computation encodes as a ZFA string
                        (expand_generation + full_zeno_prune generates all of them)
```

### Pauli Exclusion (non-vacuous)

```
fermi_antisym_eq_commutator : fermi_antisym p q = p.eval * q.eval - q.eval * p.eval
fermi_antisym_self          : fermi_antisym p p = 0   (identical processes commute)
fermi_nonzero_example       : fermi_antisym (action f_x) (action f_z) ≠ 0
                              (σ_x and σ_z do NOT commute — [σ_x,σ_z] = [[0,-2],[2,0]])
─────────────────────────────────────────────────────────────────────────────
pauli_exclusion             : fermi_antisym p p = 0  IS a genuine constraint,
                              not a vacuous identity — because fermi_antisym ≠ 0 in general
```

### Stable-State Count

```
find_stable_states_iff         : s ∈ find_stable_states(2n) ↔ s is pure-phase ∧ is_symmetric
find_stable_states_length_odd  : no symmetric pure-phase strings of odd length exist
find_stable_states_length_even : |find_stable_states(2n)| = C(2n, n)
─────────────────────────────────────────────────────────────────────────────
string_mode_count              : stringModesAtLevel n has C(2n, n) elements
                                 (same count, derived independently via ZFA)
```

---

## Logical Subsystems (Reverse Mathematics)

The QLF formalization is stratified by logical strength, following Harvey Friedman's Reverse Mathematics program:

| Subsystem | Modules | What it means |
|---|---|---|
| **RCA₀** (constructive core) | QLF_Axioms, QLF_Combinatorics, QLF_QuCalc, QLF_Universality, QLF_Critical_Line, QLF_Spectral (most), RhoQuCalc, SpacetimeDynamics, PauliExclusion, StringTheoryQLF, MTheoryQLF | Strictly computable; no Choice, no continuity, no non-constructive existence |
| **RCA₀ → WKL₀ boundary** | `spectral_hilbert_polya` axiom in QLF_Riemann | The exact point where discrete combinatorics must connect to continuous analytic functions |
| **Speculative / beyond proof** | ER_EPR_QLF | Philosophical axioms for entanglement-geometry; explicitly not derived |

The non-constructive parts of the Ruliad — non-terminating computations, Busy Beaver values, uncountable sets — are exactly what `full_zeno_prune` eliminates. Everything that survives is in RCA₀.

---

## How to Build

```bash
lake exe cache get   # fetch prebuilt Mathlib (saves ~1 hour)
lake build
```

Requires [elan](https://github.com/leanprover/elan); Lean 4.30.0-rc2 is pinned via `lean-toolchain`.

---

## Empirical Verification Scripts

These Python scripts independently confirm the Lean theorems numerically — they are not tests of the Lean build, but independent checks that the abstract theorems correspond to concrete physics:

| Script | What it checks | Lean theorem confirmed |
|---|---|---|
| [`../qlf_spectral.py`](../qlf_spectral.py) | All pure-phase strings are Hermitian; symmetric strings give scalar × I | `toSpectralMode_hermitian`, `spectral_symmetric_eq_scalar_id` |
| [`../qlf_zfa_frequency.py`](../qlf_zfa_frequency.py) | ZFA count by length = C(n, n/2); Stirling growth | `find_stable_states_length_even` |
| [`../qlf_dirichlet_search.py`](../qlf_dirichlet_search.py) | Stable-state counts vs. Dirichlet partial sums (asymptotic) | `riemann_hypothesis_in_qlf` (empirical shadow) |
| [`../qucalc_engine.py`](../qucalc_engine.py) | Phase-string generation and ZFA filtering | `expand_generation`, `full_zeno_prune` |