J_log_zero
plain-language theorem explainer
J_log vanishes at the origin and thereby locates the global minimum of the log-cost function. Researchers deriving stability conditions for discrete configurations cite this fact to fix the zero-defect reference point. The proof is a one-line simplification that unfolds the explicit definition of J_log.
Claim. $J(t) := 2^{-1}(e^{t} + e^{-t}) - 1$ satisfies $J(0) = 0$.
background
The DiscretenessForcing module recasts the Recognition cost function in logarithmic coordinates to expose the geometry of minima. J_log(t) is defined by J_log(t) := cosh(t) - 1, which is the image of the original J-cost under the substitution x = e^t and yields a convex bowl centered at t = 0. The module document states that this coordinate change converts the continuous-space drift problem into a discrete-step locking problem whose minimal cost is set by the second derivative at the origin.
proof idea
The proof is a one-line term-mode simplification that applies the definition of J_log.
why it matters
The declaration fixes the zero of the log-cost function, a prerequisite for the non-negativity and positivity statements that follow in the same file. It supplies the reference point required by the module's main argument that continuous configuration spaces admit no isolated J-minima while discrete spaces do. The result therefore participates in the forcing chain that derives discreteness from the cost landscape and aligns with the J-uniqueness step of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.