# Open Problems — QLF gap registry

**Method:** how items here are promoted, rejected, or corrected — status labels, kill conditions, the inventory-first rule — is [`ScientificApproach.md`](ScientificApproach.md).

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 **sufficient** —
the load-bearing posture is a **single premise**: in a possibilist, logically-consistent (`RCA₀`)
substrate, **Zero Free Action accounts for every terminating computation** — all possible logical Turing
machines, quantum computations, and formal languages are ZFA strings that survive the closure filter
([`qlf_universality`](lean/QLF_Universality.lean), the proven *sufficiency* pillar; the filter is
Church–Turing complete, a selection principle that discards no computable physics, not a restriction).
Its *exclusivity* is a published conjecture with named defeaters — the full ledger, typed by
evidential strength with the misses beside the hits, is [`Completeness_Evidence.md`](Completeness_Evidence.md).
Sufficiency is supported by parameter-free overdetermination (§3 there) and confirmed exclusions (§4c);
Bell/KS/PBR exclude *added* local, non-contextual, and ψ-epistemic ingredients (Bohm/Everett survive as
exact reconstructions); error-corrected QC at scale progressively excludes the deviation class
(GRW/CSL/Penrose); among the surviving exact reconstructions ZFA is distinguished by parsimony and
constants overdetermination. Exclusivity is conjectured pending the reconstruction theorem
(`Completeness_Evidence.md` §6), and it is **invariant-uniqueness, not machine-uniqueness**: the
infinitely many Turing machines, quantum computations, and languages that yield the *same* ZFA-closed
outcome are ordinary **multiple realizability** — expected, not a counterexample — and they *converge on*
the one ZFA invariant. So "ZFA is correct" means the forced *fixed point* every coherent computation
lands on, not a unique substrate machine; the reconstruction target's "isomorphic **to** ZFA" carries
exactly this (invariant forced up to realization; `comparison_isomorphism` the local proven instance,
`Completeness_Evidence.md` §0). **The reconstruction target has narrowed substantially** (§6a–§6c): the
*emergence forcing chain* (`QLF_EmergenceChain`) shows the ZFA invariant emerges from the one premise
(discreteness forced → balanced closure folds to the μ₄ algebra); the *five postulates collapse into
one-and-a-half* (`QLF_PostulateReduction`) — finite-capacity, closure-as-receipt, and reversible/
irreversible all reduce to the one postulate, leaving orthomodularity the residue; and that residue
*narrows too* to **(a1) the dagger is a proper involution — now machine-checked** (`QLF_ProperInvolution`,
`substrate_dagger_proper`) **+ (a2) the projection-lattice identification + the Baer-`*`-ring bridge**
(settled math Mathlib lacks) **+ (b) the Gleason-hard uniqueness**. So the target is no longer "five
independent postulates → ZFA" but **"the one postulate + two named settled-math bridges + the Gleason
uniqueness"**, with the substrate-side facts proven. **And the orthomodular residue is now *concretely
realized* at the minimal quantum level** (`QLF_QuantumLogic`, `Quantum_Logic_Foundations.md` §2): the
substrate realizes the smallest genuinely-quantum logic `MO2` — orthocomplemented, **orthomodular**
(`orthomodular`), and provably **non-distributive** (`not_distributive`, from the *incompatible* x/z-spin
closures whose Paulis don't commute, `incompatibility_source`) — a complete axiom-free theorem; only the
*general* orthomodular-lattice→Hilbert representation (Piron/Solèr) stays the Gleason-hard (a2)+(b) bridge.
Its defeaters are axion detection, α drift, an exhaustive 0νββ null, and
a QRNG deviation (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). |

---

## Working priority — what to do next

Recorded here so it survives a session boundary. The governing question has shifted: not *how many ways*,
but **given that everything happens every way, exactly how do those ways add?**

1. ~~**Instantiate `DivergenceCalculus`**~~ — ✅ done ([`QLF_LatticeCalculus`](lean/QLF_LatticeCalculus.lean)).
   A forward-difference calculus on `ℤ` with metric compatibility computed rather than imposed and a
   genuinely non-zero gradient, so the field-equation theorems are conditional on *satisfiable*
   hypotheses. Claimed only as that: **consistent and inhabited**, not an implementation of GR geometry.
2. ~~**Prove the full phase rule**~~ — ✅ done ([`QLF_PhaseRule`](lean/QLF_PhaseRule.lean)).
   `φ(h) = (−1)^{N₋(h)} · (−1)^{inv(axis(h))}` is a theorem (`phase_rule`), and in the stronger form
   `twist_fold_phase_normal_form` that drops the balance hypothesis and holds for *every* history. Signs
   pull out of a product regardless of order; distinct Pauli matrices anticommute, so sorting the axis
   word costs one `−1` per inversion. Balance makes each axis multiplicity even, killing the sorted
   remainder — a second, independent route to `balanced_phase_is_real`. **The phase of a way is now a
   computable integer read off the word** (`predictedPhase`), which is exactly the input item 3 needs.
2a. ~~**Basis-independence of the census**~~ — ✅ done ([`QLF_BasisIndependence`](lean/QLF_BasisIndependence.lean)).
   The canonical `{>,<}↦X`, `{^,v}↦Y`, `{/,\}↦Z` chart is a coordinate convention, not a preferred
   frame: every balanced history folds to the same scalar after any axis transposition, any axis
   reversal, or the gauge swap. Relabeling moves the sign count by an axis multiplicity and the
   inversion count by a *product* of two of them, and balance makes every multiplicity even.
   **The basis belongs to the question, not to reality.**
3. **The contextual census → signed-amplitude bridge** — the central near-term question:
   *given that everything happens every way, exactly how do those ways add **under a change of
   context**?* A context is a **partition** of the same invariant ways, and the amplitude is the
   coherent sum `A(c) = Σ_h K(c,h)·φ(h)`, weight `|A(c)|²`. Two constraints are now proven or measured,
   and both narrow the search:
   * **`K` must be derived, never chosen.** A free kernel reproduces any amplitudes at all, so by the
     method's own rule 4 it is bookkeeping. QLF's derived candidate is **joint closure**: `K(c,h) = 1`
     exactly when `h` closes together with the apparatus history of outcome `c` (`SharedClosure`,
     [`ER_EPR_QLF`](lean/ER_EPR_QLF.lean); the two-history interactor of [`MultiParticle.md`](MultiParticle.md)).
   * **A proven no-go on symmetric branches.** If the two outcome branches are related by a relabeling
     that fixes the system ensemble, basis-independence forces `A₊ = A₋` — `P = ½` identically, for
     *every* choice of "direction". Measured: apparatus pairs `(>ᵃ\ᵇ, <ᵃ/ᵇ)` over a symmetric ensemble
     give `A₊ = A₋` in every non-empty case, with no angular dependence whatsoever. So the quantum
     basis change is **not** the substrate relabeling, and Hadamard mixing `(A₊,A₋) ↦ (A₊+A₋, A₊−A₋)`
     cannot come from relabeling — a permutation of ways never sums two amplitude classes into one.
     **The asymmetry is therefore relational — `K = K(P,M)`, neither `K(P)` nor `K(M)`.** Neither side
     determines the event; their joint closure does, which is why the same prepared state must behave
     differently against an aligned and a transverse apparatus.
   * **Measured, exactly, in [`contextual_census.py`](contextual_census.py)** — the phase rule turns
     the `8^k` enumeration into a polynomial dynamic program (appending a letter costs a sign fixed by
     axis-count *parities* alone), cross-checked against brute force. Two results:
     the **transverse** geometries sit at exactly `½` at every horizon — but that is *forced* by
     basis-independence and so is bookkeeping, not evidence; the **aligned** geometries wash out:
     for any fixed preparation the branch ratio climbs monotonically toward `1` (depth 1:
     `0, .125, .200, .267, .327, .381, .429, .472, .511, .546` through `k=18`), while letting the
     preparation depth grow with the horizon drives the weight to `1` instead. **So this partition does
     not define a horizon-independent probability** — the number is set by the depth-to-horizon ratio
     and both limits are degenerate. The limit is not *proven* (monotone data to `k=18` is not a
     theorem), but a further principle is plainly needed to fix the regime.
   * **Indexing does not rescue it — lead raised and closed by computation.** The natural suspicion was
     that flat `P ++ s ++ M_c` is at fault, since it puts system and apparatus in one Pauli algebra
     where distinct axes anticommute, whereas independent factors commute
     ([`QLF_IndexedFactors`](lean/QLF_IndexedFactors.lean)). Recomputing with system and apparatus as
     separate factors — deleting exactly the cross-inversion term — gives **identical probabilities at
     every horizon**, for every geometry. The reason is structural: a strand's **axis parity is
     determined by its imbalance** (`#>+#<` and `#>−#<` agree mod 2), so within the single imbalance
     class a branch selects, the cross term is a *constant sign per branch*, and a global sign cannot
     survive `|A|²`. **So the flat/indexed distinction is invisible to Born weights here** — the
     coupled/product split governs *which* histories close, not the weights of a single-coupling
     context, and the wash-out is a property of the partition itself.
   * **The listening horizon was the candidate, and it is now run — it does not rescue the
     partition.** Closure is **capacity-relative** (`closedAtHorizon_iff_maxExcursion_le`,
     [`QLF_ClosureDepthLaw`](lean/QLF_ClosureDepthLaw.lean)), so the weight was read at a finite
     closure capacity `R` (a *physical* capacity — which histories can close at all, not an
     observer's act; "listening" is this repo's established name for the capacity-relative count):
     keep only runs whose free action (the repo's own
     `spatial_free_action + local_free_action`, maximised over prefixes — the multi-pair form of
     `maxExcursion`) never exceeds `R` (`contextual_census.py --listening 2,3,4`, exact integers).
     Result, and it is sharper than the wash-out it was meant to cure: **capacity sets the rate of
     forgetting, never the limit.** `|P(+) − ½|` decays by `0.666, 0.868, 0.906` per twist at
     `R = 2, 3, 4` — a preparation stays readable for `τ = 2.5, 7.1, 10.1` twists — and against an
     *asymmetric* branch pair (nothing symmetry-forced) the surviving limit depends on the
     preparation's **axis class only**: a preparation and its **reversal** land on the same limit
     exactly (`/` with `\`, `/>` with `/<`, `/^` with `/v`). **The sense of the prepared strand —
     precisely what a Born weight must depend on — is erased.** Mechanism, not coincidence: at
     fixed capacity the walk is a finite signed transfer operator with a degenerate `±iλ(R)`
     leading pair (`λ = 3.991, 4.383, 4.638`, 16-fold top modulus), so every preparation collapses
     onto one dominant subspace and the direction-carrying part decays no slower than the spectral
     gap `λ₂/λ₁ = 0.752, 0.951, 0.979`. **So the whole family of long-horizon readings is closed** —
     a larger listening horizon remembers longer and forgets just as completely — and whatever
     carries a Born weight lives in the **transient**, at horizons comparable to the preparation
     itself. That the substrate thermalises under long free evolution is not itself wrong physics
     (a measurement is a prompt joint closure, not an infinite free run), but it is not a Born rule.
   * **First joint closure — the absorbing census — is the answer to "which horizon", and it moves
     the problem.** A closure *is* an event; continuing a run past it describes a longer, different
     history, and that continuation is exactly what the long-horizon scans were mixing. The
     absorbing census (`contextual_census.py --first-closure`) stops each run at its **first** joint
     closure, whichever branch closes it — the run chooses its own stopping depth, so no horizon is
     chosen for it — cross-checked against enumeration. **Direction reaches the outcome again:**
     reversing the preparation changes the weights (`0.688` vs `0.312` on the ZX-mix at `R = 3`;
     `1.000` vs `0.878` for a branch pair no relabeling can exchange), where every long-horizon
     reading gave a preparation and its reversal one identical limit; and the aligned geometry
     closes at depth `0` with `P(+) = 1` exactly at every capacity. **But the complementarity is
     symmetry-forced** — `P(+|ψ) + P(+|ψ̄) = 1` holds exactly where a relabeling exchanges the
     branches *and* reverses the preparation, and fails otherwise (sums `1.878`, `0.352`), so it is
     bookkeeping by rule 4, and the script reports it as such. **What remains is a single sharp
     question: a derived measure over closure depths.** `P(+|d)` decays monotonically toward `½`
     with depth, so both pre-registered aggregations (coherent `|Σ_d A_c(d)|²`, incoherent
     `Σ_d |A_c(d)|²`) drift with the cutoff and agree with each other to three digits; and the
     unweighted aggregations drift with the cutoff.
   * **The depth measure is counted, not chosen — correcting the line above.** First closures are
     **prefix-free**, so the global cylinder measure `μ(h) = 8^{−|h|}` on the Σ₈ tree applies and
     **Kraft's inequality** caps the total at `1` by finite counting: at a common horizon `K` a
     first closure at depth `d` owns `8^{K−d}` of the `8^K` complete histories, disjointly. In QLF
     terms, **an earlier closure weighs more because more complete histories contain it** — the
     possibility tree counting itself, not a new postulate. Capacity causes **leakage**, not
     renormalisation. Measured (`R = 3`): Kraft mass `1.000` aligned, `0.321` transverse, `0.180`
     ZX-mix, always `≤ 1` and monotone, now an asserted invariant. The earlier `1.02 / 1.11` came
     from normalising depth by depth against the surviving capacity-limited population — that was
     the error, not the measure.
   * **Under it the multiplicity converges and the amplitude does not.** `P(c | closure)` from
     counts is knob-free, direction-sensitive and settling in capacity (aligned `1.000`, transverse
     `0.500`, ZX-mix `0.9164/0.9023/0.9005` at `R = 3/4/5`), but a Born weight needs
     `|A_c(d)| ≲ √8^d = 2.828^d` and the measured growth is `3.91^d, 4.35^d, 4.56^d`, widening with
     capacity. **The phases cancel too weakly to define an amplitude under the measure that makes
     the counts summable** — and counts are provably not weights, so neither is the answer. **The
     open item is now quantitative:** either the signed census cancels to `2.828^d` under some
     sharper account of which closures are the *same* event, or the amplitude does not live on this
     tree.
   * **The normalized-event weight is the best-behaved construction so far — and still not a Born
     rule.** If the `W` words closing as the same event at the same depth are *ways of one event*
     rather than `W` outcomes, the weight carries the many-to-one normalisation:
     `B(c) = Σ_d (W_c(d)/8^d)·(A_c(d)/W_c(d))²` — **multiplicity mass × coherence fraction**, with
     nothing fitted, and **summable for free** since `|A| ≤ W` puts it under the Kraft bound
     whatever the phases do. It converges absolutely by depth ~16, is nearly capacity-independent
     (`0.99386152` at `R = 3` vs `0.99383011` at `R = 4`), and gives aligned `1`, transverse `½`,
     exact complementarity. **But it does not render an angle:** apparatus tilt does not accumulate
     (`2·arccos√P` wobbles `9°–13°` over `a = 1…5` transverse letters), a `(m Z, n X)` grid sits at
     `0.97–0.99` regardless of `n/m` with one inversion to `0.075`, and *order* beats composition
     (`½` for X-then-Z against `0.994` for Z-then-X). Both correct values are symmetry-forced, so
     the unforced content is the part that fails. **The measure question is settled; the amplitude
     question is not** — the decisive test is now a geometry with a known *and unforced* QM answer
     (two-path interference, the singlet), which needs multi-history closure, not another weighting.
   * **Two-path interference fails, and provably — the decisive test.** Two paths reaching the
     same detector merge into one event, so amplitudes add before normalisation. Four runs, one
     fixed weight (`--two-path`): a matched pair gives `B(A+B) = B(A)+B(B)` **exactly** where QM
     needs a factor `2`; an unequal pair `0.999288`; the destructive configuration `0`. Destructive
     interference works, constructive interference cannot — **by theorem**: merging can only lower
     the weight, `(A₁+A₂)²/(W₁+W₂) ≤ A₁²/W₁ + A₂²/W₂`, equality exactly at equal mean phase
     ([`QLF_KraftMeasure`](lean/QLF_KraftMeasure.lean): `merge_le_sum`,
     `no_constructive_interference`, `merge_eq_sum_iff`). The inequality that bought summability
     forbids the enhancement.
   * **The divergent horn is not universal: some geometries carry a convergent amplitude with no
     normalisation at all.** It is a claim about growth, so it is checkable case by case. Measured
     (`contextual_census.py --coherent 2`, exact rationals): the transverse geometry grows `2.2361^d`
     and the ZX/ZY mixes `2.6458^d`, both **below** the `√8 = 2.828^d` threshold, so
     `T_c = Σ_d A_c(d)·8^{−d/2}` converges. Closures of one geometry share a depth parity, so the
     weight is an **exact rational**: aligned `1`; transverse `T₊ = T₋ = 8/13` giving `1/2`; the
     mixes `T₊ = −112/195`, `T₋ = 8/195` — ratio exactly `−1/14`, `P(+) = 196/197`. Unnormalized,
     merging paths adds amplitudes, so the four-run test gives `2.0000` constructive against
     `0.0000` destructive — **the factor of two quantum mechanics demands**.
   * **The `√8` threshold is forced.** One way with unit phase must weigh its own cylinder mass, so
     an amplitude scaling `μ^s` gives `μ^{2s}` and consistency forces `s = 1/2`. Where the sum
     diverges it diverges for real, not for want of a better exponent.
   * **Correction: this is geometry-dependent, not capacity-dependent.** The absorbing operator's
     spectral radius is `3.99` at `R = 2` and `4.38` at `R = 3`, both *above* `√8`, so the low growth
     measured is **subdominant** — those preparation–apparatus pairs project out the dominant modes.
     Certain pairs carry a convergent amplitude and others do not; every geometry tested at `R ≥ 3`
     is in the second class (`3.97^d`–`4.33^d`). Capacity separated the first cases looked at; it is
     not the criterion.
   * **Surveyed, and the class is structured but sparse.** Over **1,326 preparation–apparatus pairs**
     at capacity 2, measured from the series' *terms* at depth 200 (a two-point fit at depth 90 reads
     a transient — same geometry, `8.16` there against `0.19` at 200): **19 converge, 1.4%**, every
     one with **integer** squared growth `a² = 5` (7 cases) or `a² = 7` (12 cases); **20 sit exactly
     on the threshold** at `a² = 8.000000`; above it both integers (`9.000000`, 119 cases) and
     irrationals (`5+√10`, `7+√2`, … up to `15.85`) occur. **Integrality holds exactly at and below
     the threshold.** By the (fragile) earlier estimator, capacity 3 gave 0 of 5,515 — consistent,
     but not to be quoted without the term test.
   * **The selection rule.** Across all 39 convergent-or-marginal cases: `a² = 7` ⟺ the branch
     targets are **antipodal** (`t₊ = −t₋`); `a² = 5` ⟺ the branches **share a component
     anti-aligned with the preparation**, differing by a sign flip elsewhere; `a² = 8` (marginal) ⟺
     the same shape with the shared component **orthogonal** to the preparation. So whether an
     arrangement carries a Born weight at all depends on how the apparatus sits relative to the
     prepared direction. Read off the data, not proven.
   * **The invariant is spectral, and it belongs to the readout.** With `A_c(d) = u_c·M^d·v_prep`
     (`M` the absorbing closure operator), **`a²` is the largest `|λ|²` in the joint support of
     readout and preparation, and the amplitude exists iff that is `< 8`.** Predicted from the
     spectrum with no series run: **86 of 90 geometries match exactly**, and **90 of 90 agree on the
     summability verdict** (the four exceptions read `8.1623` against a predicted `9.0000`, both
     above threshold — a pre-asymptotic reading by R5). Divergent geometries have `a²` = the dominant
     `λ²` exactly; convergent ones are **blind to the dominant modes** (overlap `~10⁻¹⁶` against
     `10⁻¹`–`10⁻²`), dropping to a subdominant eigenvalue — which is where the recurring integers
     `5`, `7` come from. This also dissolves the "realized threshold" puzzle: `8` is *in* the
     spectrum. The earlier imbalance rules were proxies and behave like proxies (antipodal converges
     52% of the time).
   * **What is still open:** *which apparatus words produce dominant-blind readouts* — now a
     combinatorial question about `u_c` rather than a search over geometries — whether the excited
     eigenvalue set means anything physically, and whether 1.4% is a selection rule or the encoding
     being too rigid. The sub-additivity theorem is unaffected: it bounds the *normalized* weight
     everywhere.
   * ~~**Next Lean anchor (tractable):** the Kraft bound itself~~ — ✅ **done**
     ([`QLF_KraftMeasure`](lean/QLF_KraftMeasure.lean)). For a prefix-free set of twist words
     `Σ 8^{−|h|} ≤ 1` is finite counting (`8^{K−|h|}` disjoint continuation sets inside `8^K`), so
     **the depth measure is a theorem, not a measured regularity** (`kraft_count`, `kraft_measure`,
     `twist_kraft`). The same module carries the interference no-go it implies (`merge_le_sum`,
     `no_constructive_interference`, `merge_eq_sum_iff`) and the summability bound
     (`normalized_event_mass_le_one`).
   * **Method note, recorded because it produced a wrong answer first:** the float scan is
     contaminated past `k* ≈ 16 ln 10 / ln(λ₁/λ₂)` (≈ 730 twists at `R = 3`), where roundoff — which
     overlaps the dominant subspace — makes every preparation *appear* to share one universal limit.
     Signed transfer-matrix censuses must be run in exact integers.
   * Then test **blind** against known answers: single-spin rotation, Mach–Zehnder, the two-spin
     singlet / Bell correlations, three-path interference. **Watch for symmetry-locked results** — a
     `½` forced by a proven invariance is multiplicity-invariant bookkeeping, not evidence.
   * The harder half, and the one that would matter most: an arbitrary direction `n(θ,φ)` is **not a
     substrate object** (no continuum in a finite-information region, `QLF_Realizability`), so the goal
     is not to import `cos(θ/2)` but to derive `cos²(θ/2)` as the **large-census rendering** of
     repeated finite context changes. Open.
4. **Phase-weighted focusing / Raychaudhuri** — only after 2–3, and then ask whether matter-energy flux
   changes the *interference* structure of horizon-crossing histories rather than their raw count. The
   raw-congestion route was already shown to be bookkeeping (multiplicity-invariant, hence no content),
   so this is the substrate-native replacement.

---

## Closed — derived / machine-verified

| Item | Status | Where |
|---|---|---|
| **The depth law — what a finite capacity can close** | ✅ **Machine-verified** — `closedAtHorizon_iff_maxExcursion_le`: for a gauge-free count-balanced history, `boundedPrune R s = []` **iff** `maxExcursion s ≤ R`, so a finite-capacity horizon closes exactly the histories whose phase walk never strays further than `R` from balance — **capacity bounds excursion, not length** (capacity `R` buys length `~R²`, a balanced walk's mean maximum being `√(πn/2)`: polynomial, not exponential). Went through by generalizing to the **signed** height with an arbitrary accumulator (`hmax_zeno_prune`), valid for *unbalanced* histories — which is what the emit step needs; the naive per-pass claim fails over an accumulator and is false outright with gauge elements (`[+, gauge, −]` is prune-fixed), so both hypotheses are necessary. Also `closureDepth_eq_maxExcursion` (exact pass count) and `maxExcursion_nested`. The 0/66,196 exhaustive check is now a theorem. No axioms | [`lean/QLF_ClosureDepthLaw.lean`](lean/QLF_ClosureDepthLaw.lean), [`lean/QLF_ClosureDepth.lean`](lean/QLF_ClosureDepth.lean) |
| **The Law of Exceptions** | ✅ **Machine-verified** (given one modelling step) — *a system with more states can always break a finite closure*. Modelling a restrictive law as a **finite closure** `closedAtHorizon R`, `law_of_exceptions` gives every capacity `R` a **constructed** exception `[+^{R+1} −^{R+1}]`, unadmitted at `R` yet **genuinely closing at `R+1`** — real, merely deeper than the law can see; `closure_hierarchy_strict` / `no_final_closure` (no finite closure is final); `no_finite_closure_is_exceptionless` (the kill condition); `no_exception_to_unbounded_closure` (every exception is admitted at *some* capacity, so unbounded ZFA — which restricts nothing — is the one exceptionless law). Self-reference proves nothing and the set version `A_L ⊊ H ⟹ ∃h∉A_L` is a tautology; **capacity** earns the premise. **Modelling assumption, not a theorem:** that a restrictive law *is* a finite closure. Corollary: **construction proves possibility, not uniqueness** | [`lean/QLF_LawOfExceptions.lean`](lean/QLF_LawOfExceptions.lean), [`Law_Of_Exceptions.md`](Law_Of_Exceptions.md) |
| **Balance forces a real phase (`μ₄ → μ₂` on closures)** | ✅ **Machine-verified** — `balanced_phase_is_real`: a count-balanced history folds to `+I` or `−I`, **never `±iI`**, so the phase group on closures is `μ₂` and branch amplitudes over the balanced census are signed **integers**, not Gaussian integers. One determinant computation, and **order-blind**: every Pauli matrix has `det = −1`, every gauge matrix `+1`, `det` is multiplicative, balance makes the axis count even (`2(#^+#>+#/)`), so `det(fold) = 1` while `±iI` have `det = −1` — settling every interleaving at once with no case analysis. **Scope proven sharp from both sides:** the *unbalanced* `^ > /` folds to `−iI` (`unbalanced_can_be_imaginary`), so balance is load-bearing, not decoration. Stated as *a* proof, not *the* proof | [`lean/QLF_BalancedPhaseReal.lean`](lean/QLF_BalancedPhaseReal.lean) |
| **The phase rule — which phase a way carries** | ✅ **Machine-verified** — `φ(h) = (−1)^{#neg twists} · (−1)^{inversions of the axis word}`, the repo's flagship verified-not-proven finding (0 counterexamples over 8,134,416 balanced histories), is now `phase_rule` — and in the **stronger unrestricted form** `twist_fold_phase_normal_form`, which drops the balance hypothesis and holds for *every* history, returning the sorted product `σx^{#X}σy^{#Y}σz^{#Z}` where balance leaves the identity. **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 exactly one `−1` per **inversion** (`axisFold_eq_canon`) — equal letters commuting with themselves is why the inversion count, not the count of all distinct-letter pairs, is the right statistic. Balance makes each axis multiplicity even, killing the sorted remainder — a **second, independent route** to `balanced_phase_is_real` (`phase_rule_real`), so the determinant argument was *a* proof, not *the* proof. **Consequence:** the phase of a way is a computable **integer** read off the word (`predictedPhase`, certified by `fold_eq_predictedPhase`) — no `2×2` product per history, which is what the signed-census → amplitude bridge needs. No axioms | [`lean/QLF_PhaseRule.lean`](lean/QLF_PhaseRule.lean), [`Experimental_Consistency.md`](Experimental_Consistency.md) |
| **The census is basis-independent — *the basis belongs to the question*** | ✅ **Machine-verified** — the canonical `{>,<}↦X`, `{^,v}↦Y`, `{/,\}↦Z` chart of [`census_inventory.py`](census_inventory.py) is a coordinate convention and never was a preferred physical frame: every count-balanced history folds to the same Pauli scalar after any transposition of the axes (`fold_invariant_swapXY`, `fold_invariant_swapYZ`, composite `fold_invariant_swapXZ`), any reversal of an axis (`fold_invariant_flipX`, `fold_invariant_flipY`), and the gauge swap (`fold_invariant_swapGauge`). Mechanism: relabeling moves the sign count by an axis multiplicity and the inversion count by a **product** of two axis multiplicities (`invCount_map_swapAxXY`, `invCount_map_swapAxYZ` — proven for *all* words), and balance makes every axis multiplicity even. **Balance is load-bearing:** outside it the corrections are real. **Sharp negative consequence:** a relabeling is an involution on the census 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₋)` — the quantum basis change is not the substrate relabeling, and all contextual content sits in how a context partitions the ways. No axioms | [`lean/QLF_BasisIndependence.lean`](lean/QLF_BasisIndependence.lean) |
| **Many bodies need indexed twists, not new twists — and the sector indexing cannot reach** | ✅ **Machine-verified** — a many-body token is `(factor, twist) ∈ ℕ × Σ₈`, an indexed *use* of the same eight primitives (`IndexedTwist`, `twistOf_mem_alphabet`): `N` bodies need `N` labels, not `2ᴺ` primitives. Indexing changes the **algebra**, not the alphabet — independent bodies commute (`indexed_factors_commute`) where a flat word makes distinct axes anticommute (`not_all_flat_pairs_commute`). **The two are sectors, not rivals:** a Kronecker product is scalar exactly when both factors are, so independent-factor closure needs *each* factor closed, while the flat model lets a factor stay **open**, balanced by the other — precisely `SharedClosure`/entanglement. Product sector: phases multiply, in **`μ₄` not `μ₂`** (an open factor is not count-balanced, so `balanced_phase_is_real` does not apply — the `μ₂` version was asserted first and the inventory's checker rejected it). Coupled sector: `shared_closure_not_factorizable` — the primordial `^ \| v` is jointly balanced while **neither** side folds to a scalar, so it has no product form at all; the gauge pair `+ \| −` falls the other way, making the boundary sharp from both sides. **Measured** in the [factor census](census_inventory.py): the coupled sector is the majority, settling near four fifths (`0.750, 0.791, 0.804, 0.803` at lengths 2–8). No axioms | [`lean/QLF_IndexedFactors.lean`](lean/QLF_IndexedFactors.lean), [`eight-twists-sufficiency.md`](eight-twists-sufficiency.md) §3a |
| **Handedness is the primitive; charge is one of its four components** | ✅ **Machine-verified** — answers the question left open by the row below (*if charge is not fundamental, what is?*). A twist **is** a handedness together with an axis and nothing else — the alphabet is the signed axis frame `Twist ≃ Bool × Axis` ([`QLF_AlphabetNecessity`](lean/QLF_AlphabetNecessity.lean)) — so the only two data an elementary distinction carries are *which axis* and *which of the two ways*. **Charge is nowhere in the primitives.** Four results: **`zfa_iff_handedness_balanced`** — **ZFA is exactly zero net handedness on every axis**, so the selection principle is a statement about handedness and nothing else, 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, derived, not a substance and not a fifth axis, *and this explains rather than restates* `no_charge_between_spatial_modes` (spin and energy are the other three components, and components of a vector do not mix); **`handednessOn_map_conj`** — conjugation negates *every* component, so charge flips **because** handedness does, `chiralCharge_conj` being its `Axis.I` case; and **`electron_neutral_but_handed`** with `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 does not mean handedness-free, it means handedness balanced*. Structural corollary: **`C` flips all four components, `P` (`reflect`) flips one**, and charge is the gauge component — so spatial reflection leaves charge alone **by construction** (`reflect_preserves_charge`) while conjugation negates it; the familiar C/P asymmetry is a fact about how many handedness components each operation touches. Capstone `handedness_is_the_primitive`. **Consequence for the CP program:** a universe whose primitive is handedness has no reason to be handedness-symmetric, so CP violation no longer needs an explanation for *why* the asymmetry exists — only for its size. No axioms | [`lean/QLF_Handedness.lean`](lean/QLF_Handedness.lean), [`CP-Violation-and-Chirality.md`](CP-Violation-and-Chirality.md) §1a, [`Electron.md`](Electron.md) §1b′, [`Spin_QLF.md`](Spin_QLF.md) §5a |
| **The electron is a closed periodic mode; charge is the residue of non-closure** | ✅ **Machine-verified** — resolves a standing internal contradiction ([`Electron.md`](Electron.md) v2.1 called the free electron "an open Hermitian deficit" while the engine printed `ZFA closed: True` beside it). **Both were right, at different levels, and the levels are different axes of the alphabet.** The internal cycle `^<v>` **is** count-balanced and folds to `−I` (`electronCycle_countBalanced`, `electronCycle_folds_negI`) — a completed half-spin mode, not an unfinished fragment; what is open is the **gauge** twist, and that unmatched count **is** the charge (`electronCharged_charge = 1`, `electronCharged_not_countBalanced`), so the manifest event is the joint closure, which is neutral (`positronium_countBalanced`, `positronium_neutral`). Four further results: **`hermitian_not_implies_zfa`** — the prefix `^<v` folds to the Hermitian `−σx` with `F = 1`, so self-adjointness is a property of the *operator* and closure a property of the *history* (this is the precise content of "manifest only at full cycles"); **`zfa_closure_is_neutral`** — a closed history carries zero charge, so **charge is emergent**, a count of what has not closed, with conservation and integer quantization following from the count rather than from a field; **`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 carry **exactly zero** charge difference: *the electromagnetic weight cannot see a spin or an energy*, which **derives** QED's exact spin-independence of the direct Coulomb term (all spin dependence being exchange = closure blocking); and **`joint_closure_allows_unequal_components`** — two unbalanced halves of *different lengths* whose joint history closes, so unequal energies entering one event is the normal case, not a counterexample. Supporting: `channelKernel_diagonal` (`Γ = δ_mn δ_ss'` from `harmonics_orthogonal` + `spin_projectors_orthogonal`) and the scale results `rest_period_times_c` / `compton_full_cycle` (`λ_C = c·T_C = h/m_ec`, the full `2π` cycle). Plus the ontological half, which corrects a teleological framing: **`charge_nonzero_not_countBalanced`** — a charged history does *not* close, hence is not an event, hence has **no effect**. Nothing is pending and nothing is owed; an electron does not seek a partner, it closes or it does not. What is called Coulomb attraction/repulsion is then 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. **Scope, stated once:** what is proven about spin/energy is that the charge *difference* is zero and the coherent cross term vanishes — **not** that the shared gauge imbalance disappears; but by the above that imbalance is not an effect either. **SM contrast, and it is real** ([`Experimental_Consistency.md`](Experimental_Consistency.md) §10 Class B): exact global neutrality is a *theorem* here where the SM leaves the total a free initial condition; an integer count cannot drift, giving `no_cosmological_drift_of_alpha` where the SM permits a varying-α field; and like-charge two-body binding has *zero ways* rather than a repulsive potential. The spin-blindness itself is Class A — consistency, not a discriminator. **No hard radius** is an *absence*, not a theorem: no length parameter occurs anywhere in the closure predicate. No axioms | [`lean/QLF_ElectronClosure.lean`](lean/QLF_ElectronClosure.lean), [`Electron.md`](Electron.md) §1, [`Spin_QLF.md`](Spin_QLF.md) §5a, [`Bound_States_QLF.md`](Bound_States_QLF.md) §1, [`Experimental_Consistency.md`](Experimental_Consistency.md) §1.1 |
| **Why eight twists — the alphabet size is quantized, and six is impossible** | ✅ **Machine-verified** (given one named posit) — `eight-twists-sufficiency.md` §5 argued *parsimony*, which is a preference, not a derivation; the assumption budget ([`ScientificApproach.md`](ScientificApproach.md) §1c) classified "8" as **chosen**. It is not. 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` ≃, agreeing with the Pauli-closure normal form via `twistNF_eq_signedAxis`; conjugation *is* sign flip at fixed axis, `toSignedAxis_conj`, which is why `F(h)` has four terms) — so `\|Σ\| = 2·\|axes\|`. Axes compose, so an axis set is closed, hence a **subgroup of the Klein four-group**: `frame_axisCount_trichotomy` gives `\|axes\| ∈ {1,2,4}` and `alphabetSize_trichotomy` gives `\|Σ\| ∈ {2,4,8}`. Four consequences, each `decide`-checked over all 16 candidate axis sets: **`no_six_twist_alphabet`** — `3 ∤ 4`, so "three spatial axes, no gauge pair" is not an alphabet at all, and the gauge pair `+`/`−` is the identity axis closure **forces** (`frame_contains_I`), not an addition to the spatial six; **`two_spatial_axes_force_three`** — two distinct spatial axes force the third (their product), so the spatial axis count is **0, 1 or 3, never 2** — a second, independent and stronger route to the substrate's `3` than counting `6 = 2·3`; **`noncommuting_iff_eight`** — non-commuting observables occur at `\|Σ\| = 8` and nowhere else (`sigma_xy_noncomm`), so uncertainty, SU(2), the double cover and spin exist only at eight, the `\|Σ\|=4` alphabet being abelian and unable to reach `±iI`; and the degenerate ladder `2` (no axes, no space) / `4` (one axis) / `8`. Independently enumerated against the runtime mapping ([`alphabet_necessity.py`](alphabet_necessity.py): 16/16 candidates, fold-group orders 2/4/16). **The named posit, and it is the whole residual:** that an elementary distinction *is* a signed element of the observable frame of a two-valued system (two-valuedness itself is proved — `spin_half_is_information_atom`; for a `d`-valued atom the frame has `d²` elements, `dim_ℝ Herm(d) = d²`, so signed steps give `\|Σ\| = 2d²` and `8` is the smallest non-degenerate alphabet — that count generalizes, while the Klein-group quantization is special to `d = 2`). No axioms | [`lean/QLF_AlphabetNecessity.lean`](lean/QLF_AlphabetNecessity.lean), [`alphabet_necessity.py`](alphabet_necessity.py), [`eight-twists-sufficiency.md`](eight-twists-sufficiency.md) §7 |
| **Turbulence as a quantized-vortex tangle (structural)** | ✅ **Machine-verified (structure)** — a vortex line is one circulation quantum and total circulation an integer count of quanta (`vortex_quantum`, `circulation_integer_quantized`): **Onsager–Feynman quantization from the substrate**, so classical turbulence is the coarse-grained limit of quantum turbulence. The cascade is a frequency hierarchy with a dissipation floor; reconnection is a ZFA closure. **Superfluid picture proven** (#120): a closed ZFA loop folds to the real `{±I}`, never `±iI` (`balanced_closure_folds_real`), the `±i` quarter-turn being the open forward strand closed by its odd dagger. Two distinct Navier–Stokes questions follow — **regularity** (reduced, row below) and **statistics** (open, the `−5/3`/intermittency row) — the second *not* derived here. No new axioms | [`lean/QLF_Turbulence.lean`](lean/QLF_Turbulence.lean), [`lean/QLF_QuantumTurbulence.lean`](lean/QLF_QuantumTurbulence.lean), [`Turbulence.md`](Turbulence.md), [`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`, the `su(2)` Noether charge, a pseudovector under T); vorticity = the local discrete curl, **quantized** to `±1` per cell (`vorticity_quantized`), so it cannot diverge and the Beale–Kato–Majda blow-up criterion is unsatisfiable on the substrate. `navier_stokes_continuum_limit` is **removed** (`QLF_NavierStokesBKM` carries the work): the opaque axiom unbundles into the *proven* Planck vorticity cap + the *cited* BKM theorem + a *sharp* faithfulness bridge, from which `navier_stokes_no_blowup` is a theorem — a reduction with the gap localized to vorticity-rendering faithfulness, not a Clay proof. **Caution (the competing-route trap, [`Millennium.md`](Millennium.md)):** the discrete cap alone proves too much — *every* bounded lattice discretization has one — which is exactly why the continuum step stays an axiom | [`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) |
| **Information is realized as ½-spin (it from bit)** | ✅ **Machine-verified** — the unit of information is the two-valued ½-spin closure. A single-valued (vector) fold-alphabet `{+I}` carries `binary_kl 1 1 = 0` nats; the two-valued spinor alphabet `{+I,−I}` carries `binary_kl 1 (1/2) = log 2` — exactly one bit (`single_valued_zero_information`, `two_valued_one_bit`, `spin_half_is_information_atom`: `0 < log 2`). The **2π double-valuedness is reproven from explicit rotation matrices** — a full turn is `+I` on the vector `SO(3)` rep but `−I` on the spin-½ `SU(2)` rep (`spinor_double_valued_vector_blind`, via `Complex.exp_pi_mul_I` / `Real.cos_two_pi`) — grounding the spinor **Cartan** discovered in 1913 (cited for the general classification only). Priority runs **abstraction → physical** (it from bit): information *is* the two-valued distinction, the ½-spin closure its minimal realization; "information is physical" is the downstream toll (`ΔF=−log 2`, finite realizability, `QLF_Realizability`). No new axioms | [`lean/QLF_SpinorInformation.lean`](lean/QLF_SpinorInformation.lean), [`Mathematics_From_QLF.md`](Mathematics_From_QLF.md) §Rung 5a, [`UniversalRelativity.md`](UniversalRelativity.md) §3b |
| **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** — rotation curves are the closure-balance **RAR** `g_obs²=g_bar·(g_obs+a₀)` (`radialAccel_self_consistent`, both limits exact), and 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π` — equal to best-fit MOND, against Newton (×2.7) and NFW (294 fit parameters). **The sector is closed to its honest floor:** the scale `cH₀`, the `1/2π` prefactor (the ZFA closure-loop period, `QLF_MondScale`), the interpolation function (**unique**, not chosen from the MOND family — `radialAccel_unique`/`radialAccel_eq_nu`) and the squared form of the conjunction (forced by the logarithmic free energy, `rar_is_free_energy_balance`) are all derived. Only two premises remain: acceleration-as-closure-rate, and 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 the single axiom `mre_factorization` (`riemann_hypothesis_in_qlf_via_MRE`), whose strength is **measured**: `mellinFactorization_iff_rh` proves the two-leg factorization is equivalent to RH and `mellinFactorization_independent_of_generator` proves `Z_QLF` does no logical work, so the scaffold is motivation for believing the bridge rather than a weakening of it. 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). **A competing route is now closed:** positive Ollivier–Ricci curvature would buy a spectral gap (Ollivier's graph Lichnerowicz bound), but `census_nowhere_positively_curved` ([`QLF_CensusCurvature`](lean/QLF_CensusCurvature.lean)) proves `κ ≤ 0` at every length, and the census's normalized-Laplacian gap collapses `≈ 4×` per added layer (`0.3169 → 0.0810 → 0.0192` for `L ≤ 8, 10, 12`) — the possibility graph has **no** spectral gap, so the gap is not there to be found; the `log 2` closure quantum stands by elimination ([`Curvature.md`](Curvature.md) §1c) | [`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). **Guard (a live trap, corrected):** the `C(2n,n)` count is **not** evidence for hardness and must not be cited as such — producing *a* ZFA closure of length `2n` is an `O(n)` loop (`^ⁿvⁿ`), so the *unqualified* search problem is in **P**, and the count is a *solution* density that makes sampling **easier**. The whole asymmetry rests on the qualifier "with property `X`", and the lean rests on the **no-extension-certificate** point, not on the size of the space ([`Millennium.md`](Millennium.md) § *The competing-route trap*) | [`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 `continuum_vorticity_planck_capped` (`QLF_NavierStokesBKM`), 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`), Hodge conjugation is the adjoint `H↔H†`, and Hodge classes are its balanced fixed points. The **algebraic side** is a graded ℚ-subalgebra, the image of a ℚ-algebra homomorphism from the cycle ring (`QLF_CohomologyAlgebra`); the **transcendental side** is a full Hodge structure (`QLF_HodgeStructure`). **The gap is exactly one input — geometric realization / polarization:** *which* Hodge structure the substrate's cohomology carries. That is precisely where the classical difficulty lives, and the faithfulness swings showed even the codim-1 Lefschetz `(1,1)` case is out of reach without a genuine cohomology theory of varieties. **This is the honest floor — no further substrate scaffolding closes it.** *(Contrast, once: the classical conjecture — finite ℚ-linear algebra, not independence — is not proved here.)* B/C/D share the same one bridge | [`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) |

