J_log_nonneg
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish strict positivity away from t = 0.
- Does not treat complex arguments.
- Does not derive the quadratic approximation near zero.
- Does not address higher-order derivatives of J_log.
formal statement (Lean)
53theorem J_log_nonneg (t : ℝ) : J_log t ≥ 0 := by
proof body
Term-mode proof.
54 simp only [J_log]
55 have h : Real.cosh t ≥ 1 := Real.one_le_cosh t
56 linarith
57
58/-- J_log is zero iff t = 0.
59 Proof: cosh t = 1 iff t = 0 (by AM-GM on e^t + e^{-t}). -/