phi_zpow_neg8_eq_inv
plain-language theorem explainer
Establishes the identity φ^{-8} equals the reciprocal of φ^8 over the reals. Cosmologists deriving the Recognition Science baryogenesis prefactor cite it to convert upper bounds on φ^8 into lower bounds on the reciprocal. The proof is a one-line wrapper that normalizes the integer exponent then applies the general zpow_neg and zpow_natCast rules.
Claim. $φ^{-8} = (φ^8)^{-1}$
background
The module derives the order-one prefactor c_RS = (1 − φ^{-8})^2 that multiplies the algebraic content forced by the integration-gap rung in the baryogenesis formula η_B. The squared form encodes independent washout channels for matter and antimatter sectors, each suppressed at rate φ^{-8} per fundamental tick at D = 3. Bounds on φ^8 are first obtained from the Fibonacci identity φ^n = F_n φ + F_{n-1} together with φ ∈ (1.61, 1.62), then converted via the present identity to the interval (0.02126, 0.02137) for φ^{-8}.
proof idea
One-line wrapper. It rewrites the exponent (−8 : ℤ) as the negation of (8 : ℕ), applies zpow_neg to produce the reciprocal, and finishes with zpow_natCast to align the natural-number power.
why it matters
The lemma is invoked directly by phi_zpow_neg8_lower and phi_zpow_neg8_upper, which supply the numerical band for c_RS · φ^{-44} that matches the Planck 2018 value η_B = (6.10 ± 0.04) × 10^{-10}. It therefore closes the eight-tick washout step inside the T7 octave of the UnifiedForcingChain and supports the interpretive claim that the squared prefactor arises from two independent fermionic sectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.