Encyclopedia Foundation Foundation Continuum Limit Quadratic Approximates Jlog

ARTICLE 3 claims 3 theorems

Foundation Continuum Limit Quadratic Approximates Jlog

A discrete cost function, when the steps are small, behaves almost exactly like a simple parabola, and that one fact is the hinge between a world of ticks and a world of smooth equations.

Verify this page

The quadratic bridge

A ledger, a discrete record of events, keeps track of changes by charging a cost for each one. The framework's central cost function, written J_log, is not a parabola; it is a hyperbolic cosine minus one. But the theorem quadratic_approximates_jlog proves that for any small change ε, the difference between J_log(ε) and the simple quadratic ε²/2 is at most |ε|⁴/20. When ε is tiny, that quartic error is vanishingly small, so the cost behaves like a parabola to a very good approximation.

This is a standard pattern in mathematics and physics. Near a minimum, almost any smooth function looks quadratic; the Taylor expansion of cosh(t) - 1 is t²/2 + t⁴/24 + ..., and the leading term dominates for small t. The theorem's content is that the framework's cost function, derived from first principles, falls into this universal class. The proof is machine-checked in the framework's library of formal theorems, and it is a theorem, not a model or a hypothesis.

The reason this matters is that quadratic costs on a lattice produce the discrete Laplacian, the sum of second differences. The framework proves that this lattice Laplacian, in the long-wavelength limit, becomes the continuous Laplacian ∇². That is the bridge from the discrete ledger to the smooth differential equations of physics, such as the Klein-Gordon equation. The quadratic approximation is the first step on that bridge, and the theorem quantifies exactly how good the approximation is.

The theorem does not claim that the cost function is exactly quadratic, nor that the approximation holds for large changes. It also does not claim that the continuum limit is fully rigorous physics; the framework's own notes mark the physical recognition-to-linking bridge as open. What the theorem establishes is a precise, proved statement about the leading behavior of the cost function, and that is what makes the continuum emergence story begin on solid ground.

THEOREM quadratic_approximates_jlog · IndisputableMonolith/Foundation/ContinuumLimit.lean
quadratic_approximates_jlog · IndisputableMonolith/Foundation/ContinuumLimit.lean:75 
/-- The quadratic cost matches J_log to O(ε⁴). -/
theorem quadratic_approximates_jlog (ε : ℝ) (hε : |ε| < 1) :
    |J_log ε - quadratic_cost ε| ≤ |ε| ^ 4 / 20 := by
  unfold quadratic_cost
  exact jcost_quadratic_leading ε hε
THEOREM jcost_gives_laplacian_structure · IndisputableMonolith/Foundation/ContinuumLimit.lean
jcost_gives_laplacian_structure · IndisputableMonolith/Foundation/ContinuumLimit.lean:149 
/-- **THEOREM (J-Cost → Lattice Laplacian)**:
    In the quadratic regime (small perturbations), the J-cost of
    nearest-neighbor differences reduces to the lattice Laplacian.

    Specifically: if all field differences |f(x±eₖ) − f(x)| < 1, then

      neighbor_cost(f, x) ≈ (1/2) · ∑_k [(f(x+eₖ)−f(x))² + (f(x−eₖ)−f(x))²]

    The gradient of this with respect to f(x) is:

      −∂/∂f(x) [neighbor_cost] ≈ lattice_laplacian(f, x)

    So the variational dynamics (minimize J-cost) produces DIFFUSION
    (the Laplacian). -/
