J_log_symmetric
plain-language theorem explainer
The log-cost function satisfies J_log(-t) = J_log(t) for every real t. Number theorists proving reflection invariance of zero defects cite this when showing that functional reflection preserves defect. The proof is a one-line simplification that unfolds the cosh definition and applies the evenness of cosh.
Claim. For all real $t$, $J(t) = J(-t)$ where $J(t) := 2^{-1}(e^{t} + e^{-t}) - 1$.
background
The DiscretenessForcing module recasts the J-cost in logarithmic coordinates to expose the convex bowl structure. J_log(t) is defined by J_log(t) := cosh(t) - 1, which equals the original J(e^t) and has its unique minimum at t = 0. The same definition appears in the imported ContinuumBridge module with identical meaning.
proof idea
The proof is a one-line wrapper that applies simp only [J_log, Real.cosh_neg]. This unfolds the definition of J_log and reduces the claim to the standard identity cosh(-x) = cosh(x).
why it matters
The result feeds the two zeroDefect invariance theorems in NumberTheory.ZeroLocationCost, where it supplies the symmetry step that lets reflection across Re(s) = 1/2 preserve defect. It thereby supports the module's main claim that continuous spaces admit no isolated J-minima while discrete spaces do.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.