phi_pow_fib_succ
plain-language theorem explainer
The lemma establishes that powers of the golden ratio satisfy φ^{n+1} = F_{n+1} φ + F_n for natural numbers n. Cosmologists deriving the baryon-to-photon ratio η_B within Recognition Science invoke it to bound φ^44 and match the observed asymmetry near 6 × 10^{-10}. The proof proceeds by induction on n, applying the Fibonacci recurrence and the quadratic relation φ^2 = φ + 1 at each step.
Claim. For every natural number $n$, $φ^{n+1} = F_{n+1} φ + F_n$, where $φ$ is the golden ratio satisfying $φ^2 = φ + 1$ and $F_k$ denotes the $k$-th Fibonacci number.
background
The module COS-007 derives the baryon-to-photon ratio η ≈ 6.1 × 10^{-10} from Recognition Science's φ-structure and the intrinsic asymmetry of the 8-tick phase. The golden ratio φ arises as the self-similar fixed point in the forcing chain, and its powers obey the Fibonacci recurrence because φ satisfies the same quadratic equation as the Fibonacci characteristic equation. Upstream results supply the J-cost structure from PhiForcingDerived.of and the ledger factorization from DAlembert.LedgerFactorization.of that calibrate the discrete φ-tiers used for mass and density ladders.
proof idea
The proof is by induction on n. The base case n = 0 reduces directly via Nat.fib_zero, Nat.cast_zero and add_zero. In the successor step it invokes Nat.fib_add_two to obtain the recurrence for F_{n+2}, rewrites the inductive hypothesis, expands with ring, substitutes the identity φ^2 = φ + 1, and regroups coefficients to reach the target form.
why it matters
The lemma supplies the exact closed form needed for the numerical bounds φ^44 > 1.5 × 10^9 and φ^44 < 1.6 × 10^9 that appear in the same module. Those bounds confirm that φ^{-44} lies within a few percent of the observed η_B, closing the step from the eight-tick octave and CP violation in the 8-tick phase structure to the predicted matter abundance. It therefore anchors the COS-007 derivation inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.