Gravity Analysis Freudenthal Energy Limit Integral Witness Energy Density

The energy integral

The declaration integral_witness_energy_density is a theorem in the framework's machine-checked library of formal theorems. It evaluates a certain integral exactly. The integral is the continuum energy of a specific smooth test field, the sine wave f(x,y,z) = sin(2πx), over the unit cube. The theorem states that this integral equals a closed-form constant, A₀[0,0] · 2π², where A₀[0,0] = 1 + 2√2 + √3 is a fixed number coming from the framework's anisotropic stencil weights. The proof is a direct computation of the antiderivative of the squared cosine, done entirely inside the formal system.

The point of this theorem is not the integral itself, but what it enables. It provides the target value for a convergence result. The framework also proves that the discrete energy of the same sine wave, sampled on a periodic lattice of side length N, approaches this continuum value as N grows. The rate of approach is at most a constant divided by N, and in fact the stronger rate of a constant divided by N² holds. This is a precise, quantitative statement that the discrete lattice model reproduces the continuum energy in the limit of fine sampling, for this one chosen field.

The theorem does not claim that this convergence holds for all fields, nor that it establishes the continuum limit of the framework's gravity action in general. The scope is explicitly limited to the fixed witness field. The framework's documentation marks the broader path-sum over triangulations as still open. The result is a proof of concept for one test case, not a derivation of the Einstein-Hilbert action or any physical prediction.

What the theorem does establish is a rigorous bridge between a discrete stencil energy and a continuum integral, for a nonconstant field. It shows the machinery works on a nontrivial example, with an explicit error bound and a positive target value. This is a necessary step in the framework's program to connect its discrete recognition ledger to continuum physics, but it is only one step on a path that remains incomplete.

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

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

/-- 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 the continuum limit for all fields, only for the fixed sine wave witness field. The theorem does not derive the Einstein field equations or any physical prediction about gravity. The theorem does not establish that the framework's discrete ledger reproduces continuum physics in general.

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: