IndisputableMonolith.Cosmology.BaryonHigherOrder
Defines the leading-order baryon-to-photon ratio as φ^{-44} and packages the standard higher-order correction factors (sphaleron multiplicity and washout) that multiply it. Cosmologists matching RS η_B to the observed value cite these constants. The module is mostly positive real definitions with elementary interval lemmas; no deep derivation lives here.
claimThe leading-order baryon asymmetry is $\eta_B^{\mathrm{lead}} = \varphi^{-44}$. Higher-order factors are a sphaleron multiplicity $N_{\mathrm{sph}} > 1$ and a washout deficit $\delta \in (0,1)$, combined into a correction factor $C = N_{\mathrm{sph}}(1-\delta)$ lying in a fixed positive interval strictly below $N_{\mathrm{sph}}$.
background
Recognition Science places the baryon asymmetry on the $\varphi$-ladder. The exact rung module already proves that $\eta_B$ sits at rung $-44$ and that the power balance $\eta_B \cdot \varphi^{45} = \varphi$ holds formally. The present module isolates the pure leading power $\varphi^{-44}$ as a named constant and introduces the conventional order-one multipliers used when comparing that power to the measured baryon-to-photon ratio.
$N_{\mathrm{sph}}$ is the effective sphaleron conversion multiplicity (strictly greater than one). $\delta_{\mathrm{washout}}$ is a fractional washout deficit in $(0,1)$. Their product with a unit leading term yields a correction factor whose positivity and upper bound are recorded as elementary lemmas. Constants are taken from the RS native unit system ($c=1$, etc.).
proof idea
Definition module with short positivity and interval lemmas. Leading $\eta_B$ is the literal power $\varphi^{-44}$. Positivity of that power, of $N_{\mathrm{sph}}$, and of $\delta$ are immediate from $\varphi>1$ and the stated bounds. The correction factor is the algebraic product $N_{\mathrm{sph}}(1-\delta)$; its membership in a concrete open interval follows by multiplying the two elementary inequalities $N_{\mathrm{sph}}>1$ and $0<\delta<1$. No forcing-chain or RCL reasoning is invoked here.
why it matters in Recognition Science
Supplies the named leading term and correction scaffolding imported by the $\eta_B$ prefactor module. That downstream module treats the order-one prefactor $c_{RS}=(1-\varphi^{-8})^2$ as a selected ansatz rather than a derivation; it needs a clean leading $\varphi^{-44}$ and bounded correction factor to state the residual matching problem honestly. In the broader RS cosmology chain this sits after the exact rung $-44$ theorem and before any claim that the full numerical $\eta_B$ is forced. It does not itself close the baryon asymmetry; it only factors the leading ladder power from the $O(1)$ multipliers.
scope and limits
- Does not derive η_B from first principles; only names the leading φ^{-44} term.
- Does not prove the numerical value of N_sph or δ; they are parameters with interval bounds.
- Does not derive the order-one prefactor c_RS; that lives downstream as a selected ansatz.
- Does not address photon-to-baryon conversion efficiency beyond the washout factor δ.
- Does not invoke T5–T8 forcing, RCL, or eight-tick structure.
used by (1)
depends on (2)
declarations in this module (22)
-
theorem
eta_B_leading -
theorem
eta_B_leading_pos -
def
N_sph -
theorem
N_sph_pos -
theorem
N_sph_gt_one -
def
delta_washout -
theorem
delta_pos -
theorem
delta_lt_one -
def
correction_factor -
theorem
correction_factor_pos -
theorem
correction_factor_lt_one -
theorem
correction_factor_in_interval -
def
eta_B_corrected -
theorem
eta_B_corrected_pos -
theorem
corrected_lt_leading -
theorem
corrected_in_range -
theorem
correction_moves_toward_cmb -
theorem
correction_is_8tick_rung -
theorem
corrected_decomposition -
theorem
correction_term_rung -
structure
BaryonCorrectionCert -
theorem
baryon_correction_cert