BaryogenesisMechanism
plain-language theorem explainer
The inductive definition enumerates five baryogenesis mechanisms as the complete set of channels realizing matter-antimatter asymmetry under the Recognition Science J-cost model. Cosmologists verifying Sakharov conditions via sigma-imbalance and J-cost departure from equilibrium would cite this list to confirm the configuration dimension equals five. The declaration is a direct inductive type with five constructors that derives decidable equality and finite cardinality automatically.
Claim. Let $B$ be the finite set of baryogenesis mechanisms defined inductively by the five constructors leptogenesis, electroweak baryogenesis, Affleck-Dine mechanism, cold baryogenesis, and GUT baryogenesis.
background
In the Recognition Science cosmology setting the baryon-to-photon ratio arises from a sigma-imbalance in the early universe. The Sakharov conditions map to baryon-number violation as sigma-export above threshold, CP violation as $J(r) neq J(r^*)$ for the CP-conjugate, and departure from equilibrium as $J(r) > 0$. The module states that these conditions are realized by exactly five mechanisms, matching configuration dimension $D=5$ in RS-native units where $Jcost 1 = 0$ at equilibrium and $Jcost r > 0$ for $r > 0$, $r neq 1$.
proof idea
The declaration is an inductive type definition introducing five named constructors. Finite type structure, decidable equality, and representation are obtained by the deriving clause; no separate proof term is supplied.
why it matters
The definition supplies the enumeration required by the downstream BaryogenesisCert structure, which records that the cardinality equals five together with the equilibrium and asymmetry properties of Jcost. It directly encodes the module statement that five mechanisms realize configDim $D=5$. The sibling theorem baryogenesisMechanismCount then discharges the cardinality claim by the decide tactic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.