baryon_correction_cert
plain-language theorem explainer
Certificate packaging the first-order 8-tick washout correction to the baryon asymmetry: leading scale φ^{-44}, factor (1-φ^{-8}), corrected product positive and strictly below the leading term, absolute correction at rung -52. Cosmologists auditing the RS η_B gap to Planck would cite this bundle. Proof is a term-mode structure fill: three definitional fields by rfl, inequalities by already-proved sibling lemmas.
Claim. A certificate asserts: the leading baryon scale equals $\phi^{-44}$; the correction factor equals $1-\phi^{-8}$; the corrected prediction is their product; the factor lies in $(0,1)$; the corrected value is positive and strictly smaller than the leading term; and the absolute correction term equals $\phi^{-52}$.
background
Recognition Science predicts the baryon-to-photon ratio at leading order as $\eta_B=\phi^{-44}\approx 6.376\times 10^{-10}$. Planck 2018 reports $(6.104\pm 0.058)\times 10^{-10}$, a roughly 4.5% excess that cannot be tuned because RS has no free parameters.
This module treats the first subleading correction from 8-tick defect propagation during the electroweak phase transition. Sphalerons remain active for about $N_{\mathrm{sph}}\approx\phi^8$ recognition cycles; each cycle the recognition operator reduces baryon excess by a natural rate $\delta=\phi^{-8}$. The net first-order factor is therefore $1-\phi^{-8}\approx 0.9853$, giving $\eta_B^{(1)}=\phi^{-44}(1-\phi^{-8})$.
The certificate structure bundles the definitional identities (leading scale, correction factor, corrected product) with the elementary positivity and ordering facts already proved for those quantities, plus the rung identity that the absolute correction term is $\phi^{-52}$.
proof idea
Term-mode inhabitant of the certificate structure. The three definitional fields (leading scale equals $\phi^{-44}$, correction factor equals $1-\phi^{-8}$, corrected value equals the product) are discharged by rfl. Positivity of the factor uses correction_factor_pos (from $\delta<1$); strict upper bound uses correction_factor_lt_one (from $\delta>0$). Strict decrease of the corrected prediction relative to the leading term is corrected_lt_leading; positivity of the corrected value is eta_B_corrected_pos (product of two positive factors). The absolute correction identity $\phi^{-44}\cdot\phi^{-8}=\phi^{-52}$ is correction_term_rung via the integer power addition law.
why it matters
Closes the local certificate for the first-order 8-tick washout story attached to the leading RS prediction $\eta_B=\phi^{-44}$. The eight-tick period is the T7 landmark of the forcing chain; here it supplies the natural washout cadence $N_{\mathrm{sph}}\approx\phi^8$ and the rung step $\delta=\phi^{-8}$. Numerically the correction halves the 4.5% gap to the CMB central value (down to roughly $6.28\times 10^{-10}$).
No downstream consumers are wired yet; the object is the module-level packaging theorem. Epistemic status remains hypothesis on the sphaleron mechanism itself: the algebra is proved, the physical identification of $\delta$ with one rung per active period is not forced by T0–T8. The module states an explicit observational falsifier band around the corrected prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.