Encyclopedia Foundation Foundation Continuum Limit Continuum Limit Second Order

ARTICLE 4 claims 3 theorems 1 model

Foundation Continuum Limit Continuum Limit Second Order

A discrete world can look smooth from afar: the framework proves that small steps on a lattice reproduce the familiar second derivative of continuous calculus.

Verify this page

The smooth limit

In ordinary calculus, the second derivative measures how a function bends. For a smooth function f, the standard formula (f(x+a) + f(x-a) - 2f(x)) / a² approaches the second derivative as the step a shrinks to zero. The Recognition Science framework proves a precise version of this fact in its machine-checked library of formal theorems. The theorem continuum_limit_second_order states that for any four-times differentiable function, the error in this finite-difference approximation is bounded by a constant times a². The constant depends on the function's fourth derivative, and the bound holds for any nonzero step a.

This result matters because the framework's fundamental dynamics are discrete. The ledger, a discrete record of events, updates in ticks on a lattice of integer points. Physical fields, however, are described by smooth differential equations. The theorem bridges that gap: it shows that the discrete Laplacian, built from sums over neighboring lattice points, converges to the continuous Laplacian ∇² in the long-wavelength limit. The proof uses a Taylor expansion of the cost function J(exp(t)) = cosh(t) - 1, whose leading quadratic term t²/2 produces the lattice Laplacian. The theorem is a formal statement about real functions; it does not by itself construct a physical theory.

The framework goes further and assembles these pieces into a structure it calls the Klein-Gordon form, with a positive mass-squared and speed. The declaration rs_klein_gordon sets both mass-squared and speed to 1 in the framework's natural units. This is a definitional choice, not a derivation. The framework also proves that its cost system falls into the Gaussian universality class, meaning its large-scale fluctuations match those of a simple quadratic model. The theorem continuum_limit_certificate bundles the key properties: quadratic leading order, symmetry, zero at the vacuum, and linearity of the lattice Laplacian.

What the declaration does not claim is equally important. It does not prove that the discrete dynamics actually generate the Klein-Gordon, Dirac, or Einstein equations; those steps are documented as targets, not theorems. It does not assign a numerical value to the mass; the mass-squared is set to 1 by definition. And it does not claim that the continuum limit is unique or that the discrete theory is the only one producing it. The theorem is a rigorous statement about approximation of derivatives, a necessary ingredient for any claim that smooth physics emerges from discrete rules.

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
THEOREM rs_is_gaussian · IndisputableMonolith/Foundation/ContinuumLimit.lean
rs_is_gaussian · IndisputableMonolith/Foundation/ContinuumLimit.lean:483 
/-- The RS J-cost system satisfies Gaussian universality. -/
theorem rs_is_gaussian : GaussianUniversality where
  leading_order_quadratic := J_log_quadratic_approx
  higher_order_quartic := J_log_quadratic_approx
MODEL rs_klein_gordon · IndisputableMonolith/Foundation/ContinuumLimit.lean
rs_klein_gordon · IndisputableMonolith/Foundation/ContinuumLimit.lean:521 
/-- The RS Klein-Gordon structure. -/
noncomputable def rs_klein_gordon : KleinGordonStructure where
  mass_squared := 1
  speed := 1
  mass_from_jcost := by norm_num
  speed_from_lattice := by norm_num
THEOREM continuum_limit_certificate · IndisputableMonolith/Foundation/ContinuumLimit.lean
continuum_limit_certificate · IndisputableMonolith/Foundation/ContinuumLimit.lean:635 
/-- **F-014 CERTIFICATE: Continuum Limit**

    The discrete J-cost dynamics on ℤ³ produces continuous physics:

    1. QUADRATIC: J(exp(ε)) = ε²/2 + O(ε⁴) (leading order is quadratic)
    2. LAPLACIAN: Quadratic cost on lattice = lattice Laplacian
    3. LIMIT: Lattice Laplacian → continuous ∇² (standard finite differences)
    4. KLEIN-GORDON: The continuum equation is (□ + m²)φ = 0
    5. UNIVERSALITY: The Gaussian universality class is selected
    6. UNIQUENESS: J = cosh − 1 fixes all Taylor coefficients (no free couplings)
    7. CPT: The even symmetry J(t) = J(−t) gives CPT invariance

    The continuum limit is NOT a choice. It is FORCED by:
    - The RCL uniquely determines J = cosh − 1
    - cosh − 1 has Taylor expansion t²/2 + t⁴/24 + ···
    - t²/2 on a lattice gives the Laplacian
    - The Laplacian in the continuum limit gives ∇²
    - ∇² + mass term = Klein-Gordon = free scalar field theory
    - Higher-order terms give interactions (φ⁴ from t⁴/24) -/
theorem continuum_limit_certificate :
    -- 1. Quadratic leading order
    (∀ ε : ℝ, |ε| < 1 → |J_log ε - ε ^ 2 / 2| ≤ |ε| ^ 4 / 20) ∧
    -- 2. CPT symmetry
    (∀ t : ℝ, J_log (-t) = J_log t) ∧
    -- 3. Vacuum at t = 0
    (J_log 0 = 0) ∧
    -- 4. Lattice Laplacian vanishes on constants
    (∀ (D : ℕ) (c : ℝ) (x : Fin D → ℤ),
      lattice_laplacian (fun _ => c) x = 0) ∧
    -- 5. Lattice Laplacian is linear
    (∀ (D : ℕ) (f g : LatticeField D) (x : Fin D → ℤ),
      lattice_laplacian (fun y => f y + g y) x =
      lattice_laplacian f x + lattice_laplacian g x) :=
  ⟨J_log_quadratic_approx,
   J_log_symmetric,
   J_log_zero,
   fun D c x => lattice_laplacian_const c x,
   fun D f g x => lattice_laplacian_add f g x⟩

What this page does not claim

The theorem does not prove that the discrete dynamics generate the Einstein equations; that step remains a documented target. The declaration does not assign a numerical value to the particle mass; the mass-squared is set to 1 by definition. The theorem does not claim the continuum limit is unique or that the discrete theory is the only one producing it.

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