J_log_zero
plain-language theorem explainer
J_log vanishes at the origin, establishing the minimum of the logarithmic cost function. Researchers analyzing stability in discrete configuration spaces cite this as the base case showing zero defect at the fixed point. The proof is a one-line simplification that unfolds the definition J_log(t) := cosh(t) - 1.
Claim. $J_ {log}(0) = 0$, where $J_{log}(t) := cosh(t) - 1$.
background
The Discreteness Forcing module shows that discreteness is forced by the cost landscape. J_log is defined as the cost in logarithmic coordinates: J_log(t) := cosh(t) - 1, a convex bowl centered at t = 0. This arises from the original J(x) = (x + x^{-1})/2 - 1 by the substitution x = e^t, as stated in the upstream J_log definition.
proof idea
The proof is a one-line wrapper that applies the simp tactic with the definition of J_log, which directly evaluates cosh(0) - 1 to zero.
why it matters
This supplies the zero-cost point required for the module's main results on stable minima in discrete spaces. It feeds the argument that continuous configuration spaces admit no isolated J-minima while discrete spaces do. The result aligns with the J-uniqueness fixed point in the forcing chain and the requirement that RSExist configurations collapse defect to zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.