Ntarget
plain-language theorem explainer
Defines the directive target exponent as 44 minus the proven prefactor rung rP. Cosmology and baryogenesis workers cite it when converting a fixed prefactor rung into the f_chi scale that would place η_B on the −44 rung. The body is a one-line integer subtraction; observed η_B and −44 never enter the definition.
Claim. For an integer prefactor rung $r_P$, the target exponent is $N_{\mathrm{target}}(r_P) := 44 - r_P$. Neither the observed baryon asymmetry $\eta_B$ nor the value $-44$ appears in this definition; it is computed forward from $r_P$ alone.
background
This module stages honest theorem targets for the Steve baryogenesis derivation. The governing invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so vanishing sourced $B-L$ with equilibrated sphalerons forces surviving baryon number to zero.
In the RS mass and charge ladder, quantities sit on integer rungs of a $\varphi$-scaled tower. Here $r_P$ is the proven prefactor rung carried by the dynamics (sphaleron rate and susceptibility). The constant 44 is the arithmetic offset that links that prefactor rung to the observational $\eta_B$ rung at $-44$, without fitting to the observation inside the definition itself.
Sibling staging objects include the sphaleron reprocessing factor, freeze-out window, $\mu_{B-L}$, and equilibrium $B-L$ density. This definition only packages the forward map from $r_P$ to the $f_\chi$ target exponent.
proof idea
Pure definitional abbreviation: $N_{\mathrm{target}}(r_P)$ is the integer $44 - r_P$. No lemmas, tactics, or hypotheses. Downstream equalities discharge by unfolding this definition and applying integer arithmetic (omega).
why it matters
Closes the forward-computation half of the B8 conditional biconditional: $f_\chi$ on rung $N$ places $\eta_B$ on the $-44$ rung if and only if $N = N_{\mathrm{target}}(r_P)$. The exponent is pinned by the proven prefactor rung, not back-solved from $-44$.
Feeds N_forced_from_provenP, which evaluates the map at the proven prefactor rung $r_P = 0$ and obtains $N = 44$. That stages the claim that $\eta_B$ on the $-44$ rung is equivalent to $f_\chi$ on rung 44, with dynamics carrying rung 0 and every target rung living on the open $f_\chi$ scale.
In the broader RS ladder picture (mass yardstick $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), this keeps baryogenesis staging honest: the observational $-44$ is a consequence of arithmetic from a proven prefactor, not an input fitted into the definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.