baryogenesis_possible
plain-language theorem explainer
Under an explicit first-order electroweak-transition hypothesis, the RS ledger supplies the two structural Sakharov ingredients: baryon change per sphaleron equals 3, and the CP asymmetry parameter is nonzero. Cosmologists auditing baryogenesis in Recognition Science cite this as the conditional package. The proof is a three-field constructor: definitional equality, the upstream nonzero-Jarlskog theorem, and the hypothesis itself.
Claim. Assuming the electroweak phase transition is first-order, one has $\Delta B$ per sphaleron equal to $3$, the CP asymmetry parameter nonzero, and the first-order hypothesis retained. Equivalently: $\Delta B_{\mathrm{sph}}=3\land\varepsilon_{\mathrm{CP}}\neq 0\land$ (EW first-order).
background
Sakharov's three conditions for baryogenesis are baryon-number violation, C/CP violation, and departure from thermal equilibrium. This module treats the first two as ledger structure and carries the third as an underived hypothesis: whether the electroweak transition is first-order remains open thermal-field-theory (minimal SM with $m_H\approx 125,\mathrm{GeV}$ is a crossover).
On the $Z^3$ ledger, baryon number is interpreted as a winding charge. Sphaleron-like events are collective 8-tick multi-axis rotations; the change per event is defined as $\Delta B=\mathrm{face_pairs}(3)$, which equals the generation count forced by $D=3$. The CP asymmetry parameter is identified with the structural Jarlskog invariant from the chiral Gray-code Berry phase, already proved positive upstream.
The module doc explicitly retracts an earlier claim that all three Sakharov conditions were derived with zero imported physics; the out-of-equilibrium slot had been a True placeholder.
proof idea
Term-mode triple constructor. First component is rfl: by definition $\Delta B$ per sphaleron is face_pairs 3, which equals 3. Second component is the sibling theorem cp_asymmetry_nonzero, itself ne_of_gt jarlskog_positive on the structural Jarlskog value used as the CP asymmetry parameter. Third component reinserts the input hypothesis that the electroweak transition is first-order. No further rewriting or case analysis.
why it matters
This is the terminal packaging theorem of SakharovFromLedger: it states what RS actually delivers for baryogenesis once the out-of-equilibrium gap is named. It sits on the three-generation count forced by $D=3$ (forcing chain T8) and on the nonzero Jarlskog invariant from Gray-code chirality and the CKM phase derivation. No downstream consumers are wired yet; the declaration is the module's public conditional claim.
The doc-comment and module header both flag the scientific correction: two structural facts are unconditional, the third is hypothesis-only. Baryon number as ledger winding remains an interpretation (audit FQ4), not a derived chiral anomaly. The result therefore marks an honest boundary rather than a full derivation of the observed baryon asymmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.