eta_B_corrected_lower
plain-language theorem explainer
The theorem shows that the Recognition Science prediction for the baryon asymmetry η_B, given by the product of the two-sided washout prefactor and φ to the power minus 44, is strictly larger than 6.0 × 10^{-10}. A cosmologist matching the model to Planck measurements of the baryon-to-photon ratio would cite the result. The argument is a direct term proof that combines the lower bound on the prefactor c_RS with the lower bound on φ^{-44} inside nlinarith after unfolding the product and recording positivity.
Claim. $η_B > 6.0 × 10^{-10}$ where $η_B := c_{RS} · φ^{-44}$ and $c_{RS} := (1 - φ^{-8})^2$.
background
The module treats the baryon asymmetry as η_B = c × (algebraic content forced by integration-gap rung), with the order-one prefactor structurally derived as c_RS = (1 − φ^{-8})^2. This squared form encodes independent washout channels for the matter and antimatter sectors, each carrying one integration-gap rung at the eight-tick scale. The corrected prediction is introduced as the concrete product eta_B_corrected := c_RS · φ^{-44}.
proof idea
The proof unfolds the definition of eta_B_corrected to expose the product. It obtains c_RS > 0.956 from the lemma c_RS_lower, φ^{-44} > 6.37e-10 from phi_zpow_neg44_lower, and the positivity facts 0 < c_RS and 0 < φ^{-44} from c_RS_pos and zpow_pos. These four inequalities are passed directly to nlinarith.
why it matters
This lower bound is assembled with its upper counterpart into eta_B_corrected_in_observed_band, which asserts that the predicted interval (6.0 × 10^{-10}, 6.2 × 10^{-10}) contains the Planck 2018 central value. The result supplies the numerical content for the two-sided 8-tick washout construction in the module header, where the squared prefactor follows from the T7 octave and D = 3. It therefore anchors the claim that the Recognition Science model reproduces the observed η_B inside the stated band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.