J_log_eq_zero_iff
plain-language theorem explainer
J_log vanishes precisely at the origin, confirming the unique minimum of the logarithmic cost function. Researchers modeling stability via cost landscapes in Recognition Science cite this to isolate the zero-defect state. The proof reduces cosh(t) equals one to the injectivity of the exponential map through algebraic identities and inequalities, with the converse immediate by substitution.
Claim. $J(t) := 2^{-1}(t + t^{-1}) - 1$ in logarithmic coordinates satisfies $J(e^{t}) = 0$ if and only if $t = 0$, where $J(e^{t}) = 2^{-1}(e^{t} + e^{-t}) - 1$.
background
The Discreteness Forcing module recasts the Recognition cost function in logarithmic coordinates to analyze stability of configurations. J_log(t) is defined as cosh(t) minus one, yielding a convex bowl minimized at the origin. This local setting supports the claim that continuous spaces admit no isolated minima, since infinitesimal perturbations incur arbitrarily small costs, while discrete steps enforce a finite minimum cost.
proof idea
The tactic proof splits the biconditional via constructor. The forward direction unfolds the definition, applies linear arithmetic to obtain cosh(t) equals one, rewrites via the exponential form, and invokes nonlinear arithmetic plus exponential injectivity to reach t equals zero. The reverse direction substitutes directly.
why it matters
This equivalence is invoked by J_log_pos to obtain strict positivity away from zero and by the NumberTheory modules to equate the Riemann hypothesis with zero J-cost on the critical line. It supplies the uniqueness step in the forcing chain that isolates the zero-cost state, thereby requiring discrete configuration space for stable configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.