doubling_cascade_positive
plain-language theorem explainer
The theorem establishes that the J-cost on the phi-ladder at rung 2n is strictly positive for every nonzero integer n. Researchers tracing the generative instability of the ground state x=1 would cite it when confirming that doubling maps positive-cost rungs to positive-cost rungs. The proof is a one-line rewrite via the doubling identity followed by nlinarith on the resulting expression using base positivity and square nonnegativity.
Claim. For every nonzero integer $n$, the J-cost of the phi-ladder value at level $2n$ satisfies $0 < Jcost(phi_ladder(2n))$, where $Jcost(x) = (x + x^{-1})/2 - 1$ and $phi_ladder(k) = phi^k$ for the golden ratio $phi$.
background
The StillnessGenerative module derives from T0-T8 that the unique zero-defect state x=1 is unstable and must generate nontrivial content. The phi-ladder is the sequence of states phi^k for integer k, with phi forced as the self-similar fixed point by T6. J-cost is the recognition cost function J(x) = (x + x^{-1})/2 - 1, which vanishes only at x=1 and obeys the recognition composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). Upstream phi_ladder_positive_cost supplies the base fact that Jcost(phi_ladder(n)) > 0 whenever n ≠ 0, while doubling_cascade supplies the algebraic relation that expresses the cost at 2n in terms of the cost at n plus nonnegative quadratic terms.
proof idea
The term proof first rewrites the goal by applying the doubling_cascade lemma to n and the hypothesis n ≠ 0. This substitutes an identity that rewrites Jcost(phi_ladder(2n)) as a quadratic form in Jcost(phi_ladder(n)) whose coefficients are nonnegative. The script then closes immediately with nlinarith, citing phi_ladder_positive_cost hn together with the nonnegativity of squares.
why it matters
The result sits inside the module's Part IX argument that the Fibonacci recurrence phi^n + phi^{n+1} = phi^{n+2} populates the entire ladder with positive-cost states. It supplies the positivity step needed to guarantee that doubling never collapses back to the zero-defect ground state, thereby supporting the T7 eight-tick requirement and the claim that ledger symmetry reflects positive rungs to negative rungs. The declaration closes one link in the chain from T5 uniqueness through T6 phi-forcing to a fully populated nontrivial ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.