### Axiom dischargeability — which of the 23 axioms could become theorems

**The engine behind every bridge (path integral · all closures · Witten 1988).** Each Millennium bridge axiom
below sits under QLF's one repeated move — *generate every possibility, then let a selection principle keep the
invariant* — the exact/constructive form of the Feynman path integral (all paths happen; **ZFA closure is the
firebreak** selecting the `C(2n,n)` closing histories, [`QLF_Firebreak`](lean/QLF_Firebreak.lean); and each
closing history **is a Feynman diagram** — the closure↔diagram map is machine-checked, `IsDiagram` with order-0
= the closure census and order-1 = the `2/(3π)` one-loop coefficient, [`QLF_FractalDiagram`](lean/QLF_FractalDiagram.lean), #138) and of
Witten's 1988 Jones-polynomial path integral (a non-rigorous physics sum-over-everything that produced rigorous
mathematics, **discharged by Reshetikhin–Turaev**). The bridge is the *continuum-rendering* leg, couched in that
Witten→RT mode. So "dischargeable" = "how close is this bridge to the **knot sector's finished end-state**"
(verified all-closures core + a settled-math continuum leg *already discharged* by RT). Class B is one settled-
math lemma from that end-state; Class A carries the problem's own content and, by design, is not (see
[`Millennium.md`](Millennium.md) § *The engine*).

