fibonacci_cascade

formal source

 317/-- **Fibonacci Cascade Identity**: φ^n + φ^{n+1} = φ^{n+2}.
 318    This is the structural identity that populates the ladder.
 319    It follows directly from φ² = φ + 1. -/
 320theorem fibonacci_cascade (n : ℤ) :
 321    PhiForcing.φ ^ n + PhiForcing.φ ^ (n + 1) = PhiForcing.φ ^ (n + 2) := by
 322  have hphi_pos := PhiForcing.phi_pos
 323  have hphi_ne := hphi_pos.ne'
 324  rw [zpow_add₀ hphi_ne n 2, zpow_add₀ hphi_ne n 1]
 325  have h2 : PhiForcing.φ ^ (2 : ℤ) = PhiForcing.φ ^ (1 : ℤ) + 1 := by
 326    rw [zpow_ofNat, zpow_one]
 327    exact PhiForcing.phi_equation
 328  rw [h2]
 329  ring
 330
 331/-- Equivalent form: 1 + φ = φ² (the base case of the Fibonacci cascade). -/
 332theorem one_plus_phi_eq_phi_sq : 1 + PhiForcing.φ = PhiForcing.φ ^ 2 := by
 333  linarith [PhiForcing.phi_equation]
 334
 335/-- **Ledger Composition Populates**: If the ledger has entries at
 336    scales φ^n and φ^{n+1}, additive ledger composition (from T6
 337    closure) creates an entry at scale φ^{n+2}.
 338
 339    This is the POPULATION theorem — not a cost bound, but a structural
 340    consequence of closure. The composed entry EXISTS. -/
 341theorem closure_populates_next (n : ℤ) :
 342    PhiForcingDerived.ledgerCompose (PhiForcing.φ ^ n) (PhiForcing.φ ^ (n + 1)) =
 343    PhiForcing.φ ^ (n + 2) := by
 344  unfold PhiForcingDerived.ledgerCompose
 345  exact fibonacci_cascade n
 346
 347/-- **Rung Generation**: Every rung k ≥ 2 is the ledger composition
 348    of the two preceding rungs. Starting from rung 0 (= 1, ground state)
 349    and rung 1 (= φ, forced by T4 + T6), repeated application generates
 350    all rungs: 0,1 → 2 → 3 → 4 → ...