| Claim | Paper | Lean | Chapter |
|---|---|---|---|
| η exists as IVT root of x³−x²−x−1; η>1; weight sequence w_k=η⁻ᵏ strictly antitone, →0
The amplitude-envelope foundation, §3.2 |
nbonacci_dnls_paper / paper_v4.tex 10.5281/zenodo.20075822 |
sorry-free TribonacciDNLS.lean — η_gt_one, η_pos, η_characteristic, w_pos, w_strictAnti, w_tendsto_zero |
chEta-tribonacci.html, ch-eta-dnls.html |
| IPR functional: scale-invariant, bounded in [1/N,1]; PoreSpace compact/finite-measure; tridiagonal Hamiltonian symmetric
Functional-analytic scaffolding, not the paper's headline result |
— (infrastructure, not a paper claim itself) | 1 disclosed sorry DNLSFoundations.lean — ipr_scale_invariant, hamMatrix_isSymm, poreSpace_isCompact proved; ipr_le_one depends on sum_sq_le_sq_sum_of_nonneg (sorry) |
ch-eta-dnls.html (implicit — the live IPR demo) |
| Differential nonlinear robustness: Fibonacci IPR drops ~57%, Tribonacci <5% at λ=1.5, T=50; long-time saturation ratio 1.04±0.04 at T~3×10⁵
This is the paper's actual headline claim |
paper_v4.tex §4 | not formalized DNLS_MeasureTheory_Roadmap.lean Tiers 2/4/5/8 sketch what a proof would need (discrete Harnack via ellipticity ratio 2 vs 4); Tiers 8.2/8.3/8.5 explicitly marked "STILL OPEN" / "remains numerical" in the roadmap's own text — honest, not silently claimed |
ch-eta-dnls.html |
| Fold-event lock-in: G⁶(hex)=33, saturating counter model | NPB §4 (lock-in prediction) | sorry-free FoldEvents.lean — stability_at_threshold, g6_hex_lockin, g6_hex_lockin_in_orbit |
none No chapter narrates this result yet |
| Claim | Paper | Lean | Chapter |
|---|---|---|---|
| Theorem 5.3 — the operators C,K,F,U do not commute; order-dependent
The abstract root all D2/D3/D4 domain claims specialize |
vol1-mathematics.html §5 | 1 disclosed sorry CatGT_PROOFS_COMPLETE.lean — NonCommutativity, boundary-discontinuity step left open |
vol1-mathematics.html §5 |
| ZSM-5 (C→K→F→U) suppresses aromatics — Selectivity = 0 | ALGEBRAIC_PROOFS_ALL_7_THEOREMS.md | sorry-free CatGT_PROOFS_COMPLETE.lean — ZSM5_SupportsAromatics |
ch-catgt-zeolite.html, ch18 |
| MCM-22 (C→F→K→U) permits aromatics, Selectivity > 0.2 (~0.35 simulated) | ALGEBRAIC_PROOFS_ALL_7_THEOREMS.md | 2 disclosed sorries CatGT_PROOFS_COMPLETE.lean — MCM22_PermitsAromatics, both numerical-integral gaps; roadmap Tiers 6-7 sketch a from-first-principles close (not yet mechanized) |
ch18 |
| Operator order determines selectivity [MAIN theorem, combines the two above] | ALGEBRAIC_PROOFS_ALL_7_THEOREMS.md §4.4 | genuine gap, not just sorry CatGT_PROOFS_COMPLETE.lean — shares one K between two branches needing K = two different concrete operators at once; flagged in the file's own header, not silently patched |
ch18 |
| D3 — enzyme biocatalysis extends Thm 5.3 to a third domain (branch multiplicity, concentration-tilted selection) | — (chapter-original derivation from Vol I Assumptions 2.2/2.5/2.6, not yet a standalone paper) | not formalized | ch19-enzyme-noncommutativity.html |
| D4 — SAF/biomass bridge domain (D2 zeolite + D3 enzyme in series) | — (chapter-original) | not formalized | ch20-saf-noncommutativity.html |
| Autophagy: mTOR as fold operator F, C→K→F→U in molecular biology | criticality_paper/ (dnls repo) | "0 sorry" per living-book.html's own card AutophagyDm3.lean (dnls/criticality_paper/) — not re-read this session; status taken from the chapter card's own claim, flagging for a real re-check rather than silently trusting it |
chA-autophagy.html |
| A 0/1 aperture gate commutes exactly with a pointwise fold, for every state — there is no boundary term
Refutation. This is the false commutator lemma, previously asserted across the series as [K,F] ≠ 0 with a commutator ∝ δ(η−η*). Machine-checked to be false. |
— (defect ledger, opened 2026-07-18) | kernel-audited ZeoliteCommutation.lean (TOTOGT/io, Lean v4.33.0-rc1) — gate_commutes. 0 admits, 0 sorries; #print axioms → [propext, Classical.choice, Quot.sound] |
ch18, wp66 §2 |
| Non-commutation appears exactly when the fold carries the coupling (transport) term: inter-site coupling does not commute with the on-site fold, and the gate does not commute with F = coupling ∘ onsite
The dichotomy the zeolite argument actually rests on. Commutation proved universally; each non-commutation established by a single witness — the correct logical shape in each direction. |
— (formalised directly) | kernel-audited ZeoliteCommutation.lean — coupling_not_commute (commutator −6 on a test state), gate_fold_not_commute |
wp66 §2, wp67 §5 |
| Theorem 18.1 survives the refutation — its gate is state-dependent, K = θ(η*−d(ψ)) with F changing d(ψ)
Scope limit stated in the source: the model is a three-site DNLS lattice with gate [v₀,0,v₂]. What is formalised is the algebra — a 0/1 aperture against pointwise versus transport-carrying operations — not the atmospheric box model or any meteorology. |
ch18 §Theorem 18.1 | not formalized the state-dependent-gate mechanism is not itself mechanized; only the fixed-gate algebra above is |
ch18 |
| Claim | Paper | Lean | Chapter |
|---|---|---|---|
| β ∈ Bₙ, the braid accumulated by a chain of non-abelian anyons under the coherence rule, corresponds to G = U∘F∘K∘C
Withdrawn as an identity. Vol I §3 fixes C : X→X_C, K : X_C→X_C, F : X_C→X_F, U : X_F→X, so G : X→X is a self-map of a Riemannian manifold; Bₙ is a discrete group with no metric, no normal field, no Morse Φ. Now stated as a stage-correspondence with the debt written out: exhibit X, X_C, X_F, n(s), κ* and Φ for a configuration space of n anyons. |
— (chapter-original) | open — not a theorem nothing formalized; clause (3) marked [OPEN] on the page, and the □ removed from the proof sketch per rule 3 |
ch7-topological-orthogenesis.html |
| Braiding is universal for topological quantum computation
Model-dependent, and not a property of Bₙ. Fibonacci braiding is universal (Freedman–Larsen–Wang); Ising braiding is not — Clifford only, needing a supplementary non-topological gate. Google's 2023 superconducting realisation used projective Ising anyons, i.e. the case the clause does not cover. |
— (literature) | not formalized | ch7 §Theorem 7.1 |
| Order-dependence in an anyon chain is physical content rather than imposed structure
Testable only against emergent topological order. Every non-abelian anyon experiment to date builds the braid from a gate list the experimenter chose, so order-dependence there holds by construction. FQHE is the control case: abelian braiding observed directly at ν = 1/3 in 2020; non-abelian at ν = 5/2 still open, with hedged time-domain-braiding evidence as of 2026-08-13 (arXiv:2608.12897). |
— (experimental literature) | not formalized | ch7 §Limits of this reading |