Encyclopedia Gravity Gravity Analysis Freudenthal Energy Limit Freudenthal Witness Energy Rate Integr

ARTICLE 3 claims 3 theorems

Gravity Analysis Freudenthal Energy Limit Freudenthal Witness Energy Rate Integr

A machine-checked proof shows that a discrete energy computed on a lattice converges to a continuous integral at a known rate, with an explicit error bound.

Verify this page

The energy rate integral

In numerical analysis, a common question is how well a discrete approximation matches a continuous ideal. The declaration freudenthal_witness_energy_rate_integral_form answers this for a specific case. It considers a smooth test function, f(x,y,z) = sin(2πx), sampled on a periodic lattice of size N. The theorem states that the difference between the lattice energy and the integral of the energy density is at most a constant divided by N, for all N at least 3.

The energy in question is a quadratic form built from a stencil, a fixed pattern of weights that approximates derivatives. The integral is the continuum energy, computed by hand as the integral over the unit cube of the gradient dotted with a fixed matrix A₀. The theorem proves that the lattice energy, properly normalized, converges to this integral. The rate of convergence is explicit: the error is bounded by C/N, where C is a specific constant, A₀[0,0]·(2π)⁴/24. In fact, the proof shows the error is even smaller, on the order of 1/N².

This is a theorem in the strict sense. It is proved in a machine-checked library of formal theorems, meaning every step is verified by a computer. The proof uses exact identities, not estimates. For example, a sum of cosines vanishes exactly, and the integral of cos²(2πt) from 0 to 1 is exactly 1/2. The theorem is scoped: it applies to this specific witness field and this specific lattice family. It does not claim that all energies converge, nor does it address the full path-sum of quantum gravity, which remains an open target.

THEOREM freudenthal_witness_energy_rate_integral_form · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean
freudenthal_witness_energy_rate_integral_form · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean:476 
/-- The same rate bound stated directly against the Lean-checked integral
of the anisotropic energy density (interval form of `∫⟨∇f, A₀∇f⟩`). -/
theorem freudenthal_witness_energy_rate_integral_form (N : ℕ) [NeZero N]
    (hN : 3 ≤ N) :
    |scaledCanonicalEnergy N (sample N witnessField) -
        ∫ t in (0:ℝ)..1,
          ∑ i : Fin 3, ∑ j : Fin 3,
            stencilMomentTensor i j * witnessGrad t i * witnessGrad t j| ≤
      rateConstant / (N : ℝ) := by
  rw [integral_witness_energy_density]
  exact scaledCanonicalEnergy_witness_rate N hN
THEOREM rateConstant · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean
rateConstant · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean:410 
/-- The explicit `N`-independent rate constant `C = A₀[0,0] · (2π)⁴ / 24`. -/
def rateConstant : ℝ := stencilMomentTensor 0 0 * (2 * Real.pi) ^ (4 : ℕ) / 24
THEOREM sum_cos_shifted_vanishes · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean
sum_cos_shifted_vanishes · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean:241 
/-- Telescoping vanishing of the equally spaced cosine sum
`Σ_{k<N} cos((4k+2)π/N) = 0` for `N > 2`
(via `2 sin(2π/N) cos((4k+2)π/N) = sin(4π(k+1)/N) − sin(4πk/N)`). -/
theorem sum_cos_shifted_vanishes (N : ℕ) (hN : 2 < N) :
    (∑ k ∈ Finset.range N, Real.cos ((4 * (k : ℝ) + 2) * Real.pi / N)) = 0 := by
  have hN0 : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  have hNpos : (0 : ℝ) < (N : ℝ) := by
    have : (2 : ℝ) < (N : ℝ) := by exact_mod_cast hN
    linarith
  have hNgt : (2 : ℝ) < (N : ℝ) := by exact_mod_cast hN
  have hs_pos : 0 < Real.sin (2 * Real.pi / N) := by
    apply Real.sin_pos_of_pos_of_lt_pi
    · positivity
    · rw [div_lt_iff₀ hNpos]
      nlinarith [Real.pi_pos]
  have hs2 : (2 : ℝ) * Real.sin (2 * Real.pi / N) ≠ 0 := by positivity
  have hkey : ∀ k : ℕ,
      2 * Real.sin (2 * Real.pi / N) * Real.cos ((4 * (k : ℝ) + 2) * Real.pi / N) =
        Real.sin (4 * Real.pi * (((k + 1 : ℕ)) : ℝ) / N) -
          Real.sin (4 * Real.pi * ((k : ℕ) : ℝ) / N) := by
    intro k
    rw [Real.sin_sub_sin]
    have h1 : (4 * Real.pi * (((k + 1 : ℕ)) : ℝ) / N - 4 * Real.pi * ((k : ℕ) : ℝ) / N) / 2 =
        2 * Real.pi / N := by
      push_cast
      field_simp
      try ring
    have h2 : (4 * Real.pi * (((k + 1 : ℕ)) : ℝ) / N + 4 * Real.pi * ((k : ℕ) : ℝ) / N) / 2 =
        (4 * (k : ℝ) + 2) * Real.pi / N := by
      push_cast
      field_simp
      try ring
    rw [h1, h2]
  have hend : Real.sin (4 * Real.pi * ((N : ℕ) : ℝ) / N) = 0 := by
    have harg : 4 * Real.pi * ((N : ℕ) : ℝ) / N = ((4 : ℕ) : ℝ) * Real.pi := by
      push_cast
      field_simp
      try ring
    rw [harg]
    exact Real.sin_nat_mul_pi 4
  have h2s : (2 * Real.sin (2 * Real.pi / N)) *
      (∑ k ∈ Finset.range N, Real.cos ((4 * (k : ℝ) + 2) * Real.pi / N)) = 0 := by
    rw [Finset.mul_sum]
    calc (∑ k ∈ Finset.range N,
          2 * Real.sin (2 * Real.pi / N) * Real.cos ((4 * (k : ℝ) + 2) * Real.pi / N))
        = ∑ k ∈ Finset.range N,
            (Real.sin (4 * Real.pi * (((k + 1 : ℕ)) : ℝ) / N) -
              Real.sin (4 * Real.pi * ((k : ℕ) : ℝ) / N)) :=
          Finset.sum_congr rfl fun k _ => hkey k
      _ = Real.sin (4 * Real.pi * ((N : ℕ) : ℝ) / N) -
            Real.sin (4 * Real.pi * ((0 : ℕ) : ℝ) / N) :=
          Finset.sum_range_sub (fun k : ℕ => Real.sin (4 * Real.pi * ((k : ℕ) : ℝ) / N)) N
      _ = 0 := by
          rw [hend]
          norm_num
  exact (mul_eq_zero.mp h2s).resolve_left hs2

What this page does not claim

No claim that the lattice energy converges to the integral for all possible fields or stencils. No claim that the full path-sum of quantum gravity is established; that remains an open target. No claim that the energy is isotropic; the matrix A₀ is explicitly anisotropic.

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