BaryonCorrectionCert
plain-language theorem explainer
Certificate structure for the first-order 8-tick washout correction to the baryon asymmetry: leading scale φ^{-44} is multiplied by (1 − φ^{-8}), with positivity, strict reduction below the leading term, and the washout product at rung −52. Cosmologists comparing the RS η_B ladder to Planck CMB cite it. Pure field packaging; the inhabiting theorem discharges equalities by rfl and inequalities by sibling positivity lemmas.
Claim. A certificate asserting: the leading baryon-asymmetry scale equals $\phi^{-44}$; the correction factor equals $1-\phi^{-8}$; the corrected prediction is their product; that factor lies in $(0,1)$; the corrected value is positive and strictly smaller than the leading scale; and the leading scale times the per-cycle washout rate $\phi^{-8}$ equals $\phi^{-52}$.
background
The module computes the first subleading correction to the RS baryon asymmetry $\eta_B=\phi^{-44}$. That leading value is about $6.376\times 10^{-10}$, roughly 4.5% above the Planck 2018 CMB central value $(6.104\pm 0.058)\times 10^{-10}$. With zero free parameters the gap cannot be tuned away; the proposed reduction comes from 8-tick defect washout during the electroweak phase transition.
Sphalerons stay active for $N_{\mathrm{sph}}\approx\phi^8$ recognition cycles (one full octave). Each cycle the recognition operator reduces the baryon excess by $\delta=\phi^{-8}$. The first-order factor is therefore $1-\delta=1-\phi^{-8}\approx 0.9853$, giving $\eta_B^{(1)}=\phi^{-44}(1-\phi^{-8})$.
Upstream defs fix the leading scale as $\phi^{-44}$, the per-cycle washout as $\phi^{-8}$, and the correction factor as one minus that washout. The tick is the fundamental RS time quantum; eight ticks form one octave.
proof idea
Structure definition, not a proved theorem: it declares eight fields any inhabiting certificate must supply. Three fields are definitional equalities (leading scale, correction factor $1-\phi^{-8}$, corrected product). Two bound the correction factor in $(0,1)$. Two assert the corrected $\eta_B$ is positive and strictly below the leading scale. The last equates leading scale times per-cycle washout to $\phi^{-52}$. The companion theorem fills equalities by rfl and inequalities by sibling lemmas such as correction_factor_pos and correction_factor_lt_one.
why it matters
Packages the hypothesis that first-order 8-tick sphaleron washout halves the 4.5% gap between $\phi^{-44}$ and the CMB $\eta_B$. Downstream, baryon_correction_cert inhabits the structure and is labeled the baryon correction theorem (hypothesis): it reduces $\eta_B$ from $\phi^{-44}$ to $\phi^{-44}(1-\phi^{-8})$. The $\phi^{-8}$ washout rung ties directly to the eight-tick octave (T7) and the phi-ladder scale architecture. Epistemic status stays hypothesis: $\eta_B$ outside $[6.0,6.5]\times 10^{-10}$ at $>3\sigma$ would falsify the corrected prediction; a wider band falsifies the leading term alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.