QLF carries **13 `axiom` declarations** (the [`CLAUDE.md`](CLAUDE.md) axiom inventory lists each with its
role). The number is not maintained by hand: [`scripts/axiom_audit.sh`](scripts/axiom_audit.sh) pins the list
in `lean/axioms.expected` and fails CI on any assumption that is added or removed without review, and
[`lean/QLF_AxiomAudit.lean`](lean/QLF_AxiomAudit.lean) reports, via `#print axioms`, which of them each anchor
theorem *actually* consumes — because zero `sorry` says every goal was closed and nothing about what closed it.

Three have moved *off* the list, and the three ways of leaving it are different. **`censusTail_eq`**
(`QLF_AlphaBound`) was **discharged into a theorem** — proved from Mathlib's generalized binomial series
`Real.one_add_rpow_hasFPowerSeriesOnBall_zero` plus the identity `4ⁿ·choose(−½)n = (−1)ⁿ·C(2n,n)`.
**`navier_stokes_continuum_limit`** was **removed outright** — measured, it was satisfied by `⟨True, trivial⟩` and already superseded — with the work carried by a proven Planck vorticity cap + the *cited* BKM theorem
+ a sharp bridge (`QLF_NavierStokesBKM`). **`NonTrivialZero`** (`QLF_Riemann`) was neither: it was **never an
assumption at all**, only vocabulary listed as one, and it is now a definition over Mathlib's `riemannZeta`.
That correction *strengthens* the Riemann boundary rather than weakening it — while the predicate was opaque,
`spectral_hilbert_polya` was satisfied by the interpretation under which no complex number is a non-trivial
zero, so `riemann_hypothesis_in_qlf` held in a model where it said nothing about ζ. Naming the real object
makes the axiom carry the real content of RH. The general lesson is worth keeping: **an axiom that introduces
a name is not a boundary, and counting it as one hides how much is actually being assumed** — in either
direction.

