cosh_gt_one_plus_half_sq
plain-language theorem explainer
The strict inequality cosh(t) − 1 > t²/2 holds for every nonzero real t. Researchers deriving the universal coupling law cite this result to establish that the exact cost always exceeds its quadratic perturbative approximation. The argument reduces the claim via the double-angle identity for cosh, compares the resulting quadratic forms after setting d = cosh(t/2) − 1, and closes the gap with the non-strict sibling inequality plus positivity of the cost function away from zero.
Claim. For every real number $t ≠ 0$, $t^2/2 < cosh(t) - 1$.
background
The Unification.CouplingLaw module resolves the gap between geometric φ-ladder masses and perturbative renormalization-group running. In logarithmic coordinates the exact cost is cosh(t) − 1 while the perturbative approximation is the quadratic term t²/2; the enhancement factor is defined as twice their ratio. This factor equals 1 at t = 0 and grows for large |t|, accounting for the observed O(10²–10³) ratios between geometric residues F(Z) and perturbative coefficients f_RG.
proof idea
The proof invokes the double-angle identity cosh(t) − 1 = 2 sinh(t/2)² and rewrites the target as a comparison of 2(t/2)² against 2 sinh(t/2)². It sets d := cosh(t/2) − 1, applies the non-strict sibling inequality to obtain d ≥ (t/2)²/2, establishes d > 0 via the positivity theorem for the cost function at t/2, derives sinh²(t/2) = d² + 2d from the cosh identity, and discharges the quadratic comparison by nlinarith.
why it matters
This lemma is invoked directly by enhancement_gt_one and enhancement_unbounded in the same module. Those statements establish that the enhancement exceeds unity and is unbounded, thereby explaining the large geometric-to-perturbative ratios in the mass formula. The result therefore supplies one concrete step in the derivation of the universal coupling law forced by the Recognition Composition Law and the identification of the cost function with cosh(log x) − 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.