enhancement_symmetric
plain-language theorem explainer
The enhancement factor satisfies S(−t) = S(t) for every real t. Researchers assembling the coupling law certificate between geometric J-cost and perturbative running would cite this symmetry when confirming the four required properties. The proof is a one-line term-mode simplification that unfolds coshEnhancement and applies the evenness of cosh together with negation rules for zero and squares.
Claim. Let $S(t) := 2 (cosh t - 1)/t^2$ for $t ≠ 0$ and $S(0) := 1$. Then $S(-t) = S(t)$ for all real $t$.
background
The module resolves the gap between φ-ladder geometric masses and Standard Model perturbative running by introducing the universal enhancement S(t) forced by J-cost. J(e^t) is identified with cosh(t) − 1 via the Recognition Composition Law, so the exact-to-perturbative ratio is exactly S(t) = 2(cosh(t) − 1)/t² with no free parameters. The local setting is the four-property certificate that packages universality, the perturbative limit at t = 0, symmetry, and strict dominance over 1.
proof idea
The proof is a one-line term-mode simplification. It unfolds the definition of coshEnhancement, rewrites the negated argument using neg_eq_zero and neg_sq, and invokes Real.cosh_neg to obtain equality.
why it matters
This theorem supplies the symmetry axiom required by the CouplingLawCert structure, which certifies the full geometric-perturbative bridge. It is one of the four properties (alongside coupling_identity, enhancement_at_zero, and enhancement_gt_one) that close the universal coupling law. The result follows directly from the even character of cosh and the J = cosh − 1 identification in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.