enhancement_near_one
plain-language theorem explainer
The result bounds the deviation of the enhancement factor S(t) from unity by at most t squared over 10 for real t with absolute value below 1 and nonzero. Weak-coupling analyses in Recognition Science unification would cite it to confirm the quadratic approximation holds near the origin. The argument rewrites the deviation via the definition of S, invokes the fourth-order cosh remainder bound, and closes with nlinarith.
Claim. Let $t$ be a real number with $|t| < 1$ and $t ≠ 0$. Then $|S(t) - 1| ≤ t²/10, where $S(t) := 2(ℝ.cosh t - 1)/t²$.
background
The module develops the universal coupling law bridging the geometric J-cost side of Recognition Science to perturbative renormalization-group running. In logarithmic coordinates the J-cost is J(e^t) = cosh(t) - 1; its quadratic Taylor term t²/2 recovers the perturbative limit. The enhancement factor is S(t) = 2(cosh(t) - 1)/t², which equals 1 at t = 0 and exceeds 1 for t ≠ 0, growing exponentially at large |t| to explain O(10²) recognition-strength ratios.
proof idea
The tactic proof unfolds the enhancement definition, records positivity of t², rewrites the target difference as an absolute quotient, and calls the cosh_quadratic_bound lemma. It isolates twice the Taylor remainder by a ring identity, bounds that remainder by nlinarith against the fourth-order estimate, then applies absolute-value rules for division and finishes with nlinarith after noting t² ≤ 1.
why it matters
This theorem anchors the weak-coupling limit inside the coupling-law family and supports the claim that perturbative physics is an excellent approximation at small t. It rests on J-uniqueness (T5) that forces J(x) = cosh(log x) - 1 and on the Recognition Composition Law. The bound justifies treating the phi-ladder mass formula as perturbatively close to Standard-Model running when the deviation parameter remains small; no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.