SakharovConditions
plain-language theorem explainer
Packages the three Sakharov conditions for baryogenesis as a structure parameterized by an underived out-of-equilibrium proposition. Baryon violation is the identity ΔB = 3 per sphaleron-like event; CP violation is nonzero Jarlskog structural asymmetry. Cosmologists citing the RS ledger route to matter asymmetry use this as the typed interface. It is a pure structure definition, not a proved theorem.
Claim. A record of the three Sakharov conditions relative to a named proposition $P$ (``electroweak first-order / out of equilibrium''): (i) baryon change per sphaleron-like event equals $3$; (ii) the CP asymmetry parameter (structural Jarlskog invariant) is nonzero; (iii) $P$ holds. $P$ is an abstract hypothesis, not derived in the repository.
background
Sakharov (1967) listed three necessary conditions for a dynamical baryon asymmetry: baryon-number violation, C and CP violation, and departure from thermal equilibrium. This module treats the first two as structural ledger facts and carries the third as an explicit parameter.
Baryon number is interpreted as a winding charge on the $Z^3$ ledger. Sphaleron-like processes are collective 8-tick multi-axis rotations; the per-event change is deltaB_per_sphaleron, defined as face_pairs 3 and equal to the generation count $N_{\mathrm{gen}}=3$ forced by $D=3$. The CP side uses cp_asymmetry_parameter, defined to be the structural Jarlskog invariant from the chiral Gray-code Berry phase (nonzero by a sibling lemma).
The out-of-equilibrium slot is an arbitrary proposition EWFirstOrder. The module doc states plainly that whether the electroweak transition is first order is open thermal-field-theory territory; in the minimal SM with $m_H\approx 125,\mathrm{GeV}$ it is a crossover, and no RS derivation exists.
proof idea
No proof body: this is a structure definition. The three fields are propositions that a later constructor must supply. Downstream, sakharov_from_RS fills them by reflexivity on ΔB = 3, the lemma cp_asymmetry_nonzero for the Jarlskog slot, and the caller's hypothesis for out-of-equilibrium.
why it matters
This is the typed Sakharov package that every RS baryogenesis claim is forced to mention. BaryonAsymmetryCert requires a field sakharov : SakharovConditions EWFirstOrder, so the underived equilibrium hypothesis propagates into the full asymmetry certificate rather than being silently assumed. The companion constructor sakharov_from_RS is explicit bookkeeping of two proved pieces plus one named hypothesis, not a derivation of baryogenesis.
Framework landmarks in play: three generations from $D=3$ (forcing chain T8) fix ΔB = 3 per event; CP comes from the Gray-code chirality / Jarlskog path already proved elsewhere. The honest gap is condition 3. An earlier revision treated out-of-equilibrium as True; the present parameterization corrects that audit failure and keeps baryon-as-winding-charge flagged as interpretation (audit FQ4), not a derived anomaly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.