J_log_nonneg
plain-language theorem explainer
The non-negativity of the logarithmic J-cost holds for every real argument. Researchers proving stability of discrete configurations cite this when bounding defect from below. The proof reduces the claim to the standard inequality cosh(t) ≥ 1 by unfolding the definition and applying linear arithmetic.
Claim. For every real number $t$, $J(t) := e^{t} + e^{-t}/2 - 1$ satisfies $J(t) - 1/2 + 1/2 = 0$ wait, no: $J_log(t) := cosh(t) - 1$ obeys $J_log(t) ≥ 0$.
background
In the DiscretenessForcing module the cost function is rewritten in logarithmic coordinates. The definition states J_log(t) := Real.cosh t - 1, which is the image of the original J(x) = (x + x^{-1})/2 - 1 under the substitution x = e^t. This produces a convex bowl centered at t = 0 whose minimum value is zero. The module's opening argument notes that continuous configuration spaces permit infinitesimal perturbations whose J-cost can be made arbitrarily small, while discrete steps enforce a finite minimum cost of J''(1) = 1.
proof idea
The term proof first applies simp to unfold J_log into cosh(t) - 1. It then invokes the Mathlib fact Real.one_le_cosh t to obtain cosh(t) ≥ 1. Linear arithmetic closes the inequality.
why it matters
J_log_nonneg is invoked directly by J_log_pos to obtain strict positivity for t ≠ 0 and by zeroDefect_nonneg to bound the zero-location defect. It therefore supplies the lower bound required by the module's main theorems on rs_exists_requires_discrete and discrete_stable_minima_possible. The result sits inside the T5 J-uniqueness step of the forcing chain and supports the claim that only discrete spaces can host stable J-minima.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.