Encyclopedia Gravity Gravity Analysis Freudenthal Energy Limit Freudenthal Stencil Energy Witness

ARTICLE 5 claims 5 theorems

Gravity Analysis Freudenthal Energy Limit Freudenthal Stencil Energy Witness

A machine-checked theorem shows that a simple sine wave, sampled on a periodic lattice, has a lattice energy that converges to a known continuum value as the lattice refines.

Verify this page

The witness energy identity

The declaration freudenthalStencilEnergy_witness is a theorem in the framework's machine-checked library of formal theorems. It establishes an exact identity for a specific test function, called the witness field, on a family of periodic lattices known as the Freudenthal family. The witness field is the smooth function f(x,y,z) = sin(2πx), a single sine wave along the first coordinate axis. The theorem states that the stencil energy of this field, sampled onto a lattice with N points per side, equals N² times a constant times a sum of squared differences of the sine wave between neighboring lattice points.

The identity is not an approximation. The theorem proves an exact equality for every lattice size N greater than 2. The constant that appears is the (0,0) entry of a fixed moment tensor, with value 1 + 2√2 + √3. The sum of squared differences is a telescoping series, which the library evaluates exactly using a trigonometric identity. This closed form is the foundation for the limit result: as N grows, the scaled lattice energy approaches the continuum energy of the field, which is the integral over the unit cube of the gradient contracted with the moment tensor.

The theorem's role is to provide a concrete, checkable instance of a general principle: that a discrete lattice energy can converge to a continuum energy in a controlled way. The rate of convergence is also proved, with an explicit constant independent of N. The achieved rate is actually 1/N², better than the generic 1/N bound. This is a precise statement about a specific test case, not a claim about all fields or all lattices.

In Recognition Science, this result is part of a larger campaign to develop the continuum limit of a quadratic energy on the Freudenthal family. The framework models physical structure through a discrete record of events, and this theorem is a step toward showing that a continuum description can emerge from such a discrete starting point. However, the theorem itself is scoped: it concerns only the fixed sine wave witness field, not general fields. The framework's broader claim that a path-sum over triangulations yields a quantum gravity theory remains an open target, with a flag that is explicitly red.

The theorem does not claim isotropy. The continuum energy form is anisotropic, with a moment tensor A₀ = (1+√2)I + (√2+√3)J. The witness field's gradient points along the first axis, so only the diagonal entry of the tensor enters the target value. No claim is made that the energy is rotationally invariant. The theorem also does not establish the full continuum limit for arbitrary fields; that would require a measure-weighted sum over inequivalent triangulation classes, which is not yet proved.