theorem jcost_gives_laplacian_structure {D : ℕ}
    (f : LatticeField D) (x : Fin D → ℤ)
    (h_small : ∀ k : Fin D,
      |f (shift_plus k x) - f x| < 1 ∧
      |f (shift_minus k x) - f x| < 1) :
    |neighbor_cost f x -
      ∑ k : Fin D, ((f (shift_plus k x) - f x) ^ 2 / 2 +
                     (f (shift_minus k x) - f x) ^ 2 / 2)| ≤
    ∑ k : Fin D, (|f (shift_plus k x) - f x| ^ 4 / 20 +
                   |f (shift_minus k x) - f x| ^ 4 / 20) := by
  unfold neighbor_cost
  have h_bound : ∀ k : Fin D,
      |J_log (f (shift_plus k x) - f x) + J_log (f (shift_minus k x) - f x) -
       ((f (shift_plus k x) - f x) ^ 2 / 2 +
        (f (shift_minus k x) - f x) ^ 2 / 2)| ≤
      |f (shift_plus k x) - f x| ^ 4 / 20 +
      |f (shift_minus k x) - f x| ^ 4 / 20 := by
    intro k
    have ⟨hp, hm⟩ := h_small k
    have hp' := jcost_quadratic_leading _ hp
    have hm' := jcost_quadratic_leading _ hm
    let A := J_log (f (shift_plus k x) - f x) - (f (shift_plus k x) - f x) ^ 2 / 2
    let B := J_log (f (shift_minus k x) - f x) - (f (shift_minus k x) - f x) ^ 2 / 2
    calc |J_log (f (shift_plus k x) - f x) + J_log (f (shift_minus k x) - f x) -
           ((f (shift_plus k x) - f x) ^ 2 / 2 + (f (shift_minus k x) - f x) ^ 2 / 2)|
        ≤ |A| + |B| := by
          simpa [A, B, sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using abs_add_le A B
      _ ≤ |f (shift_plus k x) - f x| ^ 4 / 20 +
          |f (shift_minus k x) - f x| ^ 4 / 20 := by linarith
  calc |∑ k : Fin D, (J_log (f (shift_plus k x) - f x) +
                       J_log (f (shift_minus k x) - f x)) -
        ∑ k : Fin D, ((f (shift_plus k x) - f x) ^ 2 / 2 +
                       (f (shift_minus k x) - f x) ^ 2 / 2)|
      = |∑ k : Fin D, ((J_log (f (shift_plus k x) - f x) +
                         J_log (f (shift_minus k x) - f x)) -
                        ((f (shift_plus k x) - f x) ^ 2 / 2 +
                         (f (shift_minus k x) - f x) ^ 2 / 2))| := by
        congr 1; rw [← Finset.sum_sub_distrib]
    _ ≤ ∑ k : Fin D, |(J_log (f (shift_plus k x) - f x) +
                        J_log (f (shift_minus k x) - f x)) -
                       ((f (shift_plus k x) - f x) ^ 2 / 2 +
                        (f (shift_minus k x) - f x) ^ 2 / 2)| :=
        Finset.abs_sum_le_sum_abs _ _
    _ ≤ ∑ k : Fin D, (|f (shift_plus k x) - f x| ^ 4 / 20 +
                       |f (shift_minus k x) - f x| ^ 4 / 20) :=
        Finset.sum_le_sum (fun k _ => h_bound k)
THEOREM continuum_limit_second_order · IndisputableMonolith/Foundation/ContinuumLimit.lean
continuum_limit_second_order · IndisputableMonolith/Foundation/ContinuumLimit.lean:250 
/-- **THEOREM (Lattice Laplacian → Continuous Laplacian)**:
    The second-order finite difference approximation converges to f''(x)
    with error bounded by C·a², where C depends on the 4th derivative.

    For a C⁴ function f:
      (f(x+a) + f(x−a) − 2f(x))/a² = f''(x) + (a²/12)·f⁴(ξ)

    The error bound C·a² with C = fourthDerivBound/12 follows from
    Taylor's theorem with symmetric cancellation of odd-order terms.

    The `ContDiff ℝ 4 f` hypothesis guarantees the 4th derivative exists
    and is continuous, making the supremum on compact intervals finite. -/
theorem continuum_limit_second_order (f : ℝ → ℝ) (x a : ℝ) (ha : a ≠ 0)
    (hf : ContDiff ℝ 4 f) :
    ∃ (C : ℝ), 0 ≤ C ∧
    |(f (x + a) + f (x - a) - 2 * f x) / a ^ 2 - deriv (deriv f) x| ≤ C * a ^ 2 := by
  let δ : ℝ := |a|
  let M : ℝ := fourthDerivBound f x a
  let s : Set ℝ := Set.Icc (0 : ℝ) δ
  let gPlus : ℝ → ℝ := fun t => f (x + t)
  let gMinus : ℝ → ℝ := fun t => f (x - t)
  have hδpos : 0 < δ := by
    simpa [δ] using abs_pos.mpr ha
  have hδnonneg : 0 ≤ δ := by
    simp [δ]
  have ha2 : a ^ 2 = δ ^ 2 := by
    simp [δ, sq_abs]
  have hx0 : (0 : ℝ) ∈ s := by
    simp [s, hδnonneg]
  have hδmem : δ ∈ s := by
    simp [s, hδnonneg]
  have hs_unique : UniqueDiffOn ℝ s := uniqueDiffOn_Icc hδpos
  have hM_nonneg : 0 ≤ M := fourthDerivBound_nonneg f x a hf
  have hshift_plus : ContDiff ℝ 4 gPlus := by
    simpa [gPlus] using hf.comp (contDiff_const.add contDiff_id)
  have hshift_minus : ContDiff ℝ 4 gMinus := by
    simpa [gMinus, sub_eq_add_neg] using hf.comp (contDiff_const.add contDiff_id.neg)
  have hplus_bound : ∀ y ∈ s, ‖iteratedDerivWithin 4 gPlus s y‖ ≤ M := by
    intro y hy
    have hwithin :
        iteratedDerivWithin 4 gPlus s y = iteratedDeriv 4 gPlus y := by
      exact iteratedDerivWithin_eq_iteratedDeriv hs_unique (hshift_plus.contDiffAt (x := y)) hy
    have hshift :
        iteratedDeriv 4 gPlus y = iteratedDeriv 4 f (x + y) := by
      simpa [gPlus] using congrFun (iteratedDeriv_comp_const_add 4 f x) y
    have hy' : x + y ∈ Set.Icc (x - |a|) (x + |a|) := by
      rcases hy with ⟨hy0, hyδ⟩
      constructor <;> nlinarith [hδnonneg]
    rw [hwithin, hshift, Real.norm_eq_abs]
    exact le_fourthDerivBound f x a (x + y) hf hy'
  have hminus_bound : ∀ y ∈ s, ‖iteratedDerivWithin 4 gMinus s y‖ ≤ M := by
    intro y hy
    have hwithin :
        iteratedDerivWithin 4 gMinus s y = iteratedDeriv 4 gMinus y := by
      exact iteratedDerivWithin_eq_iteratedDeriv hs_unique (hshift_minus.contDiffAt (x := y)) hy
    have hshift :
        iteratedDeriv 4 gMinus y = iteratedDeriv 4 f (x - y) := by
      have hneg :
          iteratedDeriv 4 gMinus y = (-1 : ℝ) ^ 4 * iteratedDeriv 4 (fun z => f (x + z)) (-y) := by
        simpa [gMinus, sub_eq_add_neg, smul_eq_mul] using iteratedDeriv_comp_neg 4 (fun z => f (x + z)) y
      have hplus :
          iteratedDeriv 4 (fun z => f (x + z)) (-y) = iteratedDeriv 4 f (x - y) := by
        simpa using congrFun (iteratedDeriv_comp_const_add 4 f x) (-y)
      rw [hneg, hplus]
      norm_num
    have hy' : x - y ∈ Set.Icc (x - |a|) (x + |a|) := by
      rcases hy with ⟨hy0, hyδ⟩
      constructor <;> nlinarith [hδnonneg]
    rw [hwithin, hshift, Real.norm_eq_abs]
    exact le_fourthDerivBound f x a (x - y) hf hy'
  have hplus_zero :
      iteratedDerivWithin 0 gPlus s 0 = f x := by
    simp [gPlus, s]
  have hplus_one :
      iteratedDerivWithin 1 gPlus s 0 = deriv f x := by
    have hwithin :
        iteratedDerivWithin 1 gPlus s 0 = iteratedDeriv 1 gPlus 0 := by
      simpa using
        (iteratedDerivWithin_eq_iteratedDeriv (f := gPlus) (s := s) (x := 0) (n := 1)
          hs_unique
          ((hshift_plus.contDiffAt (x := 0)).of_le
            (show ((1 : ℕ∞) : WithTop ℕ∞) ≤ ((4 : ℕ∞) : WithTop ℕ∞) by decide))
          hx0)
    rw [hwithin]
    simpa [gPlus] using congrFun (iteratedDeriv_comp_const_add 1 f x) 0
  have hplus_two :
      iteratedDerivWithin 2 gPlus s 0 = deriv (deriv f) x := by
    rw [iteratedDerivWithin_eq_iteratedDeriv hs_unique
      ((hshift_plus.contDiffAt (x := 0)).of_le
        (show ((2 : ℕ∞) : WithTop ℕ∞) ≤ ((4 : ℕ∞) : WithTop ℕ∞) by decide)) hx0]
    simpa [gPlus, iteratedDeriv_eq_iterate] using congrFun (iteratedDeriv_comp_const_add 2 f x) 0
  have hplus_three :
      iteratedDerivWithin 3 gPlus s 0 = iteratedDeriv 3 f x := by
    rw [iteratedDerivWithin_eq_iteratedDeriv hs_unique
      ((hshift_plus.contDiffAt (x := 0)).of_le
        (show ((3 : ℕ∞) : WithTop ℕ∞) ≤ ((4 : ℕ∞) : WithTop ℕ∞) by decide)) hx0]
    simpa [gPlus] using congrFun (iteratedDeriv_comp_const_add 3 f x) 0
  have hminus_zero :
      iteratedDerivWithin 0 gMinus s 0 = f x := by
    simp [gMinus, s]
  have hminus_one :
      iteratedDerivWithin 1 gMinus s 0 = -deriv f x := by
    have hwithin :
        iteratedDerivWithin 1 gMinus s 0 = iteratedDeriv 1 gMinus 0 := by
      simpa using
        (iteratedDerivWithin_eq_iteratedDeriv (f := gMinus) (s := s) (x := 0) (n := 1)
          hs_unique
          ((hshift_minus.contDiffAt (x := 0)).of_le
            (show ((1 : ℕ∞) : WithTop ℕ∞) ≤ ((4 : ℕ∞) : WithTop ℕ∞) by decide))
          hx0)
    rw [hwithin]
    have hneg :
        iteratedDeriv 1 gMinus 0 = (-1 : ℝ) ^ 1 * iteratedDeriv 1 (fun z => f (x + z)) 0 := by
      simpa [gMinus, sub_eq_add_neg, smul_eq_mul] using iteratedDeriv_comp_neg 1 (fun z => f (x + z)) 0
    have hplus :
        iteratedDeriv 1 (fun z => f (x + z)) 0 = deriv f x := by
      simpa [gPlus] using congrFun (iteratedDeriv_comp_const_add 1 f x) 0
    rw [hneg, hplus]
    norm_num
  have hminus_two :
      iteratedDerivWithin 2 gMinus s 0 = deriv (deriv f) x := by
    rw [iteratedDerivWithin_eq_iteratedDeriv hs_unique
      ((hshift_minus.contDiffAt (x := 0)).of_le
        (show ((2 : ℕ∞) : WithTop ℕ∞) ≤ ((4 : ℕ∞) : WithTop ℕ∞) by decide)) hx0]
    have hneg :
        iteratedDeriv 2 gMinus 0 = (-1 : ℝ) ^ 2 * iteratedDeriv 2 (fun z => f (x + z)) 0 := by
      simpa [gMinus, sub_eq_add_neg, smul_eq_mul] using iteratedDeriv_comp_neg 2 (fun z => f (x + z)) 0
    have hplus :
        iteratedDeriv 2 (fun z => f (x + z)) 0 = deriv (deriv f) x := by
      simpa [gPlus, iteratedDeriv_eq_iterate] using congrFun (iteratedDeriv_comp_const_add 2 f x) 0
    rw [hneg, hplus]
    norm_num
  have hminus_three :
      iteratedDerivWithin 3 gMinus s 0 = -iteratedDeriv 3 f x := by
    rw [iteratedDerivWithin_eq_iteratedDeriv hs_unique
      ((hshift_minus.contDiffAt (x := 0)).of_le
        (show ((3 : ℕ∞) : WithTop ℕ∞) ≤ ((4 : ℕ∞) : WithTop ℕ∞) by decide)) hx0]
    have hneg :
        iteratedDeriv 3 gMinus 0 = (-1 : ℝ) ^ 3 * iteratedDeriv 3 (fun z => f (x + z)) 0 := by
      simpa [gMinus, sub_eq_add_neg, smul_eq_mul] using iteratedDeriv_comp_neg 3 (fun z => f (x + z)) 0
    have hplus :
        iteratedDeriv 3 (fun z => f (x + z)) 0 = iteratedDeriv 3 f x := by
      simpa [gPlus] using congrFun (iteratedDeriv_comp_const_add 3 f x) 0
    rw [hneg, hplus]
    norm_num
  have hplus_taylor :
      taylorWithinEval gPlus 3 s 0 δ =
        f x + δ * deriv f x + δ ^ 2 / 2 * deriv (deriv f) x +
          δ ^ 3 / 6 * iteratedDeriv 3 f x := by
    rw [taylorWithinEval_succ, taylorWithinEval_succ, taylorWithinEval_succ, taylor_within_zero_eval]
    simp [s, hplus_one, hplus_two, hplus_three, gPlus, smul_eq_mul]
    ring
  have hminus_taylor :
      taylorWithinEval gMinus 3 s 0 δ =
        f x - δ * deriv f x + δ ^ 2 / 2 * deriv (deriv f) x -
          δ ^ 3 / 6 * iteratedDeriv 3 f x := by
    rw [taylorWithinEval_succ, taylorWithinEval_succ, taylorWithinEval_succ, taylor_within_zero_eval]
    simp [s, hminus_one, hminus_two, hminus_three, gMinus, smul_eq_mul]
    ring
  have hplus_remainder :
      |gPlus δ - taylorWithinEval gPlus 3 s 0 δ| ≤ M * δ ^ 4 / 6 := by
    simpa [s, M] using
      taylor_mean_remainder_bound (a := (0 : ℝ)) (b := δ) (C := M) (x := δ)
        hδnonneg hshift_plus.contDiffOn hδmem hplus_bound
  have hminus_remainder :
      |gMinus δ - taylorWithinEval gMinus 3 s 0 δ| ≤ M * δ ^ 4 / 6 := by
    simpa [s, M] using
      taylor_mean_remainder_bound (a := (0 : ℝ)) (b := δ) (C := M) (x := δ)
        hδnonneg hshift_minus.contDiffOn hδmem hminus_bound
  have hsum_even :
      f (x + a) + f (x - a) = f (x + δ) + f (x - δ) := by
    by_cases ha_nonneg : 0 ≤ a
    · have hδ : δ = a := by simpa [δ] using abs_of_nonneg ha_nonneg
      simp [hδ]
    · have ha_neg : a < 0 := lt_of_not_ge ha_nonneg
      have hδ : δ = -a := by simpa [δ] using abs_of_neg ha_neg
      simp [hδ, sub_eq_add_neg, add_comm]
  have hcore :
      |(f (x + δ) + f (x - δ) - 2 * f x) - δ ^ 2 * deriv (deriv f) x| ≤ M * δ ^ 4 / 3 := by
    have hrewrite :
        (f (x + δ) + f (x - δ) - 2 * f x) - δ ^ 2 * deriv (deriv f) x =
          (gPlus δ - taylorWithinEval gPlus 3 s 0 δ) +
            (gMinus δ - taylorWithinEval gMinus 3 s 0 δ) := by
      rw [hplus_taylor, hminus_taylor]
      simp [gPlus, gMinus]
      ring
    rw [hrewrite]
    calc
      |(gPlus δ - taylorWithinEval gPlus 3 s 0 δ) +
          (gMinus δ - taylorWithinEval gMinus 3 s 0 δ)| ≤
          |gPlus δ - taylorWithinEval gPlus 3 s 0 δ| +
            |gMinus δ - taylorWithinEval gMinus 3 s 0 δ| := abs_add_le _ _
      _ ≤ M * δ ^ 4 / 6 + M * δ ^ 4 / 6 := by
            gcongr
      _ = M * δ ^ 4 / 3 := by ring
  refine ⟨M / 3, by positivity, ?_⟩
  rw [ha2]
  have hδ2_ne : δ ^ 2 ≠ 0 := by positivity
  have hrewrite :
      (f (x + a) + f (x - a) - 2 * f x) / δ ^ 2 - deriv (deriv f) x =
        ((f (x + δ) + f (x - δ) - 2 * f x) - δ ^ 2 * deriv (deriv f) x) / δ ^ 2 := by
    rw [hsum_even]
    field_simp [hδ2_ne]
  rw [hrewrite, abs_div, abs_of_pos (sq_pos_of_pos hδpos)]
  have hdiv :=
    div_le_div_of_nonneg_right hcore (sq_nonneg δ)
  have hcalc : (M * δ ^ 4 / 3) / δ ^ 2 = (M / 3) * δ ^ 2 := by
    field_simp [hδ2_ne]
  calc
    |(f (x + δ) + f (x - δ) - 2 * f x) - δ ^ 2 * deriv (deriv f) x| / δ ^ 2
        ≤ (M * δ ^ 4 / 3) / δ ^ 2 := hdiv
    _ = (M / 3) * δ ^ 2 := hcalc

What this page does not claim

The cost function is exactly quadratic for all inputs. The approximation holds for large perturbations beyond the unit interval. The derivation of the Klein-Gordon equation from the discrete ledger is a complete physical theory.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/ContinuumLimit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND