J_log_symmetric
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove that zero is the only minimum of J_log.
- Does not extend the identity to complex arguments.
- Does not derive positivity or second-derivative bounds.
- Does not address stability of discrete configurations.
formal statement (Lean)
90theorem J_log_symmetric (t : ℝ) : J_log (-t) = J_log t := by
proof body
Term-mode proof.
91 simp only [J_log, Real.cosh_neg]
92
93/-- Connection to original J: J(eᵗ) = J_log(t) for t corresponding to positive x. -/