enhancement_gt_one
plain-language theorem explainer
enhancement_gt_one proves that the cosh enhancement factor S(t) exceeds 1 for every nonzero real t. Researchers bridging geometric phi-ladder masses with perturbative renormalization cite it to guarantee that exact J-cost running always dominates its quadratic approximation. The term-mode proof unfolds the definition, rewrites the target inequality via positivity, and closes with nlinarith on the companion strict inequality cosh(t) - 1 > t²/2.
Claim. For every real number $t ≠ 0$, the enhancement factor $S(t) = 2(∀cosh(t) - 1)/t²$ satisfies $S(t) > 1$.
background
The module resolves the gap between large geometric residues F(Z) in the phi-ladder mass formula and small perturbative residues f_RG from Standard Model running. In log coordinates the exact J-cost is cosh(t) - 1 while the perturbative cost is the quadratic t²/2; the universal ratio is the enhancement S(t) = 2(cosh(t) - 1)/t² for t ≠ 0 (defined as 1 at t = 0). This S(t) equals the ratio of exact to perturbative J-cost and is forced solely by the Recognition Composition Law through J = cosh - 1.
proof idea
The term-mode proof first applies simp to unfold coshEnhancement under the hypothesis t ≠ 0, selecting the non-zero branch. It rewrites the goal 1 < 2(cosh t - 1)/t² into the equivalent form t²/2 < cosh t - 1 by clearing the positive denominator via lt_div_iff. The goal is then closed by nlinarith applied directly to the upstream lemma cosh_gt_one_plus_half_sq.
why it matters
This theorem supplies the geometric_dominance field inside the coupling_law_cert certificate that certifies the coupling law is inhabited. It thereby supports the claim that geometric residues always exceed perturbative ones, explaining the observed O(10²–10³) ratios for electrons and quarks. The result feeds both the structural_dominance theorem for fermions and the enhancement_unbounded theorem; it is forced by the J-uniqueness step of the forcing chain and the identification of J-cost with cosh - 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.