J_log_pos
plain-language theorem explainer
The theorem shows that the log-cost J_log(t) equals cosh(t) minus one is strictly positive for every real t not zero. Number theorists studying zero locations and unification researchers deriving coupling inequalities cite it to guarantee positive defect away from the critical line. The proof is a short term-mode argument that combines the zero-equivalence lemma with non-negativity and the order lemma lt_of_le_of_ne.
Claim. $J(t) > 0$ for every real $t$ with $t ≠ 0$, where $J(t) := cosh(t) - 1$.
background
In the Discreteness Forcing module the cost function is rewritten in logarithmic coordinates. The definition states: J in log coordinates: J(eᵗ) = cosh(t) - 1. This is a convex bowl centered at t = 0. The module document explains that continuous configuration spaces admit no stable J-minima because infinitesimal perturbations cost arbitrarily little, while discrete steps enforce a finite minimum cost of J''(1) = 1.
proof idea
The term proof first invokes J_log_eq_zero_iff to obtain J_log t ≠ 0 from the hypothesis t ≠ 0. It then applies J_log_nonneg to obtain J_log t ≥ 0. Finally it uses lt_of_le_of_ne on the pair of facts to conclude strict positivity.
why it matters
The result is used by defectIterate_zero_pos to show d₀ > 0 for t ≠ 0 off the critical line and by zeroDefect_pos_iff_off_critical_line to equate positive defect with departure from the critical line. It also supports the two cosh inequalities in CouplingLaw. Within the framework it supplies the strict positivity needed for the discreteness-forcing argument that stable configurations require discrete steps rather than continuous drift, consistent with T5 J-uniqueness and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.