exp_sum_minus_two_eq_sq
plain-language theorem explainer
The algebraic identity states that for real t the sum of exp(t) and exp(-t) minus two equals the square of exp(t/2) minus exp(-t/2). Researchers deriving J-cost dominance over squared logarithms in recognition thermodynamics cite it to ground the quadratic approximation that lets Shannon entropy emerge from ledger counting. The tactic proof expands the right-hand side via exponential addition formulas and closes the equality with nlinarith on a non-negative square.
Claim. $e^{t} + e^{-t} - 2 = (e^{t/2} - e^{-t/2})^{2}$ for every real number $t$.
background
J-cost is the functional J(x) = ½(x + x^{-1}) - 1. The module shows that this functional is the ancestor of Shannon entropy: for many-body ledgers the maximum-entropy distribution under fixed average J-cost is the Gibbs form exp(-J/T_R)/Z, with T_R derived rather than postulated. The supplied identity is the algebraic step that converts the hyperbolic form of J into a quadratic lower bound, supporting the claim that entropy is the second-order shadow of J-cost.
proof idea
Three auxiliary facts are established by rewriting exp(a) * exp(b) as exp(a+b) and simplifying: the square of exp(t/2) recovers exp(t), the square of exp(-t/2) recovers exp(-t), and the product of the two opposite halves equals 1. The proof then invokes nlinarith on the non-negative quantity (exp(t/2) - exp(-t/2))^{2} to obtain the desired equality.
why it matters
The lemma supplies the algebraic engine for the ancestor inequality cosh(t) - 1 ≥ t^{2}/2 that appears immediately after it in the file. That inequality is the key step toward jcost_dominates_squared_log, which in turn justifies treating Shannon entropy as the quadratic approximation to J-cost. Within the Recognition framework it anchors the thermodynamic bridge between the J-uniqueness axiom (T5) and the emergence of Gibbs weights from constrained ledger optimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.