leptonReprocessingFactor
plain-language theorem explainer
Defines the lepton-axis sphaleron equilibrium coefficient at three generations: residual lepton charge equals (−51/79) times the conserved B−L. Cosmologists and SM electroweak specialists cite it as the L partner of the baryon factor 28/79. The body is a bare rational literal; the nontrivial content is the forced identity (28/79)−(−51/79)=1 used by every B−L conservation lemma in the staging module.
Claim. The lepton reprocessing factor is the rational constant $-51/79$. At electroweak sphaleron equilibrium with $N_g=3$, the residual lepton charge satisfies $L=(-51/79)\,(B-L)$. Together with the baryon factor $28/79$ it encodes $B-L$ conservation via $(28/79)-(-51/79)=1$.
background
This module stages honest theorem targets for the Recognition Science baryogenesis loop. The governing invariant is the sphaleron zero-protection obstruction: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ forces vanishing final baryon number once sphalerons equilibrate.
In the Standard Model with three generations, chemical-potential equilibrium under rapid $B+L$ violation redistributes any preexisting $B-L$ into fixed fractions of $B$ and $L$. The baryon share is the classical $28/79$; the lepton share is forced by conservation to be the complementary $-51/79$. The sibling constant sphaleronReprocessingFactor holds $28/79$; this definition holds the lepton partner.
Upstream, obstruction_Bfinal already records that $(28/79)\cdot(B-L)=0$ if and only if $B-L=0$. The present constant supplies the missing cross-axis arithmetic so that $B$ and $L$ coefficients differ by exactly one.
proof idea
Pure definition: the rational literal $-51/79$ is assigned with no proof obligations. Downstream lemmas such as leptonReprocessingFactor_value and reprocessing_conserves_BminusL recover the same value from $B-L$ conservation plus the banked baryon factor $28/79$, confirming the literal is not an independent postulate.
why it matters
Without this constant the staging file cannot state the equilibrium map $(B,L)\mapsto\bigl((28/79)(B-L),,(-51/79)(B-L)\bigr)$. It is consumed by reprocessing_conserves_BminusL (the cross-axis identity $(28/79)-(-51/79)=1$), by output_BminusL_eq_input (fixed-point reproduction of the input $B-L$), and by fixed_point_zero_iff (no number of sphaleron passes manufactures baryon number from vanishing $B-L$).
It also feeds the sign and magnitude comparisons leptonReprocessingFactor_neg and lepton_exceeds_baryon_reprocessing, which close the loophole that all residual charge might end up baryonic. In the broader RS cosmology lane this is bookkeeping for Sakharov-from-ledger staging, not a derivation of the $28/79$ fraction itself from the forcing chain (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.