J_log_quadratic_approx
The theorem supplies a fourth-order error bound on the quadratic approximation of J_log near the origin. Workers on discreteness-forcing arguments cite it to control the cost of infinitesimal log-ratio perturbations in continuous configuration spaces. The proof rewrites J_log via its cosh definition, normalizes the absolute-value term, and invokes the pre-established cosh_quadratic_bound lemma.
claimFor every real number $ε$ with $|ε|<1$, $|J_log(ε) - ε^2/2| ≤ |ε|^4/20$, where $J_log(t) := cosh(t)-1$.
background
J_log is the cost function expressed in logarithmic coordinates: J_log(t) := cosh(t) - 1. This converts the multiplicative J-cost J(x) = (x + x^{-1})/2 - 1 into an additive convex bowl centered at t = 0, as stated in the module's core argument that continuous spaces admit no isolated J-minima. The local setting is the Discreteness Forcing module, whose main claim is that RS-existence requires discrete configuration steps because infinitesimal perturbations incur only infinitesimal J-cost. The bound itself rests on the upstream cosh_quadratic_bound theorem, which states that |cosh x - 1 - x^2/2| ≤ x^4/20 for |x|<1 by truncating the power series and dominating the tail by a geometric estimate.
proof idea
The tactic proof first rewrites J_log ε to cosh ε - 1 using the definition and the identity cosh ε = (e^ε + e^{-ε})/2. It then proves |ε|^4 = ε^4 by squaring and applying the absolute-value square identity. The resulting inequality is discharged directly by the upstream cosh_quadratic_bound lemma applied at ε.
why it matters in Recognition Science
This result supplies the quantitative control needed to show that continuous configuration spaces cannot support stable J-minima, a key step toward the module's conclusion that RS-existence forces discreteness. It sits inside the T5-T6 forcing chain by making the quadratic nature of the J-cost explicit near the fixed point, thereby supporting the later claims that only discrete steps can produce finite defect barriers. No downstream uses are recorded yet, but the bound is the natural quantitative companion to the qualitative instability argument in continuous_no_stable_minima.
scope and limits
- Does not assert the inequality for |ε| ≥ 1.
- Does not supply higher-order Taylor terms or asymptotic expansions.
- Does not address multidimensional or non-logarithmic perturbations.
- Does not claim optimality of the constant 1/20.
formal statement (Lean)
286theorem J_log_quadratic_approx (ε : ℝ) (hε : |ε| < 1) :
287 |J_log ε - ε^2 / 2| ≤ |ε|^4 / 20 := by
proof body
Tactic-mode proof.
288 -- J_log ε = Jcost (exp ε) = Real.cosh ε - 1
289 have h_cosh : J_log ε = Real.cosh ε - 1 := by
290 simp [J_log, Real.cosh_eq, Real.exp_neg]
291 rw [h_cosh]
292
293
294 have h_abs : |ε|^4 = ε^4 := by
295 calc |ε|^4 = (|ε|^2)^2 := by ring
296 _ = (ε^2)^2 := by rw [sq_abs]
297 _ = ε^4 := by ring
298 rw [h_abs]
299 exact cosh_quadratic_bound ε hε
300
301
302
303
304
305
306
307
308
309/-! ## Instability in Continuous Spaces -/
310
311/-- A configuration is "stable" if it's a strict local minimum of J.
312 This means there's a neighborhood where it's the unique minimizer. -/