eta_B_corrected_upper
The corrected baryon asymmetry eta_B equals c_RS times phi to the power -44 and is shown to lie strictly below 6.2 times 10 to the -10. Cosmologists testing Recognition Science baryogenesis against Planck data would cite this bound to close the upper edge of the predicted interval. The proof unfolds the definition of eta_B_corrected and feeds four pre-established inequalities (upper bounds on c_RS and on phi^{-44} together with positivity) directly into nlinarith.
claimLet $c_{RS} = (1 - phi^{-8})^2$ be the two-sided 8-tick washout prefactor. Define the corrected baryon-to-photon ratio by $eta_B = c_{RS} cdot phi^{-44}$. Then $eta_B < 6.2 times 10^{-10}$.
background
In the Recognition Science module on eta_B, the prefactor c_RS is defined as the square of (1 - phi^{-8}), where the exponent -8 encodes one rung per fundamental tick in the eight-tick octave at D = 3. Each factor of (1 - phi^{-8}) represents washout of one integration-gap sector of fermionic degrees of freedom. The corrected eta_B is then obtained by multiplying this prefactor by phi^{-44}, which supplies the algebraic mass-scale content forced by the integration-gap rung. Upstream lemmas establish c_RS < 0.959, phi^{-44} < 6.40e-10, and the positivity of both quantities.
proof idea
The proof is a one-line wrapper. It unfolds eta_B_corrected to the product c_RS * phi^{-44}, then supplies the four facts c_RS_upper, phi_zpow_neg44_upper, c_RS_pos, and zpow_pos. These inequalities are passed to nlinarith, which closes the strict upper bound.
why it matters in Recognition Science
This theorem supplies the upper half of the two-sided band proved in eta_B_corrected_in_observed_band, which places the Recognition Science prediction inside the Planck 2018 interval (6.10 plus or minus 0.04) times 10^{-10}. It quantifies the T7 eight-tick octave contribution to the forcing chain by bounding the washout at rung -8 and the rung -44 factor. The numerical band itself is theorem-grade; the squared interpretive form of c_RS remains hypothesis-grade pending a first-principles Boltzmann derivation.
scope and limits
- Does not derive the squared form of c_RS from a Boltzmann equation.
- Does not incorporate temperature-dependent running of constants.
- Does not address stability of the band under small changes to the phi interval.
- Does not prove the result for non-standard values of D.
formal statement (Lean)
220theorem eta_B_corrected_upper : eta_B_corrected < 6.2e-10 := by
proof body
Term-mode proof.
221 unfold eta_B_corrected
222 have hc : c_RS < 0.959 := c_RS_upper
223 have hphi : phi ^ (-44 : ℤ) < 6.40e-10 := phi_zpow_neg44_upper
224 have hcpos : (0 : ℝ) < c_RS := c_RS_pos
225 have hphi_pos : (0 : ℝ) < phi ^ (-44 : ℤ) := zpow_pos phi_pos (-44)
226 nlinarith [hc, hphi, hcpos, hphi_pos]
227
228/-- The η_B band: `c_RS · φ^(−44) ∈ (6.0 × 10⁻¹⁰, 6.2 × 10⁻¹⁰)`. -/