THEOREM freudenthalStencilEnergy_witness · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean
freudenthalStencilEnergy_witness · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean:352 
/-- Aggregation of the per-vertex stencil over the `N³` vertex lattice: the
two free coordinates contribute a factor `N²`. -/
theorem freudenthalStencilEnergy_witness (N : ℕ) [NeZero N] :
    freudenthalStencilEnergy N (witnessSample N) =
      (N : ℝ) ^ (2 : ℕ) * (stencilMomentTensor 0 0 *
        ∑ k ∈ Finset.range N,
          (Real.sin (2 * Real.pi * ((k : ℝ) + 1) / N) -
            Real.sin (2 * Real.pi * (k : ℝ) / N)) ^ (2 : ℕ)) := by
  unfold freudenthalStencilEnergy
  rw [Fintype.sum_prod_type]
  calc (∑ a : Fin N, ∑ bc : Fin N × Fin N, ∑ d : Fin 7,
        stencilWeight d *
          (witnessSample N (shiftVertex N (a, bc) d) - witnessSample N (a, bc)) ^ (2 : ℕ))
      = ∑ a : Fin N, ∑ _bc : Fin N × Fin N,
          stencilMomentTensor 0 0 *
            (Real.sin (2 * Real.pi * ((a.val : ℝ) + 1) / N) -
              Real.sin (2 * Real.pi * (a.val : ℝ) / N)) ^ (2 : ℕ) :=
        Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun bc _ =>
          stencil_inner_sum_witness N (a, bc)
    _ = ∑ a : Fin N, ((N : ℝ) * (N : ℝ)) *
          (stencilMomentTensor 0 0 *
            (Real.sin (2 * Real.pi * ((a.val : ℝ) + 1) / N) -
              Real.sin (2 * Real.pi * (a.val : ℝ) / N)) ^ (2 : ℕ)) := by
        refine Finset.sum_congr rfl fun a _ => ?_
        rw [Finset.sum_const, Finset.card_univ, Fintype.card_prod, Fintype.card_fin,
          nsmul_eq_mul]
        push_cast
        ring
    _ = (N : ℝ) ^ (2 : ℕ) * (stencilMomentTensor 0 0 *
          ∑ a : Fin N,
            (Real.sin (2 * Real.pi * ((a.val : ℝ) + 1) / N) -
              Real.sin (2 * Real.pi * (a.val : ℝ) / N)) ^ (2 : ℕ)) := by
        rw [Finset.mul_sum, Finset.mul_sum]
        refine Finset.sum_congr rfl fun a _ => ?_
        ring
    _ = (N : ℝ) ^ (2 : ℕ) * (stencilMomentTensor 0 0 *
          ∑ k ∈ Finset.range N,
            (Real.sin (2 * Real.pi * ((k : ℝ) + 1) / N) -
              Real.sin (2 * Real.pi * (k : ℝ) / N)) ^ (2 : ℕ)) := by
        rw [Fin.sum_univ_eq_sum_range
          (fun k : ℕ => (Real.sin (2 * Real.pi * ((k : ℝ) + 1) / N) -
            Real.sin (2 * Real.pi * (k : ℝ) / N)) ^ (2 : ℕ)) N]
THEOREM freudenthalStencilEnergy_witness · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean
freudenthalStencilEnergy_witness · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean:352 
/-- Aggregation of the per-vertex stencil over the `N³` vertex lattice: the
two free coordinates contribute a factor `N²`. -/
theorem freudenthalStencilEnergy_witness (N : ℕ) [NeZero N] :
    freudenthalStencilEnergy N (witnessSample N) =
      (N : ℝ) ^ (2 : ℕ) * (stencilMomentTensor 0 0 *
        ∑ k ∈ Finset.range N,
          (Real.sin (2 * Real.pi * ((k : ℝ) + 1) / N) -
            Real.sin (2 * Real.pi * (k : ℝ) / N)) ^ (2 : ℕ)) := by
  unfold freudenthalStencilEnergy
  rw [Fintype.sum_prod_type]
  calc (∑ a : Fin N, ∑ bc : Fin N × Fin N, ∑ d : Fin 7,
        stencilWeight d *
          (witnessSample N (shiftVertex N (a, bc) d) - witnessSample N (a, bc)) ^ (2 : ℕ))
      = ∑ a : Fin N, ∑ _bc : Fin N × Fin N,
          stencilMomentTensor 0 0 *
            (Real.sin (2 * Real.pi * ((a.val : ℝ) + 1) / N) -
              Real.sin (2 * Real.pi * (a.val : ℝ) / N)) ^ (2 : ℕ) :=
        Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun bc _ =>
          stencil_inner_sum_witness N (a, bc)
    _ = ∑ a : Fin N, ((N : ℝ) * (N : ℝ)) *
          (stencilMomentTensor 0 0 *
            (Real.sin (2 * Real.pi * ((a.val : ℝ) + 1) / N) -
              Real.sin (2 * Real.pi * (a.val : ℝ) / N)) ^ (2 : ℕ)) := by
        refine Finset.sum_congr rfl fun a _ => ?_
        rw [Finset.sum_const, Finset.card_univ, Fintype.card_prod, Fintype.card_fin,
          nsmul_eq_mul]
        push_cast
        ring
    _ = (N : ℝ) ^ (2 : ℕ) * (stencilMomentTensor 0 0 *
          ∑ a : Fin N,
            (Real.sin (2 * Real.pi * ((a.val : ℝ) + 1) / N) -
              Real.sin (2 * Real.pi * (a.val : ℝ) / N)) ^ (2 : ℕ)) := by
        rw [Finset.mul_sum, Finset.mul_sum]
        refine Finset.sum_congr rfl fun a _ => ?_
        ring
    _ = (N : ℝ) ^ (2 : ℕ) * (stencilMomentTensor 0 0 *
          ∑ k ∈ Finset.range N,
            (Real.sin (2 * Real.pi * ((k : ℝ) + 1) / N) -
              Real.sin (2 * Real.pi * (k : ℝ) / N)) ^ (2 : ℕ)) := by
        rw [Fin.sum_univ_eq_sum_range
          (fun k : ℕ => (Real.sin (2 * Real.pi * ((k : ℝ) + 1) / N) -
            Real.sin (2 * Real.pi * (k : ℝ) / N)) ^ (2 : ℕ)) N]
