Encyclopedia Foundation Foundation Continuum Limit Jcost Gives Laplacian Structure

ARTICLE 3 claims 3 theorems

Foundation Continuum Limit Jcost Gives Laplacian Structure

A discrete cost function, expanded to second order, becomes the familiar Laplacian operator that governs smooth diffusion and wave motion.

Verify this page

The lattice Laplacian

The Laplacian is the operator that measures how a quantity at a point differs from its immediate surroundings. In physics it appears in the diffusion equation, the wave equation, and the Schrödinger equation. On a discrete lattice, the natural analogue compares a point with its nearest neighbors: the lattice Laplacian of a field f at a site x is the sum over each direction k of f at the two neighbors minus twice f at x. This is the standard finite-difference approximation taught in numerical analysis.

Recognition Science starts from a discrete ledger: a record of events on a lattice, where each event has a recognition cost. The framework's cost function J has a forced form, and its logarithm has a Taylor expansion: for a small step ε, J(log(1+ε)) equals ε²/2 plus a correction no larger than ε⁴/20. The leading quadratic term is what matters for small perturbations. A theorem in the framework's machine-checked library, jcost_gives_laplacian_structure, proves that the total neighbor cost of a field, summed over all directions, is within a quartic error of the sum of squared differences between neighbors, which is exactly the quadratic form that produces the lattice Laplacian.

This is a statement about the discrete lattice itself. The theorem holds for any dimension D and any field whose neighbor differences are small. It does not by itself take a continuum limit. A separate result, continuum_limit_second_order, shows that the lattice Laplacian, scaled by the square of the lattice spacing, converges to the continuous Laplacian ∇² for smooth functions. Together they form the bridge the framework calls the continuum limit: discrete cost dynamics on a lattice, expanded to second order, yield the familiar smooth operator.

In Recognition Science, this bridge is how the framework claims smooth physics emerges from a discrete ledger. The framework's library also records a dictionary mapping lattice concepts to continuum ones, and a structure named KleinGordonStructure that packages a mass squared and a speed, both positive, as the form of the continuum limit. The claim is structural: the discrete cost, at leading order, has the same shape as the lattice Laplacian, and the lattice Laplacian has the same shape as the continuous one. What the framework does not claim is that this theorem alone derives the Klein-Gordon, Dirac, or Einstein equations. Those derivations, if they exist, require further steps and further theorems. The theorem here is precise and narrow: it identifies the quadratic leading order of the cost with the lattice Laplacian, and it bounds the error.

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 jcost_quadratic_leading · IndisputableMonolith/Foundation/ContinuumLimit.lean
jcost_quadratic_leading · IndisputableMonolith/Foundation/ContinuumLimit.lean:65 
/-- J-cost in the small-perturbation regime is quadratic to leading order.
    This is the bridge from discrete to continuous: quadratic costs on
    lattices give Laplacians. -/
theorem jcost_quadratic_leading (ε : ℝ) (hε : |ε| < 1) :
    |J_log ε - ε ^ 2 / 2| ≤ |ε| ^ 4 / 20 :=
  J_log_quadratic_approx ε hε
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

This theorem alone does not derive the Klein-Gordon, Dirac, or Einstein equations. The theorem does not assert that the continuum limit is physically realized, only that the mathematical limit exists under smoothness conditions. The quartic error bound does not imply the cost is exactly quadratic for any finite step size.

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