corrected_in_range
plain-language theorem explainer
The first-order 8-tick corrected baryon asymmetry lies strictly between 0 and the leading RS scale φ^{-44}. Cosmologists checking the washout-corrected η_B against the Planck CMB band would cite this sandwich. Proof is a one-line pairing of positivity and the strict washout inequality.
Claim. The first-order corrected baryon asymmetry satisfies $0 < \eta_B^{(1)} < \varphi^{-44}$, where $\eta_B^{(1)} = \varphi^{-44}\cdot(1-\delta)$ is the leading $\varphi$-ladder scale times the 8-tick washout correction factor.
background
In Recognition Science the leading baryon asymmetry sits on the φ-ladder at rung −44: η_B^{lead} := φ^{−44} ≈ 6.376×10^{−10}. That overshoots the Planck 2018 CMB central value (6.104±0.058)×10^{−10} by about 4.5%. With zero free parameters the gap cannot be tuned; the module studies the first subleading correction from 8-tick defect washout during the electroweak sphaleron epoch.
The physical picture: sphalerons stay active for N_sph ≈ φ^8 cycles of the eight-tick. Each cycle the recognition operator reduces defect by a natural rate δ = φ^{−8}, so the net washout factor is correction_factor = (1−δ) < 1. The corrected prediction is therefore η_B^{corr} := η_B^{lead} · correction_factor.
Upstream facts already proved in this module: η_B^{corr} > 0 (product of two positive factors) and η_B^{corr} < η_B^{lead} (multiplication by a factor strictly less than one). The present theorem simply packages those two inequalities.
proof idea
Term-mode one-liner. The goal is a conjunction. The left conjunct is supplied by eta_B_corrected_pos (mul_pos of the leading-scale positivity and correction_factor_pos). The right conjunct is supplied by corrected_lt_leading, which unfolds the product definition and applies mul_lt_mul_of_pos_left (or the calc form with correction_factor < 1). No further arithmetic is performed here.
why it matters
Closes the elementary range statement for the first-order 8-tick correction to η_B inside Cosmology.BaryonHigherOrder. The module doc ties the correction to the eight-tick octave (forcing-chain T7) and to the zero-parameter RS claim that the 4.5% gap must be dynamical, not fitted. Numerically the washout moves the prediction from ≈6.376×10^{−10} down toward ≈6.28×10^{−10}, roughly halving the residual to CMB. No downstream theorems yet consume this sandwich, but it is the natural hypothesis-interface guard for any later comparison against the falsifier windows stated in the module: leading-order falsified outside [5.5,7.5]×10^{−10} at >5σ; corrected prediction falsified outside [6.0,6.5]×10^{−10} at >3σ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.