BaryonAsymmetryCert
plain-language theorem explainer
BaryonAsymmetryCert bundles the rung equality, positivity of etaB_RS, and the two magnitude bounds on phi^44 and etaB_RS that certify the RS baryon asymmetry prediction. Cosmologists using the Recognition Science framework cite this structure to confirm η_B ≈ φ^{-44} satisfies the required inequalities. The definition directly assembles the four fields from sibling declarations without additional lemmas.
Claim. A certificate structure asserting that the baryon rung equals 44, that $0 < η_B^{RS}$, that $φ^{44} > 10^8$, and that $η_B^{RS} ⋅ 10^8 < 1$.
background
The module implements the A3 Baryogenesis prediction of Recognition Science. It fixes baryonRung at the integer 44 and defines etaB_RS as the reciprocal of φ raised to that power. The structure collects the four conditions that certify the predicted asymmetry η_B ≈ φ^{-44} lies below the observed upper bound while remaining positive. Upstream rung definitions in anchor policies and the cosmic microwave background module converge on the same assignment of 44 to the baryon sector. The module documentation states the RS prediction η_B ≈ φ^{-44} together with the explicit bound φ^{44} > 10^8.
proof idea
This is a structure definition. Its fields are filled by direct reference to the sibling declarations baryonRung, etaB_pos, phi44_gt_1e8, and etaB_small. No lemmas or tactics are applied.
why it matters
The structure is instantiated by baryonAsymmetryCert to produce a concrete certificate for the baryon asymmetry. It thereby completes the numerical verification step in the phi-ladder cosmology module. This step aligns with the self-similar scaling fixed by the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.