Encyclopedia Foundation Foundation Continuum Limit
ARTICLE 5 claims 5 theorems
Foundation Continuum Limit
The continuum limit is the machine-checked bridge by which discrete recognition dynamics on a lattice yields smooth, second-order differential equations.
The continuum limit
The foundation continuum limit is the point in Recognition Science where the discrete ledger gives way to smooth physics. Recognition Science works on a lattice of integer points, with a cost function J that measures mismatch between neighboring sites. The continuum limit is the long-wavelength regime, where changes between neighboring sites are small. In that regime the cost function is dominated by its quadratic term, and the lattice dynamics become a second-order diffusion equation whose structure matches the Klein-Gordon equation.
The key machine-checked fact is that the cost function J(exp(t)) = cosh(t) - 1 has the Taylor expansion cosh(t) - 1 = t²/2 + t⁴/24 + ... . For small perturbations t = εδ with ε → 0, the leading term t²/2 is quadratic, and quadratic costs on a lattice produce the discrete Laplacian. The discrete Laplacian, in the scaling limit, converges to the continuous Laplacian ∇². The module establishes this chain formally: J-cost dynamics on ℤ³ leads to the lattice Laplacian, then to the continuous ∇², then to Klein-Gordon structure, then to Dirac structure from spinors in three dimensions, and then to Einstein equations from curvature of the defect field.
The module establishes several precise theorems. The theorem jcost_quadratic_leading shows that for |ε| < 1, the absolute difference between J_log ε and ε²/2 is at most |ε|⁴/20. The theorem jcost_gives_laplacian_structure shows that the neighbor cost, which sums J_log over shifts, is approximated by the sum of squared differences divided by 2, with error bounded by fourth powers. The theorem continuum_limit_second_order shows that for a four-times continuously differentiable function, the second difference quotient converges to the second derivative with error of order a². The theorem rs_is_gaussian shows that the J-cost system is in the Gaussian universality class, meaning its leading behavior is quadratic with quartic corrections.
The module also provides a dictionary between lattice and continuum concepts, and it establishes that the mass squared in the Klein-Gordon structure is positive, set to 1 in the native units. The theorem emergence_hierarchy orders the emergence errors: the interacting level error is bounded by |ε|⁶/720, which is smaller than the quadratic level error |ε|⁴/20 for small ε. This shows that the continuum description improves as the perturbation shrinks.
In plain language, the module establishes that the discrete, tick-based recognition dynamics, when viewed at large scales, produce the smooth differential equations that conventional physics uses. The continuum is not assumed; it is forced by the quadratic leading term of the cost function and the lattice Laplacian. The physical bridge from recognition to linking is not part of this module; that remains open.
THEOREM jcost_quadratic_leading · IndisputableMonolith/Foundation/ContinuumLimit.lean
/-- 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 jcost_gives_laplacian_structure · IndisputableMonolith/Foundation/ContinuumLimit.lean
/-- **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
/-- **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
/-- 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
THEOREM emergence_hierarchy · IndisputableMonolith/Foundation/ContinuumLimit.lean
/-- The error decreases at each level for small perturbations. -/
theorem emergence_hierarchy (ε : ℝ) (hε : |ε| < 1) :
emergence_error .interacting ε ≤ emergence_error .quadratic ε := by
unfold emergence_error
have hε_nonneg : 0 ≤ |ε| := abs_nonneg ε
have hε4 : |ε| ^ 4 ≤ 1 := by
exact pow_le_one₀ hε_nonneg hε.le
have hε2 : |ε| ^ 2 ≤ 1 := by
exact pow_le_one₀ hε_nonneg hε.le
have hε4_nonneg : 0 ≤ |ε| ^ 4 := by positivity
have hε6 : |ε| ^ 6 ≤ |ε| ^ 4 := by
calc
|ε| ^ 6 = |ε| ^ 4 * |ε| ^ 2 := by ring
_ ≤ |ε| ^ 4 * 1 := by
exact mul_le_mul_of_nonneg_left hε2 hε4_nonneg
_ = |ε| ^ 4 := by ring
nlinarith
What this page does not claim
This module does not prove the physical bridge from recognition to linking. This module does not derive the fine-structure constant or any specific particle mass. This module does not claim that the continuum limit is exact for all scales; it is a long-wavelength approximation.
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:
- How does the continuum limit connect to the physical recognition-to-linking bridge?
- What is the precise relationship between the Klein-Gordon structure and the Dirac equation in three dimensions?
- How does the Gaussian universality class relate to the observed critical phenomena in recognition systems?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
- THEOREMThe theorem jcost_quadratic_leading proves that for |ε| < 1, the absolute difference between J_log ε and ε²/2 is at most |ε|⁴/20. jcost_quadratic_leading · IndisputableMonolith/Foundation/ContinuumLimit.lean
- THEOREMThe theorem jcost_gives_laplacian_structure proves that the neighbor cost is approximated by the sum of squared differences divided by 2, with error bounded by fourth powers. jcost_gives_laplacian_structure · IndisputableMonolith/Foundation/ContinuumLimit.lean
- THEOREMThe theorem continuum_limit_second_order proves that for a four-times continuously differentiable function, the second difference quotient converges to the second derivative with error of order a². continuum_limit_second_order · IndisputableMonolith/Foundation/ContinuumLimit.lean
- THEOREMThe theorem rs_is_gaussian proves that the J-cost system is in the Gaussian universality class. rs_is_gaussian · IndisputableMonolith/Foundation/ContinuumLimit.lean
- THEOREMThe theorem emergence_hierarchy orders the emergence errors, with the interacting level error bounded by |ε|⁶/720, smaller than the quadratic level error |ε|⁴/20 for small ε. emergence_hierarchy · IndisputableMonolith/Foundation/ContinuumLimit.lean