derivation_chain_complete
plain-language theorem explainer
The sign chain for baryon asymmetry is fully assembled: three generations from D=3, Gray-code chirality, positive structural Jarlskog CP violation, baryon violation ΔB=3 per sphaleron, and strictly positive structural η_B. Cosmologists citing the RS derivation that matter dominates antimatter point here. The proof is a five-conjunct term packing two reflexivities with named chirality and positivity lemmas. Magnitude is deliberately excluded.
Claim. The following hold simultaneously: the number of face pairs in dimension $3$ equals $3$ (three fermion generations); the Gray-code flip-count vector is chiral; the structural Jarlskog invariant satisfies $J_{\mathrm{CP}}>0$; each sphaleron changes baryon number by $\Delta B=3$; and the structural baryon-to-photon ratio satisfies $\eta_B^{\mathrm{struct}}>0$.
background
This module separates three layers of the baryon-to-photon story. The theorem layer is the sign: $\eta_B>0$ (matter over antimatter) from $J_{\mathrm{CP}}>0$ plus Sakharov conditions. The scaffold $\eta_B^{\mathrm{struct}}:=J_{\mathrm{CP}}/g_\star$ is textbook proportionality only; numerically $\sim 3\times 10^{-7}$, about $500\times$ the observed $6.1\times 10^{-10}$, because washout dynamics are open. A separate hypothesis layer matches the Planck band via a $\varphi$-rung formula and is not claimed here.
Upstream pieces feed the five conjuncts. Face-pair count in $D=3$ forces three generations and sets $\Delta B$ per sphaleron equal to that count. Gray-code chirality (cycle_is_chiral on the path $[0,1,3,2,6,7,5,4]$) supplies the oriented flip asymmetry. Structural Jarlskog positivity comes from Berry-phase/torsion overlap in the CKM-from-cube development. Structural $\eta_B$ is the quotient of that Jarlskog by $g_\star$ (relativistic DOF at the electroweak scale); its positivity is eta_B_positive via div_pos on $J_{\mathrm{CP}}>0$ and $g_\star>0$.
proof idea
Term-mode five-tuple. The first conjunct face_pairs 3 = 3 is rfl (definitional). Chirality is the imported lemma cycle_is_chiral on grayFlipCounts. Jarlskog positivity is the existing theorem jarlskog_positive. The sphaleron $\Delta B$ conjunct is again rfl, since deltaB_per_sphaleron is defined as face_pairs 3. The final conjunct applies eta_B_positive, which unfolds the structural quotient and uses div_pos on Jarlskog positivity and a numeric positivity proof for $g_\star$. No new arithmetic is performed; the declaration only packages the chain.
why it matters
This is the module's completeness stamp for the SIGN half of baryogenesis: every RS-derived Sakharov ingredient needed for $\eta_B^{\mathrm{struct}}>0$ is discharged in one place. Downstream, baryonAsymmetryCert consumes the positivity facts (and Sakharov-from-ledger under the named out-of-equilibrium hypothesis) to build the certificate structure; the doc there states the certificate exists only conditionally on that EW first-order hypothesis.
Framework landmarks: three generations track T8 ($D=3$ spatial dimensions) via face pairs; chirality is the Gray-code eight-tick path (T7 octave structure); CP violation is the structural Jarlskog from cube geometry. The doc-comment is explicit that the $-44$ rung magnitude match and the washout-suppressed numerical value are NOT in this chain. Open physics remains the order-parameter dynamics through the electroweak transition (Boltzmann transport, washout constant), which is why the scaffold overshoots observation by $\sim 500\times$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.