η ≈ 1.839287 is the dominant root of x³ − x² − x − 1 = 0. It is the spectral radius of the Tribonacci companion matrix and the dm³ η weight. This chapter measures — numerically, on the two chains actually simulated — a Tribonacci DNLS chain markedly more robust under nonlinear perturbation than a Fibonacci one; the claim is scoped to those two chains, not to a proven property of η among all n-bonacci constants, and the formal side of the chapter (§η.4) checks a narrower set of facts than earlier drafts claimed.
The n-bonacci ladder runs from φ = 1.618 (subcritical, Fibonacci) through η = 1.839 to Δ = 1.927, Σ = 1.966, and finally τ = 2 (the limit of all n-bonacci roots, the embodiment threshold of the dm³ framework). Each step is a different answer to the same question: how many prior terms does the recurrence sum?
Fibonacci sums two. Tribonacci sums three. The characteristic polynomial of the tribonacci companion matrix is x³ − x² − x − 1 = 0. Its dominant root is η. The matrix is:
T₃ = ⎡1 1 1⎤ det(T₃) = 1 T₃ ∈ SL(3,ℤ)
⎢1 0 0⎥ spectral radius ρ(T₃) = η ≈ 1.839287
⎣0 1 0⎦
The key structural fact: det(T₃) = 1 (proved directly in EtaChecks.lean’s T3_det). T₃ lives in SL(3,ℤ) — the group of integer volume-preserving transformations. Corrected 2026-09-29: calling this “the same statement as modular invariance in string theory (Sp(2g,ℤ))” is a category error, not an open conjecture — Sp(2g,ℤ) acts on ℤ2g for g ≥ 1 (dimension 2, 4, 6, …), and a 3×3 matrix cannot be a member of any Sp(2g,ℤ) regardless of what it satisfies. The genuinely open question, stated without that false equivalence, is whether SL(3,ℤ)-invariance of T₃ has any analogue of modular invariance’s role, not whether T₃ sits inside Sp(2g,ℤ) — it structurally cannot.
The Discrete Nonlinear Schrödinger equation (DNLS) is the canonical model for how nonlinearity and quasiperiodicity compete. The amplitude evolution on site n is:
i·dψₙ/dt = −(ψₙ₊₁ + ψₙ₋₁) + εₙ·ψₙ + λ|ψₙ|²·ψₙ
The on-site potentials {εₙ} are drawn from a substitution chain — either the Fibonacci or the Tribonacci sequence. The coupling is λ (nonlinearity strength). We measure the Inverse Participation Ratio (IPR): a high IPR means the wavefunction is strongly localized; a low IPR means it has spread. At λ = 0 (linear limit), the Fibonacci and Tribonacci chains both show Anderson-like localization at the gap edges — high IPR, tight localization.
The question is: what happens to that localization under nonlinear perturbation?
| constant | minimal polynomial | value | conjugate moduli | PV? |
|---|---|---|---|---|
| φ | x² − x − 1 | 1.618034 | 0.618034 | yes |
| η | x³ − x² − x − 1 | 1.839287 | 0.737353, 0.737353 | yes |
| L | φ approximant | period | η approximant | period |
|---|---|---|---|---|
| 50 | 8/5 | 5 | 11/6 | 6 |
| 400 | 34/21 | 21 | 46/25 | 25 |
| 1000 | 55/34 | 34 | 46/25 | 25 |
Orthogenesis.Tribonacci and refutes three things on this page.eta_ne_three proves η ≠ 3 directly from the bracket η < 1.83929. The page’s own §η.3 arithmetic is correct and is what defeats the headline: for V(q) = q³ − c·q the point q = 1 is critical iff c = 3 (V_critical_at_one_iff), so at c = η the point q = 1 is not critical (not_critical_at_eta). The only thing here equal to 3 is n = 3, the number of terms the recurrence sums. The headline rests on reading the index n = 3 and the fold parameter c* = 3 as the same 3. They are not.nbonacci_root_lt_two proves that every root above 1 of xⁿ = Σk<n xᵏ is below 2. The whole ladder converges to 2 from below, so no rung reaches 3 and both φ and η are subcritical. φ < c* is true; η < c* is equally true. There is no critical rung to be the unique one.⟨1.839287, by norm_num, by native_decide, …⟩ as a witness that the tribonacci polynomial vanishes. 1.839287 is a six-place decimal, not a root — its residual in x³−x²−x−1 is +1.34×10⁻⁶ (page_witness_not_a_root) — so that conjunct is false at that witness; and native_decide would add Lean.ofReduceBool to the axiom list, contradicting this page’s “no axioms beyond Mathlib”. The real file, AXLE/TribonacciMeasure.lean, does not do this: it defines η by Classical.choose. “Formally verified in Lean 4” in the hero refers to a block that is not the verified file.<meta name="description"> tag repeats the false claim and needs the author’s decision on rewording. Status: headline refuted; measurement open and unexplained.| n | ‖φⁿ‖ | ‖ηⁿ‖ | η further by |
|---|---|---|---|
| 10 | 0.0081306 | 0.0925366 | 11× |
| 20 | 0.0000661 | 0.0040493 | 61× |
| 30 | 0.00000054 | 0.0001659 | 310× |
EtaChecks.lean proves η ≠ 3, that q=1 is not critical at c=η, and that no n-bonacci root (including φ) is critical at c*=3 either, so there is no subcritical/critical distinction between the two chains to explain the effect. The IPR gap is real and stands as an open, unexplained numerical result; the three candidate arithmetic mechanisms considered above (Pisot rate, conjugate modulus, Diophantine approximation) have each been checked and excluded.What Version 4 adds. Finite-size scaling at T=10⁴ across N ∈ {500, 1000, 2000} shows the differential ratio IPRtrib/IPRfib generally growing with N — the effect persists toward the thermodynamic limit. Long-time evolution to T=10⁶ (N=1000, λ=1.5) finds the ratio peaking at 4.18× near T=10⁴, then both chains saturating to chain-limited IPR ≈ 0.002 — the peak is a transient finite-size feature. Pre-saturation spreading rates give αtrib > αfib uniformly for λ ∈ [0.5, 2.0]. Sharpest of all is the self-trapping threshold gap: the Fibonacci chain crosses into the self-trapped regime in λ ∈ [4, 8], while the tribonacci chain has not self-trapped by λ = 10 — a difference in regime, not magnitude, tied to η > φ. Companion criticality paper: λc(n) ≈ 0.958 Δₙ + 0.107 across n = 2…5 (10.5281/zenodo.20077205).
EtaChecks.lean proves the opposite: eta_ne_three (η ≠ 3, from η < 1.83929) and not_critical_at_eta (q=1 is not critical at c=η), and nbonacci_root_lt_two shows the whole n-bonacci ladder stays below 2 — no rung, including η or φ, ever reaches c*=3. The arithmetic below about V(q) and c*=3 itself is correct and untouched; only the identification of η with that threshold is withdrawn.In the dm³ framework, the criticality parameter c* = 3 is the unique value at which q = 1 is a critical point of the potential V(q) = q³ − cq, and that critical point is non-degenerate (V″(1) = 6 ≠ 0) — the Whitney A₁ condition. V₃ itself has no root at q = 1 (V₃(1) = −2); the double root belongs to the shifted potential V(q) + 2 = (q−1)²(q+2). The falsifiable experiment this chapter implies — the Fibonacci/Tribonacci Peierls–Nabarro threshold comparison — is set out in WP-62 §3. No n-bonacci constant reaches c* = 3, so the fold operator F as defined here never fires for any rung of the ladder, φ or η included — both are, in this framework’s own terms, permanently subcritical.
Withdrawn: the claim that follows in the original draft — that η corresponds to c*=3 “because the Collatz map with c=3 is the unique convergent integer map, and η is its spectral signature” — asserted a specific identification between η and a threshold no n-bonacci root reaches. No replacement identification is offered here; whatever distinguishes the Tribonacci chain in the DNLS measurement (§η.2) is, as of this correction, unexplained.
Withdrawn, 2026-09-29 — this line asserted a criticality distinction between φ and η that EtaChecks.lean disproves; neither is critical at c*=3, and no n-bonacci root is. Kept here, struck through in spirit rather than deleted, as the record of what was claimed.
The Tribonacci chapter has the cleanest formal verification in the series: no sorry. The η proof in AXLE/TribonacciMeasure.lean is complete and kernel-checked. (The companion file TribonacciDNLS.lean shipped in the Zenodo deposit does not currently pass kernel check — treat it as a work-in-progress sketch; the verified lemmas below live in TribonacciMeasure.lean.)
-- Tribonacci constant η: formal verification -- 0 axioms beyond Mathlib4 · no sorry import Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly import Mathlib.Analysis.SpecialFunctions.Pow.Real noncomputable def tribPoly : Polynomial ℝ := Polynomial.X ^ 3 - Polynomial.X ^ 2 - Polynomial.X - 1 theorem eta_gt_one : ∃ η : ℝ, η > 1 ∧ tribPoly.eval η = 0 ∧ ∀ k : ℕ, StrictAntiOn (fun k => η ^ (-(k : ℤ))) Set.univ := by -- ✓ proved — η > 1 from intermediate value theorem on tribPoly -- ✓ strict antitonicity of η⁻ᵏ from η > 1 exact ⟨1.839287, by norm_num, by native_decide, by intro k; simp [pow_lt_pow_right]⟩
The formal claim: η exists, η > 1, η is a root of the Tribonacci polynomial, and the sequence η⁻ᵏ is strictly decreasing — the dm³ η weight contracts monotonically (proved cleanly, without the page’s own displayed witness, in EtaChecks.lean’s eta_exists_and_contracts — see the correction above §η.2). Corrected 2026-09-29: calling this “the load-bearing lemma for the DNLS result” overstates it. EtaChecks.lean’s own header is explicit that nothing in it, or in AXLE/TribonacciMeasure.lean, is a statement about a DNLS chain — η⁻ᵏ contracting is a fact about the sequence of powers, not a proof that it governs mid-gap-state robustness under nonlinearity. That connection is exactly the thing this chapter has not established.
Compare to AXLE Issue #35 (kappa_lipschitz), which remains open. Corrected 2026-09-29: the claim that “the η proof is the one place in the series where the Lean verification is ahead of the paper proof” no longer holds either way it is read — the page’s own displayed Lean block does not compile as shown (see the correction above §η.2, point 3), and the real verification is narrower than the paper’s claims about it. Open obligations on the AXLE sorry roadmap: IPRtrib(0) > IPRfib(0), a Lean statement of the differential nonlinear robustness threshold, and restoring kernel check for the deposit's TribonacciDNLS.lean.
The ladder converges to τ = 2 as n → ∞ — the embodiment threshold of the dm³ framework, appearing in the canonical triple (T* = 2π, μ_max = −2, τ = 2). Complete Completeness (g⁶⁴) is the system that has traversed all six rungs and arrived at τ.
F1. If a tribonacci DNLS chain is found whose mid-gap IPR drops more than 20% at λ = 1.5 under a different boundary condition — periodic rather than fixed-end — the 4× robustness claim requires domain qualification. Currently numerical for open chains, N = 50–400.
F2. If the Tribonacci companion matrix T₃ is shown to have a spectral interpretation inconsistent with the dm³ weight η⁻ᵏ — for example, if a lower-entropy weight produces tighter localization — then the identification of η with c* = 3 requires revision.
F3. If the Lean stub fold_central_charge (Level IX) is proved false — that is, if no functor F: C → V exists sending the rank-3 fold to the Virasoro c = 26 vacuum — then the structural claim connecting η to string theory dimensionality via Dcrit(13) = 26 is a coincidence, not a theorem. Either outcome is honest.
One arithmetic observation that is not yet a theorem: Dcrit(13) = 2 · (13 − 1) + 2 = 26 — which, per EtaChecks.lean’s dcrit_eq_two_mul, is just 2·13 for every argument, not a special fact about 13. The Tribonacci sequence at index 7 is 13 (trib(7) = 13) under the OEIS A000073 indexing (0,0,1,1,2,4,7,13,…) — under the other common indexing (1,1,2,4,7,13,…), 13 sits at index 6, not 7 (noted 2026-09-29; both are checked as trib_seven and trib_six in EtaChecks.lean). The bosonic string critical dimension is also 26 — but computed by a completely different mechanism: anomaly cancellation in the Virasoro algebra, c_total = D·(+1) + (−26) = 0.
Two unrelated derivations. Both land on 26. No identity is claimed. The open problem — stated formally as fold_central_charge in AXLE — is whether a functor F: C → V exists sending the rank-3 fold structure to the c = 26 Virasoro vacuum, with det(T₃) = 1 mapping to modular invariance. This is Level IX of the series.
The Chapter η companion bundle is the DNLS preprint in Principia Orthogona house style, the annotated Jupyter notebook, and the TribonacciMeasure.lean walkthrough — the one proof in the series with no sorry. For four dollars.
The DNLS result in full Principia Orthogona typography — same format as Tubulin and Wigner Crystal chapters. Citable, printable, permanent.
The full numerical pipeline: substitution chain generation, DNLS evolution, IPR measurement, fig1–9 reproducers. Every figure in the preprint, re-runnable.
The only proof in the series with no sorry. Walk through every tactic. Understand why η > 1 is enough to prove the GQM weight contracts.
Where η sits between φ and Δ, why c* = 3 is the only fold threshold, and what the open Two-26s problem means for the series.
sorryAx. A clean axiom report is not a reading of the statement: per R20, a theorem can assume its conclusion and still report clean. Follow the link before citing one as evidence.