fibonacci_cascade
The Fibonacci cascade identity states that powers of the golden ratio φ obey φ^n + φ^{n+1} = φ^{n+2} for any integer n. Researchers constructing the Recognition Science phi-ladder from the ground state would cite this to show how adjacent rungs generate the next via closure. The proof is a short algebraic reduction that invokes the defining equation φ² = φ + 1 and finishes with ring normalization.
claimLet φ be the positive real satisfying φ² = φ + 1. Then for every integer n, φ^n + φ^{n+1} = φ^{n+2}.
background
The StillnessGenerative module derives that the unique zero-defect ground state x = 1 is unstable and generates structure. It relies on the Law of Existence (T5), Recognition Forcing (T4) that excludes uniform configurations, the eight-tick cycle (T7), and T6 closure that forces ratio φ on non-trivial entries. The phi-ladder is the resulting sequence of scales φ^k for integer k, with the Fibonacci cascade supplying the composition rule that populates successive rungs from the initial condition.
proof idea
The proof first obtains positivity and nonzeroness of φ from PhiForcing.phi_pos. It rewrites the powers via zpow_add₀, substitutes the base identity φ² = φ + 1 taken from PhiForcing.phi_equation (and equivalently from PhiRing.phi_equation), then closes the equation by the ring tactic.
why it matters in Recognition Science
This identity is the direct enabler for the population theorems closure_populates_next and every_rung_from_fibonacci in the same module, which together establish stillness_is_creative. It realizes the Fibonacci cascade step listed in the module derivation chain, confirming that T6 closure plus the defining equation of φ suffice to generate the entire ladder without external assumptions. It touches no open questions.
scope and limits
- Does not prove existence or uniqueness of the phi-ladder itself.
- Does not assign physical masses or constants to specific rungs.
- Does not compute the J-cost of any ladder entry.
- Does not extend the identity to non-integer exponents.
Lean usage
exact fibonacci_cascade nformal statement (Lean)
320theorem fibonacci_cascade (n : ℤ) :
321 PhiForcing.φ ^ n + PhiForcing.φ ^ (n + 1) = PhiForcing.φ ^ (n + 2) := by
proof body
Tactic-mode proof.
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). -/