enhancement_ge_one
plain-language theorem explainer
The declaration establishes that the enhancement factor S(t) satisfies S(t) ≥ 1 for every real t. Researchers modeling the geometric-perturbative bridge in Recognition Science would cite this bound to confirm that exact J-cost running never falls below its quadratic approximation. The proof proceeds by case analysis at t = 0 followed by an algebraic reduction that invokes the elementary inequality cosh x ≥ 1 + x²/2.
Claim. For every real number $t$, $1 ≤ S(t)$, where the enhancement factor is given by $S(0) := 1$ and $S(t) := 2(∅cosh t - 1)/t²$ for $t ≠ 0$.
background
Recognition Science obtains the exact J-cost from the Recognition Composition Law, giving J(e^t) = cosh(t) - 1. The perturbative approximation retains only the leading quadratic term t²/2. The module defines the universal ratio S(t) = 2(cosh(t) - 1)/t² that measures the enhancement of exact geometric running over the perturbative one; at t = 0 the value is defined to be 1.
proof idea
The tactic proof splits on whether t equals zero. When t = 0, simplification with the definition of coshEnhancement immediately yields equality to 1. When t ≠ 0, the target is rewritten via multiplication by the positive quantity t² and nlinarith closes the goal by direct appeal to the lemma cosh_ge_one_plus_half_sq.
why it matters
This result supplies the first listed property of the coupling law in the module documentation: geometric J-cost always dominates its perturbative approximation. It thereby supplies the lower bound required to explain the O(10²–10³) ratios between the geometric residue F(Z) and the small perturbative f_RG that appear in the mass formula. The theorem is a direct algebraic consequence of the Recognition Composition Law forcing J = cosh − 1 and sits inside the Unification.CouplingLaw module that bridges the phi-ladder geometry to Standard-Model renormalization-group flow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.