BaryogenesisCert
plain-language theorem explainer
BaryogenesisCert packages three assertions for matter-antimatter asymmetry in Recognition Science cosmology: the set of baryogenesis mechanisms has cardinality five, J-cost vanishes at the symmetric point r=1, and J-cost is strictly positive for every other positive r. Cosmologists deriving the observed baryon-to-photon ratio from the J-cost function would cite it when linking Sakharov conditions to the five enumerated channels. The declaration is a plain record type whose fields are supplied by sibling lemmas in the same module.
Claim. A structure certifying baryogenesis consists of three fields: the cardinality of the set of baryogenesis mechanisms equals 5; the J-cost function satisfies $J(1)=0$; and for every positive real $r$ with $r≠1$, $J(r)>0$.
background
The J-cost function measures the energetic penalty associated with a scale factor away from unity and satisfies the Recognition Composition Law. The inductive type BaryogenesisMechanism enumerates five channels (leptogenesis, electroweak, Affleck-Dine, cold, and GUT) whose count is fixed by the spatial dimension plus two additional degrees of freedom. The module translates the Sakharov conditions into RS language: baryon-number violation as sigma-export above threshold, CP violation as J(r)≠J(r*), and departure from equilibrium as J(r)>0. Upstream, the equilibrium theorem states that Jcost 1 = 0 by direct evaluation of the unit case.
proof idea
The structure is introduced as a plain record type. Its fields are populated downstream by the definition baryogenesisCert, which supplies baryogenesisMechanismCount for the cardinality, matter_balance_equilibrium for the zero at unity, and asymmetry_positive_cost for the strict positivity away from unity. No tactics are required.
why it matters
This certificate sits at the root of the baryogenesis development and is instantiated in both the phi-ladder trajectory module and the gravity RSBaryogenesis module. It directly implements the five-mechanism count required by the Recognition Composition Law and the eight-tick octave structure. The parent theorems that consume it are the baryogenesisCert definitions in sibling files, which in turn feed spectral-index predictions and eta_B bounds. It closes the loop between the J-cost asymmetry and the observed eta ≈ 6.1×10^{-10}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.