Gravity Analysis Freudenthal Energy Limit Scaled Canonical Energy Witness Rate

The convergence guarantee

The declaration scaledCanonicalEnergy_witness_rate is a formal theorem in the framework's machine-checked library of formal theorems. It concerns a specific smooth test field, f(x,y,z) = sin(2πx), and a sequence of discrete approximations to a three-dimensional cube. The theorem states that as the lattice spacing shrinks (the integer N grows), the energy computed on the discrete lattice approaches the energy computed by a continuum integral, and the difference shrinks at least as fast as 1/N. This is a quantitative convergence guarantee: it gives an explicit bound on the error, not just a statement that the error eventually vanishes.

The theorem is part of a larger program in Recognition Science to build a theory of gravity from discrete combinatorial structures. The specific field is called a witness field because it provides a test case: it is nonconstant and smooth, so it exercises the lattice approximation in a nontrivial way. The energy in question is a quadratic form built from a stencil, a fixed pattern of weights that approximates a differential operator. The theorem proves that for this witness field, the lattice energy converges to the continuum energy ∫⟨∇f, A₀∇f⟩, where A₀ is a fixed anisotropic matrix. The rate constant C is given explicitly: C = A₀[0,0]·(2π)⁴/24, where A₀[0,0] = 1 + 2√2 + √3.

The proof is notable for being exact and axiom-clean. The closed-form evaluation of the lattice sum is a telescoping identity, not a numerical estimate. The continuum integral is evaluated symbolically in the library. The theorem freudenthal_witness_energy_limit packages this into an existential statement: there exists a constant C and a threshold N₀ such that for all N ≥ N₀, the error is bounded by C/N. The proof actually achieves the sharper rate C/N², as shown by the companion theorem witness_closed_form_dist.

What the declaration does not claim is equally important. It does not establish the convergence for all fields; it establishes it for this one fixed witness field. It does not prove that the lattice energy approximates the continuum energy for arbitrary smooth functions, nor does it prove that the stencil is a good approximation to any particular differential operator in general. The theorem is scoped: it is a stage-2 result in a larger campaign, and the panel-mandated scope statement explicitly says the path-sum flag remains red, meaning the full quantum gravity construction is not yet complete. The theorem is a precise, verified statement about one test case, not a general theory of discrete gravity.

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

/-- 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 explicit `N`-independent rate constant `C = A₀[0,0] · (2π)⁴ / 24`. -/
def rateConstant : ℝ := stencilMomentTensor 0 0 * (2 * Real.pi) ^ (4 : ℕ) / 24

/-- 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 prove convergence for all fields, only for the fixed witness field sin(2πx). The theorem does not establish that the lattice energy approximates the continuum energy for arbitrary smooth functions. The theorem does not complete the quantum gravity construction; the path-sum flag remains red.

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: