phi_pow_fib

The declaration sits inside the module that derives the order-one prefactor $c_{RS} = (1 − φ^{−8})^2$ for the baryogenesis formula η_B = c × (integration-gap content). The module interprets the squared factor as two independent washout channels, each carrying one integration-gap rung at the eight-tick octave with D = 3. It relies on the quadratic identity φ² = φ + 1 supplied by Constants.phi_sq_eq and on the Fibonacci recurrence Nat.fib_add_two.

Proof by induction on n. Base case n = 0 reduces via Nat.fib_zero, Nat.cast_zero and the explicit value fib 1 = 1. Inductive step rewrites φ^{n+2} = φ^{n+1} · φ, substitutes the inductive hypothesis, distributes, replaces φ² by φ + 1 via phi_sq_eq, collects terms, and matches the target via the Fibonacci addition formula hfib : Nat.fib (n + 2) = Nat.fib n + Nat.fib (n + 1).

Supplies the exact algebraic content for the downstream theorem phi_pow_44_fib that evaluates φ^{44} = 701408733 φ + 433494437, which is then multiplied by c_RS to produce the predicted η_B band (6.0, 6.2) × 10^{-10}. It directly implements the module step “φ^8 = 21φ + 13 via the Fibonacci identity” and supports the eight-tick washout argument (T7) that yields c_RS ∈ (0.956, 0.959). The interpretive squared form remains hypothesis-grade pending a Boltzmann derivation.