SakharovCondition
plain-language theorem explainer
SakharovCondition enumerates the three requirements for baryogenesis within the Recognition Science derivation of the baryon-to-photon ratio. Cosmologists modeling matter-antimatter asymmetry from the eight-tick phase structure would cite this enumeration when stating the prerequisites for nonzero η. The declaration is a direct inductive type whose three constructors match the 1967 conditions exactly.
Claim. Baryogenesis requires baryon-number violation, combined C and CP violation, and departure from thermal equilibrium.
background
The Cosmology.MatterAntimatter module targets derivation of η ≈ 6.1 × 10^{-10} from Recognition Science's φ-structure. Its core insight states that the eight-tick phase structure supplies intrinsic asymmetry, CP violation arises from the ledger, and the resulting ε_CP sets the observed matter abundance. The module imports Constants and Mathlib; no upstream lemmas are required for this declaration.
proof idea
The declaration is an inductive type definition whose three constructors are B_violation, C_CP_violation, and out_of_equilibrium. No tactics or lemmas are applied; the type directly encodes the three conditions listed in the module documentation.
why it matters
This enumeration is consumed by allConditionsNeeded to assert that all three conditions must hold. It supplies the classic Sakharov prerequisites for the paper proposition on baryogenesis from Recognition Science, connecting directly to the eight-tick octave and ledger-induced CP violation. It leaves open the precise extraction of ε_CP ~ 10^{-10} from the φ-phases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.