Gravity Analysis Freudenthal Energy Limit Witness Closed Form Tendsto

The continuum limit

In numerical analysis, a continuum limit is the behavior of a discrete approximation as the grid spacing goes to zero. The declaration witness_closed_form_tendsto proves, for a specific test field, that a certain discrete energy converges to a continuous integral as the lattice size N grows. The test field is f(x,y,z) = sin(2πx), a smooth wave along one axis. The discrete energy is a normalized quadratic form built from differences of this field on a periodic lattice; the continuous target is the integral of the squared gradient against a fixed tensor A₀ over the unit cube.

The proof is exact, not approximate. For every lattice size N greater than 2, the discrete energy equals A₀[0,0]·2N² sin²(π/N), a closed form derived from a telescoping trigonometric identity. The continuum target is independently defined as A₀[0,0]·2π². The theorem witness_closed_form_tendsto then states that the difference between these two expressions tends to zero as N goes to infinity. The rate is explicit: the error is bounded by a constant divided by N², where the constant is A₀[0,0]·(2π)⁴/24. This is stronger than the required O(1/N) bound, and it is achieved through a squeeze argument using the toolkit's eigenvalue expansion.

What this does not claim is broader than what it proves. The result is for one fixed test field, not for all fields. It does not establish that the discrete energy converges for arbitrary smooth functions, nor does it prove that the continuum limit of the full quantum gravity path sum exists. The framework's own scope statement marks the pillar-2 path-sum flag as red, meaning the measure-weighted sum over inequivalent triangulation classes is not yet defined. The theorem also does not claim isotropy: the tensor A₀ is anisotropic, and only its diagonal entry enters because the test field's gradient points along the first axis.

The practical consequence is a benchmark. The closed form and the explicit rate give a concrete, checkable instance where the discrete-to-continuum passage works exactly. This is a step toward validating the framework's gravity program, but it is a single witness, not a general proof. The framework models the continuum limit for this test field; it does not yet derive the full theory.

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

/-- 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 : ℕ))

/-- Qualitative limit of the closed-form energy sequence, re-derived from
the rate through the Phase-2a toolkit squeeze
`eigenvalue_limit_of_uniform_bound` (toolkit composition check). -/
theorem witness_closed_form_tendsto :
    Filter.Tendsto
      (fun N : ℕ => stencilMomentTensor 0 0 *
        (2 * (N : ℝ) ^ (2 : ℕ) * Real.sin (Real.pi / N) ^ (2 : ℕ)))
      Filter.atTop (nhds continuumTarget) :=
  eigenvalue_limit_of_uniform_bound _ continuumTarget rateConstant 3
    (fun N hN => witness_closed_form_dist N hN)

/-- 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 result holds only for the fixed test field sin(2πx), not for arbitrary fields. The full quantum gravity path sum is not defined; the pillar-2 flag remains red. No isotropy of the continuum quadratic form is claimed; only the diagonal entry A₀[0,0] enters the target.

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: