correction_factor_in_interval
plain-language theorem explainer
The first-order washout correction factor 1 − φ⁻⁸ lies strictly in the open interval (0, 1). Cosmologists citing the RS η_B correction use this to guarantee the corrected asymmetry stays positive and strictly below the leading φ⁻⁴⁴ term. The proof is a one-line pairing of the already-proved positivity and strict-upper-bound lemmas.
Claim. The first-order correction factor $1 - \varphi^{-8}$ satisfies $0 < 1 - \varphi^{-8} < 1$.
background
In the RS cosmology stack the leading baryon asymmetry is $\eta_B = \varphi^{-44}$. That value sits about 4.5% above the Planck 2018 CMB central value. Because RS has no free parameters, the gap cannot be tuned; the module therefore computes the first subleading correction from 8-tick defect washout during the electroweak epoch.
Sphalerons remain active for roughly $N_{\mathrm{sph}} \approx \varphi^8$ eight-tick cycles. Each cycle the recognition operator reduces ledger defect by a fractional rate $\delta = \varphi^{-8}$. The net multiplicative washout is therefore the correction factor $1 - \delta = 1 - \varphi^{-8}$. Upstream lemmas already record that $\delta > 0$ and $\delta < 1$, so the factor is forced into $(0,1)$.
The local setting is the first-order 8-tick correction module: it packages the leading term, the sphaleron count, the washout rate, and the resulting corrected prediction $\eta_B^{(1)} = \varphi^{-44}(1-\varphi^{-8})$.
proof idea
Term-mode constructor pairing. The proof is the pair $\langle$correction_factor_pos, correction_factor_lt_one$\rangle$. The first conjunct unfolds the definition $1-\delta$ and applies linear arithmetic to $\delta < 1$; the second likewise uses $\delta > 0$. No further rewriting or case analysis is required.
why it matters
Places the washout factor inside the open unit interval, which is the minimal analytic control needed before forming the corrected prediction $\eta_B^{(1)} = \varphi^{-44}\times(1-\varphi^{-8})$. That corrected value drops the leading $6.376\times 10^{-10}$ to roughly $6.28\times 10^{-10}$, halving the residual gap to Planck. The result sits inside the T7 eight-tick octave story: the same $\varphi^8$ that fixes the octave period supplies both the sphaleron cycle count and the natural washout rung $\varphi^{-8}$. No downstream theorems yet consume it (used_by empty), but the module’s Part 3 corrected-prediction block is the intended consumer. The broader 8-tick washout picture remains a named hypothesis with explicit falsifiers on the $\eta_B$ window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.