cosh_sub_one_ge_sq_div_two
plain-language theorem explainer
The inequality cosh(t) - 1 ≥ t²/2 holds for every real t and supplies the analytic core for showing that J-cost exceeds the squared logarithm. Researchers deriving thermodynamics from recognition costs or information geometry would cite it to position J as the ancestor of Shannon entropy. The proof extracts the n=0 and n=1 terms from the Taylor series of cosh, verifies nonnegativity of all remaining even-powered terms, and compares the partial sum to the infinite sum.
Claim. For all real numbers $t$, $cosh t - 1 ≥ t^2 / 2$.
background
In the J-Cost as Entropy's Ancestor module, J-cost is the functional J(x) = (x + x^{-1})/2 - 1 for x > 0, equivalently written cosh(log x) - 1. This quantity is fixed by the Recognition Composition Law and acts as the energy functional on many-body ledgers. The module derives the Gibbs distribution p*_i = exp(-J(r_i)/T_R)/Z by maximizing Shannon entropy H(p) = -∑ p_i log p_i subject to a fixed average J-cost constraint, showing that the exponential form is forced rather than postulated.
proof idea
The proof calls hasSum_cosh to obtain the series representation cosh t = ∑ t^{2n}/(2n)!. It isolates the n=0 term (equal to 1) and n=1 term (equal to t²/2), proves nonnegativity of every term via div_nonneg and pow_nonneg, and shows that the sum of the first two terms is at most the full sum by applying summable.sum_le_tsum to the tail. Linarith finishes the comparison.
why it matters
This theorem is the direct input to jcost_dominates_squared_log, which translates the bound into J(x) ≥ (log x)²/2 and thereby establishes that Shannon entropy is the quadratic shadow of J-cost. It completes the backward direction of the module's argument that Gibbs weights and free-energy minimization emerge from ledger counting. In the Recognition framework it supports the T5 uniqueness of J and the emergence of thermodynamics from the Recognition Composition Law, with the eight-tick octave and D=3 supplying the discrete background.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.