every_rung_from_fibonacci
plain-language theorem explainer
Every integer rung k at least 2 equals the ledger composition of the two prior rungs on the phi ladder. Modelers of structure emergence from the zero-defect ground state in Recognition Science cite this identity to generate the full sequence without external assumptions. The proof proceeds by unfolding the ledger composition and reducing the resulting expression to the fibonacci cascade identity via ring normalization.
Claim. For every integer $k$ with $k$ at least 2, the ledger composition of the phi-power at exponent $k-2$ and the phi-power at exponent $k-1$ equals the phi-power at exponent $k$, where phi is the golden ratio fixed point and ledger composition realizes the Fibonacci recurrence on the ladder.
background
The module derives from T0-T8 that the ground state x=1 is unstable and generates the phi ladder. The phi ladder consists of successive powers phi^n for integer n, with rung k corresponding to phi^k. The Fibonacci cascade states that phi^n + phi^{n+1} = phi^{n+2}, realized here through ledger composition which encodes the addition of adjacent rungs into the next via the Recognition Composition Law.
proof idea
The term proof first unfolds the definition of ledgerCompose. It then applies the fibonacci_cascade lemma instantiated at argument k-2. Finally, convert using 2 followed by ring_nf aligns the sides by normalizing the ring expressions.
why it matters
This declaration completes the rung generation step in the Stillness as Generative Source derivation chain, showing how the initial conditions at rungs 0 and 1 produce all higher rungs via closure under T6. It directly implements the Fibonacci cascade listed in the module, which follows from phi forcing and the algebraic identity phi squared equals phi plus 1. The result supports constructions of the mass formula yardstick times phi to the power of rung minus 8 plus gap, though no immediate used_by sites appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.