one_minus_phi_neg8_upper
plain-language theorem explainer
The inequality (1 - φ^{-8}) < 0.979 supplies the upper endpoint needed to bound the baryogenesis prefactor c_RS from above. Workers tightening the predicted η_B interval from the eight-tick washout would cite this result to close the numerical sandwich around 0.956 to 0.959. The proof is a one-line wrapper that invokes the companion lower bound on φ^{-8} and finishes with linear arithmetic.
Claim. $1 - φ^{-8} < 0.979$, where $φ$ denotes the golden ratio satisfying $φ^2 = φ + 1$.
background
The module derives the order-one prefactor in the baryogenesis formula η_B = c × (integration-gap content) by setting c_RS = (1 - φ^{-8})^2. This squared form encodes independent washout channels for matter and antimatter sectors, each losing one rung of fermionic degrees of freedom per fundamental tick at D = 3. The eight-tick octave structure forces φ^8 = 21φ + 13 via the Fibonacci identity, which in turn yields the interval φ^{-8} ∈ (0.02126, 0.02137).
proof idea
The proof is a one-line wrapper. It imports the upstream theorem phi_zpow_neg8_lower (which states φ^{-8} > 0.02126) and applies linarith to obtain the complementary upper bound on 1 - φ^{-8}.
why it matters
The bound is invoked by c_RS_lower, c_RS_lt_one and c_RS_upper to sandwich c_RS inside (0.956, 0.959). These three results together close the predicted η_B band c_RS · φ^{-44} ∈ (6.0 × 10^{-10}, 6.2 × 10^{-10}), which contains the Planck 2018 value. The derivation fills the numerical content of the T7 eight-tick octave step in the forcing chain and supplies the concrete interval for the hypothesis that the squared washout encodes two independent channels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.