phi_zpow_neg44_lower
plain-language theorem explainer
The inequality supplies a strict numerical lower bound on the golden ratio raised to the negative forty-fourth power, which anchors the lower edge of the Recognition Science prediction for the baryon asymmetry. Cosmologists working inside the framework cite this result when verifying that the derived η_B interval overlaps the Planck 2018 measurement. The argument rewrites the negative exponent via an inversion lemma, substitutes the Fibonacci closed form for the positive power, invokes the bound φ < 1.62, and closes the comparison with standard
Claim. $φ^{-44} > 6.37 × 10^{-10}$
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 = c × (algebraic content). Here φ is the golden ratio satisfying φ^2 = φ + 1. The eight-tick octave follows from the self-similar fixed point at T6 and the period 2^3 at T7 of the forcing chain, with D = 3 spatial dimensions fixing the rung spacing. Upstream, phi_pow_44_fib asserts φ^{44} = 701408733 φ + 433494437 via the Fibonacci identity φ^{n+1} = F(n+1)φ + F(n). The lemma phi_lt_onePointSixTwo states the tighter bound φ < 1.62 because √5 < 2.24, while phi_zpow_neg44_eq_inv rewrites the negative integer power as the reciprocal of the positive power.
proof idea
The tactic proof first applies the rewrite phi_zpow_neg44_eq_inv to convert the claim into a lower bound on the reciprocal of φ^{44}. It then obtains an upper bound on φ^{44} by substituting the Fibonacci expression from phi_pow_44_fib and feeding the known inequality φ < 1.62 into nlinarith. Positivity of φ^{44} is immediate from pow_pos. Inversion of the resulting strict inequality produces the reciprocal lower bound, which is compared to 6.37e-10 by a norm_num fact and closed by linarith.
why it matters
The bound is invoked directly inside eta_B_corrected_lower to conclude that the corrected η_B prediction exceeds 6.0 × 10^{-10}. It supplies the numerical floor for the φ^{-44} term that appears in the eight-tick washout model, where the squared prefactor (1 − φ^{-8})^2 encodes two independent washout channels at rate φ^{-8}. The result places the predicted band (6.0 to 6.2) × 10^{-10} around the observed value (6.10 ± 0.04) × 10^{-10}. The interpretive squared form of c_RS remains hypothesis-grade pending a first-principles Boltzmann-equation derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.