cosh_ge_one_plus_half_sq
plain-language theorem explainer
The inequality cosh(t) - 1 ≥ t²/2 holds for every real t. Researchers deriving the universal coupling law cite it to bound the exact J-cost above its perturbative quadratic approximation. The proof rewrites via the double-angle identity cosh(t) - 1 = 2 sinh²(t/2), splits into sign cases on t, invokes sinh(u) ≥ u, and closes both branches with nlinarith.
Claim. For all real numbers $t$, $t^2/2 ≤ cosh(t) - 1$.
background
In the Universal Coupling Law module the J-cost in logarithmic coordinates is J(e^t) = cosh(t) - 1, with the perturbative approximation given by the leading Taylor term t²/2. This supplies the inequality showing the exact geometric cost is always at least as large as the perturbative one. It relies on the upstream result J_log_pos, which states that J_log t > 0 for t ≠ 0 and thereby confirms strict dominance away from the origin.
proof idea
The proof first applies Real.cosh_two_mul to obtain the identity cosh t - 1 = 2 sinh(t/2)². It then performs case analysis on whether t ≥ 0. For the non-negative case it invokes Real.self_le_sinh_iff to obtain sinh(t/2) ≥ t/2 and squares the difference. For the negative case it uses sinh symmetry together with the same inequality on the absolute value. Both branches are closed by nlinarith.
why it matters
This result is invoked directly by cosh_gt_one_plus_half_sq and by enhancement_ge_one, which together establish that the coupling enhancement S(t) = 2(cosh(t) - 1)/t² is at least 1 with equality only at t = 0. In the Recognition Science framework it closes the perturbative-to-geometric bridge of the module, confirming that the J-cost (T5) always exceeds its quadratic approximation and thereby accounts for the large residue factors F(Z) in the mass formula. It touches the scaling of enhancement at the specific rung values of the φ-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.