A fourth route off the list is **merging**, which is normally the dishonest one — three assumptions restated
as one giant assumption is a smaller number and not a smaller commitment. It is legitimate exactly when the
equivalence is *proved*, and for Riemann it now is. `MellinStructuralSingularity`, `MRE_bridge` and
`zero_is_mellin_singularity` became the single `mre_factorization`, because
[`mellinFactorization_iff_rh`](lean/QLF_RiemannMRE.lean) proves the two-leg factorization is equivalent to RH
itself — an unconstrained middle predicate constrains nothing — and
`mellinFactorization_independent_of_generator` proves the generating function does no logical work either.
The scaffold is motivation for believing the bridge, which is what a scaffold is for; it was never a
weakening, and now that is a theorem rather than a reading. The same measurement shows why the *other*
tempting move is a trap: giving the predicate a concrete definition falsifies one leg or the other and makes
the axiom set inconsistent, which is strictly worse than an opaque boundary.

BSD went the same way and returned a sharper reading. `centralMultiplicity` and `modularity_mirror_invariant`
are the single `bsd_multiplicity`, licensed by `mirrorInvariant_iff_perspectives_agree`: with two perspectives
and a mirror that swaps them, invariance is not a symmetry from which agreement follows — it *is* agreement,
in involution language. So `bsd_rank_equals_order` restates its boundary rather than deriving from something
weaker, and the `#print axioms` footprint says so independently, consuming the boundary and not even
`propext` — the signature of a pure application. `mirrorMultiplicity_nonempty` adds the second half:
constant zero satisfies the interface, so **exhibiting a model is not evidence here**, unlike
`QLF_LatticeCalculus` where a *nondegenerate* instance genuinely discharged "suppose such a calculus exists".
The arithmetic content is the claim that the intended multiplicity — the real Mordell–Weil rank, the real
order of vanishing — is an instance, which is BSD. What the reformulation builds is untouched: self-dual
central point proved, concrete curve, computed Frobenius traces.

P vs NP returned the sharpest reading of the three. Its four axioms became the single `qlf_cost_model`, and
`costModel_nonempty` satisfies every one of them with a model built from `verify` and boolean negation —
`PTime f` reads "`f` agrees with `verify` somewhere", `search` negates `verify` pointwise, verification is
polynomial because `verify` agrees with itself, and the separation holds because `!b ≠ b`. Nothing about
running times, machine models or `C(2n,n)` enters. So **the axioms as stated constrain nothing about
polynomial time**; the content is entirely the claim that the *intended* cost model is an instance, which is
P ≠ NP. Two smaller findings came with it: `verify_is_ptime` is consumed by nothing, and `p_vs_np_in_qlf` is
`generate_not_reducible_to_verify` verbatim. None of it touches the module's real content — the verify-filter
identity and the `C(2n,n)` count are proven and independent of the boundary — and it sits alongside the
`C(2n,n)` guard already recorded above rather than replacing it. The remaining axioms split:

| Class | Axioms | Provable? | What discharge requires |
|---|---|---|---|
| **A — open-conjecture content** (the deliberate boundaries) | `spectral_hilbert_polya`, `resonant_computation_for`, `mre_factorization` (Riemann); `bsd_multiplicity` (BSD); `qlf_cost_model` (P vs NP); `yang_mills_gap`;  `hodge_algebraicity` (Hodge faithfulness — the located wall) | **No** — proving one *is* solving the corresponding open problem (Riemann / BSD / P-vs-NP / Yang–Mills, or the Hodge cycle-faithful encoding). These are the explicit `RCA₀→analytic/WKL₀` boundaries, not gaps. **Audited, not assumed:** each Class-A bridge sits where a *cheaper-looking* derivation appears available, and all six such routes were checked and found closed — the cheap fact is in every case automatic, pointed the wrong way, or about a different object ([`Millennium.md`](Millennium.md) § *The competing-route trap*). None is a near miss. | The very analytic / continuum / independence content the reformulation isolates — not a Mathlib lemma away. |
| **B — settled math Mathlib lacks assembled** | `lorentz_generated_by_boosts_rotations` (most feasible); `benincasa_dowker_limit`, `order_metric_continuum_limit`; `beale_kato_majda`, `continuum_vorticity_planck_capped` | **In principle, yes** — each is a *published* theorem (Lie generation of `SO⁺(1,3)`; Benincasa–Dowker 2010; Malament / Bombelli–Henson–Sorkin; BKM 1984), so provable but not yet in Lean. | A real multi-hundred-line Lean project: `sl(2,ℂ)≅so(1,3)` + exp-surjectivity onto the identity component (Lorentz); Poisson processes on Lorentzian regions (CST limits); Sobolev/Gronwall PDE regularity (BKM). Mathlib has fragments, not the assembly. |

