Encyclopedia Foundation Foundation Continuum Limit Fourth Deriv Continuous

ARTICLE 2 claims 2 theorems

Foundation Continuum Limit Fourth Deriv Continuous

A small formal lemma about smooth functions is the technical hinge that lets a discrete ledger of events produce the continuous equations of physics.

Verify this page

The fourth derivative

In classical analysis, a function is called four times continuously differentiable when its fourth derivative exists and is itself a continuous function. The declaration fourth_deriv_continuous in the framework's machine-checked library of formal theorems proves exactly this implication: if a real function is four times continuously differentiable, then its fourth derivative is continuous. That is a standard fact, but the framework needs it as a precise technical step, not as a hand-wave.

The reason matters is the continuum limit. The framework models the world as a discrete record of recognition events on a lattice, a grid of points with integer coordinates. The cost of a small change between neighboring points is approximated by a quadratic term, and the framework proves that this quadratic cost produces the discrete Laplacian, the sum of second differences. To pass from the discrete Laplacian to the continuous Laplacian, one needs a bound on how fast the approximation improves as the lattice spacing shrinks. That bound uses the fourth derivative: the error between the finite difference and the true second derivative is controlled by the size of the fourth derivative times the square of the spacing. The theorem continuum_limit_second_order states this bound, and it relies on the continuity of the fourth derivative to make the bound finite.

In Recognition Science, the chain of results then extends further: the continuous Laplacian leads to a Klein-Gordon equation, and from there to Dirac and Einstein equations. But fourth_deriv_continuous itself does not prove any of that. It is a small lemma about real functions, not about physics. It does not assert that the continuum limit is physically correct, nor that the Klein-Gordon structure is unique. Those are separate claims in the library, with their own proofs and conditions.

What the declaration does establish is a clean analytical fact: smoothness of order four guarantees the fourth derivative is continuous, which is exactly what the error bound needs. Without it, the bound could blow up and the limit would not be justified. The lemma is the quiet hinge that lets the discrete-to-continuous passage go through rigorously.

THEOREM fourth_deriv_continuous · IndisputableMonolith/Foundation/ContinuumLimit.lean
fourth_deriv_continuous · IndisputableMonolith/Foundation/ContinuumLimit.lean:212 
/-- The **lattice spacing** parameter a. In the continuum limit, a → 0
    while the physical distance x_phys = a · x_lattice is held fixed. -/
noncomputable def lattice_spacing : ℝ := 1

/- **THEOREM (Lattice Laplacian → Continuous Laplacian)**:
    The lattice Laplacian scaled by 1/a² converges to the continuous
    Laplacian ∇² as the lattice spacing a → 0.

    For a smooth function φ : ℝ^D → ℝ and lattice spacing a:

      (1/a²) ∑_k [φ(x + aeₖ) + φ(x − aeₖ) − 2φ(x)] → ∑_k ∂²φ/∂xₖ²

    This is a standard result from numerical analysis (second-order
    finite difference approximation to the second derivative). -/
/-- The 4th derivative of a C⁴ function exists and is continuous. -/
private theorem fourth_deriv_continuous (f : ℝ → ℝ) (hf : ContDiff ℝ 4 f) :
    Continuous (iteratedDeriv 4 f) :=
  hf.continuous_iteratedDeriv' 4
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 declaration does not prove that the continuum limit is physically correct. The declaration does not establish the Klein-Gordon, Dirac, or Einstein equations. The declaration does not claim that all smooth functions have a continuous fourth derivative.

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