cosh_quadratic_bound
plain-language theorem explainer
For real x with absolute value less than one, the absolute deviation of cosh x from its quadratic Taylor polynomial 1 plus x squared over 2 is bounded above by x to the fourth over 20. Workers on Recognition Science discreteness arguments and on the GCIC thermodynamics calculations cite the result when controlling the J-cost bowl near its minimum. The proof splits the power series for cosh at the first two terms, invokes the known quadratic lower bound to confirm non-negativity of the remainder, then dominates the tail by a geometric series via
Claim. For all real $x$ with $|x|<1$, $|cosh x - 1 - x^2/2| ≤ x^4/20$.
background
The DiscretenessForcing module shows that continuous configuration spaces admit no stable J-minima because infinitesimal perturbations cost arbitrarily little J-cost, while discrete spaces permit isolated minima at finite cost. In log coordinates the cost function becomes J(e^t) = cosh t - 1, so local control on the cosh Taylor remainder directly controls the cost landscape near the origin. The upstream result Cost.cosh_quadratic_lower_bound supplies the matching inequality cosh x ≥ 1 + x²/2 that is used to establish non-negativity of the remainder before the upper bound is derived.
proof idea
The tactic proof begins by invoking Real.hasSum_cosh to obtain the series representation, splits the sum at n=0 and n=1, and rewrites the difference as the tail sum starting at n=2. It applies Cost.cosh_quadratic_lower_bound to obtain non-negativity, reduces the absolute value to the tail, then introduces r = x²/30 < 1 and the comparison series b_n = (x⁴/24) r^n. A separate induction establishes the factorial lower bound (2(n+2))! ≥ 24·30^n, which yields term-by-term domination; the geometric sum of b_n is then evaluated explicitly to close the x⁴/20 estimate.
why it matters
The bound is invoked directly by J_log_quadratic_approx in the same module and supplies the error control used in phase_barrier_upper and phase_barrier_lower of the GCIC Thermodynamics paper as well as in enhancement_near_one of CouplingLaw. It therefore participates in the chain that converts the continuous J-cost bowl into quantitative statements about phase barriers and perturbative enhancements. The result sits inside the broader discreteness-forcing argument that continuous spaces cannot support stable RSExist configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.