IndisputableMonolith.Gravity.Analysis.FreudenthalEnergyLimit

   1import IndisputableMonolith.Gravity.Analysis.FreudenthalStencilPreflight
   2import IndisputableMonolith.Gravity.Analysis.SpectralConvergence
   3
   4/-!
   5# Freudenthal energy limit: rated action-level limit on a sampled witness field
   6
   7QG full-theory campaign, Phase 2b, panel-locked Test G stage 2 (candidate C8,
   8tensor-first anisotropic action continuum limit).
   9
  10Scope statement (panel-mandated): this module and its stage-1 companion
  11(`FreudenthalStencilPreflight`) develop the action-level continuum limit of
  12the frozen quadratic energy on the canonical Freudenthal family; scoped
  13partial; the pillar-2 path-sum flag stays red (flipping it requires the
  14refinement-indexed measure-weighted sum over inequivalent triangulation
  15classes).
  16
  17## Status: THEOREM (everything below is proved, axiom-clean; no sorry, no
  18## admit, no native_decide, no `: True` shells).
  19
  20## What this module proves
  21
  22For the FIXED nonconstant C² witness field `f(x,y,z) = sin(2πx)`
  23(`witnessField`), sampled onto the side-`N` canonical periodic Freudenthal
  24family (`sample`):
  25
  26* `scaledCanonicalEnergy_witness_closed_form`: the `ρ(N)`-normalized
  27  canonical Regge-Hessian quadratic energy of the sampled field evaluates
  28  EXACTLY (for every `N > 2`) to
  29  `A₀[0,0] · 2N² sin²(π/N)` with `A₀[0,0] = 1 + 2√2 + √3` the stage-1
  30  moment-tensor entry. The trig evaluation is a telescoping identity
  31  (`sum_cos_shifted_vanishes`), not an estimate.
  32* `continuumTarget` (defined INDEPENDENTLY of the lattice computation):
  33  the by-hand continuum energy `∫_{[0,1]³} ⟨∇f, A₀ ∇f⟩ = A₀[0,0] · 2π²`.
  34  Since `⟨∇f(p), A₀ ∇f(p)⟩ = A₀[0,0] (2π cos(2πp₀))²` depends only on the
  35  first coordinate, the cube integral reduces by hand to the interval
  36  integral `∫₀¹ A₀[0,0] (2π cos(2πt))² dt`, which is evaluated IN LEAN
  37  (`integral_witness_energy_density`, via the closed-form antiderivative);
  38  the gradient component is justified in Lean by
  39  `witnessField_section_hasDerivAt`. `continuumTarget_pos`: the target is
  40  strictly positive (no `0 = 0` trap; `witnessField_nonconstant`).
  41* `scaledCanonicalEnergy_witness_rate` /
  42  `freudenthal_witness_energy_limit`: the panel-locked stage-2 observable
  43  `∃ C N₀, ∀ N ≥ N₀, |scaledCanonicalEnergy N (sample N f) − ∫⟨∇f, A₀∇f⟩| ≤ C/N`
  44  with the EXPLICIT constant `C = rateConstant = A₀[0,0]·(2π)⁴/24`,
  45  independent of `N` (`N₀ = 3`); the achieved rate is in fact `C/N²`
  46  (`witness_closed_form_dist`), consuming the Phase-2a toolkit bound
  47  `discrete_sine_eigenvalue_expansion` at wavenumber 1.
  48* `witness_closed_form_tendsto`: the qualitative limit, re-derived through
  49  the Phase-2a `eigenvalue_limit_of_uniform_bound` squeeze, verifying that
  50  the two toolkit pieces compose.
  51
  52Anisotropy note (stage-1 finding, inherited): the continuum quadratic form
  53is `⟨∇f, A₀ ∇f⟩` with the ANISOTROPIC `A₀ = (1+√2)I + (√2+√3)J`; the
  54witness field's gradient points along the first axis, so only the diagonal
  55entry `A₀[0,0] = 1 + 2√2 + √3` enters its target. No isotropy is claimed.
  56-/
  57
  58namespace IndisputableMonolith
  59namespace Gravity
  60namespace Analysis
  61namespace FreudenthalEnergyLimit
  62
  63open Geometry.PeriodicFreudenthalTorus
  64open FreudenthalStencilPreflight
  65
  66noncomputable section
  67
  68/-! ## §1. The witness field and its lattice sampling -/
  69
  70/-- The fixed nonconstant C² witness field `f(p) = sin(2π p₀)` on `ℝ³`. -/
  71def witnessField (p : Fin 3 → ℝ) : ℝ := Real.sin (2 * Real.pi * p 0)
  72
  73/-- Sampling a continuum field onto the side-`N` periodic vertex lattice
  74(vertex `x` sits at the point `x/N` of the unit 3-torus). -/
  75def sample (N : ℕ) (f : (Fin 3 → ℝ) → ℝ) (x : Vertex N N N) : ℝ :=
  76  f ![(x.1.val : ℝ) / N, (x.2.1.val : ℝ) / N, (x.2.2.val : ℝ) / N]
  77
  78/-- The sampled witness field in explicit first-coordinate form. -/
  79def witnessSample (N : ℕ) (x : Vertex N N N) : ℝ :=
  80  Real.sin (2 * Real.pi * (x.1.val : ℝ) / N)
  81
  82theorem sample_witnessField (N : ℕ) (x : Vertex N N N) :
  83    sample N witnessField x = witnessSample N x := by
  84  unfold sample witnessField witnessSample
  85  rw [Matrix.cons_val_zero, mul_div_assoc]
  86
  87/-- The witness field is nonconstant: it separates `(1/4,0,0)` from the
  88origin (`sin(π/2) = 1 ≠ 0 = sin 0`). -/
  89theorem witnessField_nonconstant :
  90    witnessField ![(1:ℝ)/4, 0, 0] ≠ witnessField ![0, 0, 0] := by
  91  unfold witnessField
  92  rw [Matrix.cons_val_zero, Matrix.cons_val_zero]
  93  have harg : 2 * Real.pi * ((1:ℝ)/4) = Real.pi / 2 := by ring
  94  rw [harg]
  95  rw [Real.sin_pi_div_two]
  96  simp only [mul_zero, Real.sin_zero]
  97  norm_num
  98
  99/-! ## §2. The by-hand continuum target and its Lean-checked integral -/
 100
 101/-- By-hand gradient of the witness field: `∇f(p) = (2π cos(2πp₀), 0, 0)`.
 102The nonzero component is certified against the one-dimensional section in
 103`witnessField_section_hasDerivAt`; the vanishing components hold because
 104`witnessField` does not depend on `p₁, p₂` (definitionally: `p₁, p₂` do not
 105occur in `witnessField`). -/
 106def witnessGrad (t : ℝ) : Fin 3 → ℝ := fun i =>
 107  if i = 0 then 2 * Real.pi * Real.cos (2 * Real.pi * t) else 0
 108
 109theorem hasDerivAt_sin_const_mul (c t : ℝ) :
 110    HasDerivAt (fun s : ℝ => Real.sin (c * s)) (Real.cos (c * t) * c) t := by
 111  have h := ((hasDerivAt_id t).const_mul c).sin
 112  simpa using h
 113
 114/-- The first gradient component is the honest derivative of the witness
 115field along the first coordinate axis. -/
 116theorem witnessField_section_hasDerivAt (t : ℝ) :
 117    HasDerivAt (fun s : ℝ => witnessField ![s, 0, 0]) (witnessGrad t 0) t := by
 118  have hg : witnessGrad t 0 = Real.cos (2 * Real.pi * t) * (2 * Real.pi) := by
 119    show (if (0 : Fin 3) = 0 then 2 * Real.pi * Real.cos (2 * Real.pi * t) else 0) =
 120      Real.cos (2 * Real.pi * t) * (2 * Real.pi)
 121    rw [if_pos rfl]
 122    ring
 123  rw [hg]
 124  simp only [witnessField, Matrix.cons_val_zero]
 125  exact hasDerivAt_sin_const_mul (2 * Real.pi) t
 126
 127/-- The continuum target `∫_{[0,1]³} ⟨∇f, A₀ ∇f⟩ = A₀[0,0] · 2π²`, defined
 128INDEPENDENTLY of the lattice computation as an exact constant (by-hand cube
 129integral; the integrand depends only on the first coordinate, so the cube
 130integral equals the interval integral certified in
 131`integral_witness_energy_density`). -/
 132def continuumTarget : ℝ := stencilMomentTensor 0 0 * (2 * Real.pi ^ (2 : ℕ))
 133
 134/-- Gate (vi): the continuum target is strictly positive (nonzero limit;
 135this witness is not in the `0 = 0` trap). -/
 136theorem continuumTarget_pos : 0 < continuumTarget := by
 137  unfold continuumTarget
 138  have hpi : 0 < Real.pi := Real.pi_pos
 139  exact mul_pos (stencilMomentTensor_diag_pos 0) (by positivity)
 140
 141/-- Pointwise anisotropic energy density of the witness field:
 142`⟨∇f, A₀ ∇f⟩(t) = A₀[0,0] · (2π cos(2πt))²`. -/
 143theorem witness_energy_density_eq (t : ℝ) :
 144    (∑ i : Fin 3, ∑ j : Fin 3,
 145        stencilMomentTensor i j * witnessGrad t i * witnessGrad t j) =
 146      stencilMomentTensor 0 0 *
 147        (2 * Real.pi * Real.cos (2 * Real.pi * t)) ^ (2 : ℕ) := by
 148  simp only [witnessGrad, Fin.sum_univ_three,
 149    show ((1 : Fin 3) = 0) = False by decide, show ((2 : Fin 3) = 0) = False by decide,
 150    if_false, if_true]
 151  ring
 152
 153theorem integral_cos_sq_two_pi :
 154    (∫ x in (0:ℝ)..1, Real.cos (2 * Real.pi * x) ^ (2 : ℕ)) = 1 / 2 := by
 155  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
 156  have hderiv : ∀ x ∈ Set.uIcc (0:ℝ) 1,
 157      HasDerivAt (fun t : ℝ => t / 2 + Real.sin (4 * Real.pi * t) / (8 * Real.pi))
 158        (Real.cos (2 * Real.pi * x) ^ (2 : ℕ)) x := by
 159    intro x _
 160    have h1 : HasDerivAt (fun t : ℝ => t / 2) ((1:ℝ) / 2) x := by
 161      simpa using (hasDerivAt_id x).div_const 2
 162    have h2 : HasDerivAt (fun t : ℝ => Real.sin (4 * Real.pi * t) / (8 * Real.pi))
 163        ((Real.cos (4 * Real.pi * x) * (4 * Real.pi)) / (8 * Real.pi)) x :=
 164      (hasDerivAt_sin_const_mul (4 * Real.pi) x).div_const (8 * Real.pi)
 165    have hval : (1:ℝ) / 2 + (Real.cos (4 * Real.pi * x) * (4 * Real.pi)) / (8 * Real.pi) =
 166        Real.cos (2 * Real.pi * x) ^ (2 : ℕ) := by
 167      rw [Real.cos_sq]
 168      have h4 : 2 * (2 * Real.pi * x) = 4 * Real.pi * x := by ring
 169      rw [h4]
 170      field_simp
 171      try ring
 172    rw [← hval]
 173    exact h1.add h2
 174  have hcont : Continuous fun x : ℝ => Real.cos (2 * Real.pi * x) ^ (2 : ℕ) := by
 175    fun_prop
 176  have hint := intervalIntegral.integral_eq_sub_of_hasDerivAt hderiv
 177    (hcont.intervalIntegrable 0 1)
 178  rw [hint]
 179  have hsin4 : Real.sin (4 * Real.pi) = 0 := by
 180    have h := Real.sin_nat_mul_pi 4
 181    push_cast at h
 182    exact h
 183  norm_num [hsin4]
 184
 185/-- Lean-checked evaluation of the continuum target: the interval integral
 186of the anisotropic energy density is exactly `continuumTarget`. -/
 187theorem integral_witness_energy_density :
 188    (∫ t in (0:ℝ)..1,
 189        ∑ i : Fin 3, ∑ j : Fin 3,
 190          stencilMomentTensor i j * witnessGrad t i * witnessGrad t j) =
 191      continuumTarget := by
 192  have hpt : (fun t : ℝ =>
 193      ∑ i : Fin 3, ∑ j : Fin 3,
 194        stencilMomentTensor i j * witnessGrad t i * witnessGrad t j) =
 195      fun t : ℝ =>
 196        (stencilMomentTensor 0 0 * (2 * Real.pi) ^ (2 : ℕ)) *
 197          Real.cos (2 * Real.pi * t) ^ (2 : ℕ) := by
 198    funext t
 199    rw [witness_energy_density_eq]
 200    ring
 201  rw [hpt, intervalIntegral.integral_const_mul, integral_cos_sq_two_pi]
 202  unfold continuumTarget
 203  ring
 204
 205/-! ## §3. Exact closed-form evaluation of the sampled lattice energy -/
 206
 207/-- Periodic wraparound of the sampled sine: shifting one lattice step in
 208the first coordinate is an honest `+1` inside the sine, including at the
 209wraparound seam (where both sides are `sin` of a full period). -/
 210theorem witnessSample_addBit_true (N : ℕ) [NeZero N] (i : Fin N) :
 211    Real.sin (2 * Real.pi * ((addBit i true).val : ℝ) / N) =
 212      Real.sin (2 * Real.pi * ((i.val : ℝ) + 1) / N) := by
 213  have hval : (addBit i true).val = (i.val + 1) % N := rfl
 214  rcases lt_or_eq_of_le (Nat.succ_le_of_lt i.isLt) with h | h
 215  · rw [hval, Nat.mod_eq_of_lt h]
 216    norm_cast
 217  · have hN0 : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne N)
 218    have h' : i.val + 1 = N := h
 219    have h1 : ((i.val : ℝ) + 1) = (N : ℝ) := by exact_mod_cast h'
 220    rw [hval, h', Nat.mod_self, h1]
 221    have h2 : 2 * Real.pi * (N : ℝ) / N = 2 * Real.pi := by field_simp
 222    rw [h2]
 223    simp [Real.sin_two_pi]
 224
 225/-- Per-vertex evaluation of the seven-class stencil on the sampled witness
 226field: the three classes with no first-coordinate step contribute zero, and
 227the four classes stepping in the first coordinate (weights
 228`1, √2, √2, √3`) sum to exactly the moment-tensor entry `A₀[0,0]`. -/
 229theorem stencil_inner_sum_witness (N : ℕ) [NeZero N] (x : Vertex N N N) :
 230    (∑ d : Fin 7, stencilWeight d *
 231        (witnessSample N (shiftVertex N x d) - witnessSample N x) ^ (2 : ℕ)) =
 232      stencilMomentTensor 0 0 *
 233        (Real.sin (2 * Real.pi * ((x.1.val : ℝ) + 1) / N) -
 234          Real.sin (2 * Real.pi * (x.1.val : ℝ) / N)) ^ (2 : ℕ) := by
 235  simp only [Fin.sum_univ_seven, shiftVertex, addBits, dispBits, addBit_false,
 236    witnessSample, witnessSample_addBit_true]
 237  rw [stencilMomentTensor_eq]
 238  norm_num [stencilWeight, periodicDispSqEdge, Real.sqrt_one]
 239  try ring
 240
 241/-- Telescoping vanishing of the equally spaced cosine sum
 242`Σ_{k<N} cos((4k+2)π/N) = 0` for `N > 2`
 243(via `2 sin(2π/N) cos((4k+2)π/N) = sin(4π(k+1)/N) − sin(4πk/N)`). -/
 244theorem sum_cos_shifted_vanishes (N : ℕ) (hN : 2 < N) :
 245    (∑ k ∈ Finset.range N, Real.cos ((4 * (k : ℝ) + 2) * Real.pi / N)) = 0 := by
 246  have hN0 : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
 247  have hNpos : (0 : ℝ) < (N : ℝ) := by
 248    have : (2 : ℝ) < (N : ℝ) := by exact_mod_cast hN
 249    linarith
 250  have hNgt : (2 : ℝ) < (N : ℝ) := by exact_mod_cast hN
 251  have hs_pos : 0 < Real.sin (2 * Real.pi / N) := by
 252    apply Real.sin_pos_of_pos_of_lt_pi
 253    · positivity
 254    · rw [div_lt_iff₀ hNpos]
 255      nlinarith [Real.pi_pos]
 256  have hs2 : (2 : ℝ) * Real.sin (2 * Real.pi / N) ≠ 0 := by positivity
 257  have hkey : ∀ k : ℕ,
 258      2 * Real.sin (2 * Real.pi / N) * Real.cos ((4 * (k : ℝ) + 2) * Real.pi / N) =
 259        Real.sin (4 * Real.pi * (((k + 1 : ℕ)) : ℝ) / N) -
 260          Real.sin (4 * Real.pi * ((k : ℕ) : ℝ) / N) := by
 261    intro k
 262    rw [Real.sin_sub_sin]
 263    have h1 : (4 * Real.pi * (((k + 1 : ℕ)) : ℝ) / N - 4 * Real.pi * ((k : ℕ) : ℝ) / N) / 2 =
 264        2 * Real.pi / N := by
 265      push_cast
 266      field_simp
 267      try ring
 268    have h2 : (4 * Real.pi * (((k + 1 : ℕ)) : ℝ) / N + 4 * Real.pi * ((k : ℕ) : ℝ) / N) / 2 =
 269        (4 * (k : ℝ) + 2) * Real.pi / N := by
 270      push_cast
 271      field_simp
 272      try ring
 273    rw [h1, h2]
 274  have hend : Real.sin (4 * Real.pi * ((N : ℕ) : ℝ) / N) = 0 := by
 275    have harg : 4 * Real.pi * ((N : ℕ) : ℝ) / N = ((4 : ℕ) : ℝ) * Real.pi := by
 276      push_cast
 277      field_simp
 278      try ring
 279    rw [harg]
 280    exact Real.sin_nat_mul_pi 4
 281  have h2s : (2 * Real.sin (2 * Real.pi / N)) *
 282      (∑ k ∈ Finset.range N, Real.cos ((4 * (k : ℝ) + 2) * Real.pi / N)) = 0 := by
 283    rw [Finset.mul_sum]
 284    calc (∑ k ∈ Finset.range N,
 285          2 * Real.sin (2 * Real.pi / N) * Real.cos ((4 * (k : ℝ) + 2) * Real.pi / N))
 286        = ∑ k ∈ Finset.range N,
 287            (Real.sin (4 * Real.pi * (((k + 1 : ℕ)) : ℝ) / N) -
 288              Real.sin (4 * Real.pi * ((k : ℕ) : ℝ) / N)) :=
 289          Finset.sum_congr rfl fun k _ => hkey k
 290      _ = Real.sin (4 * Real.pi * ((N : ℕ) : ℝ) / N) -
 291            Real.sin (4 * Real.pi * ((0 : ℕ) : ℝ) / N) :=
 292          Finset.sum_range_sub (fun k : ℕ => Real.sin (4 * Real.pi * ((k : ℕ) : ℝ) / N)) N
 293      _ = 0 := by
 294          rw [hend]
 295          norm_num
 296  exact (mul_eq_zero.mp h2s).resolve_left hs2
 297
 298/-- Exact evaluation of the first-difference sine sum:
 299`Σ_{k<N} (sin(2π(k+1)/N) − sin(2πk/N))² = 2N sin²(π/N)` for `N > 2`. -/
 300theorem sum_range_sq_sinDiff (N : ℕ) (hN : 2 < N) :
 301    (∑ k ∈ Finset.range N,
 302        (Real.sin (2 * Real.pi * ((k : ℝ) + 1) / N) -
 303          Real.sin (2 * Real.pi * (k : ℝ) / N)) ^ (2 : ℕ)) =
 304      2 * (N : ℝ) * Real.sin (Real.pi / N) ^ (2 : ℕ) := by
 305  have hN0 : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
 306  have hterm : ∀ k : ℕ,
 307      (Real.sin (2 * Real.pi * ((k : ℝ) + 1) / N) -
 308          Real.sin (2 * Real.pi * (k : ℝ) / N)) ^ (2 : ℕ) =
 309        2 * Real.sin (Real.pi / N) ^ (2 : ℕ) +
 310          2 * Real.sin (Real.pi / N) ^ (2 : ℕ) *
 311            Real.cos ((4 * (k : ℝ) + 2) * Real.pi / N) := by
 312    intro k
 313    rw [Real.sin_sub_sin]
 314    have h1 : (2 * Real.pi * ((k : ℝ) + 1) / N - 2 * Real.pi * (k : ℝ) / N) / 2 =
 315        Real.pi / N := by
 316      field_simp
 317      try ring
 318    have h2 : (2 * Real.pi * ((k : ℝ) + 1) / N + 2 * Real.pi * (k : ℝ) / N) / 2 =
 319        (2 * (k : ℝ) + 1) * Real.pi / N := by
 320      field_simp
 321      try ring
 322    rw [h1, h2]
 323    have h3 : 2 * ((2 * (k : ℝ) + 1) * Real.pi / N) = (4 * (k : ℝ) + 2) * Real.pi / N := by
 324      field_simp
 325      try ring
 326    calc (2 * Real.sin (Real.pi / N) * Real.cos ((2 * (k : ℝ) + 1) * Real.pi / N)) ^ (2 : ℕ)
 327        = 4 * Real.sin (Real.pi / N) ^ (2 : ℕ) *
 328            Real.cos ((2 * (k : ℝ) + 1) * Real.pi / N) ^ (2 : ℕ) := by ring
 329      _ = 4 * Real.sin (Real.pi / N) ^ (2 : ℕ) *
 330            (1 / 2 + Real.cos ((4 * (k : ℝ) + 2) * Real.pi / N) / 2) := by
 331          rw [Real.cos_sq, h3]
 332      _ = 2 * Real.sin (Real.pi / N) ^ (2 : ℕ) +
 333            2 * Real.sin (Real.pi / N) ^ (2 : ℕ) *
 334              Real.cos ((4 * (k : ℝ) + 2) * Real.pi / N) := by ring
 335  calc (∑ k ∈ Finset.range N,
 336        (Real.sin (2 * Real.pi * ((k : ℝ) + 1) / N) -
 337          Real.sin (2 * Real.pi * (k : ℝ) / N)) ^ (2 : ℕ))
 338      = ∑ k ∈ Finset.range N,
 339          (2 * Real.sin (Real.pi / N) ^ (2 : ℕ) +
 340            2 * Real.sin (Real.pi / N) ^ (2 : ℕ) *
 341              Real.cos ((4 * (k : ℝ) + 2) * Real.pi / N)) :=
 342        Finset.sum_congr rfl fun k _ => hterm k
 343    _ = (N : ℝ) * (2 * Real.sin (Real.pi / N) ^ (2 : ℕ)) +
 344          2 * Real.sin (Real.pi / N) ^ (2 : ℕ) *
 345            ∑ k ∈ Finset.range N, Real.cos ((4 * (k : ℝ) + 2) * Real.pi / N) := by
 346        rw [Finset.sum_add_distrib, Finset.sum_const, Finset.card_range,
 347          nsmul_eq_mul, ← Finset.mul_sum]
 348    _ = 2 * (N : ℝ) * Real.sin (Real.pi / N) ^ (2 : ℕ) := by
 349        rw [sum_cos_shifted_vanishes N hN]
 350        ring
 351
 352/-- Aggregation of the per-vertex stencil over the `N³` vertex lattice: the
 353two free coordinates contribute a factor `N²`. -/
 354theorem freudenthalStencilEnergy_witness (N : ℕ) [NeZero N] :
 355    freudenthalStencilEnergy N (witnessSample N) =
 356      (N : ℝ) ^ (2 : ℕ) * (stencilMomentTensor 0 0 *
 357        ∑ k ∈ Finset.range N,
 358          (Real.sin (2 * Real.pi * ((k : ℝ) + 1) / N) -
 359            Real.sin (2 * Real.pi * (k : ℝ) / N)) ^ (2 : ℕ)) := by
 360  unfold freudenthalStencilEnergy
 361  rw [Fintype.sum_prod_type]
 362  calc (∑ a : Fin N, ∑ bc : Fin N × Fin N, ∑ d : Fin 7,
 363        stencilWeight d *
 364          (witnessSample N (shiftVertex N (a, bc) d) - witnessSample N (a, bc)) ^ (2 : ℕ))
 365      = ∑ a : Fin N, ∑ _bc : Fin N × Fin N,
 366          stencilMomentTensor 0 0 *
 367            (Real.sin (2 * Real.pi * ((a.val : ℝ) + 1) / N) -
 368              Real.sin (2 * Real.pi * (a.val : ℝ) / N)) ^ (2 : ℕ) :=
 369        Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun bc _ =>
 370          stencil_inner_sum_witness N (a, bc)
 371    _ = ∑ a : Fin N, ((N : ℝ) * (N : ℝ)) *
 372          (stencilMomentTensor 0 0 *
 373            (Real.sin (2 * Real.pi * ((a.val : ℝ) + 1) / N) -
 374              Real.sin (2 * Real.pi * (a.val : ℝ) / N)) ^ (2 : ℕ)) := by
 375        refine Finset.sum_congr rfl fun a _ => ?_
 376        rw [Finset.sum_const, Finset.card_univ, Fintype.card_prod, Fintype.card_fin,
 377          nsmul_eq_mul]
 378        push_cast
 379        ring
 380    _ = (N : ℝ) ^ (2 : ℕ) * (stencilMomentTensor 0 0 *
 381          ∑ a : Fin N,
 382            (Real.sin (2 * Real.pi * ((a.val : ℝ) + 1) / N) -
 383              Real.sin (2 * Real.pi * (a.val : ℝ) / N)) ^ (2 : ℕ)) := by
 384        rw [Finset.mul_sum, Finset.mul_sum]
 385        refine Finset.sum_congr rfl fun a _ => ?_
 386        ring
 387    _ = (N : ℝ) ^ (2 : ℕ) * (stencilMomentTensor 0 0 *
 388          ∑ k ∈ Finset.range N,
 389            (Real.sin (2 * Real.pi * ((k : ℝ) + 1) / N) -
 390              Real.sin (2 * Real.pi * (k : ℝ) / N)) ^ (2 : ℕ)) := by
 391        rw [Fin.sum_univ_eq_sum_range
 392          (fun k : ℕ => (Real.sin (2 * Real.pi * ((k : ℝ) + 1) / N) -
 393            Real.sin (2 * Real.pi * (k : ℝ) / N)) ^ (2 : ℕ)) N]
 394
 395/-- EXACT closed form of the normalized sampled energy for every `N > 2`:
 396`scaledCanonicalEnergy N (witnessSample N) = A₀[0,0] · 2N² sin²(π/N)`. -/
 397theorem scaledCanonicalEnergy_witness_closed_form (N : ℕ) [NeZero N] (hN : 2 < N) :
 398    scaledCanonicalEnergy N (witnessSample N) =
 399      stencilMomentTensor 0 0 *
 400        (2 * (N : ℝ) ^ (2 : ℕ) * Real.sin (Real.pi / N) ^ (2 : ℕ)) := by
 401  rw [scaledCanonicalEnergy_eq_scaled_stencil N hN, freudenthalStencilEnergy_witness N,
 402    sum_range_sq_sinDiff N hN]
 403  unfold stencilNormalization
 404  have hN0 : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
 405  field_simp
 406  try ring
 407
 408/-! ## §4. The rated limit -/
 409
 410/-- The explicit `N`-independent rate constant `C = A₀[0,0] · (2π)⁴ / 24`. -/
 411def rateConstant : ℝ := stencilMomentTensor 0 0 * (2 * Real.pi) ^ (4 : ℕ) / 24
 412
 413theorem rateConstant_nonneg : 0 ≤ rateConstant := by
 414  unfold rateConstant
 415  have hA : 0 ≤ stencilMomentTensor 0 0 := le_of_lt (stencilMomentTensor_diag_pos 0)
 416  have hpi : 0 ≤ (2 * Real.pi) ^ (4 : ℕ) := by positivity
 417  exact div_nonneg (mul_nonneg hA hpi) (by norm_num)
 418
 419/-- Quantitative distance of the closed form from the continuum target:
 420`|A₀[0,0]·2N²sin²(π/N) − continuumTarget| ≤ rateConstant/N²`, consuming the
 421Phase-2a toolkit bound `discrete_sine_eigenvalue_expansion` at wavenumber 1.
 422The achieved rate is `1/N²`, strictly better than the demanded `1/N`. -/
 423theorem witness_closed_form_dist (N : ℕ) (hN : 3 ≤ N) :
 424    |stencilMomentTensor 0 0 *
 425        (2 * (N : ℝ) ^ (2 : ℕ) * Real.sin (Real.pi / N) ^ (2 : ℕ)) -
 426      continuumTarget| ≤ rateConstant / (N : ℝ) ^ (2 : ℕ) := by
 427  have hA : 0 ≤ stencilMomentTensor 0 0 := le_of_lt (stencilMomentTensor_diag_pos 0)
 428  have hexp := discrete_sine_eigenvalue_expansion 1 N (by omega)
 429  simp only [Nat.cast_one, mul_one] at hexp
 430  have hkey : stencilMomentTensor 0 0 *
 431      (2 * (N : ℝ) ^ (2 : ℕ) * Real.sin (Real.pi / N) ^ (2 : ℕ)) - continuumTarget =
 432      (stencilMomentTensor 0 0 / 2) *
 433        (4 * (N : ℝ) ^ 2 * Real.sin (Real.pi / (N : ℝ)) ^ 2 - (2 * Real.pi) ^ 2) := by
 434    unfold continuumTarget
 435    ring
 436  rw [hkey, abs_mul, abs_of_nonneg (div_nonneg hA (by norm_num))]
 437  calc (stencilMomentTensor 0 0 / 2) *
 438        |4 * (N : ℝ) ^ 2 * Real.sin (Real.pi / (N : ℝ)) ^ 2 - (2 * Real.pi) ^ 2|
 439      ≤ (stencilMomentTensor 0 0 / 2) * ((2 * Real.pi) ^ 4 / 12 / (N : ℝ) ^ 2) :=
 440        mul_le_mul_of_nonneg_left hexp (div_nonneg hA (by norm_num))
 441    _ = rateConstant / (N : ℝ) ^ (2 : ℕ) := by
 442        unfold rateConstant
 443        ring
 444
 445/-- Panel-locked stage-2 rate bound, explicit-constant form: for every
 446`N ≥ 3`,
 447`|scaledCanonicalEnergy N (sample N witnessField) − continuumTarget| ≤ rateConstant / N`,
 448with `rateConstant` independent of `N`. -/
 449theorem scaledCanonicalEnergy_witness_rate (N : ℕ) [NeZero N] (hN : 3 ≤ N) :
 450    |scaledCanonicalEnergy N (sample N witnessField) - continuumTarget| ≤
 451      rateConstant / (N : ℝ) := by
 452  have hN2 : 2 < N := hN
 453  have hs : sample N witnessField = witnessSample N :=
 454    funext fun x => sample_witnessField N x
 455  rw [hs, scaledCanonicalEnergy_witness_closed_form N hN2]
 456  refine le_trans (witness_closed_form_dist N hN) ?_
 457  have hN1 : (1 : ℝ) ≤ (N : ℝ) := by exact_mod_cast (by omega : 1 ≤ N)
 458  have hNpos : (0 : ℝ) < (N : ℝ) := by linarith
 459  have hsq : (N : ℝ) ≤ (N : ℝ) ^ (2 : ℕ) := by nlinarith
 460  have hrc : 0 ≤ rateConstant := rateConstant_nonneg
 461  gcongr
 462
 463/-- Panel-locked stage-2 observable (existential form): there is a constant
 464`C` and a threshold `N₀` with
 465`∀ N ≥ N₀, |scaledCanonicalEnergy N (sample N f) − ∫⟨∇f, A₀∇f⟩| ≤ C/N`
 466for the fixed nonconstant witness `f = witnessField`; the witnesses are the
 467explicit `rateConstant` and `N₀ = 3`. -/
 468theorem freudenthal_witness_energy_limit :
 469    ∃ C : ℝ, ∃ N₀ : ℕ, ∀ (N : ℕ) [NeZero N], N₀ ≤ N →
 470      |scaledCanonicalEnergy N (sample N witnessField) - continuumTarget| ≤
 471        C / (N : ℝ) := by
 472  refine ⟨rateConstant, 3, ?_⟩
 473  intro N _ hN
 474  exact scaledCanonicalEnergy_witness_rate N hN
 475
 476/-- The same rate bound stated directly against the Lean-checked integral
 477of the anisotropic energy density (interval form of `∫⟨∇f, A₀∇f⟩`). -/
 478theorem freudenthal_witness_energy_rate_integral_form (N : ℕ) [NeZero N]
 479    (hN : 3 ≤ N) :
 480    |scaledCanonicalEnergy N (sample N witnessField) -
 481        ∫ t in (0:ℝ)..1,
 482          ∑ i : Fin 3, ∑ j : Fin 3,
 483            stencilMomentTensor i j * witnessGrad t i * witnessGrad t j| ≤
 484      rateConstant / (N : ℝ) := by
 485  rw [integral_witness_energy_density]
 486  exact scaledCanonicalEnergy_witness_rate N hN
 487
 488/-- Qualitative limit of the closed-form energy sequence, re-derived from
 489the rate through the Phase-2a toolkit squeeze
 490`eigenvalue_limit_of_uniform_bound` (toolkit composition check). -/
 491theorem witness_closed_form_tendsto :
 492    Filter.Tendsto
 493      (fun N : ℕ => stencilMomentTensor 0 0 *
 494        (2 * (N : ℝ) ^ (2 : ℕ) * Real.sin (Real.pi / N) ^ (2 : ℕ)))
 495      Filter.atTop (nhds continuumTarget) :=
 496  eigenvalue_limit_of_uniform_bound _ continuumTarget rateConstant 3
 497    (fun N hN => witness_closed_form_dist N hN)
 498
 499/-! ## §5. Status record (documentation, not mathematics) -/
 500
 501/-- Status flags for the Freudenthal energy limit (documentation record;
 502the mathematics lives in the theorems above, not in these booleans).
 503
 504Honest scope: with stage 1 this certifies the action-level continuum limit
 505of the frozen quadratic energy on the canonical Freudenthal family, for one
 506fixed nonconstant sampled witness field, with an explicit `N`-independent
 507rate constant. SCOPED PARTIAL: the pillar-2 path-sum flag stays red
 508(flipping it requires the refinement-indexed measure-weighted sum over
 509inequivalent triangulation classes); the anisotropic tensor `A₀` (stage-1
 510finding) governs the target, and no isotropy is claimed. -/
 511structure EnergyLimitStatus where
 512  /-- `scaledCanonicalEnergy_witness_closed_form`: exact lattice evaluation
 513  for every `N > 2` (telescoping identity, not an estimate). -/
 514  exact_closed_form : Bool
 515  /-- `continuumTarget` defined independently; `continuumTarget_pos`;
 516  `integral_witness_energy_density` checked in Lean. -/
 517  independent_positive_target : Bool
 518  /-- `scaledCanonicalEnergy_witness_rate`: rate `C/N` with explicit
 519  `C = rateConstant` independent of `N` (achieved rate `C/N²`). -/
 520  explicit_rate_constant : Bool
 521  /-- `witness_closed_form_dist` and `witness_closed_form_tendsto` consume
 522  the Phase-2a toolkit (`discrete_sine_eigenvalue_expansion`,
 523  `eigenvalue_limit_of_uniform_bound`). -/
 524  toolkit_consumed : Bool
 525
 526/-- The canonical status inhabitant (documentation record, not a proof
 527obligation). -/
 528def energyLimitStatus : EnergyLimitStatus where
 529  exact_closed_form := true
 530  independent_positive_target := true
 531  explicit_rate_constant := true
 532  toolkit_consumed := true
 533
 534end
 535
 536end FreudenthalEnergyLimit
 537end Analysis
 538end Gravity
 539end IndisputableMonolith
 540