# Open Problems — QLF gap registry

A single map of what is **closed**, what is a **principled boundary**, and what is
genuinely **open**, with a pointer to the document that owns each item. This is an
*index*, not a re-derivation: the substance lives in the linked docs. Its mirror is
[`Beyond_Standard_Model.md`](Beyond_Standard_Model.md) (what QLF *derives / predicts* past the SM).
For a **physics-facing** view of the same picture — the canonical mysteries of physics organized by
the question a physicist would name (addressed / value-open / boundary / predicted-absent / open) —
see [`Mysteries_Of_Physics.md`](Mysteries_Of_Physics.md).
It complements
[`Experimental_Consistency.md`](Experimental_Consistency.md) (which tracks per-result
precision) by collecting the *forward* work in one place.

**What "open" means here (issue [#78](https://github.com/jimscarver/quantum-logical-framework/issues/78)).**
🔵/🟣 "open" means **a value not yet calculated / a rendering not yet formalized — work requiring
deeper investigation**, *not* a hole where the theory could be wrong. QLF's ontology is **complete**:
the quantum logical (ZFA) description has no hidden variables, and quantum computation is the standing
experimental verdict that it has no missing causal ingredient (gravity is emergent, so it cannot be a
hidden influence — [`Beyond_Standard_Model.md`](Beyond_Standard_Model.md) §3b). So these are the
*calculational frontier* of a complete foundation, the same way "derive the proton mass from QCD" is
open *within* a complete Standard Model. The **only** genuinely *external* limits are the 🧱 bridge
axioms of the Millennium program — and these split honestly: for the *continuum-analytic* problems
(Riemann, Yang–Mills, Navier–Stokes) the bridge is QLF's continuum/choice thesis (where ZFC's continuum
machinery is pathological); for the *finitary* problems (Hodge, BSD, P vs NP) the bridge is a
full-strength faithfulness step — the genuine open conjecture itself, **not** "ZFC's defect" (that would
be a category error). The Hodge thread is the first **closed at its honest floor**: both sides built, the
residual reduced to the one geometric-realization bridge.

**Why a registry.** Open items were scattered across ~25 documents, each with its own
"Open work" section. When a status changes, the claim can drift out of sync across docs
(as the Hadronic-Depth attribution did before its correction). This file is the
canonical status list; when an item moves, update it here and in its owning doc.

## Status legend

| Tag | Meaning |
|---|---|
| ✅ **Closed** | Derived / machine-verified; no longer open. |
| 🧱 **Boundary** | A *principled* limit (like an explicit axiom), not a gap to be closed by more work. The structural form is fixed; a number or bridge is inherited. |
| 🔵 **Open — quantitative** | Mechanism identified; a specific number is not yet derived from substrate. |
| 🟣 **Open — structural / Lean** | Result holds in prose/numerics; a clean theorem or Lean anchor is not yet written. |
| ⚪ **Future work** | Out of current scope by specification (not by doubt about the mechanism). |

---

## Closed — derived / machine-verified

| Item | Status | Where |
|---|---|---|
| **Turbulence as a quantized-vortex tangle (structural)** | ✅ **Machine-verified (structure)** — vorticity quantization applied to turbulence (`QLF_Turbulence`): a vortex line is one circulation quantum (`vortex_quantum`), total circulation an integer count of quanta (`circulation_integer_quantized`) — **Onsager–Feynman quantization from the substrate**, so classical turbulence = the coarse-grained limit of quantum turbulence; the cascade is a **frequency hierarchy** (`cascade_frequency_increases`) with a dissipation floor (`cascade_capped`), reconnection = a ZFA closure. It is all Navier–Stokes, two questions: the Clay **regularity** (no-blow-up, reduced in `QLF_NavierStokesBKM`) and the **statistics** (Kolmogorov `−5/3` / intermittency — distinct and **open**, *not* derived here). No new axioms | [`lean/QLF_Turbulence.lean`](lean/QLF_Turbulence.lean), [`Navier_Stokes_Geometry.md`](Navier_Stokes_Geometry.md) §6 |
| **Relativistic energy–momentum `E² = p² + m²`** | ✅ **Machine-verified** — read off the verified Minkowski interval (`QLF_EnergyMomentum`): the 4-momentum `(E,p)` is a Minkowski `Form` whose interval `E²−\|p\|²` is the invariant mass² (`energy_momentum_relation`); `m² = det(4-momentum)` (`massSq_eq_det`), a Lorentz invariant (`mass_lorentz_invariant`); rest energy `E=mc²` (`rest_energy_sq`); massless ⟹ null `E=\|p\|` (`massless_null`, the photon). Momentum enters QLF through the verified Lorentzian state space, not as a bare additive count. No new axioms | [`lean/QLF_EnergyMomentum.lean`](lean/QLF_EnergyMomentum.lean), [`The_QLF_State_Space.md`](The_QLF_State_Space.md) §7 |
| **Angular momentum + the Navier–Stokes no-blow-up geometry** | ✅ **Machine-verified (mechanism)** — angular momentum = circulation (`circulation = baryonNumber`, Σ `signTriple`; the `su(2)` Noether charge, a pseudovector `L→−L` under T via `circulation_reverses_under_time_reversal`); vorticity = the local discrete curl `signTriple`, **quantized** (`vorticity_quantized`, `|ω| ≤ 1`/cell), so it **cannot diverge** — the Beale–Kato–Majda vorticity-blow-up criterion is unsatisfiable on the substrate, the mechanism behind `realized_flow_is_stable`. `circulation_bounded` (`|L| ≤ n`), `continuum_vorticity_unrealizable` (continuum `ℝ`-vorticity unrealizable in a finite cell). The correction is the quantization/discreteness. The continuum-PDE inheritance stays the named boundary `navier_stokes_continuum_limit` — **now reduced** (`QLF_NavierStokesBKM`): the opaque axiom is unbundled into the *proven* Planck vorticity cap `≤1/L_P²` (`planck_caps_vorticity`, no axiom) + the *cited* Beale–Kato–Majda criterion + a *sharp* faithfulness bridge (`continuum_vorticity_planck_capped`), from which `navier_stokes_no_blowup` is a theorem. A reduction (mechanism explicit, BKM cited, gap localized to vorticity-rendering faithfulness), not a Clay proof — sufficient at the fixed Planck floor; the Clay `v→∞` limit is the rendering step. No new axioms beyond the (sharper) bridge | [`lean/QLF_AngularMomentum.lean`](lean/QLF_AngularMomentum.lean), [`lean/QLF_NavierStokesBKM.lean`](lean/QLF_NavierStokesBKM.lean), [`Navier_Stokes_Geometry.md`](Navier_Stokes_Geometry.md) |
| **Prime topology stability — prime frequencies are irreducible (first Lean anchor)** | ✅ **Machine-verified** — a closure of prime period has no nontrivial sub-closure repeat (`prime_freq_irreducible`, via `Nat.Prime`), so the vacuum can't factor it into a repeat of a shorter stable closure (the proton `n=3` lock); composites factor (`composite_freq_factors`). Higher frequencies dominate (`higher_freq_dominates`). The **half-spin prime-3 keystone** (balanced + prime: `half_spin_balanced_steps`, `half_spin_prime`, `half_spin_irreducible`) puts the same lock at the fundamental fermion. Anchors `Prime_Topology_Stability.md` (previously prose). Honest scope: the `Nat.Prime` irreducibility is exact; the 3-axis/120° cut of the 720° fermion is a reading (`fold_electron` is the 4-twist 2-D cut). No new axioms | [`lean/QLF_PrimeResonance.lean`](lean/QLF_PrimeResonance.lean), [`Geometry_Of_Space.md`](Geometry_Of_Space.md) |
| **ZFA closure is the firebreak on path-integral possibility-space** (issue #103) | ✅ **Machine-verified** — the path integral's "not every kinematic path becomes a physical receipt" as generate-then-close. The QuCalc tree generates `4^n` paths at length `2n` (`generated_count`); only the closing ones survive (`verify` filter, size `C(2n,n)`); the firebreak = `4^n − C(2n,n)` (`firebreakCount_eq`), which is **real** (`firebreak_nonempty`/`not_all_paths_close` — `[+,+]` is generated but doesn't close) and **asymptotically all** of possibility-space (`C(2n,n)/4^n → 0`, the `QLF_PhysicalPi` census). So `full_zeno_prune` is the substrate firebreak that keeps the path sum from exploding — phase/projectors/exclusion preventing runaway occupation. No new axioms; the `e^{iS/ℏ}` phase cancellation is the continuum rendering | [`lean/QLF_Firebreak.lean`](lean/QLF_Firebreak.lean), [`P_vs_NP_QLF.md`](P_vs_NP_QLF.md) |
| **Closure is horizon-relative; observation is bounded closure** (issue #104) | ✅ **Machine-verified** — a finite-resolution horizon `boundedPrune R` (prune only `R` passes) gives `closedAtHorizon R s`, closure as a usable receipt at resolution `R`. `horizon_relative` — the nested singlet `[+,+,−,−]` is open at horizon 1, closed at horizon 2 (the same history reads open to a shallow observer, closed to a deeper one); `closedAtHorizon_mono` — closure stable as the horizon widens; `nestedSinglet_zfa` — the witness closed at horizon 2 is also absolutely `achieves_ZFA`, so the deep-horizon reading is the genuine receipt and absolute closure is the asymptotic ideal the finite horizons approach. The observer = a local finite-capacity information horizon (`QLF_Realizability`) reading `closedAtHorizon` at its own resolution. No new axioms | [`lean/QLF_HorizonClosure.lean`](lean/QLF_HorizonClosure.lean) |
| **ER = EPR — derived from the substrate core (zero axioms)** | ✅ **Machine-verified, zero axioms** — the module does not *posit* the wormhole relation. Entanglement = a shared ZFA closure (`SharedClosure A B := achieves_ZFA (A++B)` — two histories that *close together*); a wormhole = that shared closure between **spacelike** events (`Spacelike` = neither `reachable`, the substrate causal set `QLF_ReachableEvent`), `ERBridge := SharedClosure ∧ Spacelike`. **`er_equals_epr`** (given spacelike, the bridge IS the shared closure — an identity, not a duality), **`no_ftl_in_epr`** (spacelike ⟹ neither end reaches the other), **`entanglement_is_logical_wormhole`**, and a **verified witness `primordial_wormhole`** (the conjugate pair `[+,−]` closes — `conjugate_pair_closes` via `native_decide` — and is spacelike). Non-locality dissolves: the two ends are one closure; **distance is perspectival** — zero closure-distance through the bridge, large through synthesized space | [`lean/ER_EPR_QLF.lean`](lean/ER_EPR_QLF.lean), [`ER_EPR_QLF.md`](ER_EPR_QLF.md), [`Primordial_Entanglement.md`](Primordial_Entanglement.md) |
| **What space QLF lives in — Gaussian-integer state space + Minkowski + the Lorentz double cover** | ✅ **Machine-verified** — Hilbert space is *too general*; QLF's state space is a finite-rank **`ℤ[i]`-lattice** with `μ₄={±1,±i}=(ℤ[i])ˣ` phases (`QLF_StateSpace`: `pauliScalar_pow_four_eq_one`, `toComplex_pow_four`), Hilbert space its continuum completion. The **`ℤ[i]` vs `ℤ[ζ₈]` question is resolved → `ℤ[i]`**: the Hadamard `√2` is a projectively-inert global normalization (`bornProb_global_scale`, `hadamard_born_half`), `ζ₈` entering only with the non-Clifford `T`-gate (the Clifford↔`T` = computable↔universal boundary). The state **is Minkowski space** — `det(Form)=t²−x²−y²−z²` = the interval (`QLF_Minkowski.det_toMatrix_eq_interval`), pure states null (Bloch=celestial sphere), dynamics interval-preserving (`interval_preserved_of_unit_det`). The **`SL(2,ℂ)→SO⁺(1,3)` double cover is machine-checked** (`QLF_LorentzCover`): homomorphism + explicit boost/rotation generators + **kernel `{±I}`** (`spinor_kernel`, the 2-to-1) + **surjectivity** (`spinor_surjective`, via the one bridge `lorentz_generated_by_boosts_rotations`) | [`lean/QLF_StateSpace.lean`](lean/QLF_StateSpace.lean), [`lean/QLF_Minkowski.lean`](lean/QLF_Minkowski.lean), [`lean/QLF_LorentzCover.lean`](lean/QLF_LorentzCover.lean), [`The_QLF_State_Space.md`](The_QLF_State_Space.md), [`UniversalRelativity.md`](UniversalRelativity.md) §3a |
| **Hodge conjecture — the cohomology build + the `(p,q)` structure** | ✅ **Reformulation complete; thread closed at its honest floor** — both sides of the Hodge picture are concrete substrate objects: the **algebraic** side a graded ℚ-**subalgebra** (the cohomology build `QLF_GradedCohomology`→`QLF_CohomologyRing`→`QLF_CohomologyLinear`→`QLF_CohomologyAlgebra`, the image of a ℚ-algebra hom `cl` from the cycle ring), and the **transcendental** side a genuine pure Hodge structure (`QLF_HodgeStructure` — weight, Hodge numbers, the real structure = the substrate `H↔H†`, Tate/Lefschetz objects, odd-weight vanishing). The gap is located at **one** input — **geometric realization / polarization** (the bridge `substrate_realization_is_algebraic`), which carries the conjecture's full strength and is where the classical difficulty lives. **No further substrate scaffolding can close it** (the swings showed even codim-1 Lefschetz needs a real cohomology theory of varieties = the open program). The one non-scaffolding path is QLF's thesis as a long research bet (emergent Kähler geometry + period map). Thread **closed as far as the substrate reaches** (the bridge stays a 🧱 boundary; see the Hodge boundary row below) | [`lean/QLF_HodgeStructure.lean`](lean/QLF_HodgeStructure.lean), [`Hodge_QLF.md`](Hodge_QLF.md), [`Millennium.md`](Millennium.md) |
| **Reversibility — reversible *logic*, irreversible *process*** | ✅ **Machine-verified (capstone)** — time-reversal **is** the Hermitian conjugate (`eval_dagger`), an *involution* (`antiparticle_involutive`, a bijection ⟹ reversible laws); the forward ZFA closure is *many-to-one* (`C(2n,n) ≥ 2` histories per closure for `n≥1` — `two_le_central_binom` + `disjunct_count_eq_central_binomial`) ⟹ non-injective ⟹ irreversible process. **`time_reverse_involutive_but_closure_degenerate`** packages both clauses; no new axioms. The arrow of time is the non-injectivity, not any failure of the reverse to exist; the `H↔H†` fixed points = the critical line (shared with Riemann/BSD/Hodge). **Energy conservation is the same lesson** — each event *creates* energy, half lent to the future = dark energy; global conservation is emergent-local (`Conservation.md` §2b). TOEs that axiomatize reversibility *or* global energy conservation fail by mistaking the present-local closure balance for the whole | [`lean/QLF_Reversibility.lean`](lean/QLF_Reversibility.lean), [`Reversibility.md`](Reversibility.md), [`Conservation.md`](Conservation.md) §2b |
| **Muon-catalyzed cold fusion** | ✅ **Machine-verified (the QLF claim) + SM agreement** — muon-catalyzed fusion = the *legitimate* cold fusion (room-temperature; distinct from Fleischmann–Pons), reproduced in agreement with the Standard Model. QLF owns: **catalysis touches the rate, never the β⁺ necessity** (`catalyzed_join_still_requires_beta`, `catalysis_preserves_necessity`); "cold" = crossing the density threshold by **generation-depth** not temperature; **α-sticking** = the muon blanket captured into the deep ⁴He closure. Open (SM/engineering, **not** a QLF gap): the muon economy (~2× energy-negative — production cost + α-sticking), `muon_catalysis_in_progress` | [`lean/QLF_MuonCatalysis.lean`](lean/QLF_MuonCatalysis.lean), [`Fusion.md`](Fusion.md) §3b |
| **Information synthesis = disjunctive (OR) closure** | ✅ **Machine-verified** — a ZFA closure takes the random possibility stream and **closes on an OR condition** (`List.any verify` = the Boolean OR-fold): `disjunctive_closure` (the OR *is* the existential), `disjunct_count_eq_central_binomial` (`C(2n,n)` satisfying disjuncts), `closure_always_fires` (always satisfiable). MRE picks the maximally-relevant disjunct — one bit `log 2`/event. No new axioms | [`lean/QLF_InfoSynthesis.lean`](lean/QLF_InfoSynthesis.lean), [`MRE.md`](MRE.md) §2.5 |
| **Horizon temperature (Unruh / Hawking / de Sitter)** | ✅ **Machine-verified (unification)** — all three are the Unruh master `T = ℏa/(2πck_B)` at the right acceleration, the `2π` = loop phase; Hawking `ℏc³/(8πGMk_B)` (`hawking_temperature_eq`), de Sitter `ℏH₀/(2πk_B)` (`desitter_temperature_eq`); dark-sector tie `a₀ = cH₀/(2π)` (`mond_accel_is_hubble_over_loop`). Algebraic unification + loop-phase ID, not from-scratch QFT-in-curved-spacetime | [`lean/QLF_HorizonTemperature.lean`](lean/QLF_HorizonTemperature.lean), [`Gravity_From_Delay.md`](Gravity_From_Delay.md) §5.1 |
| **Spin demystified — spin IS the twists** | ✅ **Machine-verified** — 720°/SU(2)→SO(3) double cover (`rotation_360_eq_negI`, `rotation_720_eq_id`, `spin_double_cover_nontrivial`), worked qucalc folds incl. the electron fold `^<v>=−I` (`fold_electron`), charge conjugation = view-from-behind (`C_eq_motional_reversal`), integer spin = composite half-spins, like-spin exclusion / opposite-spin singlet. Naming defs (charge/chirality), no new axiom | [`lean/QLF_Spin.lean`](lean/QLF_Spin.lean), [`Spin_QLF.md`](Spin_QLF.md) |
| **Hadrons are quantum black holes** | ✅ **Machine-verified (unification)** — every hadron = Markov-blanket horizon; Compton–Schwarzschild crossing at the Planck mass (`compton_eq_schwarzschild_iff`), area law `S=4πR²log2`, meson/baryon split; decay = Hawking evaporation. Not a mass derivation (`R` is an input) | [`lean/QLF_QuantumBlackHole.lean`](lean/QLF_QuantumBlackHole.lean), [`Hadron_BlackHoles.md`](Hadron_BlackHoles.md) |
| **Dark matter = denser logic near masses** | 🟢 **Derived + blind-tested** — the rotation-curve law is the closure-balance **RAR** `g_obs²=g_bar·(g_obs+a₀)` (`radialAccel_self_consistent`, both limits exact); the **blind SPARC benchmark** (#77, 147 curated galaxies, baryonic-only, SHA-256-sealed) reproduces the Radial Acceleration Relation **parameter-free** at the observational floor (`0.133 dex`, zero offset) with the derived `a₀=cH₀/2π` — = best-fit MOND, vs Newton (×2.7), vs NFW (294 fit params). Transition radius, Tully–Fisher, Gaussian MRE bump also Lean-anchored. **`1/2π` prefactor confirmed** by the SPARC fit at the local `H₀` (`a₀=cH₀/2π` at `H₀=72.9`, <1%; the ~13% was a wrong-form comparison — residual = the Hubble tension). **The `2π` is derived** (`QLF_MondScale`): it is the **ZFA closure-loop period** `τ_ZFA` — `a₀ = cH₀/τ_ZFA` is the Hubble acceleration per closure loop, `H₀` the horizon's *angular* rate (the de Sitter `T=ℏH₀/(2πk_B)` is its evidence), `τ_ZFA = 2·π_QLF` census-grounded (`QLF_PhysicalPi`); not a fitted constant. **And the interpolation function `ν` is derived as *unique*** (`QLF_MondNu`): the closure-balance ZFA conjunction `g_obs²=g_bar·(g_obs+a₀)` has a **unique** non-negative solution (`radialAccel_unique`), `g_obs=ν(g_bar/a₀)·g_bar` with `ν(y)=(1+√(1+4/y))/2` (`radialAccel_eq_nu`) — fixed by the principle, not chosen from the MOND family. **And the structural reading of the conjunction is derived** (`QLF_RarBalance`): the squared/multiplicative form is forced by the logarithmic free energy (`QLF_FreeEnergy`, `ΔF=−log 2`) — ZFA balance puts the observed closure at the *average* of the two conditions' free energies, and since `F=−log` an average of logs is a geometric mean = the squared form (`rar_is_free_energy_balance`). **Dark-matter sector closed** to its honest floor — scale (`cH₀`), prefactor (`1/2π` = closure-loop period), shape (unique `ν`), and the conjunction's structure all derived; the only premises left are acceleration-as-closure-rate + balance-as-free-energy-average | [`lean/QLF_MondScale.lean`](lean/QLF_MondScale.lean), [`lean/QLF_MondNu.lean`](lean/QLF_MondNu.lean), [`lean/QLF_RarBalance.lean`](lean/QLF_RarBalance.lean), [`DarkMatter.md`](DarkMatter.md), [`SPARC.md`](SPARC.md) |
| **Neutrino is Majorana → 0νββ** | ✅ **Machine-verified** — `neutrino_majorana` ([`lean/QLF_Majorana.lean`](lean/QLF_Majorana.lean)): the antiparticle is the Hermitian conjugate (conjugate-and-reverse), and the `^v` loop is a fixed point of it (the electron is not — `electron_not_majorana`, so it is Dirac). The neutrino is the unique self-conjugate fermion ⟹ lepton number violated ⟹ **neutrinoless double-beta decay** is the signature (LEGEND/nEXO). Conditional on the `^v` assignment + antiparticle = Hermitian-conjugate | [`lean/QLF_Majorana.lean`](lean/QLF_Majorana.lean), [`Beta_Decay_Neutrino_Nature.md`](Beta_Decay_Neutrino_Nature.md) §1, [`Experimental_Consistency.md`](Experimental_Consistency.md) §9–10 |
| **Pauli closure** — count balance ⟹ Pauli scalar, all twist histories (incl. cross-axis interleaving) | ✅ **Closed** — `count_balanced_pauli_closed` | [`lean/QLF_TwistAlphabet.lean`](lean/QLF_TwistAlphabet.lean), [`Experimental_Consistency.md`](Experimental_Consistency.md) §2.1 |

---

## Principled boundaries (not gaps)

| Item | Why it is a boundary | Where |
|---|---|---|
| **Riemann critical line** | Substrate bridges proven; RH reduced to one explicit boundary, `spectral_hilbert_polya` (RCA₀ → WKL₀ crossing). Now **constructively scaffolded** by the MRE bridge: `Z_QLF` concrete, MRE saturation grounded in `binary_kl` and located at the critical-line prior `1/2`, refining the boundary to `MRE_bridge` (`riemann_hypothesis_in_qlf_via_MRE`). The residual Mellin↔ζ step is the analytic sector QLF's thesis identifies as where ZFC's continuum machinery is pathological — the honest open bridge, not a discharged one (RH is not a known independence result; `rh_proof_in_progress`) | [`lean/QLF_Riemann.lean`](lean/QLF_Riemann.lean), [`lean/QLF_RiemannMRE.lean`](lean/QLF_RiemannMRE.lean) |
| **Yang–Mills mass gap** | Gap proven on the substrate (lightest non-vacuum closure = one `log 2` quantum; `mass_gap_quantum_pos`, `gaugeMassGap = log 2 > 0`); only the continuum-QFT reconstruction remains, carried by the explicit boundary axiom `yang_mills_continuum_gap` — the continuum sector QLF's thesis flags as ZFC-pathological, stated as the honest open bridge (`mass_gap_proven_constructively` on the substrate) | [`lean/QLF_MassGap.lean`](lean/QLF_MassGap.lean), [`YangMills_MassGap_QLF.md`](YangMills_MassGap_QLF.md) |
| **P vs NP** | Lean-anchored: the realized (verifiable) set IS the O(n) verify-filter of the generated candidates (`realized_is_verify_filter`) with cardinality the real `C(2n,n)` (`realized_count_eq_central_binomial`, reusing `find_stable_states_length_even`). The formal separation is the boundary axiom `generate_not_reducible_to_verify`, over an abstract cost model — the honest open bridge (P vs NP is a *finitary* statement, not a known independence phenomenon, so "ZFC's defect" does not apply) | [`lean/QLF_PvsNP.lean`](lean/QLF_PvsNP.lean), [`P_vs_NP_QLF.md`](P_vs_NP_QLF.md) |
| **Navier–Stokes smoothness** | Lean-anchored: 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; blow-up = non-terminating history pruned by `full_zeno_prune`. Only continuum-PDE inheritance remains — the boundary axiom `navier_stokes_continuum_limit`, the continuum sector QLF's thesis flags as ZFC-pathological, stated as the honest open bridge | [`lean/QLF_NavierStokes.lean`](lean/QLF_NavierStokes.lean), [`NavierStokes_QLF.md`](NavierStokes_QLF.md) |
| **Birch–Swinnerton-Dyer** | Self-dual central point `s=1` proven (`bsd_central_point_self_dual`), grounded in the same `H↔H†` involution as Riemann (`bsd_riemann_shared_involution`); the **elliptic-curve→closure encoding is built** — concrete `EllipticCurveQLF` with computed Frobenius traces (`frobeniusTrace`, `Ecn1_frobenius_two`). **The gap is faithfulness:** `rank = ord` (`bsd_rank_equals_order`) and `bsd_in_qlf` follow from the bridge `modularity_mirror_invariant` (mirror preserves the central multiplicity at the self-dual fixed point), which on BSD has the conjecture's full strength. *(Contrast: the classical BSD conjecture is not proved here.)* (`bsd_proof_in_progress`) | [`lean/QLF_BSD.lean`](lean/QLF_BSD.lean), [`BSD_QLF.md`](BSD_QLF.md), [`Langlands.md`](Langlands.md) |
| **Hodge conjecture** — ✅ **reformulation complete (substrate side closed); residual = the 🧱 geometric-realization bridge** | Both sides of the Hodge picture are built concretely on the substrate. **Proven (no axiom):** Hodge classes are exactly the substrate-realized closures (`hodge_realized_on_substrate`; the Hodge conjugation = the adjoint `H↔H†`, `conj_involutive`; Hodge classes = its balanced fixed points, `conj_fixed_of_isHodge`). **The algebraic side complete** — the cohomology build (`QLF_GradedCohomology` → `QLF_CohomologyRing` → `QLF_CohomologyLinear` → `QLF_CohomologyAlgebra`) gives a graded ℚ-**subalgebra**, the image of a ℚ-algebra homomorphism `cl` from the cycle ring. **The transcendental side built** — `QLF_HodgeStructure` (weight, bigraded Hodge numbers, the real-structure symmetry = the substrate `H↔H†`, Tate/Lefschetz objects, Hodge classes with odd-weight vanishing). **The gap is located at exactly one input: geometric realization / polarization** — *which* Hodge structure the substrate's cohomology carries (its periods) — which is precisely where the classical difficulty lives. **This is the honest floor: no further substrate scaffolding can close it** — the bridge `substrate_realization_is_algebraic` carries the conjecture's full strength, and the faithfulness swings (`QLF_HodgeExpSequence`) showed even the codim-1 Lefschetz `(1,1)` case is out of reach without a genuine cohomology theory of varieties (= the open program, not a module). The one non-scaffolding path is QLF's thesis itself: build the substrate's emergent Kähler geometry + period map and test whether it *forces* Hodge → algebraic (a long research bet, not a commit). *(Contrast: the classical Hodge conjecture — finite ℚ-linear algebra, not independence — is not proved here.)* Thread **closed as far as the substrate reaches** (`hodge_proof_in_progress`). B/C/D share the same one bridge (`standard_conjectures_on_substrate`). | [`lean/QLF_Hodge.lean`](lean/QLF_Hodge.lean), [`lean/QLF_HodgeStructure.lean`](lean/QLF_HodgeStructure.lean), [`Hodge_QLF.md`](Hodge_QLF.md), [`Grothendieck_QLF.md`](Grothendieck_QLF.md) |
| **Speed of light `c`** | The substrate event quantum (one Planck length × one Planck tick *together*) sets `c = L_P/τ_P` — no Tier-3 below it | [`Experimental_Consistency.md`](Experimental_Consistency.md) §3, [`Kitada_Local_Time_GR.md`](Kitada_Local_Time_GR.md) §5.3 |
| **Planck scale / substrate granularity** | **The Planck *scale* is the closure floor by construction — not a free input.** The minimal coherent Markov-blanket closure is the Compton–Schwarzschild self-dual point `μ²=1/2`: below the Planck length a blanket is inside its own horizon and cannot close (`coherent_iff_subplanck`, `planck_length_floor`, `planck_self_dual`, reusing the `QLF_QuantumBlackHole` crossing). What remains is **not a flaw**: the SI *value in metres* is a unit convention, and the matter-depth-above-floor is the `14π` hierarchy (`QLF_AlphaS`, tracked at *Cosmic depth / hierarchy*) | [`lean/QLF_PlanckScale.lean`](lean/QLF_PlanckScale.lean), [`Planck_Scale.md`](Planck_Scale.md) |
| **Bethe constant `k(n,0)`** (Lamb shift) | 🧱 **Boundary** — continuum-dominated (`I_1S ≈ 19.77 Ry`, all bound `ΔE < 1 Ry`); free-electron sector above the RCA₀ floor | [`Lamb_Shift.md`](Lamb_Shift.md) §6.1, [`bethe_log_demo.py`](bethe_log_demo.py) |

---

## Open — quantitative (the hard front)

| Item | Status | Where |
|---|---|---|
| **Nuclear fusion / the β⁺ keystone** | 🔵 **Open — quantitative (necessity Lean-anchored)** — fusion is two Markov blankets joining; two *identical* proton blankets have **no** bound fermionic channel (`pauli_exclusion`, no diproton), so the pp-chain's first join `p+p→²H+e⁺+ν` *must* convert one proton to a neutron by a weak β⁺ step to make the pair distinguishable — the proton/neutron "sex" (`pp_join_requires_distinguishability`). Open: the β⁺ **rate** (the weak `G_F` that sets how slow the pp-chain is — same open weak sector, `fusion_weak_rate_in_progress`) | [`lean/QLF_Fusion.lean`](lean/QLF_Fusion.lean), [`Fusion.md`](Fusion.md) §3a, [`SEX.md`](SEX.md) |
| **Muon `g−2`** | 🔵 **Open — quantitative (placed honestly)** — leading `a_μ = α/2π = a_e` (universal, `a_mu_leading_eq_a_e`, ~0.6%); the muon's `(m_μ/m_e)²≈42753` hadronic-sensitivity amplification (`hadronic_sensitivity_value`) is why the discrepancy is a muon effect. The residual is the hadronic-vacuum-polarization sector — QLF's open hadronic frontier (pion-dominated) **and** experimentally unsettled (data-driven ~5σ vs lattice/CMD-3 ~1σ); QLF claims no new-physics anomaly (`muon_g2_in_progress`) | [`lean/QLF_MuonG2.lean`](lean/QLF_MuonG2.lean), [`g_minus_2.md`](g_minus_2.md) §4a |
| **Gravitational waves** | 🔵 **Open — quantitative (features Lean-anchored)** — a GW is a massless transverse ripple of synthesized spacetime ⇒ speed `= c` (`gw_speed_eq_planck_ratio`, GW170817 to `10⁻¹⁵`); graviton spin-2 = four half-spins (`graviton_integer_spin`); 2 transverse polarizations from masslessness (`massless_two_polarizations`). Open: the linearized wave equation `□h_μν=0` and the quadrupole luminosity — they need the *dynamical* substrate metric (the same gap as the full Einstein field equations), `gravitational_waves_in_progress` | [`lean/QLF_GravitationalWaves.lean`](lean/QLF_GravitationalWaves.lean), [`GR_Schwarzschild.md`](GR_Schwarzschild.md) |
| **Running couplings / renormalization** | 🔵 **Open — quantitative (structure Lean-anchored)** — one-loop log running `1/α(t)=1/α₀+(b/2π)·t` with the `2π` loop phase (`inv_coupling`); asymptotic freedom (`asymptotic_freedom`) vs screening; the Landau pole located (`landau_pole_location`) but **cut off by the substrate's discrete UV floor** ⟹ no continuum UV catastrophe. **The strong β-coefficient is substrate-fixed**: `b₀ = 11N_c/3 − 2n_f/3 = 7` from `N_c=3` (axes) + `n_f=6` (3 gens × 2 flavours) (`beta_coefficient_eq_seven`, `QLF_BetaFunction`), feeding `ln R_p = 2π/(7 α_s)`. Open: the electroweak `b_i`, the GUT scale, and `α_s` — so `sin²θ_W 3/8→0.231` and the hierarchy *value* are consistent-with not derived. **Scale of α:** the **leading value** `α=1/137` is the fully-rendered-3D **IR (`q²→0`) anchor** — bounds Lean-verified `137 < α⁻¹ < 137.048` (`QLF_AlphaBound`), residual to the measured `137.036` open; the QED running reads as the effective-dimension flow `3→2` toward the UV (direction structural via `alpha_QLF_2d_counterfactual`, magnitude open); and `α(0)` carries **no cosmological-time drift** (proven: `α(d)=1/(128+d²)` has no time argument — `no_cosmological_drift_of_alpha`), a falsifiable prediction sharper than the SM ([**Alpha.md**](Alpha.md)) | [`lean/QLF_RunningCouplings.lean`](lean/QLF_RunningCouplings.lean), [`lean/QLF_BetaFunction.lean`](lean/QLF_BetaFunction.lean), [`TheContinuum.md`](TheContinuum.md) §3.1, [`Alpha.md`](Alpha.md) |
| **Weinberg angle `sin²θ_W`** | 🔵 **Open — quantitative (structural value Lean-anchored)** — at the unification scale `sin²θ_W = 3/8` = spatial/alphabet fraction = the SU(5) GUT normalization (`sin2_weinberg_substrate_eq`), the third constant from the 6+2 split (with α's `3²` and `Ω_Λ`'s `2/8`, `electroweak_substrate_signature`); tree-level `ρ=1`/`cos²θ_W=(M_W/M_Z)²` anchored. The RG running to the measured `0.231` at `M_Z`, and the absolute `W/Z`/`G_F` (Higgs VEV), stay open (`weinberg_running_in_progress`) | [`lean/QLF_WeinbergAngle.lean`](lean/QLF_WeinbergAngle.lean), [`Weak_Force.md`](Weak_Force.md) §2 |
| **Pion mass ratio `m_π±/m_e = 2/α`** | 🔵 **Open — quantitative** — `\|S₂\|=2` (two quarks) solid + arithmetic `2/α=274` (0.3%) Lean-verified (`pion_electron_ratio_eq`); the `1/α` from exposed chirality is a structural reading of Nambu's coincidence, not yet first-principles (`pion_mass_ratio_in_progress`) | [`lean/QLF_PionMassRatio.lean`](lean/QLF_PionMassRatio.lean), [`Pion_QLF.md`](Pion_QLF.md) |
| **Cosmic depth `n` / the hierarchy** | The geometric depth `n ≈ 6.7×10⁶⁰` is firm but defined via `R_H`; the hierarchy `R_p≈10¹⁹` is read as **dimensional transmutation with both inputs substrate-fixed**: `ln R_p = 2π/(b₀ α_s)` with `b₀=7` (`QLF_BetaFunction`, from `N_c=3`,`n_f=6`) and `α_s=1/b₀²` (`QLF_AlphaS`, running-consistent) ⟹ **`ln R_p = 2π·b₀ = 14π ≈ 43.98` vs measured 44.01 — 0.07%** (`hierarchy_log_eq_fourteen_pi`). So the hierarchy = `e^{14π}` from the single integer 7. **Bounds pass:** `ln R_p` is exp-sensitive to `α_s`, so the `0.07%` is the agreement *at the posit* — the running-consistent window `1/α_s∈[49,52]` gives the log-band `[14π, 104π/7]≈[43.98, 46.67]` (`hierarchy_log_band`), measured 44.01 inside near the `14π` edge (data implies `1/α_s≈49.0`, so `b₀²=49` is favoured); the integer-7 result is a clean *log*-level reduction, not a tight value prediction (band ≈ ×15 in value, `hierarchy_band_width`). Residual: `α_s=1/b₀²` as a *derivation* (running-consistent posit) + the ~3% value-level calibration | [`lean/QLF_AlphaS.lean`](lean/QLF_AlphaS.lean), [`lean/QLF_MassSpectrum.lean`](lean/QLF_MassSpectrum.lean), [`Per_Qubit_Mass_Quantum.md`](Per_Qubit_Mass_Quantum.md) §3.3b |
| **`H₀` from substrate** | Reduces to deriving `n` (above); currently `H₀` enters as one observable. Would close the last cosmological empirical input | [`Cosmological_Constant.md`](Cosmological_Constant.md) §196 |
| **Hubble tension** | The residual 8.7% in Λ tracks the Planck-vs-SH0ES `H₀` discrepancy; not predicted | [`Cosmological_Constant.md`](Cosmological_Constant.md) §197 |
| **`G` SI value / Einstein `8π·G` coefficients** | Form `G = L_P²c³/ℏ` derived; absolute SI value is substrate-quantum calibration (~37% prediction residual). **The `8πG` coefficient is Lean-anchored** via Jacobson's equation of state: `8πG = 2π/η`, `η=1/4G`, both inputs (area law + Unruh `T`) QLF substrate results (`einstein_coupling_from_thermodynamics`, [`lean/QLF_EinsteinEquations.lean`](lean/QLF_EinsteinEquations.lean)); same `8π=4π·2`; `Λ = Ω_Λ = log 2` = the Kitada local-clock tick | [`lean/QLF_EinsteinEquations.lean`](lean/QLF_EinsteinEquations.lean), [`Kitada_Local_Time_GR.md`](Kitada_Local_Time_GR.md) §5.2 |
| **Full Einstein field equations (tensor derivation)** | 🔵 **Open — both sides substrate-routed.** *Coefficient/equation of state* done (Jacobson: `8πG = 2π/η`, `Λ = log 2`, local horizon = Kitada clock). *Curvature side* is the concrete **causal-set order→metric program** (Sorkin / Benincasa–Dowker) on QLF's causal set (`QLF_ReachableEvent`); its **number↔volume / proper-time rung is Lean-anchored** — `causalInterval`, `intervalVolume = depth difference = Kitada tick count`, proper-time additivity (`QLF_CausalInterval`). **The Benincasa–Dowker curvature operator is Lean-anchored at its flat baseline** (`bdCoeff`, `bdCoeff_sum_zero`, `layerCard_chain`, `bdCurvature`, **`bdCurvature_chain_zero`**): the layer stencil `+1,−2,+1` is balanced, a single-history chain's in-range layers are singletons, so the BD reading on a chain of depth ≥2 collapses to `+1−2+1=0` — `R=0` in the actual operator (the 1-D discrete second difference annihilating a constant). Past the baseline, the Ricci scalar — *and the spatial dimensions* — are both the *growth* of layer cardinalities `|L_k|` once the closure graph branches (dovetails with the 3D graph-rendering, `SpaceTime.md` §3a). **2-D anchored + the branching layer-growth computed** (`QLF_CausalDimension`): the product of two chains = `1+1` Minkowski, volume = product of chain volumes; and the BD layer cardinality `prodLayerCard` of the actual product order grows from `1` (one history) to `2` (two combined — the apex's two immediate predecessors = the two null directions), `layer_growth_from_branching`, a size-independent dimension fingerprint (`prodLayerCard_link_stable`) — `|L_k|` growth past the `bdCurvature_chain_zero` flat baseline made concrete. **Statistical continuum limit anchored** (`QLF_CausalContinuum`): the Poisson occupation kernel `poissonOccupation` + its layer recurrence `poissonOccupation_succ` (proven — the discrete `|L_k|` counts pass to the sprinkling expectations), with the full `ρ→∞` Benincasa–Dowker convergence `→ −R/2` the explicit **bridge axiom `benincasa_dowker_limit`** (settled CST Poisson+Lorentzian machinery, the `RCA₀→analytic` boundary parallel to `yang_mills_continuum_gap`/`navier_stokes_continuum_limit`), from which `flat_curvature_zero_in_mean` (flat ⟹ `R=0` in the mean) is derived. **So the Einstein curvature side has the Millennium shape — verified discrete core + one continuum bridge.** **Open (`einstein_curvature_in_progress`/`causal_dimension_in_progress`):** general `d≥3`, and assembling the full tensor `G_μν = 8πG T_μν` from the BD action | [`lean/QLF_EinsteinEquations.lean`](lean/QLF_EinsteinEquations.lean), [`lean/QLF_CausalInterval.lean`](lean/QLF_CausalInterval.lean), [`Einstein_Equations.md`](Einstein_Equations.md) §6a |
| **First-principles `R_e` / absolute scale** | `α R_e = m_e` identifies `R_e` with the measured electron; deriving `R_e` from closure-multiplicity is open. **Reframed (`QLF_MassSpectrum`):** the *whole* spectrum is one scale `m_p` × verified ratios (`spectrum_one_scale`; `m_e=m_p/6π⁵`), and `R_p` is exponentially generated by dimensional transmutation — so only **one** number (`b`, `α_s`, calibration / the `R_e≈2.4×10²²` count) is open | [`lean/QLF_MassSpectrum.lean`](lean/QLF_MassSpectrum.lean), [`Per_Qubit_Mass_Quantum.md`](Per_Qubit_Mass_Quantum.md) §3.3a |
| **Mass spectrum from multiplicity** | 3rd-generation masses; τ-decay-vertex topology. **Handle:** Koide `Q=2/3` is **machine-verified** as following by construction from `N=3` (three axes) ∧ `A²=2` (two transverse axes) — `koide_two_thirds`, [`lean/QLF_Koide.lean`](lean/QLF_Koide.lean) — and predicts `m_τ` from `m_e,m_μ` to **0.006%** (`Weak_Force.md §5a–5b`). Still open: the lepton-√mass↔axis-phase *identification*, the Koide angle, the scale (so `m_e,m_μ` are inputs). **Quark sector reframed** (`QLF_QuarkMass`): quark masses are *not* closure observables (confinement — `quark_not_closed`), so the target is the hadron mass *splittings* (`m_n−m_p`), not a quark-mass relation; the neutrino mass is **Majorana** (`QLF_NeutrinoMass`) | [`Standard_Model.md`](Standard_Model.md) §4.1, [`Weak_Force.md`](Weak_Force.md) §5b |
| **Weak sector (W/Z)** | Weak-isospin **SU(2) Lie algebra machine-verified** in Σ₈ (`weak_isospin_su2`, `Q₈⊂SU(2)`); still open: `R_W`/`R_Z` (hence W/Z masses + Weinberg-angle value), coupling `g`, `G_F`, flavor-change & τ-decay vertex topology, the Koide angle `δ` (lepton-sector input; `2/9` a flagged coincidence) | [`Weak_Force.md`](Weak_Force.md), [`lean/BraKetRhoQuCalc.lean`](lean/BraKetRhoQuCalc.lean) |
| **Gauge unification (forces from 3 axes)** | Structural: `dim(U(1)×SU(2)×SU(3)) = 12 = 1+3+8`, with `1+8 = 9 = N` (the α tensor). **The gauge algebras *and* the gauge dynamics are machine-verified** — the three algebras (U(1) `no_magnetic_monopoles`, SU(2) `weak_isospin_su2`, SU(3) `trace_commutator_zero`+`gluon_commutator_nonzero`); the gauge *force* as the **holonomy** of the closure connection (`QLF_GaugeHolonomy`: abelian-flat photon vs curved non-abelian `W`/gluon); **confinement** = the singlet-closure obstruction (`QLF_Confinement`); **mass = the gauge-fold delay** with custodial `ρ=1` (`QLF_HiggsMechanism`); and **weak chirality / parity violation** (`QLF_WeakChirality`). Open: the coupling *values* `g₁,g₂,g₃`, the string tension, and the Higgs VEV — the value sector (couplings root in α + one mass, `Forces_From_Alpha.md`) | [`Forces_From_Three_Axes.md`](Forces_From_Three_Axes.md), [`lean/QLF_GaugeHolonomy.lean`](lean/QLF_GaugeHolonomy.lean) |
| **Constants program** (π, e, δ; α below the 0.026% floor) | Methods exist in `constants_mapper.py`; full CODATA agreement is the active research front | [`Experimental_Consistency.md`](Experimental_Consistency.md) §6.3, §11 |
| **Lamb shift radiative pieces** | AMM `+68 MHz` (Schwinger `α/2π` on the bound moment) and vacuum polarization (Uehling) `−27 MHz` taken as inputs | [`Lamb_Shift.md`](Lamb_Shift.md) §8 |
| **Condensed matter (quantum Hall, superconductivity)** | 🔵 **Open — quantitative (anchors Lean-verified)** — von Klitzing `R_K = Z₀/(2α) = Z₀·137/2` from the substrate α (`von_klitzing_substrate`, 0.026%); integer-QHE plateaus `R_xy = R_K/ν`; Cooper pair = boson (`cooper_pair_boson`). **Anyon statistics anchored** — 2D braiding gives a continuous phase `e^{iθ}` (3D forces `±1`; `QLF_Anyons`, `boson_phase`/`fermion_phase`/`double_braid`). Open: the BCS gap equation, the FQHE *filling fractions* `ν` / the Laughlin wavefunction, topological band structure (`condensed_matter_in_progress`, `anyons_in_progress`) | [`lean/QLF_CondensedMatter.lean`](lean/QLF_CondensedMatter.lean), [`lean/QLF_Anyons.lean`](lean/QLF_Anyons.lean), [`Electricity.md`](Electricity.md) §6–§7 |
| **CKM / PMNS mixing** | 🔵 **Open — quantitative (count + CP condition + unitarity Lean-anchored)** — 3 generations ⟹ exactly 3 mixing angles + 1 CP phase (`substrate_mixing_parameters`), Kobayashi–Maskawa (CP needs ≥3 generations, `cp_requires_three_generations`), and the mixing matrix is **unitary** (`cabibbo_row_unitarity`/`cabibbo_rows_orthogonal`, `QLF_CKM` — `V Vᵀ=I` = flavor conserved by closure). Because the neutrino is **Majorana**, **PMNS carries 2 extra Majorana phases** (`pmns_total_cp_phases = 1 Dirac + 2 Majorana = 3`, `QLF_PMNS`), unlike CKM's one. Open: the angle *values* (Cabibbo, PMNS) + the Dirac/Majorana phases — the Yukawa sector; quark-small vs lepton-large is the hidden/exposed-chirality reading (`flavor_mixing_in_progress`) | [`lean/QLF_CKM.lean`](lean/QLF_CKM.lean), [`lean/QLF_PMNS.lean`](lean/QLF_PMNS.lean), [`Standard_Model.md`](Standard_Model.md) §4.2 |
| **Neutrino masses / oscillations / seesaw** | Nature solved — neutrino is **Majorana** (`neutrino_majorana`, ✅ above). Open: the tiny masses (`m ∝ 1/R` with very large depth `R`), the PMNS mixing angles + mass-squared splittings (oscillation = gauge-fold harmonic desync, `Frequency_Synchronization.md`), and the seesaw — none quantitatively derived | [`Beta_Decay_Neutrino_Nature.md`](Beta_Decay_Neutrino_Nature.md), [`Standard_Model.md`](Standard_Model.md) §4.2 |
| **Baryogenesis (matter–antimatter asymmetry)** | 🔵 **Open — quantitative (Sakharov conditions Lean-anchored)** — all three hold: B-violation (matter/antimatter opposite winding, `matter_antimatter_opposite` from `baryon_dagger_odd`; `B−L` via Majorana), C/CP violation (chirality engine + `QLF_StrongCP`), out-of-equilibrium (`QLF_CosmicInflation`) ⟹ asymmetry generic. Open: the *magnitude* `η_B ≈ 6×10⁻¹⁰`, undetermined as in the SM (`baryogenesis_in_progress`) | [`lean/QLF_Baryogenesis.lean`](lean/QLF_Baryogenesis.lean), [`CP-Violation-and-Chirality.md`](CP-Violation-and-Chirality.md) §4b |
| **Strong CP problem (`θ̄ ≈ 0`)** | ✅ **Mechanism Lean-anchored** — the `θ`-term is a CP-odd topological winding, and every CP-odd signed count is **zero on every ZFA closure** (`theta_zero_on_closure` / `cp_odd_winding_zero_on_closure`, reusing `wcount_zero_on_ZFA`) ⟹ `θ̄ = 0` with **no axion**, ZFA closure doing the Peccei–Quinn job. Structural: the QCD θ-vacuum↔winding identification is not field-theoretically constructed (`strong_cp_in_progress`) | [`lean/QLF_StrongCP.lean`](lean/QLF_StrongCP.lean), [`CP-Violation-and-Chirality.md`](CP-Violation-and-Chirality.md) §4a |

---

## Open — structural / Lean-anchoring

| Item | Status | Where |
|---|---|---|
| **Grothendieck's dream on the substrate** (motives + the Millennium spine) | 🟣 **Reformulation, not a proof** — the standard conjectures (Hodge, B, C, D) are *reformulated* as a verified discrete core (`count_balanced_pauli_closed`, a theorem about twist strings) + **one bridge axiom `substrate_realization_is_algebraic` of full conjecture strength** (on Hodge classes it *is* Hodge; `isAlgebraic` abstract). `hodge_class_is_algebraic` etc. are *derivations from that axiom*, not proofs. **Genuinely built** (real structures/theorems): the **motive object** (`QLF_Motives`), the **motivic Galois group** as a group (`QLF_MotivicGalois`), the **anabelian** full-faithful functor (`QLF_Anabelian`), the **anabelian/Galois sequence** (`QLF_AnabelianGalois`), and **`π`,`ζ(3)` from the census** (`QLF_PhysicalPi`, `QLF_AperyPeriod` — Wallis/Apéry, classical). The standard conjectures are **finite ℚ-linear algebra, not independence phenomena** — so "ZFC's defect" does *not* apply. The defensible claim is the substrate ontology + the reformulation, a conjectural synthesis. **Cohomology built** — the cohomology build (`QLF_GradedCohomology`→`QLF_CohomologyRing`→`QLF_CohomologyLinear`→`QLF_CohomologyAlgebra`) gives the algebraic side as a graded ℚ-**subalgebra**, and `QLF_HodgeStructure` gives the transcendental `(p,q)` side; so the bridge no longer "carries everything" — both sides are concrete and the gap is reduced to **geometric realization** (the genuine open problem). **The Hodge sub-thread is closed at its honest floor** — see the Hodge rows above and the closure capstone in [`Hodge_QLF.md`](Hodge_QLF.md). | [`Grothendieck_QLF.md`](Grothendieck_QLF.md) (§1, §5 reconciled to the closure), [`Hodge_QLF.md`](Hodge_QLF.md) (closure capstone), [`lean/QLF_CohomologyAlgebra.lean`](lean/QLF_CohomologyAlgebra.lean), [`lean/QLF_HodgeStructure.lean`](lean/QLF_HodgeStructure.lean), [`Millennium.md`](Millennium.md), [`lean/QLF_AnabelianGalois.lean`](lean/QLF_AnabelianGalois.lean) |
| **Why three fermion generations** | 🟣 **Structural (Lean)** — generation count = `substrate_spatial_dimension = 3` (`num_generations_eq_three`); the *same* `3` behind Koide (N=3 phases), colour SU(3), and α (`N=9=3²`) — `three_axis_signature` — with the 3 generations realized concretely as Koide's three 120° phases (`three_generations_satisfy_koide`). Reduces "why 3 generations" to "why 3 spatial dimensions" — and that is **derived**, not deferred: 3 is the *minimal dimension in which any relational/causal graph renders faithfully* (every finite graph embeds crossing-free in ℝ³; 2D fails for non-planar graphs), so the closure graph's faithful rendering (space) is minimally 3D ([`SpaceTime.md`](SpaceTime.md) §3a, [`lean/QLF_ReachableEvent.lean`](lean/QLF_ReachableEvent.lean)). Newton `1/r²`, magic numbers, α=N=3² are cross-checks, not posits | [`lean/QLF_Generations.lean`](lean/QLF_Generations.lean), [`SpaceTime.md`](SpaceTime.md) §3a |
| **Lamb prefactor `4/(3π n³)`** | Mostly resolved: `= 4·(2/3)·(1/(2π))·(1/n³)` (Lean `lamb_prefactor_loop_phase`); the π is the g-2-validated loop-phase primitive (0.2%), `1/n³`/`2/3` clean. Only the rational `4` (two-vertex/solid-angle) wants a cleaner origin | [`Lamb_Shift.md`](Lamb_Shift.md) §5 |
| **Dirac correction, per-mechanism Lean** | Kinematic / spin-orbit / Darwin α² pieces are doc-anchored, not yet individual Lean chains from [`QLF_Pauli`](lean/QLF_Pauli.lean)/`QLF_TwistAlphabet` | [`Dirac_Correction.md`](Dirac_Correction.md) §6 |
| **Lorentz boost as a Lean theorem** | ✅ **Machine-verified** — the Lorentz boost is now a Lean theorem in spinor form: `boostZ_action` ([`lean/QLF_LorentzCover.lean`](lean/QLF_LorentzCover.lean)) proves the `SL(2,ℂ)` diagonal `diag(a,b)` (`a·b=1`) acts on the Hermitian state as a boost, rescaling the null coordinates `u=t+z↦a²u`, `v=t−z↦b²v`. (The frequency-of-basis reading of `Cross_Frequency_Lorentz.md` §7 is the same boost in the `f=1/t` picture.) | [`lean/QLF_LorentzCover.lean`](lean/QLF_LorentzCover.lean), [`Cross_Frequency_Lorentz.md`](Cross_Frequency_Lorentz.md) §7 |
| **Maxwell curl laws** (`∇×B=μ₀J`, `∇×E=−∂B/∂t`) | ✅ **Conservation form machine-verified** (#93, `QLF_MaxwellCurl`): on the time-indexed event sequence, Faraday's EMF telescopes to minus the net flux change (`faraday_integral`), so a closed magnetic cycle induces zero net EMF (`faraday_closed_cycle` — Faraday as a ZFA closure); Ampère–Maxwell is the dual with source + displacement current (`ampere_integral`). With `∇·B=0` (`no_magnetic_monopoles`) all four are substrate-anchored at the conservation level. The full 3-D vector `∇×` (Stokes on the synthesized metric) is the continuum rendering | [`lean/QLF_MaxwellCurl.lean`](lean/QLF_MaxwellCurl.lean), [`Maxwell.md`](Maxwell.md), [`Electricity.md`](Electricity.md) |
| **γ (Euler–Mascheroni) convergence** | Structural form Lean-anchored; `lim (H_N − ln N) = γ` convergence proof deferred (standard real analysis) | [`lean/QLF_EulerMascheroni.lean`](lean/QLF_EulerMascheroni.lean) |
| **Borromean 5-angle** | `chirality-mixing-per-pair = 2` not yet derived rigorously from [`QLF_Pauli`](lean/QLF_Pauli.lean)'s scalar group | [`lean/QLF_BorromeanAngles.lean`](lean/QLF_BorromeanAngles.lean) |
| **Charge vs `B−L`** | **Charge conservation ✅ Lean-anchored** (`signed_count_conserved`); every closure is neutral. **`B−L` is not a conserved signed count** — proved via `wcount_zero_on_ZFA` (conserved counts vanish on closures, but the deuteron has `B−L=1`; baryon vs antibaryon share a twist multiset yet `B−L=±1`). `B−L` is at most winding, and in the lepton sector it is **violated** (neutrino Majorana, `neutrino_majorana`) ⟹ 0νββ. So only the gauge charge is exact — QLF carries no exact global `B−L`. **Baryon number ✅ Lean-anchored as a signed 3-axis linking (winding) invariant** — `baryonNumber` ([`lean/QLF_BaryonWinding.lean`](lean/QLF_BaryonWinding.lean)): proton `>^/` `B=+1`, antiproton `B=−1`, leptons & meson `B=0`; `baryon_zero_of_noZ` proves the whole z-free lepton/EM sector is baryon-neutral; and **`baryon_dagger_odd` proves the general conjugation-oddness** `B(ts†) = −B(ts)` for *all* histories (so baryon/antibaryon carry `±B` universally). ✅ Closed | [`lean/QLF_BaryonWinding.lean`](lean/QLF_BaryonWinding.lean), [`lean/QLF_Majorana.lean`](lean/QLF_Majorana.lean), [`Conservation.md`](Conservation.md) §8 |

---

## Future work (scope-limited by specification)

| Item | Where |
|---|---|
| Periodic table `Z ≥ 21` (d-shell synthesis; Cr/Cu/La anomalies) — current routing capped at neon | [`Magic_numbers.md`](Magic_numbers.md) |
| QuantumOS active-inference scheduler on QPU silicon (today: browser control plane) | [`Crystal_QuantumOS.md`](Crystal_QuantumOS.md) §7 |
| Quantitative delayed-choice visibility match (Kim et al. 1999) | [`Delayed_Choice_Eraser.md`](Delayed_Choice_Eraser.md) |
| Strong-field FLRW coupling for the cosmological constant | [`Cosmological_Constant.md`](Cosmological_Constant.md) |
| Cosmic inflation — initial conditions / e-folds / `n_s` / `r` / reheating, and the vacuum-frequency evolution `f(t)`, remain open. **Structure Lean-anchored:** inflation and dark energy are the same `w=−1` event-synthesis field at two energy scales (no inflaton — `inflation_and_dark_energy_same_field`); early high-`V` ⇒ faster expansion (`higher_energy_faster_expansion`) | [`lean/QLF_CosmicInflation.lean`](lean/QLF_CosmicInflation.lean), [`Curvature.md`](Curvature.md) §8 |
| BBN primordial abundances — **`Y_p = 2r/(1+r)` funnel Lean-anchored** (neutrons → ⁴He, `r≈1/7 ⟹ Y_p≈1/4`, matching 0.247; `helium_fraction_one_seventh`). Open: `r` itself (n–p splitting + `G_F`), D/⁷Li abundances, and the CMB power spectrum (`nucleosynthesis_in_progress`) | [`lean/QLF_Nucleosynthesis.lean`](lean/QLF_Nucleosynthesis.lean), [`Fusion.md`](Fusion.md) §7a |
| Proton decay / GUT lifetime (higher-order gauge-fold re-entry forbidden at low logical density) — beyond the gauge-algebra alignment already verified | [`Forces_From_Three_Axes.md`](Forces_From_Three_Axes.md) |
| Material-specific carrier-scattering / `ρ(T)` / `T_c` | [`Electricity.md`](Electricity.md) |
| QRNG Closure Observatory — falsifiable test of whether QRNG streams deviate from the analytic ZFA-closure null (predeclared sieve + controls; expected Tier-0) | [`QRNG_Closure_Observatory.md`](QRNG_Closure_Observatory.md) |

---

## Foundational reframings (substrate vs continuum-notation — issues #36–#52, #23)

A critique series (Allen / "find the machine, not the notation"): continuum objects — `π`, complex
amplitudes, real numbers, Hilbert space, light cones, `U(1)` optics — should be **emergent
renderings of the finite ZFA substrate**, not primitives. The framing is largely owned by
[`TheContinuum.md`](TheContinuum.md) (continuum emergent, RCA₀ floor, no infinite precision); what
remains is the **ZFA-native operator formalization** of each.

| Item | Status | Where |
|---|---|---|
| **`π` — derived by construction from the closure census** (#36, #50, #59, #71, #73, **#86/#89/#90**) | ✅ **Derived by construction.** The substrate's own census `C(2n,n)` (`closure_census`, theorem) gives a finite `Real.pi`-free rational `n·(C(2n,n)/4ⁿ)²` (`returnDensity`, theorem) whose limit is `1/π` by the Wallis/Stirling asymptotic (**settled mathematics**) — so `π = lim 1/(n·returnDensity n)`, π from intrinsic substrate counting, no circle. **Loop closure** side: `phase = (· % N)` is `Real.pi`-free; the continuum `2π` is *inserted* in `renderAngle`, not recovered. **Narrow residuals (don't undermine the construction):** A.1 *formalize* the (already-settled) convergence in our Lean — housekeeping (`physical_pi_in_progress`); A.2 physically ground the 2-D squaring (the random-walk probability space from ZFA dynamics); A.3 the **separate** effective-limit geometry `C(r)/2r→π`, `A(r)/r²→π` (the emergent-spacetime burden — owed because QLF uses `Real.pi` in `α`/GR). **Declined only:** the continuum as *fundamental substrate* | [`lean/QLF_PhysicalPi.lean`](lean/QLF_PhysicalPi.lean), [`lean/QLF_LoopClosure.lean`](lean/QLF_LoopClosure.lean), [`Physical_Pi.md`](Physical_Pi.md) |
| **Finite phase precision (a non-issue: `π` is computable)** (#37) | ✅ **Resolved.** `π` is a *computable* real — a finite algorithm yields any precision — so it is RCA₀, not the continuum fallacy; "infinite precision" was never required. Audit ([`pi_precision_demo.py`](pi_precision_demo.py)): the most demanding *audited* observable (H 1S–2S) needs only **~15** significant digits; `g−2`/α ~10–11; `a₀` ~1. The only real point is the **dependency direction**, Lean-anchored: closure is `phase = · % N` (`Real.pi`-free), `2π` is its rendering (`QLF_LoopClosure`) | [`pi_precision_demo.py`](pi_precision_demo.py), [`lean/QLF_LoopClosure.lean`](lean/QLF_LoopClosure.lean), [`TheContinuum.md`](TheContinuum.md) |
| **Complex amplitudes / reals as finite bookkeeping** (#39, #40, #44) | 🟣 **The state ring is `ℤ[i]`.** The substrate is finite registers; `i` is the σ-rotation (`QLF_Spin`: `i•σ`), and the state space is a finite-rank **Gaussian-integer (`ℤ[i]`) lattice** with `μ₄` phases and rational Born probabilities (`QLF_StateSpace`), Hilbert space its continuum completion — the `√2`/`ζ₈` entering only at the Clifford↔`T` (computable↔universal) boundary. So "reals/`ℂ` are finite bookkeeping" is made precise (a cyclotomic integer ring, not `ℂ`). Replacing `ℝ`/`ℂ` *in the Lean kernel* with finite phase registers is still a large refactor, not done | [`The_QLF_State_Space.md`](The_QLF_State_Space.md), [`lean/QLF_StateSpace.lean`](lean/QLF_StateSpace.lean), [`TheContinuum.md`](TheContinuum.md) §3 |
| **ZFA as a pruning/filter operator before Hilbert** (#39) | ✅ Already so: `full_zeno_prune` is the filter, applied *before* the spectral/Hilbert representation (`toSpectralMode`); the discrete combinatorial core is RCA₀, the Hilbert side is downstream | [`lean/QLF_Axioms.lean`](lean/QLF_Axioms.lean), [`lean/QLF_Spectral.lean`](lean/QLF_Spectral.lean) |
| **Optics as finite phase cycles, not continuum U(1)** (#38) | 🟣 `phase = distance/wavelength` in cycles; the finite-closure optics formalization is open | [`Maxwell.md`](Maxwell.md), [`TheContinuum.md`](TheContinuum.md) |
| **Light cones / causal diamonds as emergent, not primitive** (#46, #63, #72) | ✅ **Lean-anchored.** The ZFA-native reachable-event object is a Lean def: `reachable A B := A <+: B` (history-extension, **no spacetime primitive**), a partial order / **causal set** (`reachable_refl`/`trans`/`antisymm`); `futureCone` = the set the light cone *renders* (`futureCone_subset`). **Answers #72** (the pre-temporal succession driver IS this partial order; time is its rendered read-out). Open: the order→metric reconstruction (Causal-Set continuum step) + binding to `full_zeno_prune` (`light_cone_rendering_in_progress`) | [`lean/QLF_ReachableEvent.lean`](lean/QLF_ReachableEvent.lean), [`SpaceTime.md`](SpaceTime.md) |
| **What drives closure succession before time** (#72) | ✅ **Lean-anchored** (via #46/#63): the **closure-reachability partial order** is the pre-temporal driver — `reachable` exists with no time coordinate; time is its rendered total-order read-out. Open piece = the same order→metric/rendering boundary | [`lean/QLF_ReachableEvent.lean`](lean/QLF_ReachableEvent.lean), [`Time.md`](Time.md) |
| **Operational 3D from the deeper 8-twist structure** (#42) | ✅ Anchored: `substrate_spatial_dimension = 3` from the 6+2 alphabet (6 spatial twists = 3 axis-pairs), the same `3` behind α/SU(3)/generations; apparent 3D *is* the stable rendering of the 8-twist machine. **Open follow-up (#62):** the pre-geometric *pointer-swap mechanism* by which n-dimensional swap-fuzz renders as sparse operational 3D for embedded observers (chromodynamic binding + relational event delay) — a mechanism layer below the dimension count | [`lean/QLF_FineStructureSubstrate.lean`](lean/QLF_FineStructureSubstrate.lean), [`Magic_numbers.md`](Magic_numbers.md) |
| **Dark-matter `a_cl(r)` predictor (#41, #77)** | 🟢 **Built + benchmarked (#77 closed)** — the radial-acceleration law `g_obs²=g_bar·(g_obs+a₀)` is derived (closure-balance, `radialAccel_self_consistent`) and the **blind forward predictor** runs: baryonic inputs → `a_cl(r)` → SHA-256-sealed `Vpred`, scored on 147 curated SPARC galaxies — **parameter-free**, observational-floor `0.133 dex`, = best-fit MOND, vs Newton (×2.7), vs NFW (294 params). Pipeline + sealed receipt in [`sparc/`](sparc/). **Still open:** the `ρ_logic(r)` *generating mechanism* (central-organizer / impedance harmonics) and the interpolation form as the *unique* forced ν; the `1/2π` prefactor (~13%). NB Zajda's Omega-RTR (#74) *fits* the residual per-galaxy — not a prediction, "closure" is coincidental terminology, not ZFA | [`SPARC.md`](SPARC.md), [`lean/QLF_DarkMatter.lean`](lean/QLF_DarkMatter.lean), [`DarkMatter.md`](DarkMatter.md) |
| **Time-as-driving-force / thermodynamics refactor** (#45) | ⚪ Parking-lot: heat/energy as emergent appearances of temporal-closure dynamics; a later thermodynamics refactor | [`Time.md`](Time.md), [`Entropy.md`](Entropy.md) |
| **QLF as a generative discrete latent space; LLM-native physics** (#23, #52) | ⚪ Framing: the macroscopic universe is the decoded manifestation of a discrete logical latent space; LLMs given a bitwise vocabulary of substrate constants are a natural semantic engine for it | [`QLF_as_Intelligence.md`](QLF_as_Intelligence.md), [`Active_Inference_Mathematics.md`](Active_Inference_Mathematics.md) |
| **QLF-native AI runtime: closure tokens vs float logits** (#65) | 🔵 Architecture proposed ([`QLF_as_Intelligence.md`](QLF_as_Intelligence.md) §6a): closure tokens → integer ledgers → admissible transitions (decidable `full_zeno_prune`) → semantic closure, vs embeddings → floats → logits → softmax. The *operation* (synthesis = disjunctive closure) + token-as-proof are anchored; whether integer-ledger transitions **train** better than float gradient descent (credit assignment without differentiability) is open (`qlf_native_ai_in_progress`) | [`QLF_as_Intelligence.md`](QLF_as_Intelligence.md) §6a, [`lean/QLF_InfoSynthesis.lean`](lean/QLF_InfoSynthesis.lean) |
| **Reversibility & energy conservation are emergent, not fundamental** (the convergence-table audit) | ✅ **Positioned.** Reversibility is a symmetry of the *laws* (the dagger involution, `time_reverse_involutive_but_closure_degenerate`), energy conservation a *present-local* balance — both **outputs** of the forward ZFA closure, not foundations (each event *creates* energy, half lent to the future = dark energy). The 18-program convergence table is *irreversibility-native by selection* — CST growth, Girard use-once, Friston dissipation, Shannon→Landauer erasure (`ΔF=−log 2`), Wolfram's derived 2nd law are positive evidence. **Two standard-form caveats repaired by synthesized time** (`f=1/t`): AdS/CFT holography (static negative-Λ unitary background → QLF's **de Sitter / ZFA-closure** boundary, `Λ=log 2`) and canonical / Wheeler–DeWitt LQG (frozen `H=0` "problem of time" → the synthesized arrow). The flaw-*failing* TOEs (string S-matrix, no-collapse Everett, block universe, 't Hooft reversible CA) are **not** in the table — convergence and casualty sets disjoint | [`lean/QLF_Reversibility.lean`](lean/QLF_Reversibility.lean), [`Reversibility.md`](Reversibility.md) §6, [`Conservation.md`](Conservation.md) §2b |

---

## Notes

- **Tiers vs. this file.** `Experimental_Consistency.md` uses Tier-1/2/3 for *achieved precision*; this registry uses the status tags above for *forward work*. A "Tier-3 open" result there maps to 🔵/🟣 here, unless it is a 🧱 boundary.
- **Maintenance.** When an item closes or is reclassified, edit its row here **and** its owning doc in the same change, and (if it gains a theorem) the relevant `lean/` module and `lean/README.md` row.