phi_zpow_neg44_upper
plain-language theorem explainer
The upper bound φ^{-44} < 6.40 × 10^{-10} is established here. Cosmologists using the Recognition Science derivation of the baryon asymmetry cite it to fix the upper edge of the predicted η_B interval. The proof rewrites the negative exponent as a reciprocal, substitutes the Fibonacci closed form for the positive power, invokes the bound φ > 1.61, and closes the comparison with nlinarith and linarith.
Claim. $φ^{-44} < 6.40 × 10^{-10}$
background
The module derives the prefactor c_RS = (1 − φ^{-8})^2 for the baryogenesis formula η_B = c × (algebraic content forced by the integration-gap rung). The squared form encodes two independent washout channels, each proceeding at rate φ^{-8} (one rung per fundamental tick at D = 3). This supplies the numerical upper bound on φ^{-44} needed to place the corrected prediction inside the observed band. It relies on the Fibonacci identity φ^{44} = 701408733 φ + 433494437 together with the auxiliary bound φ > 1.61.
proof idea
The argument first rewrites φ^{-44} as the reciprocal of φ^{44} via the dedicated inversion lemma. It then proves φ^{44} > 1.5627 × 10^9 by substituting the Fibonacci expression and applying the lower bound φ > 1.61, followed by nlinarith. Inversion of the inequality (via inv_lt_inv₀) and a direct numerical comparison of the reciprocal to 6.40 × 10^{-10} (via norm_num and linarith) finish the chain.
why it matters
The result is invoked by the downstream theorem that bounds the corrected η_B from above by 6.2 × 10^{-10}. It completes the verification that c_RS · φ^{-44} lies in (6.0 × 10^{-10}, 6.2 × 10^{-10}), which contains the Planck 2018 measurement (6.10 ± 0.04) × 10^{-10}. In the framework it closes the upper numerical edge of the two-sided 8-tick washout derivation, consistent with the eight-tick octave and D = 3. The interpretive squared form of c_RS remains hypothesis-grade pending a first-principles Boltzmann derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.