phi_pow_44_lt_1pt6e9
plain-language theorem explainer
Recognition Science cosmologists use the bound φ^44 < 1.6 × 10^9 to anchor the prediction that φ^{-44} approximates the observed baryon asymmetry η ≈ 6.1 × 10^{-10}. This numerical fact appears in the derivation of matter abundance from the eight-tick phase structure. The proof reduces the exponent via the Fibonacci identity φ^{n+1} = F_{n+1} φ + F_n, substitutes the explicit Fibonacci numbers for 44 and 43, multiplies by the bound φ < 1.62, and concludes with linarith.
Claim. $φ^{44} < 1.6 × 10^{9}$
background
In the Cosmology.MatterAntimatter module the baryon-to-photon ratio η is derived from the intrinsic asymmetry in the 8-tick phase structure of Recognition Science. The golden ratio φ satisfies the recurrence that links its powers to Fibonacci numbers, allowing exact algebraic expressions for high powers. Upstream, the lemma phi_pow_fib_succ states that φ^{n+1} = (Nat.fib (n+1)) φ + Nat.fib n. The bound phi_lt_onePointSixTwo supplies φ < 1.62. These combine with arithmetic facts from the Foundation modules to control the size of φ^44. The local setting targets the Sakharov conditions for baryogenesis, where CP violation from the ledger produces ε_CP ~ 10^{-10} matching η.
proof idea
The tactic proof first rewrites the real exponentiation as a natural number power using Real.rpow_natCast. It then invokes phi_pow_fib_succ 43 to obtain the exact expression (701408733) φ + 433494437, where the Fibonacci numbers are inserted by native_decide. The inequality φ < 1.62 is applied to bound the linear term from above, after which linarith closes the proof.
why it matters
This bound is the key numerical step feeding the theorem phi_power_matches_eta, which concludes that φ^{-44} lies between 5.5e-10 and 7.5e-10 and therefore matches the observed η within 4.5 percent. It realizes the paper proposition that η emerges from φ-related phases in the 8-tick octave (T7). The exponent 44 encodes flip_count(axis_0) times torsion_gap(Δτ₁₂), linking directly to the alpha inverse formula in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.