baryonAsymmetryCert
plain-language theorem explainer
The definition assembles a certificate that the baryon asymmetry equals phi to the power of negative 44 at rung 44, satisfying positivity, the bound phi to the 44 exceeding 10 to the 8, and the smallness condition eta_B times 10 to the 8 less than 1. Cosmologists using Recognition Science would cite it to confirm the phi-ladder prediction matches the required scale bounds. It is a direct structure constructor that references the rung equality and the three supporting bound theorems.
Claim. Let $η_B = φ^{-44}$. The certificate asserts that the rung equals 44, $0 < η_B$, $φ^{44} > 10^8$, and $η_B · 10^8 < 1$.
background
The module treats baryon asymmetry as an A3 baryogenesis outcome on the phi-ladder, with the explicit RS prediction η_B ≈ φ^{-44} and the auxiliary bound φ^{44} > 10^8. The structure BaryonAsymmetryCert packages four fields: the rung fixed at 44, positivity of η_B, the largeness of φ^{44}, and the upper bound η_B < 10^{-8}. The upstream etaB_pos theorem from BaryogenesisTrajectoryFromPhiLadder states that η_B is strictly positive on the whole trajectory, while the local etaB_small derives the 10^{-8} bound by unfolding the rung and invoking the phi44 inequality.
proof idea
The definition constructs the BaryonAsymmetryCert record by setting the rung field to baryonRung_gap45, which is reflexivity proving baryonRung = 44. It then supplies eta_pos from the local etaB_pos theorem, phi44_large from phi44_gt_1e8, and eta_small from the etaB_small theorem that reduces the product inequality directly to the phi44 bound.
why it matters
This definition supplies the assembled certificate for the A3 baryogenesis step in the Recognition Science cosmology module, confirming that the phi-ladder at rung 44 yields an asymmetry inside the observed window. It closes the local development by combining the rung theorem with the positivity and scale lemmas into a single usable object. The construction aligns with the forcing chain landmarks T5 J-uniqueness and T6 phi fixed point that generate the ladder itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.