doubling_cascade
plain-language theorem explainer
The doubling relation equates the recognition cost at rung 2n on the phi-ladder to twice the squared cost at rung n plus four times that cost. Researchers tracing the generative instability of the ground state cite it when showing how the ladder acquires positive costs from the initial condition at unity. The proof substitutes the exponential definition into the d'Alembert identity applied to equal arguments, reduces the quotient to one via the unit-cost lemma, and concludes by linear arithmetic.
Claim. For every nonzero integer $n$, $J(φ^{2n}) = 2[J(φ^n)]^2 + 4 J(φ^n)$, where $J$ is the recognition cost $J(x) = (x-1)^2/(2x)$ and $φ$ is the golden-ratio fixed point.
background
The phi-ladder is the map $n ↦ φ^n$ for $n ∈ ℤ$, with $φ$ the self-similar fixed point forced by T6. The J-cost satisfies the d'Alembert identity $J(xy) + J(x/y) = 2J(x) + 2J(y) + 2J(x)J(y)$ for positive arguments and the unit lemma $J(1) = 0$. This module derives from T0–T8 that the unique zero-defect state $x=1$ is not passive equilibrium but the source of all structure: recognition forcing (T4) and the eight-tick requirement (T7) compel departure from uniformity, while closure (T6) forces every nontrivial entry onto the phi-ladder.
proof idea
The tactic proof unfolds the ladder definition, obtains positivity of $φ$, applies the d'Alembert identity to the pair $(φ^n, φ^n)$, rewrites the product as $φ^{2n}$ and the quotient as 1, substitutes the unit-cost lemma, and finishes by linear arithmetic on the resulting quadratic.
why it matters
It supplies the doubling step in the Fibonacci cascade that populates the full ladder from the initial condition at $x=1$. The result is invoked directly by the positivity theorem doubling_cascade_positive to confirm every rung carries positive cost. The step supports the module claim that the ground state is the maximally creative source via the recognition composition law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.