IndisputableMonolith.Cosmology.EtaBPrefactorDerivation
Derives the order-one structural prefactor in the baryon-to-photon ratio η_B from two-sided 8-tick sphaleron washout. Matter and antimatter each contribute one dimension-gap of fermionic degrees of freedom, so the washout factor (1 − φ^{-8}) appears once per sector and squares. Cosmologists matching the RS φ-ladder prediction to the observed η_B cite this module for the explicit constant c_RS and its unit-interval bounds.
claimThe RS order-one prefactor is $c_{\mathrm{RS}} = (1 - \varphi^{-8})^2$, where $\varphi$ is the golden ratio. The module proves $0 < c_{\mathrm{RS}} < 1$, supplies Fibonacci bounds on $\varphi^8$ and $\varphi^{-8}$, and lower-bounds $1 - \varphi^{-8}$.
background
Recognition Science places the baryon-to-photon ratio on the φ-ladder at rung −44: the leading-order claim is η_B = φ^{-44}. Upstream modules already certify that this value lies in (5.5, 7.5) × 10^{-10} and that the exact balance η_B × φ^{45} = φ holds formally. A residual ~4.5% gap relative to Planck 2018 motivates a first subleading correction.
The eight-tick octave (forcing step T7) sets the sphaleron washout timescale. GapDerivation identifies the coherence-energy exponent with configuration dimension D+2, so at D=3 one has E_coh = φ^{-5} and a single dimension-gap of fermionic DOF per sector. The present module isolates the pure structural prefactor that multiplies the leading φ-power once both matter and antimatter sectors are washed out.
proof idea
The module is definition-plus-bounds, not a single deep theorem. It defines c_RS as (1 − φ^{-8})^2 (equivalently the expanded polynomial form), then chains elementary inequalities: positivity of φ and of 1 − φ^{-8}, Fibonacci sandwich bounds on φ^8 and hence on φ^{-8}, and the resulting strict enclosure 0 < c_RS < 1. Companion lemmas record φ^{-8} = 1/φ^8 and one-sided bounds on 1 − φ^{-8} for use by higher-order η_B corrections.
why it matters in Recognition Science
Feeds the Unified Forcing Chain, which imports the cosmology stack to keep the baryon-asymmetry sector inside the T0–T8 inevitability argument. Supplies the concrete order-one constant that BaryonHigherOrder multiplies onto φ^{-44} when closing the 4.5% gap, and that EtaBIntervalCert and BaryonAsymmetryExact treat as the structural coefficient in front of the rung-−44 prediction. Ties directly to the eight-tick octave (T7) and to the dimension-gap counting from GapDerivation (D=3).
scope and limits
- Does not derive the rung −44 placement of η_B; that lives in BaryonAsymmetryExact.
- Does not compute the numerical 4.5% correction; only the structural prefactor c_RS.
- Does not claim c_RS equals the full Sakharov or electroweak prefactor outside RS units.
- Does not re-prove φ bounds from scratch; relies on Constants and Fibonacci identities.
used by (1)
depends on (5)
declarations in this module (29)
-
def
c_RS -
theorem
c_RS_expanded -
theorem
c_RS_pos -
theorem
c_RS_lt_one -
theorem
c_RS_in_unit_interval -
theorem
phi_pow_8_fib -
theorem
phi_pow_8_lower -
theorem
phi_pow_8_upper -
lemma
phi_zpow_neg8_eq_inv -
theorem
phi_zpow_neg8_lower -
theorem
phi_zpow_neg8_upper -
theorem
one_minus_phi_neg8_lower -
theorem
one_minus_phi_neg8_upper -
theorem
c_RS_lower -
theorem
c_RS_upper -
lemma
phi_zpow_neg44_eq_inv -
theorem
phi_zpow_neg44_lower -
theorem
phi_zpow_neg44_upper -
def
eta_B_corrected_two_sided -
theorem
eta_B_corrected_two_sided_pos -
theorem
corrected_lt_leading -
theorem
eta_B_corrected_lower -
theorem
eta_B_corrected_upper -
theorem
eta_B_corrected_in_observed_band -
theorem
observed_in_predicted_band -
theorem
two_sided_stronger_than_one_sided -
theorem
two_sided_corrected_lt_one_sided -
structure
EtaBPrefactorCert -
theorem
eta_B_prefactor_cert