THEOREM freudenthal_witness_energy_limit · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean
freudenthal_witness_energy_limit · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean:463 
/-- Panel-locked stage-2 observable (existential form): there is a constant
`C` and a threshold `N₀` with
`∀ N ≥ N₀, |scaledCanonicalEnergy N (sample N f) − ∫⟨∇f, A₀∇f⟩| ≤ C/N`
for the fixed nonconstant witness `f = witnessField`; the witnesses are the
explicit `rateConstant` and `N₀ = 3`. -/
theorem freudenthal_witness_energy_limit :
    ∃ C : ℝ, ∃ N₀ : ℕ, ∀ (N : ℕ) [NeZero N], N₀ ≤ N →
      |scaledCanonicalEnergy N (sample N witnessField) - continuumTarget| ≤
        C / (N : ℝ) := by
  refine ⟨rateConstant, 3, ?_⟩
  intro N _ hN
  exact scaledCanonicalEnergy_witness_rate N hN
THEOREM scaledCanonicalEnergy_witness_rate · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean
scaledCanonicalEnergy_witness_rate · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean:445 
/-- Panel-locked stage-2 rate bound, explicit-constant form: for every
`N ≥ 3`,
`|scaledCanonicalEnergy N (sample N witnessField) − continuumTarget| ≤ rateConstant / N`,
with `rateConstant` independent of `N`. -/
theorem scaledCanonicalEnergy_witness_rate (N : ℕ) [NeZero N] (hN : 3 ≤ N) :
    |scaledCanonicalEnergy N (sample N witnessField) - continuumTarget| ≤
      rateConstant / (N : ℝ) := by
  have hN2 : 2 < N := hN
  have hs : sample N witnessField = witnessSample N :=
    funext fun x => sample_witnessField N x
  rw [hs, scaledCanonicalEnergy_witness_closed_form N hN2]
  refine le_trans (witness_closed_form_dist N hN) ?_
  have hN1 : (1 : ℝ) ≤ (N : ℝ) := by exact_mod_cast (by omega : 1 ≤ N)
  have hNpos : (0 : ℝ) < (N : ℝ) := by linarith
  have hsq : (N : ℝ) ≤ (N : ℝ) ^ (2 : ℕ) := by nlinarith
  have hrc : 0 ≤ rateConstant := rateConstant_nonneg
  gcongr
THEOREM continuumTarget · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean
continuumTarget · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean:127 
/-- The continuum target `∫_{[0,1]³} ⟨∇f, A₀ ∇f⟩ = A₀[0,0] · 2π²`, defined
INDEPENDENTLY of the lattice computation as an exact constant (by-hand cube
integral; the integrand depends only on the first coordinate, so the cube
integral equals the interval integral certified in
`integral_witness_energy_density`). -/
def continuumTarget : ℝ := stencilMomentTensor 0 0 * (2 * Real.pi ^ (2 : ℕ))

What this page does not claim

The theorem does not prove the continuum limit for arbitrary fields, only for the specific sine wave witness. The theorem does not establish isotropy of the energy; the moment tensor is explicitly anisotropic. The theorem does not imply the full path-sum quantum gravity theory, whose pillar-2 flag remains red.

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/Gravity/Analysis/FreudenthalEnergyLimit.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