coupling_law_cert
plain-language theorem explainer
The coupling law certificate establishes that exact J-cost running equals the cosh enhancement factor times its perturbative quadratic approximation for all real t. Researchers reconciling geometric mass residues on the φ-ladder with Standard Model renormalization group flows would cite it. The proof is a direct structure construction that assigns the four certificate fields from sibling identities already proved in the same module.
Claim. The coupling law certificate holds: for all real $t ≠ 0$, exactCost$(t) = $coshEnhancement$(t) ·$ perturbativeCost$(t)$, with coshEnhancement$(0) = 1$, coshEnhancement$(-t) =$ coshEnhancement$(t)$, and coshEnhancement$(t) > 1$ for $t ≠ 0$.
background
In the Unification.CouplingLaw module the coupling law supplies the universal ratio between geometric (φ-ladder) and perturbative (SM RG) descriptions of running. The J-cost is defined by J(e^t) = cosh(t) − 1, the unique solution of the Recognition Composition Law that is convex and minimized at t = 0. The perturbative approximation retains only the t²/2 term, so the enhancement S(t) = 2(cosh(t) − 1)/t² measures the non-perturbative correction forced by the functional equation.
proof idea
The proof constructs the CouplingLawCert structure by direct field assignment. It maps enhancement_universal to the coupling_identity lemma, perturbative_limit to enhancement_at_zero, enhancement_symmetric to the symmetry lemma of the same name, and geometric_dominance to enhancement_gt_one. No further tactics are required once these four sibling results are available.
why it matters
This theorem certifies the third bridge object in the Recognition Science unification program, the ratio function S(t) determined solely by J-cost. It explains why geometric gap(Z) exceeds perturbative f_RG by factors of 10²–10³ for leptons while recovering the SM limit at weak coupling, and it rests on the T5 J-uniqueness and RCL landmarks. The module’s physical-interpretation section states that the law resolves the “Missing Something” without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.