baryogenesisMechanismCount
plain-language theorem explainer
The declaration establishes that exactly five baryogenesis mechanisms are admitted in the Recognition Science model. Cosmologists studying the early-universe matter asymmetry would cite the count when mapping Sakharov conditions onto J-cost imbalance. The proof is a one-line decision procedure that exhausts the finite inductive type.
Claim. The finite set of baryogenesis mechanisms has cardinality five: $ |{leptogenesis, electroweak, Affleck-Dine, cold, GUT}| = 5 $.
background
The module treats the observed baryon-to-photon ratio as a sigma-imbalance in the early universe. Sakharov conditions translate directly: baryon violation equals sigma-export above threshold, CP violation equals J(r) inequality for conjugate states, and departure from equilibrium equals positive J-cost. The inductive type BaryogenesisMechanism enumerates the five processes (leptogenesis, electroweak, Affleck-Dine, cold, GUT) and derives Fintype, DecidableEq, and Repr.
proof idea
The proof is a one-line wrapper that applies the decide tactic to Fintype.card. The tactic succeeds because the inductive definition of BaryogenesisMechanism supplies an explicit Fintype instance whose cardinality is five.
why it matters
The result supplies the mechanism count to baryogenesisCert, which packages the full asymmetry certificate. It realizes the module claim that five mechanisms equal configDim D = 5 and sits inside the Recognition Science forcing chain after J-uniqueness and the phi fixed point. No open scaffolding remains in the supplied material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.