Gravity Analysis Freudenthal Energy Limit

The Freudenthal energy limit

The Freudenthal energy limit is a proved result about how a discrete approximation to a field's energy behaves as the lattice gets finer. The framework's machine-checked library of formal theorems establishes that, for a fixed smooth test field, the energy computed on a periodic lattice of side length N approaches a specific continuum value, and the error shrinks at least as fast as 1/N. The test field is f(x,y,z) = sin(2πx), a simple wave along one axis.

The lattice is the canonical Freudenthal family, a standard way to triangulate a cube periodically. The energy is a quadratic form built from a stencil, a fixed set of weights applied to differences between neighboring lattice points. The continuum target is the integral of the energy density, computed by hand as A₀[0,0]·2π², where A₀[0,0] = 1 + 2√2 + √3 is a constant from the stencil's moment tensor. The proof shows the discrete energy equals A₀[0,0]·2N²sin²(π/N) exactly for every N > 2, and this expression tends to the continuum target as N grows.

The rate of convergence is also explicit. The theorem states that for all N ≥ 3, the absolute difference between the scaled discrete energy and the continuum target is at most rateConstant/N, where rateConstant = A₀[0,0]·(2π)⁴/24. In fact, the achieved rate is better, C/N², because the closed-form expression converges quadratically. The qualitative limit is re-derived through a separate squeeze argument, confirming the two toolkit pieces compose correctly.

In Recognition Science, this result is part of a larger campaign to build a quantum gravity theory from first principles. The module is scoped as partial: it establishes the continuum limit for this one fixed witness field, not for all fields. The path-sum flag, which would require summing over all triangulation classes with a measure, remains red. The anisotropy note is inherited from stage 1: the continuum quadratic form is anisotropic, with A₀ = (1+√2)I + (√2+√3)J, but the test field's gradient points along the first axis, so only the diagonal entry A₀[0,0] enters the target. No isotropy is claimed.

The practical payoff is a certified benchmark. Any future lattice gravity computation can test its own convergence against this exact, machine-checked rate. The proof gives a concrete constant, not just an asymptotic statement, so a numerical implementation can verify it is within the predicted bound at every resolution.

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

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

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

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

/-- The canonical status inhabitant (documentation record, not a proof
obligation). -/
def energyLimitStatus : EnergyLimitStatus where
  exact_closed_form := true
  independent_positive_target := true
  explicit_rate_constant := true
  toolkit_consumed := true

What this page does not claim

The result applies only to the fixed witness field f(x,y,z) = sin(2πx), not to arbitrary fields. The path-sum flag remains red; the full quantum gravity path integral is not established. The continuum limit is for the energy, not for the field itself or any derived observable.

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: