enhancement_unbounded
plain-language theorem explainer
For any real M there exists nonzero real t such that the enhancement S(t) exceeds M. Researchers closing the gap between geometric mass residues and perturbative running in Recognition Science cite the result to guarantee that J-cost corrections can accommodate arbitrarily large ratios. The proof splits on whether M is at most 1, then for M greater than 1 constructs t linear in the square root of M and applies the double-angle identity for cosh together with the strict quadratic lower bound on cosh(x) minus one.
Claim. For every real number $M$ there exists a nonzero real number $t$ such that $M < S(t)$, where the enhancement function is given by $S(t) = 2(cosh(t) - 1)/t^2$ for $t ≠ 0$.
background
The module resolves the discrepancy between geometric residues F(Z) on the phi-ladder and small perturbative factors f_RG by introducing a non-perturbative enhancement derived from J-cost. In logarithmic coordinates the exact J(e^t) equals cosh(t) minus 1; its quadratic term t²/2 recovers the perturbative limit, so the universal ratio is S(t) = 2(cosh(t) - 1)/t². This S depends on no free parameters and is forced by the Recognition Composition Law whose unique solution is the hyperbolic cosine (T5 J-uniqueness).
proof idea
The tactic proof proceeds by cases on M ≤ 1. The case M ≤ 1 is discharged by the witness t = 1 together with the already-proved strict inequality S(1) > 1. For M > 1 one defines t := 4√M + 2, clears the positive denominator t²/2, sets c = cosh(t/2) and d = c - 1, invokes the double-angle identity cosh(t) = 2c² - 1, expands cosh(t) - 1 = 2d² + 4d, and applies the lower bound d > (t/2)²/2 together with 16M < t² to obtain the required comparison via nlinarith.
why it matters
The theorem supplies the unboundedness property required by the ILG asymptotic enhancement certificates. It is invoked by ILGAsymptoticEnhancementCert and ilgAsymptoticEnhancementCert_holds to guarantee that the radial weight w_radial can be made arbitrarily large, thereby ensuring the ILG velocity always dominates the Newtonian value at large radii. Within the Recognition framework it realises the claim that S(t) grows exponentially for large |t| and accounts for the O(10²–10³) ratios between geometric residues (F ≈ 5–14 for electrons and quarks) and perturbative running, all without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.