enhancement_at_zero
The theorem establishes that the cosh enhancement factor equals exactly 1 at argument zero, recovering the perturbative limit of the coupling law. Researchers bridging geometric Recognition Science mass formulas to Standard Model renormalization-group running would cite this when populating the CouplingLawCert structure. The proof is a one-line simplification that invokes the definition of coshEnhancement at t = 0.
claimLet $S(t) := 2( (e^t + e^{-t})/2 - 1 ) / t^2$ for $t ≠ 0$, with $S(0) := 1$. Then $S(0) = 1$.
background
The module supplies the universal ratio between exact J-cost running and its quadratic perturbative approximation. J-cost is defined via the Recognition Composition Law as J(e^t) = cosh(t) − 1, so the perturbative piece is the leading term t²/2. The enhancement is therefore S(t) = 2(cosh(t) − 1)/t² for t ≠ 0 and S(0) = 1 by continuity. The local setting is the geometric-to-perturbative bridge required by the mass formula residue gap(Z). Upstream, the definition of coshEnhancement states: “The perturbative (quadratic) cost: t²/2.”
proof idea
The proof is a one-line wrapper that applies the definition of coshEnhancement and reduces the t = 0 case by the if-then clause.
why it matters in Recognition Science
This supplies the perturbative_limit field inside the CouplingLawCert structure (see downstream coupling_law_cert). It confirms the first of the four key properties listed in the module documentation: S(0) = 1 recovers the perturbative limit exactly. The result is forced by the J-cost construction that originates in the Recognition Composition Law and the eight-tick octave; it closes the weak-coupling anchor of the universal coupling law without introducing free parameters.
scope and limits
- Does not derive the functional form of S(t) from the Recognition Composition Law.
- Does not evaluate S(t) for any nonzero t or connect to specific Z values.
- Does not address convergence of the phi-ladder mass formula.
- Does not constrain the alpha band or spatial dimension D = 3.
formal statement (Lean)
148theorem enhancement_at_zero : coshEnhancement 0 = 1 := by
proof body
Term-mode proof.
149 simp [coshEnhancement]
150
151/-- Enhancement is symmetric: S(−t) = S(t). -/