phi_zpow_neg8_lower
plain-language theorem explainer
The theorem establishes the strict lower bound φ^{-8} > 0.02126 on the eighth negative power of the golden ratio. Cosmologists deriving the baryon asymmetry prefactor c_RS in Recognition Science would cite this bound when constructing the numerical interval for η_B. The proof inverts the companion upper bound on φ^8 via the reciprocal identity and closes the comparison with linarith after a norm_num check.
Claim. $φ^{-8} > 0.02126$, where $φ = (1 + √5)/2$ denotes the golden ratio.
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. This squared form encodes independent washout of matter and antimatter sectors, each carrying one integration-gap worth of fermionic degrees of freedom at the eight-tick octave (T7) with D = 3. Upstream, phi_pow_8_upper supplies φ^8 < 47.03 from the Fibonacci identity φ^8 = 21φ + 13 together with φ < 1.62; the private lemma phi_zpow_neg8_eq_inv rewrites the negative integer power as the reciprocal of the positive power.
proof idea
The tactic proof first rewrites φ^{-8} as (φ^8)^{-1} using phi_zpow_neg8_eq_inv. It obtains the hypothesis φ^8 < 47.03 directly from phi_pow_8_upper, records positivity of φ^8, and applies inv_lt_inv₀ to produce the reciprocal inequality. A norm_num step confirms 1/47.03 ≥ 0.02126, after which linarith closes the goal.
why it matters
This bound is invoked by one_minus_phi_neg8_upper to produce the matching upper estimate on (1 − φ^{-8}), completing the two-sided numerical control on c_RS that yields the predicted η_B band (6.0–6.2) × 10^{-10}. It supplies the concrete lower edge of φ^{-8} ∈ (0.02126, 0.02137) listed in the module documentation, thereby anchoring the eight-tick washout interpretation at T7–T8 against the Planck 2018 measurement. The interpretive squared prefactor remains hypothesis-grade pending a first-principles Boltzmann derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.