Encyclopedia Foundation Foundation Continuum Limit Jcost Quadratic Leading

ARTICLE 5 claims 5 theorems

Foundation Continuum Limit Jcost Quadratic Leading

A small perturbation of the recognition cost behaves like a parabola, and that simple fact is what lets a discrete ledger produce smooth, continuous physics.

Verify this page

The quadratic approximation

The cost function in Recognition Science measures how expensive it is for the universe to recognize a change. For small changes, that cost is almost exactly a parabola: the square of the change, divided by two. The formal statement, jcost_quadratic_leading, says that if the change ε is smaller than 1 in absolute value, then the true cost differs from ε²/2 by at most ε⁴/20. In plain terms, the error shrinks as the fourth power of the change, so for tiny perturbations the quadratic term dominates completely.

This is not a coincidence of the framework. The cost function is forced by five plain conditions, and one of them, the composition law, pins down its shape. The result that J(exp(t)) = cosh(t) − 1, with Taylor expansion t²/2 + t⁴/24 + …, is a theorem in the machine-checked library of formal theorems. The quadratic leading term is therefore a derived property, not an assumption.

Why does this matter? On a discrete lattice, a quadratic cost produces the discrete Laplacian, the sum of second differences. In the continuum limit, as the lattice spacing goes to zero, that discrete Laplacian becomes the continuous Laplacian ∇². And the continuous Laplacian is the spatial part of the Klein-Gordon equation, the relativistic wave equation for a scalar field. So the chain is: discrete cost → quadratic approximation → lattice Laplacian → continuous Laplacian → Klein-Gordon structure. The framework proves each link in that chain as a theorem, with the mass term emerging from the curvature of the cost at its minimum.

In Recognition Science, this is the bridge from the discrete ledger to smooth physics. The framework models the universe as a lattice of discrete events, and this theorem shows how a continuous differential equation can emerge from that discreteness in the long-wavelength limit. The result also places the system in the Gaussian universality class, meaning that at large scales the details of the discrete dynamics wash out and only the quadratic term survives.

What the theorem does not claim is just as important. It does not say that the full cost function is quadratic; it only bounds the error for small perturbations. It does not derive the Klein-Gordon equation from first principles; it shows that the continuum limit has Klein-Gordon form, with mass and speed set to 1 in the framework's units. And it does not prove that the physical universe is a lattice; that is a modeling choice, not a theorem. The theorem is a precise statement about the cost function's local behavior, and everything else is built on top of it.

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 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
THEOREM 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 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

What this page does not claim

The full cost function is not quadratic; the theorem only bounds the error for small perturbations. The Klein-Gordon equation is not derived from first principles; only its structure is shown to emerge in the continuum limit. The physical universe is not proven to be a lattice; that is a modeling choice, not a theorem.

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