nEqBL
plain-language theorem explainer
Equilibrium B−L number density is the product of thermal susceptibility and the B−L chemical potential induced by a rolling scalar. Cosmologists working the RS baryogenesis staging lane cite it as the linear-response bridge from (c_χ, T, K_x, χ̇) to n_{B−L}^{eq}. The body is a one-line product of two local abbreviations.
Claim. Define the equilibrium $B-L$ number density by $n_{B-L}^{\mathrm{eq}}(c_\chi,T,K_x,\dot\chi) := \chi(c_\chi,T)\,\mu_{B-L}(K_x,\dot\chi)$, where the susceptibility is $\chi(c_\chi,T)=c_\chi T^2$ and the chemical potential is $\mu_{B-L}(K_x,\dot\chi)=K_x\dot\chi$.
background
This module stages honest theorem targets for the RS baryogenesis derivation. The governing invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ with sphaleron equilibration forces vanishing relic baryon number.
Two local abbreviations feed the definition. Susceptibility is the standard thermal linear-response factor $\chi=c_\chi T^2$. The $B-L$ chemical potential is the product $\mu_{B-L}=K_x\dot\chi$ of a coupling $K_x$ and the rolling background velocity $\dot\chi$. Their product is the equilibrium charge density that sources later washout and freeze-out gates.
The parameters are ordinary reals; temperature $T$ here is a real scalar, not the exp/log RS field or the Freudenthal strip index that share the same short name elsewhere in the monolith.
proof idea
Pure definitional abbreviation: unfold to the product of susceptibility and $\mu_{B-L}$. No lemmas, tactics, or hypotheses. Downstream proofs (e.g. source-off and orientation-oddness) simply unfold this name together with muBL and susceptibility, then finish by ring.
why it matters
Gives the linear-response density that sourceBL multiplies by a rate $\Gamma$ to obtain the $B-L$ source term. That source is the object whose vanishing when $\dot\chi=0$ is the gate theorem sourceBL_zero_of_chiDot_zero, and whose oddness under $\dot\chi\mapsto -\dot\chi$ is a3SourceBL_odd.
In the staging loop this keeps the baryogenesis lane from inventing a nonzero $B-L$ by hand: every source must factor through this equilibrium density. It sits upstream of the sphaleron reprocessing and freeze-out window siblings that enforce the module's core obstruction (zero sourced $B-L$ implies zero final $B$). No forcing-chain landmark (T5–T8) is invoked here; the link is cosmological staging only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.