deltaB_per_sphaleron
plain-language theorem explainer
Baryon-number change per sphaleron is fixed at three: the number of opposite-face pairs on the D=3 cube, identified with three fermion generations. Cosmologists working the RS Sakharov ledger cite this as the structural ΔB bookkeeping constant. The definition is a one-line alias of face_pairs at dimension three.
Claim. Define the baryon-number shift per sphaleron event by $\Delta B_{\mathrm{sph}} := N_{\mathrm{face\ pairs}}(3)$, where $N_{\mathrm{face\ pairs}}(D)=D$ is the number of opposite-face pairs of a $D$-cube. Thus $\Delta B_{\mathrm{sph}}=3$, matching three generations forced by $D=3$.
background
The module reconstructs Sakharov's three conditions for baryogenesis from the RS ledger. Condition 1 (B violation) is treated as a winding-charge bookkeeping identity on the $Z^3$ ledger: sphaleron-like events are collective 8-tick multi-axis phase rotations that shift all three winding numbers at once. Baryon number itself is interpreted as a ledger winding charge, not a derived chiral anomaly (audit FQ4).
Upstream, face_pairs D is simply $D$: a $D$-cube has $D$ pairs of opposite faces. In ParticleGenerations this count is identified with the number of fermion generations, and the forcing chain already gives $D=3$ (T8). The present definition therefore pins $\Delta B$ per sphaleron to that generation count.
Sibling bookkeeping sets $\Delta L$ equal to the same constant, so $B-L$ is preserved; CP violation is handled separately via the Jarlskog invariant from the chiral Gray-code Berry phase.
proof idea
Pure definitional abbreviation: unfold to face_pairs 3, and face_pairs D := D, so the value is definitionally $3$. No tactics or lemmas beyond that reduction. Downstream equalities such as sphaleron_changes_B_by_3 are then rfl.
why it matters
This constant is the structural content of Sakharov condition 1 in the ledger story. It appears as the field b_violation : deltaB_per_sphaleron = 3 inside SakharovConditions, and as a conjunct in baryogenesis_possible and in derivation_chain_complete ("3 generations → from D = 3 (face_pairs)"). The baryon-asymmetry certificate BaryonAsymmetryCert packages those Sakharov data with a positive structural $\eta_B$.
Framework landmark: T8 forces $D=3$, hence three face-pairs and three generations, hence $\Delta B=3$ per sphaleron. The module is explicit that the out-of-equilibrium condition remains an undervived hypothesis (EWFirstOrder), and that the anomaly interpretation of B is imported SM bookkeeping rather than a pure ledger derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.