FreezeOutWindow
plain-language theorem explainer
Packages the kinematic data of a baryogenesis freeze-out window: Hubble rate, washout rate, and a rolling background that is static outside a closed time interval. Freeze-out is the unique crossing where washout equals Hubble. Cosmologists citing staged B-L freeze-out or sphaleron washout would use it. Pure structure definition: field bundle plus positivity and ordering axioms, no derived content.
Claim. A freeze-out window is a 5-tuple of real functions and times $(H,\Gamma_{\mathrm{wash}},\dot\chi,t_0,t_f)$ such that $H(t)>0$ and $\Gamma_{\mathrm{wash}}(t)\ge 0$ for all $t$, $t_0\le t_f$, $\Gamma_{\mathrm{wash}}(t_f)=H(t_f)$, and $\dot\chi(t)=0$ whenever $t<t_0$ or $t>t_f$.
background
This module stages honest intermediate targets for a Recognition Science baryogenesis derivation. The governing invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ vanishes and sphalerons equilibrate, the final baryon number is zero. Sibling definitions in the file encode the reprocessing factor, washout exponent, and the obstruction that $B_{\mathrm{final}}=0$ whenever $B-L=0$.
In standard cosmology, freeze-out is the epoch when a process rate drops through the Hubble expansion rate $H(t)$. Here $\Gamma_{\mathrm{wash}}$ is that washout rate and the equality $\Gamma_{\mathrm{wash}}(t_f)=H(t_f)$ marks the close of the active window. The rolling background $\dot\chi$ (e.g. a CP-violating phase velocity) is required to vanish both before the window opens and after it closes, so charge production is confined to $[t_0,t_f]$.
The name $H$ collides with the RS cost reparametrization $H(x)=J(x)+1$, but in this structure $H$ is the cosmological Hubble function, not the cost functional.
proof idea
No proof: this is a structure definition. It bundles five data fields with six propositional fields that axiomatize positivity of Hubble, nonnegativity of washout, temporal ordering of the window, the freeze-out crossing identity, and staticity of the rolling background outside the window. Downstream theorems are expected to inhabit or quantify over this type rather than derive the fields from first principles here.
why it matters
Keeps the baryogenesis lane from smuggling an implicit freeze-out mechanism. By forcing any later relic-charge or washout calculation to name an explicit window (crossing time, static exterior), it makes the staging loop's missing physics visible rather than hidden in True placeholders. The module header states that loop-generated targets must not introduce new axioms or fake conditions; this structure is the kinematic interface those targets should consume.
No downstream users are wired yet (used_by empty). Natural parents are the sibling obstruction lemmas (Bfinal zero iff $B-L$ zero, washout exponent, relic charge) once they are upgraded from pure algebraic identities to time-dependent statements on a window. Framework contact is cosmological rather than T0–T8: it sits downstream of Sakharov-from-ledger and sphaleron-rate imports, not on the J-uniqueness or eight-tick chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.