fibonacci_cascade
plain-language theorem explainer
The identity φ^n + φ^{n+1} = φ^{n+2} for integer n populates successive rungs on the phi-ladder from the ground state in Recognition Science. Workers deriving generative consequences of the zero-defect state cite it when applying T6 closure to ledger entries. The proof is a short tactic sequence that rewrites exponents, reduces the base case to the defining equation φ² = φ + 1, and finishes by ring simplification.
Claim. For any integer $n$, $φ^n + φ^{n+1} = φ^{n+2}$, where $φ$ satisfies the equation $φ^2 = φ + 1$.
background
The StillnessGenerative module derives from the T0–T8 chain that the unique zero-defect state x=1 is not passive but forces non-trivial structure. Its derivation chain explicitly lists the Fibonacci cascade as step 7: “φ^n + φ^{n+1} = φ^{n+2} (from φ² = φ + 1). Adjacent rungs compose into the next rung, populating the entire ladder.” The phi-ladder is the sequence of scales φ^k for k ∈ ℤ that arises once T4 recognition and T6 closure force the ratio φ. The identity rests on the upstream theorem phi_equation (both in PhiRing and PhiForcing), which states φ² = φ + 1.
proof idea
The tactic proof obtains positivity and non-equality of φ from PhiForcing.phi_pos, rewrites the left-hand side via zpow_add₀, reduces the base case φ² = φ + 1 by invoking PhiForcing.phi_equation (after zpow_ofNat and zpow_one), and concludes with ring.
why it matters
This identity supplies the structural engine for the module’s claim that stillness is creative. It is invoked directly by closure_populates_next (“If the ledger has entries at scales φ^n and φ^{n+1}, additive ledger composition creates an entry at scale φ^{n+2}”) and by every_rung_from_fibonacci to generate all rungs from the ground state. It fills the explicit “Fibonacci cascade” step in the T0–T8 derivation chain, linking T6 closure to the population of the ladder without external assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.