coupling_identity
plain-language theorem explainer
The coupling identity equates the exact J-cost to the product of the cosh enhancement factor and the perturbative quadratic cost for any nonzero real t. Researchers bridging geometric mass ladders to Standard Model running would cite it to explain large recognition residues without free parameters. The term-mode proof reduces the equality by unfolding definitions and applying field simplification after ruling out division by zero.
Claim. For all real numbers $t ≠ 0$, the exact J-cost equals the cosh-enhancement factor times the perturbative quadratic cost: $J(e^t) = S(t) · (t²/2)$, where the enhancement factor is $S(t) = 2(cosh(t) - 1)/t²$.
background
The Unification.CouplingLaw module bridges the geometric φ-ladder side of Recognition Science to the perturbative renormalization-group side of the Standard Model. The J-cost in log coordinates is given by J(e^t) = cosh(t) - 1, whose Taylor series begins with the quadratic term t²/2 that defines the perturbative approximation. The exact cost is recovered by multiplying the perturbative piece by the enhancement S(t) = 2(cosh(t) - 1)/t², which is forced by the Recognition Composition Law with no free parameters.
proof idea
The proof unfolds the definitions of exactCost, J_log, coshEnhancement and perturbativeCost with simp, establishes t² ≠ 0 from the hypothesis t ≠ 0, and finishes with field_simp to equate the two sides algebraically.
why it matters
This theorem provides the enhancement_universal field required by the coupling_law_cert theorem that certifies the complete coupling law. It fills the central gap in the unification program by showing how geometric dominance arises automatically from the J-cost convexity. The result realizes the T5 J-uniqueness landmark and explains the O(10²–10³) enhancement ratios observed between geometric residues and perturbative running without introducing new constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.