**Bottom line.** The axioms that *can* be proven are the **Class B** "settled math" ones — chiefly
**`lorentz_generated_by_boosts_rotations`** (the standard Lie-generation fact; its generators `boostZ_action`,
`rotZ_action`, the `{±I}` kernel, **all generator families realized** (`boost_realized` + `rot_realized` +
`rotY_realized`, two rotation axes), **their KAK products** (`so3_euler_realized` + `kak_realized`), **and the
forward inclusion** — all three generators preserve the Minkowski metric (`boostMatrix_preserves_metric` etc.,
so `{realized} = {KAK products} ⊆ O(1,3)`) — are proven in `QLF_LorentzGeneration`, so only the *reverse*
inclusion "every `L` **is** such a product" — the KAK angle-extraction surjectivity — is axiomatic. **The
reverse recovery is now partly built too:** `su2_realized` (general `SU(2)→SO(3)` from a unit quaternion),
`exists_boost_params` (constructive boost rapidity, nested √, no `arccosh`), and `su2Matrix_recovery` +
`recovered_quaternion_norm` (the reverse quaternion trace identities and the division-free `‖·‖²=4(1+tr)`
normalization well-definedness) — localizing the residual to the `SO(3)` angle-extraction case split (the
geometric counterpart of the Millennium continuum bridges). But **none is a quick win**: each needs Mathlib
machinery not yet assembled. The **Class A**
axioms cannot be proven without solving the underlying conjecture — that is their purpose. The one clean
discharge available (`censusTail_eq`) is done, and `navier_stokes_continuum_limit` is removed as vacuous; QLF refines
these boundaries as the machinery arrives (`QLF_RiemannMRE`, `QLF_NavierStokesBKM`) rather than
posit-and-forget. For *why* the Class A conjectures should nonetheless be **true** — the active-inference
reason the substrate side holds (each conjecture asserts one of the closure conditions the construction
enforces) — see [`Active_Inference_Mathematics.md`](Active_Inference_Mathematics.md) §6.

---

## Open — quantitative (the hard front)

**Frontier consolidation — the remaining value-open targets collapse to *three* numbers, not a dozen**
(and, with #121 resolved and the QED running structure census-complete, effectively toward *one input +
one classification*).
The honest structure of what's left (see the per-item rows below): most of the open quantitative targets
are **the same open number** wearing different hats, so they are not separately "nail-able" — deriving one
closes many at once. The three genuinely-distinct open quantities are:

> **Update — #121 resolved (fork 1): the electroweak-scale *mechanism* is derived; `v` is QLF's one
> irreducible anchor.** Item 1 below is no longer an *open coupling* to derive but a *closed mechanism*
> plus a *single honest input*. The interacting closure-binding is a proven chain — attraction is a
> theorem (`QLF_ClosureAttraction`), it supplies the restoring force creating a finite steady density
> (`QLF_SteadyStateDensity`), the loop to `v` is closed (`QLF_ElectroweakScale`), and the cascade
> self-organizes to a scale-free fractal critical state (`fractal_cascade.py`, `τ=3/2=`census) — *why*
> `v ≪ M_Pl` is stable **without fine-tuning**. What is *not* derived is the **absolute** scale `v`
> itself, and that is honest: `b_EW = ln(M_Pl/v)/2π = 6.118` provably has **no clean substrate count**
> (refused as a fit-trap, `closure_binding.py §4`), and `v` is the SM's *second* dimensionful scale,
> distinct in origin from the derived `m_p` (`14π`). So QLF reduces the SM's dimensionful sector to
> **{Planck floor + one electroweak anchor `v`}** — mirroring the SM's single dimensionful input — with
> everything else (`m_t`/`M_H`/`G_F`, the absolute mass spectrum, the mass-scale halves of `α` and `G`,
> #136) derived *relative* to `v`. **Not a bug — the framework's one honest low-energy input.**

1. **The self-organized-critical closure-binding coupling `g`** ✅ **mechanism resolved (#121, fork 1);
   `v` is the one irreducible anchor** — (the interacting *substrate-dynamics*
   problem — *not* a counting exercise, established at #121 / `Higgs.md` §5a). Fixing `g` fixes the absolute
   scale `R_stable = v`, and with it: the electroweak `v`/`m_t`/`M_H`/`G_F` (#121); the absolute lepton &
   quark mass *values* (the ratios like `m_p/m_e=6π⁵` are already derived — only the overall scale is `g`);
   the neutrino absolute `Δm²` (oscillation *structure* done, `QLF_NeutrinoOscillation`); `α_s(M_Z)`'s
   absolute value (`b₀=7` done, only the `Λ_QCD`-to-floor scale is `g`); and the mass-scale half of the
   absolute SI `G` (`α_G = exp(−28π)` done, `QLF_GravitationalCoupling`). **Diagnosis (#121):** this is
   condensation criticality, so it is *not* a clean count (`b_EW` has none) — it needs the interacting
   many-closure density at the critical point. **The residual is now precisely localized in Lean**
   (`QLF_BindingStrength`): the gravitational floor `g_grav = c·N_c/(4π²) = 9/(8π) ≈ 0.36` at
   Kibble–Sciama `c=3π/2` is **subcritical** (`gravBinding_subcritical`, `< g_crit=1`), so
   closure-binding must supply the rest (`binding_must_supply_rest`); and `g = (log 2)·channel·packing`
   (`bindingCoupling`, monotone in the packing) pins the open number to the single **packing factor** —
   the interacting many-closure density at the SOC point. **The packing factor was then modelled from the
   8-twist combinatorics and the verdict Lean-anchored** (`QLF_PackingFactor`): in the standard NJL loop
   form `closureLoopCoupling mult = mult·N_c/(4π²)` (like `g_grav`), the bare packing is **O(1)** and
   subcritical for any alphabet multiplicity `mult ≤ 8` (`bare_packing_subcritical`, `= 6/π² ≈ 0.61` at 8),
   and since `condensationDepth = π/(4g²)` is antitone (`condensationDepth_antitone`), an O(1) coupling
   gives only O(1) depth — so a bare count **cannot** produce the `v ≪ M_Pl` hierarchy (which needs
   `g ~ 10⁻⁸`). So `g`/`v` is **not a clean combinatorial count** — now shown *by construction*, not merely
   asserted — it is the near-critical SOC value (interacting dynamics; **not fitted**, not derived; `v`
   stays calibrated, not predicted). **The interacting dynamics is now modelled the substrate-native way**
   (Grok's roadmap), reducing the residual to a *single* SOC observable: (i) **gauge folds attract** — a
   *theorem*, `QLF_ClosureAttraction`: free action `|count_pos−count_neg|` is subadditive
   (`freeAction_subadditive`), strictly reduced for opposite gauge (`opposite_gauge_attracts`), to zero for
   complementary (`complementary_binding_closes`) — channel selection is the *sign*, not a posit; (ii) that
   attraction **supplies the restoring force** that creates a finite steady defect density the bare
   (monotone) census lacks — `QLF_SteadyStateDensity`: `netRate = c − k·ρ²`, unique attractive fixed point
   `ρ* = √(c/k)` (`steady_is_fixed_point`, `netRate_strictly_decreasing`), and at `k=0` **no** steady state
   (`no_steady_without_binding`) — the interaction is the lever; (iii) the **loop to the electroweak scale
   is closed** — `QLF_ElectroweakScale`: `g = (log 2)·channel·packing(ρ*)` (`g_eq_binding_quantum`) and
   `R_stable = 1/ρ*` (`RStable_eq`), so `g` and `v` are both functions of the one density `ρ*`. Engine
   measurement: [`defect_density.py`](defect_density.py) (converges to `√(c/k)`, `k=0` diverges, reported
   honestly). **So the residual is now the single SOC observable `ρ* = √(c/k)`** — the creation rate `c`
   (cascade generation) and binding rate `k` (shared-closure combinatorics + `log 2`), derivable in
   principle from the 8-twist alphabet, the one remaining number (**not fitted**; `v` calibrated, not
   predicted).
2. **The QED one-loop running coefficient `2/(3π)` per charged fermion** (the α-residual / running,
   [#117](https://github.com/jimscarver/quantum-logical-framework/issues/117)) — a *value-free* census
   vacuum-polarization target (horizon-weighted, `closedAtHorizon`), distinct from `g`. **The leading
   coefficient is now census-anchored** (`QLF_VacuumPolarization`, committed before comparison to QED —
   Step-0): `2/(3π) = 2·(1/6)·2·(1/π)`, where the two non-trivial factors are *derived* — the **`3`** is
   the two-vertex split census `∑_{k=0}^{n} k(n−k) = (n+1)n(n−1)/6 = C(n+1,3)` (`census_split`, so the
   split-average `→1/6 = 1/3!`, the discrete Feynman integral `∫₀¹x(1−x)dx`), and the **`π`** is the
   Wallis census return density (`QLF_PhysicalPi`); the per-fermion β-coefficient is `b = −4/3` in the
   `inv_coupling` convention (`qed_beta_coeff_per_fermion`, the screening sign). **And the horizon→scale
   *tower* is now anchored too** (`QLF_VacuumPolarizationTower`) — the running *function* `α⁻¹(Q²)`, not
   just the coefficient: the finding is that **the QED logarithm IS the census octave count**. The
   horizon map `Q(R)=Q₀·2^R` makes the `closedAtHorizon` resolution pass `R` the octave counter
   (`log_scale_additive`: `ln Q(R_Q)=ln Q(R_f)+(R_Q−R_f)·ln 2`); each octave adds the *scale-free*
   increment `(2/3π)·Q_f²·log 2` (`perOctaveIncrement`, octave-independence *reused* from Kolmogorov's
   `flux_scale_invariant`); and the discrete octave count renders *exactly* to the smooth QED
   `ln(Q/m_f)` (`octave_tower_recovers_qed_log`, via `k·log 2 = ln 2^k`). Fermion **thresholds are
   automatic** (ℕ-truncated `R_Q−R_f` → 0 below threshold, `inactive_below_threshold`), the tower is
   the sum over active elementary closures (`towerRunning`), and `α⁻¹` decreases monotonically toward
   the UV (`towerRunning_le_alpha0`, screening). So `α⁻¹(Q²)=α⁻¹₀−Σ_f (2/3π)Q_f²·ln(Q²/m_f²)` is
   assembled with every factor census-sourced. **And the charge-census factor is now derived too**
   (`QLF_ChargeCensus`): the `Q_f²` weighting summed over QLF's own Standard-Model content — 3
   generations (`num_generations_eq_three`), 3 colours, charges `1, 2/3, 1/3` (thirds forced by the 3
   colours, `charge_quantum_from_colours`/`down_quark_charge_third`), neutrinos neutral
   (`neutrino_neutral`) — is **`Σ Nᶜ Q_f² = 8 = 2³`** (`totalChargeCensus_eq_eight`,
   `totalChargeCensus_eq_two_cubed`): the charge census *equals the 8-twist alphabet size* (cousin of
   the `128 = 2⁷` in `α⁻¹ = 128 + d²`), split **leptonic 3 + hadronic 5** (`census_lep_plus_had`,
   the `Δα_lep ≈ Δα_had` near-equality). So the fully-active running slope's charge factor is the
   QLF-derived `8` — `smRunningSlope = qedVacPolCoeff·8 = 16/(3π)` per `ln Q` (`smRunningSlope_eq`),
   the correct SM electromagnetic β-slope, which tightens `α(M_Z)`. *Open (the residual value, not the
   structure):* the two integer `2`s (e⁺e⁻ pair, `μ²=2ln μ` round-trip) are rendered vertex structure,
   not counted; and fixing the `0.036` value now needs only the **threshold octaves** `R_f` — the
   fermion **mass spectrum** (`QLF_MassSpectrum`: ratios derived, absolute scale = the open `g`/`v`,
   frontier #1) — **plus** the **non-perturbative hadronic** `Δα_had` (open in the Standard Model
   itself, measured dispersively). So the residual has moved from "which closures, weighted how" (now
   the QLF-derived `8 = 2³`) to {mass-spectrum thresholds + the SM's own hadronic problem + absolute
   scale} (**not fitted**; the `0.036` minefield stays pre-buried, `QLF_AlphaRigidity`). The tower
   supplies the skeleton, the census the charges; the thresholds are the mass spectrum. Success also
   tightens `α(M_Z)` and the `sin²θ_W` running.
3. **The holographic-density resolution** — *why* the realized horizon entropy is `N/4` not `N log 2`
   (the residual is **exactly `4 log 2 = 4 × log 2`**, quantified + decomposed into derived constants,
   `QLF_HolographicDensity`; the *classification* — floor deviation vs. `1/(4 log 2)` packing vs.
   area-element — is open). This is the entropy-normalization half of the absolute `G`.

So "nailing" the frontier is really **two hard problems + one classification**: the interacting-substrate
coupling `g` (1), the census running coefficient (2), and the entropy packing (3). **Update — (2)'s
*structure* is now census-complete** (`QLF_VacuumPolarization`/`…Tower`/`QLF_ChargeCensus`, #117): the
coefficient `2/(3π)` (split census + Wallis, the `→1/6` limit **proven**), the running *function* (the
QED log = the census octave count), and the charge weighting `Σ Nᶜ Q_f² = 8 = 2³` are all derived
value-free — so (2) is no longer a *distinct* open number: its residual *value* is precisely the
threshold octaves (the mass spectrum, i.e. **(1)'s scale `g`**) **plus** the non-perturbative hadronic
`Δα_had` (**open in the Standard Model itself**, not a QLF gap). **Update — #117 closed:** with the
structure census-complete and the residual cleanly attributed to (1)'s scale + the SM's own hadronic
piece, [#117](https://github.com/jimscarver/quantum-logical-framework/issues/117) is closed. **Update —
the census-diagram carrier landed (#138):** the "sum over nested closures" of the tower now has a
machine-checked inductive carrier — `QLF_FractalDiagram`'s `IsDiagram` (closure-as-Feynman-diagram, order
= depth) with its two gates *order-0 = the closure census* (`order_zero_iff_closure`) and *order-1 weight
= `2/(3π)`* (`orderOneWeight_eq`); the depth-≥3 tail (the `0.036`) stays exactly the frontier-#1 +
SM-hadronic residual above ([#138](https://github.com/jimscarver/quantum-logical-framework/issues/138)
closed; `Frequency_Synchronization.md` §0a). **Update — (1) is resolved (#121, fork
1):** its *mechanism* is derived (the proven attraction → restoring-force → EW-loop chain + SOC
self-tuning) and its *value* `v` is QLF's **one irreducible electroweak anchor** — the SM's second
dimensionful scale, not a clean count (`b_EW` refused), *not a bug*. So the frontier is really **{one
honest input `v`} + the entropy classification (3)**, with an SM-external hadronic problem attached to the
α-value and everything dimensionful derived *relative* to `v`. CKM/PMNS *angles* and the Jarlskog invariant
are a Yukawa-sector target (structure done, `QLF_CKM`/`QLF_PMNS`); `H₀` is the same absolute-time-delay
calibration as `v`. Attempting to *derive* `v` by *counting* is a fit-trap (as `b_EW` showed); the honest
posture is that `v` is the anchor and the mechanism around it is derived — the disciplined end-state.

| 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) |
| **Turbulence statistics — Kolmogorov `−5/3` + intermittency** | 🔵 **Open — quantitative (self-similar-closure reading, made falsifiable).** The *statistics* side of Navier–Stokes, distinct from the regularity boundary above. **`−5/3`** reduces to flux-invariance + K41 dimensional analysis, Lean-anchored (`flux_scale_invariant`; `kolmogorov_exponents` = `(2/3,−5/3)`, the *unique* dimensional solution), and `ζ₃ = 1` (the exact `4/5` law) holds by flux conservation. **Intermittency:** closures are rare quasi-independent events ⟹ Poisson occupation ⟹ **log-Poisson = She–Leveque**, not log-normal — decided on realizability, since log-normal `ζ_p` turns over past `p ≈ 14.5`. Both parameters are anchored with distinct origins (`C₀ = d−1 = 2`, the codim of 1-D filaments; `β = 2/3` from the dimension-independent Hölder `h = 1/3`) ⟹ `μ = 0.222`, parameter-free, matching data. **Open:** one residual posit — most-singular-flux = inverse-turnover — standard phenomenology QLF supplies the geometry for. Lives or dies by it | [`lean/QLF_Kolmogorov.lean`](lean/QLF_Kolmogorov.lean), [`turbulence_intermittency.py`](turbulence_intermittency.py), [`Navier_Stokes_Geometry.md`](Navier_Stokes_Geometry.md) §6a, [`lean/QLF_Turbulence.lean`](lean/QLF_Turbulence.lean) |
| **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 — reduced (wave equation now 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`). **The linearized wave equation is now anchored via the density-perturbation route:** a GW is a propagating modulation `δρ` of the closure density around the SOC equilibrium `ρ*`, and the discrete d'Alembertian annihilates every traveling-wave profile (`boxD_dAlembert`, `boxD_metricPerturbation`) ⟹ `□_d δρ = 0` at `c`, continuum limit `□h_μν = 0`; the **quadrupole is the leading radiative multipole** (`quadrupole_is_leading_radiative`: monopole/dipole non-radiative by mass/momentum conservation). **Localized-open:** deriving the operator `boxD` from the SOC rate equations (`QLF_ClosureAttraction`/`QLF_SteadyStateDensity`) — the dynamical-metric step, the same gap as the full Einstein field equations — and the luminosity *coefficient* `G/(5c⁵)`; `gravitational_waves_in_progress` | [`lean/QLF_GravitationalWaves.lean`](lean/QLF_GravitationalWaves.lean), [`gw_density_wave.py`](gw_density_wave.py), [`GR_Schwarzschild.md`](GR_Schwarzschild.md) |
| **Running couplings / renormalization** | 🔵 **Open — quantitative (structure Lean-anchored)** — one-loop log running with the `2π` loop phase, asymptotic freedom vs screening, and the Landau pole located but **cut off by the substrate's discrete UV floor** (no continuum UV catastrophe). **Substrate-fixed:** the QCD β-coefficient `b₀ = 7` from `N_c=3` axes + `n_f=6`; the full SM triple `(b₁,b₂,b₃) = (41/10, −19/6, −7)` from QLF counts + standard one-loop weights; the `sin²θ_W` flow *direction*; and the GUT-scale *structure* (`t*` formula, slope `109/15`, target `3/8`). **The electroweak sector collapses to one open scale.** `λ(M_Pl)=0` (SOC boundary) runs down to `λ(v)≈0.13`; `m_t = v/√2` (0.8% from pole) via the QCD IR quasi-fixed point; so `M_H → λ → m_t → v → R_stable → G` bottoms out in **one** unknown. Condensation itself is **settled** — the NJL loop *is* the closure census, which diverges (Wallis), so `g_crit → 0` at the Planck floor and condensation is generic ([#121](https://github.com/jimscarver/quantum-logical-framework/issues/121)); the open number is the coupling magnitude `g`, its irreducible piece the 8-twist packing factor. **For `α`:** bounds `137 < α⁻¹ < 137.048` Lean-verified, the `+0.036` residual open; the one-loop coefficient `2/(3π)` is **census-anchored** (the `3` from the two-vertex split census, the `π` from Wallis), the QED logarithm **is** the census octave count, and `Σ Nᶜ Q_f² = 8` — the alphabet size. Residual now needs only threshold octaves + non-perturbative `Δα_had` (open in the SM too), **not fitted**; one-term geometric patterns (`dim Gr(3,15)`, `9/250`, `(3/15)²`) are **refuted** — they match only the rounded `0.036`, fail at the 5th decimal, and are static where the residual runs. `α(0)` carries **no cosmological drift** (proven) — a falsifiable prediction sharper than the SM. Absolute scale (`M_GUT`, `α_s`, `v`) is frontier #1, the same boundary the SM/MSSM have. Full detail: [`Alpha.md`](Alpha.md), [`Higgs.md`](Higgs.md), [#117](https://github.com/jimscarver/quantum-logical-framework/issues/117) | [`lean/QLF_VacuumPolarization.lean`](lean/QLF_VacuumPolarization.lean), [`lean/QLF_VacuumPolarizationTower.lean`](lean/QLF_VacuumPolarizationTower.lean), [`lean/QLF_ChargeCensus.lean`](lean/QLF_ChargeCensus.lean), [`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** | Not *numerically* resolved (the absolute `H₀` is the one cosmological calibration). But QLF says something: it is a **dynamical-dark-energy, non-ΛCDM** cosmology (`ρ_Λ ∝ H²` ⟹ early-DE character = the *resolution-favorable* class; emergent gravity, no particle CDM), so the CMB `H₀≈67` is a ΛCDM *inference* QLF doesn't share; and its blind SPARC dark-matter fit (`a₀=cH₀/2π`) independently **votes local** (`H₀≈72.9`). The tension is reframed as ΛCDM-inference-dependence, not a crisis — *a perspective + a data vote, not a derivation* | [`DarkMatter.md`](DarkMatter.md) §5a, [`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 causal-set order→metric program on QLF's causal set: the **number↔volume / proper-time rung is Lean-anchored** (`QLF_CausalInterval`); the **Benincasa–Dowker operator is anchored at its flat baseline** (`bdCurvature_chain_zero` — the balanced `+1,−2,+1` layer stencil annihilates a chain); **2-D is anchored with the branching layer-growth computed** (`layer_growth_from_branching`, a size-independent dimension fingerprint); and the **statistical continuum limit** is carried by the explicit bridge axiom `benincasa_dowker_limit` (settled CST Poisson/Lorentzian machinery), from which `flat_curvature_zero_in_mean` is derived. **So the curvature side has the Millennium shape — verified discrete core + one continuum bridge.** *Tensor route*: Jacobson's derivation splits into three arrows (horizon thermodynamics → `S_ab k^a k^b = 0` → `S_ab = f g_ab` → `f = −R/2 + Λ`) and the **algebraic middle arrow is closed with no axiom** — `finite_null_probes_force_metric` forces the metric form from **nine integer null probes** of the substrate Hermitian lattice ((1,±1,0,0) and the `3-4-5` triples), the continuum of null directions being gratuitous; `null_annihilator_iff_metric_multiple` makes it a characterization (the annihilators are exactly the multiples of `g`), `axis_probes_insufficient` shows the nine are sharp. **Arrow 3 is closed too, with zero new axioms** — `einstein_field_equations` derives `G_ab + Λ g_ab = κ T_ab` from the metric form via contracted Bianchi + conservation, `Λ` falling out as the integration **constant** (`scalar_multiple_is_curvature`); the differential-geometry boundary is a `DivergenceCalculus` **structure** (a hypothesis in each signature, discharged by *building* an instance) rather than an axiom, and `metric_form_from_null_probes` chains arrow 2 into it. **Open:** the single remaining arrow 1 — `δQ = T δS ⟹ (R_ab − κT_ab)k^ak^b = 0` (local Rindler + Raychaudhuri focusing); plus general `d ≥ 3` and the BD-action assembly on the curvature route | [`lean/QLF_EinsteinEquations.lean`](lean/QLF_EinsteinEquations.lean), [`lean/QLF_NullTensorReconstruction.lean`](lean/QLF_NullTensorReconstruction.lean), [`lean/QLF_BianchiClosure.lean`](lean/QLF_BianchiClosure.lean), [`lean/QLF_CausalInterval.lean`](lean/QLF_CausalInterval.lean), [`Einstein_Equations.md`](Einstein_Equations.md) §6a–§6c |
| **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 + the Weinberg-angle value), coupling `g`, `G_F`, flavor-change & τ-decay vertex topology, and **the Koide phase** — the invariant is `Δ = 3δ = 2/3`, which **is** `m_μ/m_e = 206.77` in other coordinates, so it is the honest difficulty class. Standing results: the hierarchy needs **no large number** (the electron sits `2.27°` from the massless wall of `1+√2cos θ`, and the `3477×` ratio is that deficit squared); the wall exists **only because `A² = 2`**, which QLF derives, so substrate geometry is what makes a lepton hierarchy *possible*; the `+9.83 ppm` residual is **retired** as a coordinate artefact (the near-zero amplifies by `12.5`, so the ansatz's own `3.4×10⁻⁵` knowledge of `Δ` covers `±424 ppm`); and the *pole-mass* form of the relation is a **confirmed** prediction (running is 183× worse). Eleven derivation routes are **closed** — `Δ = Q` refuted, census count-ratios, circle divisions, all three curvature notions, symmetric-functional extremization, and more — each with its reason tabulated in [`Weak_Force.md`](Weak_Force.md) §5c⁗ and the round-by-round record in [#140](https://github.com/jimscarver/quantum-logical-framework/issues/140). Any derivation must produce an **`O(1)` rational in radians**, **forced rather than selected** (a route costing more bits than the constant is a re-encoding). One live candidate: `Δ` as a **rotation number**, mode-locked at a simple rational — which explains why a *simple rational at all* and retro-explains the bit-cost ordering (Farey depth = description length), but does not pick `2/3` | [`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α)` from the substrate α (`von_klitzing_substrate`, 0.026%); integer-QHE plateaus; Cooper pair = boson; **anyon statistics anchored** (2-D braiding gives a continuous phase, 3-D forces `±1`). **FQHE:** the composite-fermion tower is closures-within-closures, and the **odd-denominator rule is derived from closure parity** — the composite stays a fermion ⟹ even flux ⟹ odd denominator; the enumeration reproduces all 10 observed principal fractions and reads even-denominator `5/2, 7/2` as paired non-Abelian (Moore–Read) closures. **Stability ordering Lean-anchored** (`jainDenom_odd`, `jainDenom_depth_mono`, `particle_hole_same_depth`): the observed `1/3~2/3 > 2/5~3/5 > 3/7~4/7 > 4/9` is exactly the depth order `3<5<7<9`. **Open:** the one physical premise (deeper = smaller gap, named not derived), the BCS gap equation, absolute FQHE gap values, topological band structure | [`lean/QLF_FQHE.lean`](lean/QLF_FQHE.lean), [`lean/QLF_CondensedMatter.lean`](lean/QLF_CondensedMatter.lean), [`lean/QLF_Anyons.lean`](lean/QLF_Anyons.lean), [`Electricity.md`](Electricity.md) §6–§7a |
| **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). **Oscillation *structure* now Lean-anchored** (`QLF_NeutrinoOscillation`, verifies `Decay.md` §2.1): flavor conversion is a norm-preserving precession `dP/dt=Ω×P` that **conserves neutrino number** (`flavor_precession_conserves_number`; incl. the turbulent prime-kick, `prime_kick_conserves_number` — a rotation, not a decay); two-flavor unitarity + bounds (`two_flavor_unitarity`/`_bounds`, rooted in PMNS `mixing_unitary`); driven by the fold-depth splitting `Δm²=1/R_i²−1/R_j²` (`deltaMSq`/`no_oscillation_iff_degenerate` — requires non-degenerate depths ⟹ nonzero Majorana masses). Open: the tiny mass *values* (`m∝1/R`, very large `R`), the PMNS mixing *angles* + absolute `Δm²`, and the seesaw — none quantitatively derived (`pmns_in_progress`) | [`lean/QLF_NeutrinoOscillation.lean`](lean/QLF_NeutrinoOscillation.lean), [`Beta_Decay_Neutrino_Nature.md`](Beta_Decay_Neutrino_Nature.md) §3, [`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 |
|---|---|---|
| **Turbulence-forced decay + the prime-synchronized cascade dump** (the decay chain) | 🟣 **Structural skeleton Lean-anchored; dynamics phenomenological** (reuse + genuine proofs, no new axioms). Turbulence rains prime `±i` phase-slips; a slip that drives a stable closure out of balance **ends** it (`slip_out_of_balance_ends_closure` — no receipt, hence no closure), releasing `log 2`. The resonant rate has a proven vacuum limit and enhancement-only monotonicity, and constant hazard **is** the exponential law (`exponential_decay_from_constant_hazard`). **Decay is deterministic** — the exponential is the incoherent-bath statistics of a determined prime-lock, not fundamental randomness. The chain: neutrino (a number-conserving *rotation*, `flavor_precession_conserves_number`) → muon (a *true* number-changing decay) → neutron (same form once the Pauli block is a ZFA stability condition) → supernova (the collective `log 2` dump). **Open:** the rates — couplings `Γ_p, Q, S, κ`, the same coupling-*strength* residual as the four-fermion binding. **Not** a claim about lab muonium or real supernovae | [`lean/QLF_PrimeCascadeDecay.lean`](lean/QLF_PrimeCascadeDecay.lean), [`lean/QLF_NeutrinoOscillation.lean`](lean/QLF_NeutrinoOscillation.lean), [`Decay.md`](Decay.md), [`Turbulence.md`](Turbulence.md) |
| **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**; `hodge_class_is_algebraic` etc. are *derivations from that axiom*, not proofs. **Genuinely built** (real structures and theorems): the motive object, the motivic Galois group, the anabelian full-faithful functor and its Galois sequence, and **`π`, `ζ(3)` from the census** (Wallis / Apéry). Both cohomology sides are now concrete — the algebraic as a graded ℚ-subalgebra, the transcendental as a Hodge structure — so the bridge no longer carries everything and the gap reduces to **geometric realization**. The standard conjectures are **finite ℚ-linear algebra, not independence phenomena**, so "ZFC's defect" does *not* apply. The defensible claim is the substrate ontology plus the reformulation | [`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 |
| **Evolution as generate-and-select** (#119) | 🟣 **Structural reading** (reuse-only, no new axioms) — biological evolution *instantiates* the ZFA generate-and-select census: the structured mutational landscape = the generated possibility space, fixation = closure, the niche = the closure horizon (`QLF_Firebreak`'s `4ⁿ`-generated / `C(2n,n)`-realized firebreak, `not_all_paths_close`; horizon-relative closure, `QLF_HorizonClosure`). Anti-teleology **by construction** (closure is a filter, not a goal — directed mutation refuted and never needed). §3 answers *how a possible niche can stay unfilled* — three tiers (generated / closing / **reached**, `QLF_ReachableEvent`) + five constraints (unrealizable / unreachable / excluded / unaffordable / untimely), the possibility-vs-realization gap that makes selection non-vacuous. The **generate step is quantum → ZFA** (proton tunnelling in DNA, Löwdin / Slocombe–Al-Khalili) under QLF's QM=ZFA reading. **Honest floor (by design, not a gap):** QLF supplies the *structure* of evolution, **not** a biological constant — no mutation rate/spectrum derived (the named defeater); the quantum-generate claim is as strong as QLF's core QM=ZFA program, no stronger | [`Evolution.md`](Evolution.md), [`lean/QLF_Firebreak.lean`](lean/QLF_Firebreak.lean), [`lean/QLF_ReachableEvent.lean`](lean/QLF_ReachableEvent.lean), [`Creation.md`](Creation.md) |
| **Feigenbaum δ — rejected as a substrate constant; universality is the live question** | 🔴 **Rejected route** (kept, per [`ScientificApproach.md`](ScientificApproach.md): a rejected route constrains the next attempt). `constants_mapper.emerge_feigenbaum()` was reported as **DERIVED** in the NATIVE QLF CONSTANTS REPORT beside `4.669201609`. It is not a derivation and has been **removed from the report**: the construction picks prime bases, searches for `p, 2p, 4p, 8p` ladders with `2**k` written in, reads the load off the *minimum* entropy density, drops non-monotone ladders, and averages the last five ratios — a free fitted kernel (R2), and multiplicity-invariant, so bookkeeping by the method's own rule 4. **Why no substrate answer is expected:** δ is a property of *smooth unimodal maps with a quadratic critical point*, and is class-dependent (quartic ≈ 7.2846, sextic ≈ 9.296); a discrete substrate has no critical-point order until a rendering is chosen, so δ belongs to the **rendering layer** — which is what QLF's own thesis predicts. *(Scoping an overstatement: discreteness is no bar to an accumulation point — integer `R` can generate derived reals `λ_R → λ_∞`. The correct narrower claim is only that δ is not a primitive substrate constant.)* **The replacement question, which needs no target number:** do microscopically different closure rules flow to the same coarse-grained census statistics — same first-closure distribution, depth spectrum, transfer spectrum? That tests universality itself, on existing `contextual_census.py` machinery. **Kill condition, stated first:** if the coarse-grained limit depends materially on the microscopic rule, there is no universality class and the route closes. **The sharp follow-on, if it survives:** characterize the common effective map's critical point, and ask whether QLF *forces* the generic quadratic class (a symmetric extremum with `a₂ ≠ 0`). Deriving the class would make δ and `α_F ≈ −2.5029` predictions of the rendering rather than fitted constants — the result worth having, and strictly stronger than a decimal match | [`constants_mapper.py`](constants_mapper.py) (`emerge_feigenbaum`, docstring), [`ScientificApproach.md`](ScientificApproach.md) §labels, [`contextual_census.py`](contextual_census.py), [`Mathematics_From_QLF.md`](Mathematics_From_QLF.md) |
| **The frame posit — what an elementary distinction *is*** | 🔵 **Open, and now isolated to one sentence.** The alphabet-necessity result above derives `\|Σ\| = 8` from a single remaining assumption: *an elementary distinction is a signed element of the observable frame of a two-valued system.* Everything downstream — four conjugate pairs, four terms in `F(h)`, three spatial axes, the gauge pair, non-commutativity — follows. **Why this is progress and not relabelling:** the posit is now attackable on its own, where before it was hidden inside a number that looked chosen. **What would discharge it:** a derivation of "signed frame element" from the information atom alone — i.e. showing that the minimal *distinguishing act* on a two-valued system is necessarily a signed frame element rather than, say, an arbitrary unitary or a projector. **What would refute the surrounding argument:** a physically motivated alphabet that is composition-closed and not of size `2`, `4` or `8` — by `no_six_twist_alphabet` this cannot be done inside the Klein frame, so a refutation must attack the frame reading itself. Tracked here rather than in the budget because it is the last structural (not bridge) assumption in the stack | [`ScientificApproach.md`](ScientificApproach.md) §1c, [`eight-twists-sufficiency.md`](eight-twists-sufficiency.md) §7c, [`lean/QLF_AlphabetNecessity.lean`](lean/QLF_AlphabetNecessity.lean) |
| **The bridge layer — from substrate object to laboratory observable** | 🔵 **Open as a programme, now with a protocol.** Every empirical QLF claim passes through a *bridge*, and a bridge is where a formally impeccable result can become a physically empty one. [`ScientificApproach.md`](ScientificApproach.md) §5 now types the arrows (definition / theorem / physical identification / calibration / conjecture), states four admissibility constraints that information physics imposes before any physics is done (closure invariants only; one calibration per dimensionful observable, counted; capacity is a census axis not a parameter; a bridge earns content only by changing a count of ways), and grades bridges on the ladder *arbitrary → pre-registered → constrained → **derived***. **The standard is already met once:** `μ(h) = 8^{−\|h\|}` is *derived*, not chosen — prefix-freeness plus Kraft force it ([`QLF_KraftMeasure`](lean/QLF_KraftMeasure.lean)). **The open work is to constrain the rest:** show how few maps §5b admits for the context-geometry and probability bridges, rather than freezing one. **Sharpened statuses that came out of writing it down:** the cylinder measure is *two* claims — a **proved** measure and an **open** identification with event probability (the Born frontier); and `\|Σ\| ∈ {2,4,8}` is **internal**, constraining the budget rather than any observable | [`ScientificApproach.md`](ScientificApproach.md) §1c, §3, §5, §7a, [`Born_Rule.md`](Born_Rule.md) §8 |
| **The horizon re-basing map `ρ_H`** (nested domains — the central bridge) | 🔴 **Open, and now stated precisely enough to attempt.** [`BLACK-HOLES.md`](BLACK-HOLES.md) §4a's nested reading needs a map from the parent's balanced census to the child's with four properties: `ZFA(h) ↔ ZFA(ρ_H h)`; `fold(ρ_H h) = fold(h)`; bijectivity of censuses; and **reachability transport**, `h₁ ≺ h₂ ↔ ρ_H h₁ ≺_C ρ_H h₂`. The first three give *the same possibilities, independently rendered*; **the fourth is what earns the word "universe"**, since transported reachability is what gives an interior a chain `E₀ ≺ E₁ ≺ …` rather than a single closure — and a chain is what an internal clock needs to have anything to count. **Already proven and reusable:** [`QLF_BasisIndependence`](lean/QLF_BasisIndependence.lean) gives exactly properties 1–2 for the *discrete* relabeling group (48 signed axis permutations + gauge swap), with balance the hypothesis that earns it. **The gap:** the horizon chart change (a fold opening an orthogonal direction, [`Tunnelling.md`](Tunnelling.md) §2) is **not** one of those relabelings, and no theorem says it is. **`QLF_HorizonBasis.lean` now exists** (zero axioms): `HorizonRebasis` plus closure/fold/order preservation, with the finding that **order preservation is a theorem, not a fourth assumption** — reachability is list-prefix and `List.map` preserves prefixes, so causal succession survives a rebasing automatically. Per R6a the interface is trivially inhabited (identity), so the evidence is the non-identity instances and the proved order half. **And the obvious candidate for `ρ_H` is now measured and rejected:** taking [`Tunnelling.md`](Tunnelling.md) §2's spatial→gauge push literally, over all 5296 balanced histories of length ≤ 6 it preserves balance `5296/5296` but the fold only `3536/5296` — it satisfies `balance_iff` and **fails `fold_eq`**, smallest counterexample `^/v\ ↦ ^+v−` (`−I → +I`); the gauge-swap control preserves both `5296/5296`. The failure is structured: all 1760 changes are `±I` sign flips, 880 each way, `±iI` never appearing. Since `−I` is the half-spin signature, the mechanism changes **spin character**. **The statistic is multiplicity, not fraction** — exact `W_keep : W_flip` = `8:0`, `136:32`, `3392:1728`, `110248:79872`, so `R(L) = ∞, 17/4, 53/27, 13781/9984` (≈`4.25, 1.96, 1.38`), **rebasing the most-way channel at every depth enumerated** but falling toward `1`. Depths are *not* comparable to each other (rule 2: accessibility first, then multiplicity among what is accessible). **Open and sharp:** `R → 1` (neither dominates), `R → c > 1` (rebasing always preferred), or `R < 1` past some depth (the flipped sector wins and the nested claim fails there). Also reframed: `HorizonRebasis` is the crossing's **fold-preserving sector**, not the whole crossing — a channel decomposition, which is why a populated minority channel is not a refutation. *Correction:* earlier sampled estimates at `L=8,10,12` are **withdrawn** — exact `L=8` is `0.5799` kept, not the sampled `0.655`; the sampler was biased. **But "which one is it?" was the wrong question** — things happen every way, so the method asks which happens in the *most* ways (rules 1 and 3), and the aggregate was hiding the answer by averaging over lengths. Per length, exactly: `L=2` → **8/8 kept, zero flips — the push *is* a rebasing there**; `L=4` → `17/21`; `L=6` → `53/80`. The flip sector does not exist until length 4 and grows after. So the three readings are not alternatives but **one depth-dependent split**: a shallow crossing is a rebasing and the interior *is* the exterior in another basis; a deep crossing increasingly carries `±I` flips, where the nested claim fails as stated and a **spin-character** difference appears. Same capacity story as §4a.1. **Not claimed:** deeper sampling (`L=8,10,12`) suggests the fraction keeps falling (~`0.65/0.61/0.58`) but under a *different, non-uniform* measure — indicative only, and three exact points plus a tail is not an asymptotic law (R5). Open: where the split goes, and what "shallow" means physically | [`BLACK-HOLES.md`](BLACK-HOLES.md) §4a, [`lean/QLF_BasisIndependence.lean`](lean/QLF_BasisIndependence.lean) |
| **Interior persistence, and the Planck-crossing sealing test** | 🔴 **Open; the second is a live consistency test rather than a gap to fill.** *Persistence:* nothing shows a causally sealed interior supports a long causal chain rather than one closure — until it does, "child universe" names something not shown to have a history. *Sealing:* `sub_planck_compton_gt_schwarzschild` removes **sub-Planck** objects from scope (`μ² < 1/2`, Compton side, no Schwarzschild horizon), but the constructor's holes sit **at** the crossing `μ² = 1/2` where `r_s = λ_C`, which the theorem characterises without deciding. Whatever criterion eventually settles sealing must decide that row **without being tuned to it** — which is what makes it a test. Also open and *not* QLF-derived: horizon formation from capacity rather than imported classically, and the TOV limit (`2.2–2.3 M_☉` is measured input, as the `0.782 MeV` of [`Decay.md`](Decay.md) §2.4a is) | [`BLACK-HOLES.md`](BLACK-HOLES.md) §4a, [`Decay.md`](Decay.md) §2.4a, [`lean/QLF_QuantumBlackHole.lean`](lean/QLF_QuantumBlackHole.lean) |
| **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) |
| **Spin-statistics bridge** (#107) | 🔵 **Reading, not derivation** — spin-½ as pass-counted closure (one pass → `−I` residue, complementary second pass → `+I`) is anchored ([`Spin_QLF.md`](Spin_QLF.md) §9, reusing `rotation_360_eq_negI`/`rotation_720_eq_id`/`horizon_relative`); "360°/720°" is flagged as the post-geometry SU(2)/SO(3) rendering of the pass-count, **not** the pre-spatial primitive. The reused `pauli_exclusion` (`like_spin_excludes`) proves the commutator/self-exclusion form `[p,p]=0`, **not** the full spin-statistics theorem — the missing bridge from closure residue to antisymmetric exchange under particle swap stays a labelled reading (`spin_statistics_bridge_in_progress`) | [`lean/QLF_Spin.lean`](lean/QLF_Spin.lean), [`lean/QLF_HorizonClosure.lean`](lean/QLF_HorizonClosure.lean), [`Spin_QLF.md`](Spin_QLF.md) §9 |
| **The Mpemba effect (anomalous relaxation)** | 🟡 **Partly closed — instances proven, the ensemble effect not.** Relaxation to equilibrium *is* closure and its time *is* the maximum excursion (`closedAtHorizon_iff_maxExcursion_le`), making three things decidable. *No-go:* `relaxation_ge_distance` — if distance means the history's **imbalance**, relaxation is bounded *below* by it, so the effect is **impossible** for that measure and any claim must name another. *Enabler:* `equal_length_unequal_relaxation` — at one length and equal imbalance, relaxation differs by a factor of `n` (pair matching 1 pass, nested fold `n`), so no scalar determines it. *Translation:* `strong_mpemba` — the spectral `a_slow = 0` becomes sector emptiness `W_H(deep) = 0`, no eigenmodes. *Instances:* `mpemba_instance` / `mpemba_ordering` — for every `d>1`, `n>d`, two balanced preparations closing to the same equilibrium where `2n` twists close in **one** pass and `2d < 2n` need **`d`**; and uniform draws cross **13–17%** of the time at a 2× energy ratio ([`mpemba_census.py`](mpemba_census.py)). **Open:** the *ensemble* effect — median relaxation stays monotone in energy, so the crossing is a property of **individual preparations**, which is also the substrate's account of **why the effect is hard to duplicate**: an experiment fixing temperature while preparation varies averages over a census whose depths span an order of magnitude, so irreproducibility is the signature rather than the refutation; whether **energy** is an admissible distance is what thermomajorization asks of the ordinary effect; and no quantitative claim about **water** is made. *Would make it a result:* deriving the slow-mode amplitudes `a_n` from an actual census for a physically specified preparation (a laser-cooled ion ladder being the tractable candidate, not water) | [`lean/QLF_Mpemba.lean`](lean/QLF_Mpemba.lean), [`Mpemba.md`](Mpemba.md), [`mpemba_census.py`](mpemba_census.py) |
| **Line spectra as multiplicity spectra** | 🟡 **Partly closed — three of four claims.** *Proven:* a spectrum is a **finite line list** and it is **capacity**, not integrality, that makes it so (`lines_card_le` `≤ R²`, `lines_mono` — the list grows with capacity; over an unbounded census the differences `1/a − 1/b` accumulate arbitrarily finely, so discreteness is a capacity effect); and a level's statistical weight **is** a multiplicity — the *cardinality* of its orientation set (`orientations_card = 2ℓ+1`). *Theorem over a cited empirical law:* summed intensities from a common level stand in the ratio of those counts (`intensity_ratio_is_multiplicity_ratio`), over the **Burger–Dorgelo–Ornstein sum rules** (1924–25) carried as an `IntensityModel` **interface**, not an axiom. **Not proven, and withdrawn as originally stated:** that an *individual* line's strength is a way-count — oscillator strengths and dipole matrix elements are not derived, and the sum rules constrain only sums | [`lean/QLF_LineSpectra.lean`](lean/QLF_LineSpectra.lean), [`Law_Of_Exceptions.md`](Law_Of_Exceptions.md) §4c, [`Photon_Energy_Bits.md`](Photon_Energy_Bits.md) §7 |
| **Born-norm ↔ multiplicity bridge** | 🟡 **Open — sharply reduced.** *Closed:* the **exponent**. A realized event is a closed Hermitian pair, so its way-count is ket × bra — `pairCount_eq_leg_times_dagger` — which is exactly the `ℤ[i]` norm, so `bornProb` is the normalized pair count (`born_is_pair_count_ratio`); independently the modulus **cannot** be a count (irrational for `1+i`, `modulus_not_a_count`), so integrality alone forces the square. *Also closed:* **uniqueness of the form** given the pair structure — `unique_pair_form` (`a·ā` is the only form linear on the ket leg, conjugate-linear on the bra leg, normalized on the trivial closure); **not** Gleason, which assumes no form. *Checked and half-failing:* the census identification — [`born_generator_check.py`](born_generator_check.py) agrees **exactly** on the pair generator (`norm(1+i)=2` = the two ways a pair closes; `2ⁿ` for `n` pairs, `onePass_ways_iff`) but **fails** for arbitrary partitions, since a `ℤ[i]` norm is a sum of two squares (Fermat) while depth strata `38, 14, 70` and sign-splits `3, 35, 126` are not — and **no two Gaussian integers have norm ratio `3:1`** (`v₃` parity) though such Born weights are routine (Clebsch–Gordan `3/4 : 1/4`). *Forced repair:* a weight of `3` is **three degenerate unit-norm branches**, never one amplitude of norm `3` — weight is the **sum** of norms over degenerate components. *Residue now **answered** ([`QLF_Degeneracy`](lean/QLF_Degeneracy.lean)):* the decomposition is **not** free — every closed history folds to a Pauli scalar in `μ₄` (`QLF_Pauli`, reachable from count balance via `count_balanced_pauli_closed`), so a branch is **one unit-norm μ₄ component per way** and its amplitude is their **sum**; hence `weight_is_always_a_norm` and the obstruction dissolves, because **counts are not weights**. The gap between them is exactly **interference**: orthogonal phases give weight = count (`orthogonal_two_ways` — why the pair generator matched, its two ways being the orderings `+−`/`−+`), aligned give `n²` (`aligned_weight`; three ways weigh `9`, not the impossible `3`), opposed give `0`. *Phase assignment — now partly settled* ([`QLF_PhaseAssignment`](lean/QLF_PhaseAssignment.lean), [`QLF_BalancedPhaseReal`](lean/QLF_BalancedPhaseReal.lean)): the phase is the history's `pauli_fold`, proven for the pair sector (both orderings fold to `−I`, so those ways are **aligned**), and balance is proven to force a **real** phase (`μ₂`, never `±i`). The general two-factor rule `(−1)^{#neg}·sign(axis permutation)` is **verified not proven** (0 counterexamples over all 5,296 balanced histories ≤ 6). **Two corrections recorded there:** the census pair's ways are *not* orthogonal (so the earlier "pair-generator agreement" compares a count with a norm — a coincidence), and alignment is a **sector** property, not a census property (both phases occur; a census-spanning branch has the *signed* sum as amplitude). **Open:** the census↔amplitude identification itself — known **false** in the naive form, since counts are not weights. Untouched: Gleason-style uniqueness against all alternatives | [`lean/QLF_BornCounting.lean`](lean/QLF_BornCounting.lean), [`lean/QLF_Degeneracy.lean`](lean/QLF_Degeneracy.lean), [`born_generator_check.py`](born_generator_check.py), [`Born_Rule.md`](Born_Rule.md) §4/§8 |
| **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 |
| **Embedded-knot geometry** (the Kauffman lineage) | 🟣 **Enrichment direction** (reuse-only, no new axioms) — an embedded ZFA closure is a spatial knot/link, and its ZFA-conserved invariant is a *knot* invariant. **Proven footing:** `linkingNumber = baryonNumber`, orientation-odd with `mirror_reverses_linking` (the chiral Jones signature), and the **baryon is a Borromean/Brunnian 3-link** (`borromean_remove_one_unlinks`, `brunnian_needs_all_three`). **Reidemeister invariance Lean-anchored** — `signTriple` *is* the oriented Levi-Civita symbol, and full ambient R1/R2/R3 invariance is proven on Gauss-code diagrams (`linking_r1/r2/r3_invariant`; Hopf link `= 2`), with Reidemeister's 1927 theorem cited. **Kauffman-bracket bridge** — the bracket *as* a firebreak state-sum, proven to satisfy the defining relations (`bracket_skein`), so **the firebreak is the bracket**. **Open:** framing / writhe / chirality / knot-type. The continuum Chern–Simons TQFT leg is **already discharged** (Witten 1988 → Reshetikhin–Turaev, QLF's firmest bridge); QLF does not prove Witten's theorem | [`lean/QLF_KnotInvariant.lean`](lean/QLF_KnotInvariant.lean), [`lean/QLF_ReidemeisterLinking.lean`](lean/QLF_ReidemeisterLinking.lean), [`lean/QLF_LinkDiagram.lean`](lean/QLF_LinkDiagram.lean), [`lean/QLF_KauffmanBracket.lean`](lean/QLF_KauffmanBracket.lean), [`Knot_Theory_QLF.md`](Knot_Theory_QLF.md) §4–§5 |

---

## 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) |
| Molecular **shape** — the closure *count* a formula carries is derived (`b₁ = Σ(vᵢ−2)/2 + 1`, [`QLF_Unsaturation`](lean/QLF_Unsaturation.lean)), but **where** the closures sit is not: resonance, regiochemistry and bond placement stay open, and so do **bond angles** — the naive reading of the cubic lattice gives linear H₂O and square-planar CH₄, so VSEPR geometry needs a different attack, not more counting. **Stereochemistry is a proven no-go for counting alone**: a valence graph is mirror-symmetric, the same bijection argument that stops the fold census picking a handedness ([`Protein_Folding.md`](Protein_Folding.md) §7), so *cis*/*trans* and chirality need the substrate asymmetry ([`QLF_Handedness`](lean/QLF_Handedness.lean)). **Structure proven:** a ring and a double bond are one closure, *saturated* = zero closures, valence 2 is closure-neutral (hence chains) | [`Chemistry.md`](Chemistry.md) §10, [`lean/QLF_Unsaturation.lean`](lean/QLF_Unsaturation.lean), [`hydrocarbon_census.py`](hydrocarbon_census.py) |
| **Inertia, and the rotational sector (frame dragging)** — a *plan*, not a result ([`Inertia.md`](Inertia.md)). Hypothesis: a mass's **active frequency window** is isotropic at any constant velocity and asymmetric under acceleration, and the free-action cost of that asymmetry *is* inertia; frame dragging is the same shear sourced azimuthally by a rotating mass. **Already built, do not re-derive:** the equivalence principle structurally (one delay read as inertia and as curvature), the Unruh master relation, `holographic_entropy_eq`, and the Casimir finite-census result — **but `accelerated_boundary_is_unruh` is `rfl` and anchors nothing** (audited; §0a), so the dynamical-Casimir tie is asserted rather than established. **Route A is now run** ([`QLF_Inertia`](lean/QLF_Inertia.lean), no axioms): for a two-leg null circulation `netForce = −E·δ/L` (the circulation speed cancels), and the equivalence-principle shift `δ = aL/c²` gives `F = −(E/c²)a` with the size `L` cancelling too — and `force_scales_with_shift` makes the shift law **forced, not fitted**. **Still open:** the *counting* version of the imbalance (rule 4 asked for a signed integer; this is continuum algebra), the identification of the circulation with the gauge-fold depth (KC3), and the rotational sector. Two hard gates stated before any derivation: the **Hughes–Drever** inertial-mass-anisotropy bound (better than 1 part in 10²⁰), and an **R6a check** on the entropic route, since `F = ma` from a definitional entropy gradient would restate its own premise (the `yang_mills_gap` failure mode). **Named prior attempt:** Haisch–Rueda–Puthoff (1994) is this hypothesis in continuum language and did not converge — QLF owes a statement of how it differs, or inherits it | [`Inertia.md`](Inertia.md), [`Cross_Frequency_Lorentz.md`](Cross_Frequency_Lorentz.md) §7, [`VacuumEnergy.md`](VacuumEnergy.md) |
| Protein folding — the **contact-order regression is settled, and the prediction FAILED** (`Protein_Folding.md` §5e): on the 26 two-state proteins of Weikl 2006 the derived quantity `Σ log ℓ` correlates with `log k_f` at **0.21** against **0.91** for plain relative contact order, so the **multiplicity-factorization bridge is withdrawn** — `closedLoop_append` is true, but a fold's multiplicities do not factorize over its contacts, because prior contacts short-circuit the chain (effective contact order is the repair direction, un-derived). The pipeline validates by reproducing all four of Weikl's published correlation coefficients. Still open: **cooperative folding at realistic `N`** (exhaustive enumeration ends near `N ≈ 16`; the route is composing catalogued motifs as weighted classes rather than re-enumerating — *ways as a coefficient*). **Structure proven:** conformation = twist history, contact = ZFA closure, the odd-separation parity rule, closure composability, the `log 2` contact quantum, and the **mirror no-go** (counting cannot select a handedness — homochirality is upstream, in [`QLF_Handedness`](lean/QLF_Handedness.lean)). Also open: the peptide bond and the 20 residues as explicit closures — §6 is a one-bit valence rule (17/20 vs Kyte–Doolittle), not a derivation | [`Protein_Folding.md`](Protein_Folding.md), [`lean/QLF_Folding.lean`](lean/QLF_Folding.lean), [`protein_census.py`](protein_census.py) |
| 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. **The α connection is a machine-checked cross-sector overdetermination joint** (`QLF_AlphaRigidity`, `Alpha.md` §6a): `α⁻¹ = 137` is where the *dimension* sector (`d = 3`), the *bare-coupling* sector (`128 = 2⁷`), and *elementarity* (`137` prime) meet with **zero slack** (`alpha_unique`/`rival_excluded`; `d` substrate-derived, not a fit) — overdetermination, not free-parameter rigidity. **#116 closed:** the free-grammar census `N(d)` is computed (`alpha_rigidity_census.py`, `Alpha.md` §6a) — the look-elsewhere over the free grammar is *large* (137 reachable at depth 2, the `[128,146]` band saturated by depth 3), so grammar sparsity is non-load-bearing and the rigidity rests entirely on the proven template lock; a Lean `reachable_finite` would be true but non-load-bearing. Remaining thread: the counting→mechanism check (the #62 swap-graph, tracked in `Pointer_Swap_Fuzz.md`). | [`lean/QLF_AlphaRigidity.lean`](lean/QLF_AlphaRigidity.lean), [`alpha_rigidity_census.py`](alpha_rigidity_census.py), [`lean/QLF_FineStructureSubstrate.lean`](lean/QLF_FineStructureSubstrate.lean), [`Alpha.md`](Alpha.md) §6a, [`Magic_numbers.md`](Magic_numbers.md) |
| **Pointer-swap-fuzz mechanism behind operational 3D** (#62) | 🔵 **Specified + made falsifiable.** The mechanism layer below #42's count: how `n`-dimensional pointer-swap fuzz renders as sparse operational 3-D for embedded observers. **The decisive correction (#112/#114):** raw pointer fuzz has *no geometry to measure* — operational geometry appears only once matter integrates recurring coincidences into stable **receipts**, whose swap-invariant content is the per-axis signed count `axisWindingVector ∈ ℤ³`, a *count* and hence genuinely permutation-invariant (**not** `baryonNumber`, which is sequence-dependent). The receipt quotient is `ℤ^d` with growth dimension **exactly `d`, stably**; for the 8-twist alphabet `d = 3` ⟹ renders **3-D**, and the `d = 1,2,4` rows show the exponent tracks the axis count rather than a chosen 3. The raw permutohedron by contrast **does not converge** — it climbs past 3 at ≈`0.27`/k (`D ~ k·log2/log k → ∞`), a *crossing, not a limit* — and the excess is not waste, reading as the internal gauge/colour dimensions. Back-stops the α cross-sector theorem (`QLF_AlphaRigidity`). **Open (`pointer_swap_fuzz_in_progress`):** the modelling map (atomic integration = `axisWindingVector` accumulation is posited, not derived); the `ℤ³`→continuum step; the swap-group→su(3) homomorphism (gluon connection vs numerology); Lean formalization of the swap action | [`Pointer_Swap_Fuzz.md`](Pointer_Swap_Fuzz.md), [`pointer_swap_fuzz.py`](pointer_swap_fuzz.py), [`Genesis.md`](Genesis.md) §4b (`genesis.py` full run), [`lean/QLF_CausalDimension.lean`](lean/QLF_CausalDimension.lean), [`SpaceTime.md`](SpaceTime.md) §3a |
| **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.