CouplingLawCert
plain-language theorem explainer
The CouplingLawCert structure packages the universal factorization of exact J-cost into the cosh enhancement factor times the quadratic perturbative term, together with the limit, symmetry, and dominance properties of the enhancement. Researchers bridging the phi-ladder mass formula to Standard Model running would cite it to certify that the non-perturbative correction is parameter-free and forced by the Recognition Composition Law. The structure is populated directly by the four supporting identities on coshEnhancement and perturbativeCost.
Claim. Let $S(t) = 2(cosh t - 1)/t^2$ for $t ≠ 0$ and $S(0) = 1$. The certificate asserts that exact J-cost satisfies exactCost$(t) = S(t) · (t^2/2)$ for all $t ≠ 0$, together with $S(0) = 1$, $S(-t) = S(t)$, and $S(t) > 1$ for all $t ≠ 0$.
background
In the Unification.CouplingLaw module the J-cost is obtained from the Recognition Composition Law as J(x) = cosh(log x) - 1. The module resolves the gap between large geometric residues F(Z) on the phi-ladder and small perturbative f_RG from Standard Model running by introducing the non-perturbative enhancement S(t). The function coshEnhancement implements S(t) exactly as the ratio of full J-cost to its quadratic approximation t²/2, with the value 1 at t = 0.
proof idea
This is a structure definition that directly records the four properties. The universal factorization is supplied by the sibling coupling_identity, the limit at zero by enhancement_at_zero, symmetry by enhancement_symmetric, and strict dominance by enhancement_gt_one.
why it matters
The certificate completes the bridge asserted in the module documentation and is used by the downstream theorem coupling_law_cert to witness inhabitance. It realizes the claim that S(t) accounts for the O(10²–10³) ratios between geometric and perturbative contributions with no free parameters, as required by the J-cost forced from the Recognition Composition Law. It leaves open the explicit matching of individual particle Z values to their observed masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.