dm³ 102 · Week 05 · Constant: η (n=3)

η — The Tribonacci Constant

η ≈ 1.839, the dominant root at rank n=3, and what “critical” does and doesn’t mean here
dm³ 102 · Week 05 · Constant: η (n=3)
η — The Tribonacci Constant
Course: dm³ 102  ·  Constant: η (n=3)  ·  Source: Book 3, Chapter η + 3 Lean files

The Tribonacci sequence \(T(n)=T(n-1)+T(n-2)+T(n-3)\) has characteristic polynomial \(x^3-x^2-x-1=0\), dominant root \(\eta \approx 1.839286755214161\). Theorem η.1 (proved). \(\eta\) is the unique real root of that cubic, and in the dm³ framework it’s the constant tied to the 12-phase Collatz orbit’s amplitude envelope \(w(k) = \eta^{{-k}}\), machine-verified in three separate Lean files: TribonacciMeasure.lean (strict antitonicity of the weighted sequence), TribonacciRatioConvergence.lean (the ratio \(T(n{{+}}1)/T(n) \to \eta\)), and TribonacciDNLS.lean (a discrete nonlinear Schrödinger realisation on a Tribonacci substitution chain, amplitude decay \(A_k \sim \eta^{{-k}}\)). All three: sorry_count: 0.

Deriving η exactly, not just citing it
Substitute \(x = t + 1/3\) to remove the quadratic term: \(x^3-x^2-x-1=0\) becomes the depressed cubic \(t^3 - \tfrac{{4}}{{3}}t - \tfrac{{38}}{{27}} = 0\), so \(p=-4/3\), \(q=-38/27\) in Cardano’s form \(t^3+pt+q=0\). The discriminant \((q/2)^2+(p/3)^3 = 11/27 > 0\), which is exactly the condition for one real root and a complex conjugate pair — matching the three roots of a genuine n-bonacci polynomial. Cardano’s formula then gives \(t = \sqrt[3]{{19/27+\sqrt{{11/27}}}} + \sqrt[3]{{19/27-\sqrt{{11/27}}}} \approx 1.505953422\), and \(\eta = t + 1/3 \approx 1.839286755214161\) — verified symbolically (SymPy) to 20 decimal places against the same value cited throughout this course. η is not an assumed or curve-fit number; it is this cubic’s actual algebraic root in closed radical form.
A distinction the source material blurs — worth getting exactly right
Book 3’s own chapter says \(\eta\) “sits exactly at \(c^*=3\) on the criticality ladder.” Read literally that’s wrong: \(\eta \approx 1.839\), not \(3\); plugging \(c=\eta\) into \(V(q)=q^3-cq\) does not produce the exact double-root fold at \(q=1\) (only \(c=3\) exactly does that — Theorem C.1 from 101). What’s actually meant, and stated precisely elsewhere in the same corpus (dm3CriticalityPrinciple_extended.lean, Week 7): \(\eta\) is the rank-3 (\(n=3\)) n-bonacci constant, and rank \(n=3\) is separately argued to be the critical recurrence depth — a discrete-index notion of criticality, not the same object as the continuous curvature coefficient \(c=3\). The two criticality claims (continuous \(c^*=3\) in the fold potential; discrete rank \(n^*=3\) in the recurrence-depth ladder) are related by the framework’s overall design, but they are not numerically the same statement, and treating “\(\eta\) sits at \(c^*=3\)” as literal is a category error worth not repeating.

Keep both facts distinct going forward: \(\eta \approx 1.839\) is a real, proved, well-formalized number governing amplitude decay; “rank 3 is critical” is a separate, partly-axiomatic claim covered in full in Weeks 7–8.

This week’s content is grounded in the AXLE Lean sources and Book 3 chapters cited above — where a claim rests on an axiom, that is stated explicitly rather than presented as independently verified.
-- dm³ 102 · Week 05 · η, derived (Cardano), not just cited

-- x³ - x² - x - 1 = 0.  Substitute x = t + 1/3:
--   t³ - (4/3)t - 38/27 = 0     (depressed cubic, p=-4/3, q=-38/27)
--   discriminant (q/2)²+(p/3)³ = 11/27 > 0  ⟹  1 real + 2 complex roots
--   t = ∛(19/27+√(11/27)) + ∛(19/27-√(11/27)) ≈ 1.505953422
--   η = t + 1/3 ≈ 1.839286755214161   (SymPy-verified, 20dp)

-- Proved, 0 sorry each:
--   TribonacciMeasure.lean          -- strict antitonicity
--   TribonacciRatioConvergence.lean -- T(n+1)/T(n) → η
--   TribonacciDNLS.lean             -- DNLS amplitude decay A_k ~ η^{-k}

-- NOTE: η ≈ 1.839 ≠ c* = 3. "η sits at criticality" refers to RANK
-- n=3 in the discrete n-bonacci ladder (Week 7-8), not the numeric
-- value of the curvature coefficient c in V(q)=q³-cq.
example : (1.839:ℝ) ≠ 3 := by norm_num
← Week 4 ↑ dm³ 102 Course Week 6 →