Encyclopedia Gravity Gravity Analysis Freudenthal Energy Limit Freudenthal Witness Energy Limit

ARTICLE 4 claims 4 theorems

Gravity Analysis Freudenthal Energy Limit Freudenthal Witness Energy Limit

A machine-checked proof shows that a discrete lattice energy converges to a continuous integral at a known rate for one specific test field.

Verify this page

The Freudenthal energy limit

The Freudenthal energy limit is a convergence result in numerical analysis. It compares two ways of computing the energy of a wave-like field on a three-dimensional grid. The first way samples the field at grid points and applies a local stencil, a fixed pattern of weights, to approximate derivatives. The second way treats the field as a smooth function and integrates its gradient energy exactly over a unit cube. The declaration freudenthal_witness_energy_limit proves that, as the grid becomes finer, the discrete stencil energy approaches the continuous integral energy, and it bounds the difference by a constant divided by the grid size.

The proof is not a general statement about all fields. It concerns one fixed test field, the sine function sin(2πx), which varies only along the first coordinate. For this field, the module derives an exact closed form for the scaled stencil energy at every grid size N greater than 2. That closed form, scaledCanonicalEnergy_witness_closed_form, equals A₀[0,0] · 2N² sin²(π/N), where A₀[0,0] = 1 + 2√2 + √3 is a constant coming from the stencil's moment tensor. The continuous target, defined independently of the lattice, is the integral of the gradient energy density, which evaluates to A₀[0,0] · 2π². The difference between the two is bounded by rateConstant / N, with rateConstant = A₀[0,0] · (2π)⁴ / 24, and the achieved rate is actually C/N².

This result is part of a larger campaign. The module is scoped as a partial step toward a continuum limit of a quadratic energy on a family of triangulations. The panel-mandated scope statement is explicit: the path-sum flag, which would require summing over inequivalent triangulation classes with a measure, remains red. The theorem here does not establish that the energy limit exists for arbitrary fields, nor does it prove isotropy of the continuum form. The continuum quadratic form is anisotropic, with A₀ = (1+√2)I + (√2+√3)J, and the witness field's gradient points along the first axis, so only the diagonal entry enters the target. No claim is made about other directions or other fields.

What the declaration does establish, with full machine-checked rigor, is a concrete instance of convergence: for this sine field, the discrete stencil energy converges to the continuous integral at a known rate, with an explicit constant. This is a sanity check on the discretization scheme, not a proof of the full continuum limit. The value lies in the exactness: the closed form is a telescoping identity, not an estimate, and the continuum target is strictly positive, avoiding a trivial zero-equals-zero trap. The result composes two toolkit pieces, the discrete sine eigenvalue expansion and a uniform bound, verifying that they work together.

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_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 continuumTarget_pos · integral_witness_energy_density · 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)
integral_witness_energy_density · IndisputableMonolith/Gravity/Analysis/FreudenthalEnergyLimit.lean:185 
/-- Lean-checked evaluation of the continuum target: the interval integral
of the anisotropic energy density is exactly `continuumTarget`. -/
theorem integral_witness_energy_density :
    (∫ t in (0:ℝ)..1,
        ∑ i : Fin 3, ∑ j : Fin 3,
          stencilMomentTensor i j * witnessGrad t i * witnessGrad t j) =
      continuumTarget := by
  have hpt : (fun t : ℝ =>
      ∑ i : Fin 3, ∑ j : Fin 3,
        stencilMomentTensor i j * witnessGrad t i * witnessGrad t j) =
      fun t : ℝ =>
        (stencilMomentTensor 0 0 * (2 * Real.pi) ^ (2 : ℕ)) *
          Real.cos (2 * Real.pi * t) ^ (2 : ℕ) := by
    funext t
    rw [witness_energy_density_eq]
    ring
  rw [hpt, intervalIntegral.integral_const_mul, integral_cos_sq_two_pi]
  unfold continuumTarget
  ring
THEOREM scaledCanonicalEnergy_witness_rate · witness_closed_form_dist · 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
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

What this page does not claim

The theorem does not establish convergence for arbitrary fields, only for the fixed sine test field. It does not prove isotropy of the continuum energy form; the form is explicitly anisotropic. It does not complete the full continuum limit, which requires summing over inequivalent triangulation classes with a measure.

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