AsymmetryMechanism
plain-language theorem explainer
The type of asymmetry mechanisms enumerates the five standard baryogenesis processes recognized in Recognition Science cosmology. Researchers formalizing the observed matter-antimatter imbalance would cite this enumeration when fixing the number of viable mechanisms at five under the configDim D = 5 constraint. The definition proceeds by direct inductive listing of the five constructors followed by derivation of Fintype to support immediate cardinality results.
Claim. The type of asymmetry mechanisms is the inductive type whose five constructors are electroweak baryogenesis, leptogenesis, grand-unified-theory baryogenesis, the Affleck-Dine mechanism, and spontaneous CP violation.
background
The module treats the cosmological matter-antimatter asymmetry within Recognition Science. It identifies exactly five canonical generation mechanisms and equates their count to configDim D = 5. Recognition Science supplies the numerical prediction η_B = φ^{-44} ≈ 6 × 10^{-10} for the baryon-to-photon ratio.
proof idea
The declaration is the inductive definition that lists the five constructors and derives the type classes DecidableEq, Repr, BEq, and Fintype.
why it matters
This supplies the finite enumeration required by the downstream theorem that proves the cardinality equals five and by the certificate structure that records the same fact. It implements the configDim D = 5 slot in the RS cosmology framework, consistent with the forcing chain T0-T8 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.