baryogenesisCert
plain-language theorem explainer
The declaration supplies a concrete certificate that the J-cost function satisfies the three Sakharov conditions for baryogenesis in the Recognition Science setting. Cosmologists modeling early-universe asymmetry would cite this to confirm that five mechanisms, equilibrium at equal matter-antimatter, and positive J for imbalance are all realized. The proof is a direct structure construction that assembles the certificate from three prior results on mechanism count, J-unit vanishing, and positivity.
Claim. Let $B$ be the structure whose fields assert that there exist exactly five baryogenesis mechanisms, that the J-cost vanishes at unit ratio ($J(1)=0$), and that the J-cost is strictly positive for every positive ratio not equal to one. The definition constructs an explicit instance of $B$ by direct assignment of the three fields from the corresponding count, vanishing, and positivity results.
background
The module maps the observed baryon-to-photon ratio to an early-universe sigma-imbalance expressed through the J-cost function. Sakharov conditions are realized as: baryon violation equals sigma-export above threshold, CP violation equals $J(r) neq J(r^*)$ for the CP-conjugate, and departure from equilibrium equals $J(r)>0$. Five mechanisms (leptogenesis, electroweak, Affleck-Dine, cold baryogenesis, GUT) correspond to configuration dimension 5. The J-cost is the function $J(x)=(x+x^{-1})/2-1$ whose positivity and vanishing properties are established upstream. The structure BaryogenesisCert packages these three properties into a single certificate object.
proof idea
The definition is a direct structure constructor. It populates the five_mechanisms field with the result of the mechanism-count theorem, the equilibrium field with the unit-vanishing theorem, and the asymmetry field with the positivity theorem. No additional tactics or reductions are required beyond the field assignments.
why it matters
This certificate is referenced by the phi-ladder trajectory definition in BaryogenesisTrajectoryFromPhiLadder, which lifts the basic J-cost realization to the full etaB rung-ratio computation. It supplies the J-cost foundation before the phi-ladder extension and before the gravity-module version. The construction closes the elementary realization of the five-dimensional mechanism space required by the cosmology module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.