coshEnhancement
plain-language theorem explainer
coshEnhancement defines the universal ratio S(t) between exact J-cost running and its quadratic perturbative approximation in log coordinates. Unification researchers bridging φ-ladder geometric residues to Standard Model running would cite this when quantifying the non-perturbative boost forced by the recognition composition law. The definition is a direct piecewise construction that returns 1 at t = 0 and otherwise evaluates 2(cosh t − 1)/t².
Claim. The cosh enhancement factor is the function $S:ℝ→ℝ$ defined by $S(t)=1$ when $t=0$ and $S(t)=2(ℝ.cosh t−1)/t²$ otherwise. This supplies the exact-to-perturbative ratio of J-cost for any recognition event.
background
The Unification.CouplingLaw module resolves the mismatch between large geometric residues F(Z) on the φ-ladder and small perturbative residues f_RG from renormalization-group running. J-cost is the cost function induced by a multiplicative recognizer (derivedCost of its comparator) and equivalently the J-cost of any recognition event. In log coordinates the exact J-cost is cosh(t)−1 while the perturbative approximation is the quadratic term t²/2; their ratio is forced by the recognition composition law and the uniqueness of J.
proof idea
This is a direct definition with a single conditional: the zero case returns the constant 1 and the nonzero case normalizes the difference cosh t − 1 by t²/2. No upstream lemmas are invoked; the expression is the primitive object that later theorems apply to exactCost and perturbativeCost.
why it matters
This definition is the central object for the coupling-law package. It is invoked by coupling_identity to obtain exactCost t = coshEnhancement t ⋅ perturbativeCost t, by CouplingLawCert to certify the full geometric–perturbative bridge, and by coupling_law_determines_strength to conclude that recognition strength equals coshEnhancement evaluated at the perturbative residue. The construction thereby shows that the O(10²–10³) ratios observed in mass ladders are determined solely by the Taylor structure of cosh, which follows from RCL and the forcing chain to J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.