sphaleron_rate_cert
plain-language theorem explainer
Packages the RS sphaleron-rate package into a single certificate: κ_sph equals 3/4 from Q₃ Hamiltonian-cycle combinatorics, both κ_sph and α_W are positive, and the dimensionless rate Γ_sph/T⁴ equals κ_sph α_W⁵ and is positive. Cosmologists citing the electroweak baryon-violation rate in Recognition Science would use this. The proof is a pure structure inhabitant that wires five already-proved field lemmas and reflexivity for the formula.
Claim. There exists a sphaleron-rate certificate asserting: the dimensionless prefactor satisfies $\kappa_{\mathrm{sph}} = 3/4$; $0 < \kappa_{\mathrm{sph}}$; $0 < \alpha_W$; the dimensionless rate $\Gamma_{\mathrm{sph}}/T^4$ is positive; and $\Gamma_{\mathrm{sph}}/T^4 = \kappa_{\mathrm{sph}}\,\alpha_W^5$.
background
Sphalerons are nonperturbative SU(2) gauge configurations that violate baryon number. Above the electroweak phase transition the rate per unit volume is written $\Gamma_{\mathrm{sph}}/T^4 = \kappa_{\mathrm{sph}}\cdot\alpha_W^5$, with $\alpha_W$ the weak coupling and $\kappa_{\mathrm{sph}}$ a dimensionless $O(1)$ prefactor.
In Recognition Science, $\kappa_{\mathrm{sph}}$ is fixed by $Q_3$ topology: a sphaleron path changes all three winding numbers at once. The even sign-flip subgroup $(\mathbb{Z}/2\mathbb{Z})^2$ has four elements; the complete graph $K_4$ on those vertices has three Hamiltonian cycles, each of length four. The combinatorial ratio is $3\times 4/4^2 = 3/4$. Lattice estimates place $\kappa_{\mathrm{sph}}$ in roughly $0.1$–$1.0$; the RS value $0.75$ sits inside that band.
The certificate structure records five claims: equality $\kappa_{\mathrm{sph}}=3/4$, positivity of $\kappa_{\mathrm{sph}}$ and of $\alpha_W$, positivity of the dimensionless rate, and the exact product formula. Upstream, $\alpha_W$ positivity comes from WeakCoupling ($\alpha$ and $\sin^2\theta_W$ both positive); the rate positivity multiplies $\kappa_{\mathrm{sph}}>0$ by $\alpha_W^5>0$.
proof idea
Term-mode structure inhabitant. Each field is filled by a named upstream lemma: kappa_from_Q3 by kappa_sph_eq (unfold the cycle/edge/sign-flip counts and norm_num to $3/4$); kappa_positive by kappa_sph_pos (rewrite to $3/4$ and compare); alpha_W_positive by alpha_W_pos from WeakCoupling; rate_positive by sphaleron_rate_pos (product of two positive factors); rate_formula by rfl against the definition of the dimensionless rate. No new arithmetic is performed here.
why it matters
Closes the module's main provenance bundle for the electroweak sphaleron rate under RS first principles. The combinatorial half is structural ($Q_3$ Hamiltonian cycles on the even sign-flip subgroup), while $\alpha_W$ still carries the RS construction value of $\alpha$ as a boundary datum rather than a fully derived constant. That honesty is explicit in the certificate doc-comment.
No downstream dependents are recorded yet; the certificate is the export surface for cosmology consumers that need a single object asserting formula, positivity, and the $3/4$ prefactor together. It sits beside the weak-coupling development and the cube/gauge foundation imports, and is consistent with the eight-tick / $D=3$ forcing chain only insofar as $Q_3$ topology is the ambient discrete geometry. Status in-module: zero sorry, zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.