Encyclopedia Gravity Gravity Analysis Freudenthal Energy Limit Scaled Canonical Energy Witness Closed

ARTICLE 3 claims 3 theorems

Gravity Analysis Freudenthal Energy Limit Scaled Canonical Energy Witness Closed

A machine-checked theorem shows that a lattice version of a field's energy converges to its continuous counterpart, with an explicit error bound.

Verify this page

The discrete energy limit

In numerical analysis, when you approximate a continuous problem on a discrete grid, you want to know how fast the approximation improves as the grid gets finer. The declaration scaledCanonicalEnergy_witness_closed_form proves such a convergence result for a specific test case: the energy of a sine wave field on a three-dimensional periodic lattice.

The field in question is f(x,y,z) = sin(2πx), a simple wave along one axis. The lattice is the Freudenthal family, a standard triangulation of the cube into tetrahedra, with side length N. The theorem computes the normalized quadratic energy of this field on the lattice exactly, for every N greater than 2. The exact formula is A₀[0,0] · 2N² sin²(π/N), where A₀[0,0] = 1 + 2√2 + √3 is a fixed constant from the discretization stencil.

This closed form is not an estimate. It is a telescoping identity, proved in the machine-checked library of formal theorems, that the sum of shifted cosine terms vanishes. The key consequence is a convergence statement: as N grows, the lattice energy approaches the continuum energy ∫⟨∇f, A₀∇f⟩ = A₀[0,0] · 2π², with an error bounded by C/N², where C = A₀[0,0]·(2π)⁴/24 is an explicit constant independent of N. The rate C/N² is faster than the generic C/N bound that the theorem also establishes.

What this does not claim is broader. It does not assert that this convergence holds for all fields, nor that the Freudenthal triangulation is the unique or best discretization. It does not claim isotropy: the tensor A₀ is anisotropic, and only its first diagonal entry enters because the test field's gradient points along the first axis. The result is scoped to this specific witness field, and the framework's own status marks the general path-sum over triangulation classes as an open target, not a proved theorem.

THEOREM scaledCanonicalEnergy_witness_closed_form · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean
scaledCanonicalEnergy_witness_closed_form · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean:395 
/-- EXACT closed form of the normalized sampled energy for every `N > 2`:
`scaledCanonicalEnergy N (witnessSample N) = A₀[0,0] · 2N² sin²(π/N)`. -/
theorem scaledCanonicalEnergy_witness_closed_form (N : ℕ) [NeZero N] (hN : 2 < N) :
    scaledCanonicalEnergy N (witnessSample N) =
      stencilMomentTensor 0 0 *
        (2 * (N : ℝ) ^ (2 : ℕ) * Real.sin (Real.pi / N) ^ (2 : ℕ)) := by
  rw [scaledCanonicalEnergy_eq_scaled_stencil N hN, freudenthalStencilEnergy_witness N,
    sum_range_sq_sinDiff N hN]
  unfold stencilNormalization
  have hN0 : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  field_simp
  try ring
THEOREM witness_closed_form_dist · freudenthal_witness_energy_limit · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean
witness_closed_form_dist · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean:419 
/-- Quantitative distance of the closed form from the continuum target:
`|A₀[0,0]·2N²sin²(π/N) − continuumTarget| ≤ rateConstant/N²`, consuming the
Phase-2a toolkit bound `discrete_sine_eigenvalue_expansion` at wavenumber 1.
The achieved rate is `1/N²`, strictly better than the demanded `1/N`. -/
theorem witness_closed_form_dist (N : ℕ) (hN : 3 ≤ N) :
    |stencilMomentTensor 0 0 *
        (2 * (N : ℝ) ^ (2 : ℕ) * Real.sin (Real.pi / N) ^ (2 : ℕ)) -
      continuumTarget| ≤ rateConstant / (N : ℝ) ^ (2 : ℕ) := by
  have hA : 0 ≤ stencilMomentTensor 0 0 := le_of_lt (stencilMomentTensor_diag_pos 0)
  have hexp := discrete_sine_eigenvalue_expansion 1 N (by omega)
  simp only [Nat.cast_one, mul_one] at hexp
  have hkey : stencilMomentTensor 0 0 *
      (2 * (N : ℝ) ^ (2 : ℕ) * Real.sin (Real.pi / N) ^ (2 : ℕ)) - continuumTarget =
      (stencilMomentTensor 0 0 / 2) *
        (4 * (N : ℝ) ^ 2 * Real.sin (Real.pi / (N : ℝ)) ^ 2 - (2 * Real.pi) ^ 2) := by
    unfold continuumTarget
    ring
  rw [hkey, abs_mul, abs_of_nonneg (div_nonneg hA (by norm_num))]
  calc (stencilMomentTensor 0 0 / 2) *
        |4 * (N : ℝ) ^ 2 * Real.sin (Real.pi / (N : ℝ)) ^ 2 - (2 * Real.pi) ^ 2|
      ≤ (stencilMomentTensor 0 0 / 2) * ((2 * Real.pi) ^ 4 / 12 / (N : ℝ) ^ 2) :=
        mul_le_mul_of_nonneg_left hexp (div_nonneg hA (by norm_num))
    _ = rateConstant / (N : ℝ) ^ (2 : ℕ) := by
        unfold rateConstant
        ring
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 continuumTarget_pos · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean
continuumTarget_pos · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean:134 
/-- Gate (vi): the continuum target is strictly positive (nonzero limit;
this witness is not in the `0 = 0` trap). -/
theorem continuumTarget_pos : 0 < continuumTarget := by
  unfold continuumTarget
  have hpi : 0 < Real.pi := Real.pi_pos
  exact mul_pos (stencilMomentTensor_diag_pos 0) (by positivity)

What this page does not claim

The convergence result applies to all fields, not just the sine wave witness field. The Freudenthal triangulation is the unique or optimal discretization for this problem. The energy tensor A₀ is isotropic; only its first diagonal entry is used here.

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