IndisputableMonolith.Gravity.Analysis.ReggeTTLocalSymbolExistence

   1import IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolPreflight
   2import IndisputableMonolith.Gravity.Analysis.ReggeTTDerivativeGate
   3
   4/-!
   5# Regge TT local symbol existence at fixed `N` (Gate A1)
   6
   7QG full-theory campaign, `ReggeTTContinuumSymbol` program, Crux-1(c) lane,
   8Gate A1 of the panel-locked protocol "Normalization-Gated Schläfli Two-Jet"
   9(Gate A0 is `ReggeTTSymbolSpecificationAudit`).
  10
  11## What this module proves (all THEOREM)
  12
  13* (a) `planeWaveTetSqEdges_apply` / `planeWaveTetSqEdges_contDiff`: along
  14  the plane-wave family, every tetrahedron's local squared-edge tuple is an
  15  AFFINE path `t ↦ flat + t · v` through the flat Freudenthal tuple
  16  (coefficients named in `planeWaveTetVelocity`), smooth of every order.
  17* (b) `planeWaveTetSqEdges_zero` + `tetDihedralAngle_planeWave_contDiffAt`:
  18  at `t = 0` the tuple is EXACTLY `freudenthalTetSqEdges` (where `cm3 = 8 >
  19  0`, all six squared edges positive, all six cosines strictly inside
  20  `(-1, 1)` — Gate-0 facts of `ReggeTTDerivativeGate`), and each local
  21  dihedral angle along the family is `ContDiffAt` at `0` of every finite
  22  order, by composing the angle's `ContDiffAt` at the nondegenerate flat
  23  tetrahedron with the affine path.
  24* (c) `planeWaveActionProfile_contDiffAt`: the plane-wave action profile
  25  `S(t)` of the TRUE nonlinear Regge action is `ContDiffAt ℝ n` at `t = 0`
  26  for every finite `n` — finite sums over edges and tetrahedra, `√`
  27  factors safe because every flat edge value is `≥ 1 > 0`, the
  28  `canonicalEdgeSlot?` match is a finite case split whose `none` branch is
  29  constant.
  30* (d) `tendsto_centeredSecondDifference_of_contDiffAt` (REUSABLE, general
  31  `f : ℝ → ℝ`): if `f` is `C²` at `0` (`ContDiffAt ℝ 2 f 0`), the centered
  32  second difference `(f(t) − 2f(0) + f(−t))/t²` converges on the punctured
  33  neighborhood filter to `iteratedDeriv 2 f 0`.  Proof: one L'Hôpital pass
  34  (`HasDerivAt.lhopital_zero_nhdsNE`) reduces to
  35  `(f'(t) − f'(−t))/(2t) → f''(0)`, which is the average of the two slope
  36  quotients of `deriv f` at `0` (`hasDerivAt_iff_tendsto_slope`).  The
  37  panel-forbidden global route (`ContinuumLimit.continuum_limit_second_order`,
  38  whose global `ContDiff ℝ 4` hypothesis is false for this family) is NOT
  39  used anywhere.
  40* (e) `planeWave_TTBlochSymbolIs_secondVariation`: THE FIXED-`N` TT BLOCH
  41  SYMBOL EXISTS — for every polarization matrix and every integer wave
  42  vector, `TTBlochSymbolIs N E m ((2/N³) · S''(0))` where `S''(0) =
  43  iteratedDeriv 2 (planeWaveActionProfile N E (commensurateMomentum N m)) 0`.
  44  Exact bookkeeping: `(S(t) − 2S(0) + S(−t))/t² → S''(0)` with no stray
  45  `1/2`; the `2/N³` is the preflight's per-unit-cell normalization carried
  46  verbatim.  First existence theorem of the program.
  47
  48## What this module does NOT prove (binding scope disclosure)
  49
  50* No VALUE of the symbol: `H = (2/N³)·S''(0)` is existence + identification
  51  of the limit, not an evaluation.  The continuum `-(1/4)` target stays
  52  OPEN, its status flag stays `false`, and the C10 numerics remain
  53  NUMERICAL EVIDENCE only.
  54* No continuum limit in `N`: everything here is at fixed `N`.
  55
  56## Inherited axiom footprint (disclosure)
  57
  58`planeWaveTetSqEdges_zero` and everything downstream of it (b, c, e) factor
  59through Stage-1's `tetSqEdgesOfField_flat`, which is pure algebra; but (e)
  60also uses `planeWaveActionProfile_zero`-adjacent structure only through the
  61general bridge (d), so the flat-value theorems of the certified angle-sum
  62chain are NOT on the dependency path of the headline (e) — expected
  63footprint is the standard `[propext, Classical.choice, Quot.sound]`.  The
  64`#print axioms` receipt is recorded by the conductor's audit; if the
  65`Lean.ofReduceBool`/`Lean.trustCompiler` pair appears through any imported
  66flat-point fact, it is inherited disclosure, not new axioms.
  67
  68No `sorry`, no `admit`, no new axioms, no `native_decide` in this file.
  69-/
  70
  71namespace IndisputableMonolith
  72namespace Gravity
  73namespace Analysis
  74namespace ReggeTTLocalSymbolExistence
  75
  76open Geometry.PeriodicFreudenthalTorus
  77open Geometry.CayleyMengerPolynomial (SqEdges)
  78open Geometry.DihedralDerivatives (dihedralAngle3Sq)
  79open Geometry.FreudenthalCubeTriangulation (freudenthalTetSqEdges freudenthalTet)
  80open ReggeTTSymbolPreflight
  81
  82noncomputable section
  83
  84variable (N : ℕ) [NeZero N]
  85
  86/-! ## §1. (a) The plane-wave local squared-edge path is affine and smooth -/
  87
  88/-- Squared displacement class values are strictly positive (they are
  89`1, 1, 1, 2, 2, 2, 3`). -/
  90theorem periodicDispSqEdge_pos (d : Fin 7) : 0 < periodicDispSqEdge d := by
  91  fin_cases d <;> norm_num [periodicDispSqEdge]
  92
  93/-- The affine velocity of the local squared-edge tuple of tetrahedron
  94`cellTet` along the plane-wave family:
  95`v_f = polEdgeCoeff E d_f · cos(k · x_mid(f))`. -/
  96def planeWaveTetVelocity (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
  97    (cellTet : PeriodicTet N N N) : Fin 6 → ℝ :=
  98  fun f =>
  99    polEdgeCoeff E (localEdgeOf cellTet.1 cellTet.2 f).disp *
 100      Real.cos (edgeMidpointPhase N k (localEdgeOf cellTet.1 cellTet.2 f))
 101
 102/-- (a) THEOREM, affine coordinates: along the plane-wave family every
 103local squared-edge coordinate is `flat + t · velocity`, with the flat value
 104the canonical Freudenthal tuple. -/
 105theorem planeWaveTetSqEdges_apply (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
 106    (cellTet : PeriodicTet N N N) (t : ℝ) (f : Fin 6) :
 107    tetSqEdgesOfField N (planeWaveEdgeField N E k t) cellTet f =
 108      freudenthalTetSqEdges f + t * planeWaveTetVelocity N E k cellTet f := by
 109  simp only [tetSqEdgesOfField, planeWaveEdgeField, planeWaveTetVelocity]
 110  rw [show freudenthalTetSqEdges f =
 111      periodicDispSqEdge ((localEdgeOf cellTet.1 cellTet.2 f).disp) from
 112    freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf cellTet.1 cellTet.2 f]
 113  ring
 114
 115/-- At `t = 0` the local tuple is exactly the flat Freudenthal tuple. -/
 116theorem planeWaveTetSqEdges_zero (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
 117    (cellTet : PeriodicTet N N N) :
 118    tetSqEdgesOfField N (planeWaveEdgeField N E k 0) cellTet =
 119      freudenthalTetSqEdges := by
 120  funext f
 121  rw [planeWaveTetSqEdges_apply, zero_mul, add_zero]
 122
 123/-- (a) THEOREM, smoothness: the local squared-edge path is `C^n` in the
 124amplitude for every order (it is affine). -/
 125theorem planeWaveTetSqEdges_contDiff (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
 126    (cellTet : PeriodicTet N N N) (n : ℕ∞) :
 127    ContDiff ℝ n
 128      (fun t : ℝ => tetSqEdgesOfField N (planeWaveEdgeField N E k t) cellTet) := by
 129  have h : (fun t : ℝ => tetSqEdgesOfField N (planeWaveEdgeField N E k t) cellTet) =
 130      fun t : ℝ => fun f : Fin 6 =>
 131        freudenthalTetSqEdges f + t * planeWaveTetVelocity N E k cellTet f := by
 132    funext t f
 133    exact planeWaveTetSqEdges_apply N E k cellTet t f
 134  rw [h]
 135  refine contDiff_pi.mpr fun f => ?_
 136  exact contDiff_const.add (contDiff_id.mul contDiff_const)
 137
 138/-- Each single plane-wave edge value is `C^n` in the amplitude (affine). -/
 139theorem planeWaveEdgeValue_contDiff (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
 140    (e : PeriodicEdge N N N) (n : ℕ∞) :
 141    ContDiff ℝ n (fun t : ℝ => planeWaveEdgeField N E k t e) := by
 142  have h : (fun t : ℝ => planeWaveEdgeField N E k t e) =
 143      fun t : ℝ => periodicDispSqEdge e.disp +
 144        t * (polEdgeCoeff E e.disp * Real.cos (edgeMidpointPhase N k e)) := by
 145    funext t
 146    simp only [planeWaveEdgeField]
 147    ring
 148  rw [h]
 149  exact contDiff_const.add (contDiff_id.mul contDiff_const)
 150
 151/-! ## §2. (b) Endpoint/positivity safety at flat and angle smoothness -/
 152
 153/-- (b) THEOREM: each local dihedral angle along the plane-wave family is
 154`ContDiffAt` at amplitude `0` of every finite order.  The flat point is the
 155nondegenerate Freudenthal tetrahedron (`cm3 = 8 > 0`, cosines
 156`√2/2, 0, 1/2` strictly inside `(-1,1)` — `ReggeTTDerivativeGate`
 157`flatCos_ne_endpoints`), so the angle map is `ContDiffAt` in the 6-tuple
 158there; composition with the affine path gives the amplitude smoothness. -/
 159theorem tetDihedralAngle_planeWave_contDiffAt (E : Fin 3 → Fin 3 → ℝ)
 160    (k : Fin 3 → ℝ) (cellTet : PeriodicTet N N N) (f : Fin 6) (n : ℕ∞) :
 161    ContDiffAt ℝ n
 162      (fun t : ℝ => tetDihedralAngleOfField N (planeWaveEdgeField N E k t) cellTet f)
 163      0 := by
 164  have hangle : ContDiffAt ℝ n (fun a : SqEdges => dihedralAngle3Sq a f)
 165      freudenthalTetSqEdges :=
 166    Geometry.ReggeActionFirstVariation.dihedralAngle3Sq_contDiffAt_nonDegenerate
 167      freudenthalTet f n (ReggeTTDerivativeGate.flatCos_ne_endpoints f)
 168  have hpath : ContDiffAt ℝ n
 169      (fun t : ℝ => tetSqEdgesOfField N (planeWaveEdgeField N E k t) cellTet) 0 :=
 170    (planeWaveTetSqEdges_contDiff N E k cellTet n).contDiffAt
 171  have hangle' : ContDiffAt ℝ n (fun a : SqEdges => dihedralAngle3Sq a f)
 172      (tetSqEdgesOfField N (planeWaveEdgeField N E k 0) cellTet) := by
 173    rw [planeWaveTetSqEdges_zero]
 174    exact hangle
 175  have hcomp := ContDiffAt.comp (x := (0 : ℝ)) hangle' hpath
 176  exact hcomp.congr_of_eventuallyEq (by
 177    filter_upwards with t
 178    rfl)
 179
 180/-! ## §3. (c) The action profile is `ContDiffAt` at `0` of every order -/
 181
 182/-- The per-tetrahedron angle contribution to one edge's angle sum is
 183`ContDiffAt` at `0` (finite case split on the slot lookup; `none` branch is
 184the constant `0`). -/
 185theorem edgeAngleContribution_planeWave_contDiffAt (E : Fin 3 → Fin 3 → ℝ)
 186    (k : Fin 3 → ℝ) (e : PeriodicEdge N N N) (cellTet : PeriodicTet N N N)
 187    (n : ℕ∞) :
 188    ContDiffAt ℝ n
 189      (fun t : ℝ =>
 190        edgeAngleContributionOfField N (planeWaveEdgeField N E k t) e cellTet)
 191      0 := by
 192  unfold edgeAngleContributionOfField
 193  cases h : canonicalEdgeSlot? e cellTet.1 cellTet.2 with
 194  | none => simpa [h] using contDiffAt_const (c := (0 : ℝ))
 195  | some f =>
 196      simpa [h] using
 197        tetDihedralAngle_planeWave_contDiffAt N E k cellTet f n
 198
 199/-- Each edge deficit along the plane-wave family is `ContDiffAt` at `0`
 200(constant `2π` minus a finite sum of smooth contributions). -/
 201theorem deficit_planeWave_contDiffAt (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
 202    (e : PeriodicEdge N N N) (n : ℕ∞) :
 203    ContDiffAt ℝ n
 204      (fun t : ℝ => deficitOfField N (planeWaveEdgeField N E k t) e) 0 := by
 205  unfold deficitOfField
 206  refine ContDiffAt.sub contDiffAt_const ?_
 207  exact ContDiffAt.sum fun cellTet _ =>
 208    edgeAngleContribution_planeWave_contDiffAt N E k e cellTet n
 209
 210/-- The square-root hinge factor of each edge is `ContDiffAt` at `0`: the
 211edge value at `t = 0` is `periodicDispSqEdge ∈ {1,2,3} > 0`, so `√` is
 212smooth there. -/
 213theorem sqrtEdge_planeWave_contDiffAt (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
 214    (e : PeriodicEdge N N N) (n : ℕ∞) :
 215    ContDiffAt ℝ n
 216      (fun t : ℝ => Real.sqrt (planeWaveEdgeField N E k t e)) 0 := by
 217  refine ContDiffAt.sqrt ((planeWaveEdgeValue_contDiff N E k e n).contDiffAt) ?_
 218  simp only [planeWaveEdgeField, zero_mul, add_zero]
 219  exact ne_of_gt (periodicDispSqEdge_pos e.disp)
 220
 221/-- (c) THEOREM: the plane-wave action profile of the TRUE nonlinear Regge
 222action is `ContDiffAt ℝ n` at `t = 0` for every finite order `n`. -/
 223theorem planeWaveActionProfile_contDiffAt (E : Fin 3 → Fin 3 → ℝ)
 224    (k : Fin 3 → ℝ) (n : ℕ∞) :
 225    ContDiffAt ℝ n (planeWaveActionProfile N E k) 0 := by
 226  have h : planeWaveActionProfile N E k =
 227      fun t : ℝ => ∑ e : PeriodicEdge N N N,
 228        Real.sqrt (planeWaveEdgeField N E k t e) *
 229          deficitOfField N (planeWaveEdgeField N E k t) e := by
 230    funext t
 231    rfl
 232  rw [h]
 233  exact ContDiffAt.sum fun e _ =>
 234    (sqrtEdge_planeWave_contDiffAt N E k e n).mul
 235      (deficit_planeWave_contDiffAt N E k e n)
 236
 237/-! ## §4. (d) The reusable centered second-difference bridge -/
 238
 239/-- Slope average identity: for `t ≠ 0`,
 240`(g(t) − g(−t))/(2t) = (slope g 0 t + slope g 0 (−t))/2`. -/
 241theorem slope_average_eq (g : ℝ → ℝ) {t : ℝ} (_ht : t ≠ 0) :
 242    (g t - g (-t)) / (2 * t) =
 243      (slope g 0 t + slope g 0 (-t)) / 2 := by
 244  rw [slope_def_field, slope_def_field, sub_zero, sub_zero, div_neg,
 245    ← sub_eq_add_neg, div_sub_div_same, sub_sub_sub_cancel_right,
 246    div_div, mul_comm t 2]
 247
 248/-- (d) THEOREM, THE REUSABLE LOCAL BRIDGE: if `f : ℝ → ℝ` is `C²` at `0`,
 249the centered second difference `(f(t) − 2f(0) + f(−t))/t²` converges along
 250the punctured neighborhood filter to `iteratedDeriv 2 f 0`.
 251
 252Route (LOCAL Taylor / L'Hôpital, panel-approved): one pass of L'Hôpital's
 253rule for `0/0` forms on the punctured neighborhood
 254(`HasDerivAt.lhopital_zero_nhdsNE`) with numerator `g(t) = f(t) − 2f(0) +
 255f(−t)` and denominator `t²` reduces the limit to
 256`(f'(t) − f'(−t))/(2t) → f''(0)`, which is the average of the two slope
 257quotients of `deriv f` at `0` and converges by
 258`hasDerivAt_iff_tendsto_slope` applied to `deriv f` (differentiable at `0`
 259with derivative `deriv (deriv f) 0` since `f` is `C²` on a neighborhood).
 260The forbidden global lemma (`continuum_limit_second_order`, global
 261`ContDiff ℝ 4`) is not used. -/
 262theorem tendsto_centeredSecondDifference_of_contDiffAt (f : ℝ → ℝ)
 263    (hf : ContDiffAt ℝ 2 f 0) :
 264    Filter.Tendsto
 265      (fun t : ℝ => (f t - 2 * f 0 + f (-t)) / t ^ (2 : ℕ))
 266      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds (iteratedDeriv 2 f 0)) := by
 267  -- Extract a symmetric open ball on which f is C².
 268  obtain ⟨u, hu_mem, hu⟩ := hf.contDiffOn (le_refl 2) (by simp)
 269  obtain ⟨ε, hε, hball⟩ := Metric.mem_nhds_iff.mp hu_mem
 270  have hfC2 : ContDiffOn ℝ 2 f (Metric.ball (0 : ℝ) ε) := hu.mono hball
 271  have hopen : IsOpen (Metric.ball (0 : ℝ) ε) := Metric.isOpen_ball
 272  have h0mem : (0 : ℝ) ∈ Metric.ball (0 : ℝ) ε := Metric.mem_ball_self hε
 273  -- deriv f is C¹ on the ball, hence differentiable at 0 with the second derivative.
 274  have hderivC1 : ContDiffOn ℝ 1 (deriv f) (Metric.ball (0 : ℝ) ε) :=
 275    hfC2.deriv_of_isOpen hopen (by norm_num)
 276  have hderiv_diffAt : DifferentiableAt ℝ (deriv f) 0 :=
 277    ((hderivC1.contDiffAt (hopen.mem_nhds h0mem)).differentiableAt (by norm_num))
 278  have hD : HasDerivAt (deriv f) (deriv (deriv f) 0) 0 := hderiv_diffAt.hasDerivAt
 279  set D : ℝ := deriv (deriv f) 0 with hD_def
 280  -- Membership of ±t in the ball, eventually on the punctured filter.
 281  have hmem_event : ∀ᶠ t in nhdsWithin (0 : ℝ) {(0 : ℝ)}ᶜ,
 282      t ∈ Metric.ball (0 : ℝ) ε ∧ -t ∈ Metric.ball (0 : ℝ) ε := by
 283    have hball_event : ∀ᶠ t in nhds (0 : ℝ),
 284        t ∈ Metric.ball (0 : ℝ) ε ∧ -t ∈ Metric.ball (0 : ℝ) ε := by
 285      have h1 : ∀ᶠ t in nhds (0 : ℝ), t ∈ Metric.ball (0 : ℝ) ε :=
 286        hopen.mem_nhds h0mem
 287      have hneg_cont : Filter.Tendsto (fun t : ℝ => -t) (nhds 0) (nhds 0) := by
 288        simpa using (continuous_neg (G := ℝ)).tendsto (0 : ℝ)
 289      have h2 : ∀ᶠ t in nhds (0 : ℝ), -t ∈ Metric.ball (0 : ℝ) ε :=
 290        hneg_cont.eventually h1
 291      exact h1.and h2
 292    exact hball_event.filter_mono nhdsWithin_le_nhds
 293  -- f is differentiable at every point of the ball, with derivative deriv f.
 294  have hfd : ∀ x ∈ Metric.ball (0 : ℝ) ε, HasDerivAt f (deriv f x) x := by
 295    intro x hx
 296    exact ((hfC2.contDiffAt (hopen.mem_nhds hx)).differentiableAt
 297      (by norm_num)).hasDerivAt
 298  -- The numerator g and its derivative on the punctured ball.
 299  have hgg' : ∀ᶠ t in nhdsWithin (0 : ℝ) {(0 : ℝ)}ᶜ,
 300      HasDerivAt (fun s : ℝ => f s - 2 * f 0 + f (-s))
 301        (deriv f t - deriv f (-t)) t := by
 302    filter_upwards [hmem_event] with t hmem
 303    have hft : HasDerivAt f (deriv f t) t := hfd t hmem.1
 304    have hfnt : HasDerivAt f (deriv f (-t)) (-t) := hfd (-t) hmem.2
 305    have hneg : HasDerivAt (fun s : ℝ => -s) (-1 : ℝ) t := hasDerivAt_neg' t
 306    have hcomp : HasDerivAt (fun s : ℝ => f (-s)) (deriv f (-t) * (-1)) t :=
 307      HasDerivAt.comp t hfnt hneg
 308    have hsum := ((hft.sub_const (2 * f 0)).add hcomp)
 309    have hval : deriv f t + deriv f (-t) * (-1) = deriv f t - deriv f (-t) := by
 310      ring
 311    rw [hval] at hsum
 312    exact hsum
 313  -- The denominator t² and its derivative 2t.
 314  have hhh' : ∀ᶠ t in nhdsWithin (0 : ℝ) {(0 : ℝ)}ᶜ,
 315      HasDerivAt (fun s : ℝ => s ^ (2 : ℕ)) (2 * t) t := by
 316    filter_upwards with t
 317    simpa using hasDerivAt_pow 2 t
 318  have hden_ne : ∀ᶠ t in nhdsWithin (0 : ℝ) {(0 : ℝ)}ᶜ, 2 * t ≠ 0 := by
 319    filter_upwards [self_mem_nhdsWithin] with t ht
 320    exact mul_ne_zero two_ne_zero ht
 321  -- Both numerator and denominator tend to 0.
 322  have hf_cont : ContinuousAt f 0 := hf.continuousAt
 323  have hnum_tendsto : Filter.Tendsto (fun s : ℝ => f s - 2 * f 0 + f (-s))
 324      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds 0) := by
 325    have hneg_cont : Filter.Tendsto (fun t : ℝ => -t) (nhds (0 : ℝ)) (nhds 0) := by
 326      simpa using (continuous_neg (G := ℝ)).tendsto (0 : ℝ)
 327    have hcompneg : Filter.Tendsto (fun s : ℝ => f (-s)) (nhds 0) (nhds (f 0)) := by
 328      simpa [Function.comp_def] using hf_cont.tendsto.comp hneg_cont
 329    have h1 : Filter.Tendsto (fun s : ℝ => f s - 2 * f 0 + f (-s))
 330        (nhds 0) (nhds (f 0 - 2 * f 0 + f 0)) :=
 331      (hf_cont.tendsto.sub tendsto_const_nhds).add hcompneg
 332    have hval : f 0 - 2 * f 0 + f 0 = 0 := by ring
 333    rw [hval] at h1
 334    exact h1.mono_left nhdsWithin_le_nhds
 335  have hden_tendsto : Filter.Tendsto (fun s : ℝ => s ^ (2 : ℕ))
 336      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds 0) := by
 337    have h1 : Filter.Tendsto (fun s : ℝ => s ^ (2 : ℕ)) (nhds 0)
 338        (nhds ((0 : ℝ) ^ (2 : ℕ))) :=
 339      (continuous_pow 2).tendsto (0 : ℝ)
 340    rw [show ((0 : ℝ) ^ (2 : ℕ)) = 0 by norm_num] at h1
 341    exact h1.mono_left nhdsWithin_le_nhds
 342  -- The derivative quotient tends to D by slope averaging.
 343  have hslope : Filter.Tendsto (slope (deriv f) 0)
 344      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds D) :=
 345    hasDerivAt_iff_tendsto_slope.mp hD
 346  have hnegmap : Filter.Tendsto (fun t : ℝ => -t)
 347      (nhdsWithin (0 : ℝ) {(0 : ℝ)}ᶜ) (nhdsWithin (0 : ℝ) {(0 : ℝ)}ᶜ) := by
 348    have h1 : Filter.Tendsto (fun t : ℝ => -t) (nhds 0) (nhds 0) := by
 349      simpa using (continuous_neg (G := ℝ)).tendsto (0 : ℝ)
 350    refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
 351      (h1.mono_left nhdsWithin_le_nhds) ?_
 352    filter_upwards [self_mem_nhdsWithin] with t ht
 353    exact neg_ne_zero.mpr ht
 354  have hslope_neg : Filter.Tendsto (fun t : ℝ => slope (deriv f) 0 (-t))
 355      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds D) :=
 356    hslope.comp hnegmap
 357  have havg : Filter.Tendsto
 358      (fun t : ℝ =>
 359        (slope (deriv f) 0 t + slope (deriv f) 0 (-t)) / 2)
 360      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds ((D + D) / 2)) :=
 361    (hslope.add hslope_neg).div_const 2
 362  rw [show (D + D) / 2 = D by ring] at havg
 363  have hdiv : Filter.Tendsto
 364      (fun t : ℝ => (deriv f t - deriv f (-t)) / (2 * t))
 365      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds D) := by
 366    refine havg.congr' ?_
 367    filter_upwards [self_mem_nhdsWithin] with t ht
 368    exact (slope_average_eq (deriv f) ht).symm
 369  -- One L'Hôpital pass assembles the limit.
 370  have hlim := HasDerivAt.lhopital_zero_nhdsNE hgg' hhh' hden_ne
 371    hnum_tendsto hden_tendsto hdiv
 372  have hiter : iteratedDeriv 2 f 0 = D := by
 373    rw [show (2 : ℕ) = 1 + 1 from rfl, iteratedDeriv_succ, iteratedDeriv_one]
 374  rw [hiter]
 375  exact hlim
 376
 377/-! ## §5. (e) THE FIXED-`N` TT BLOCH SYMBOL EXISTS -/
 378
 379/-- (e) HEADLINE THEOREM (first existence theorem of the program): for
 380every side `N`, every polarization matrix `E`, and every integer wave
 381vector `m`, the fixed-`N` TT Bloch symbol EXISTS and equals
 382`(2/N³) · S''(0)` where `S` is the plane-wave action profile of the TRUE
 383nonlinear Regge action.  Exact bookkeeping: the preflight's
 384`ttSecondDifference` is `(2/N³) · [(S(t) − 2S(0) + S(−t))/t²]` and the
 385bracket converges to `iteratedDeriv 2 S 0` by the local bridge (d) — no
 386stray `1/2` anywhere.  NOTE: this identifies the LIMIT, not its value; the
 387continuum `-(1/4)` target remains OPEN. -/
 388theorem planeWave_TTBlochSymbolIs_secondVariation (E : Fin 3 → Fin 3 → ℝ)
 389    (m : Fin 3 → ℤ) :
 390    TTBlochSymbolIs N E m
 391      ((2 / (N : ℝ) ^ (3 : ℕ)) *
 392        iteratedDeriv 2 (planeWaveActionProfile N E (commensurateMomentum N m)) 0) := by
 393  set k : Fin 3 → ℝ := commensurateMomentum N m with hk
 394  set S : ℝ → ℝ := planeWaveActionProfile N E k with hS
 395  have hC2 : ContDiffAt ℝ 2 S 0 := planeWaveActionProfile_contDiffAt N E k 2
 396  have hbridge := tendsto_centeredSecondDifference_of_contDiffAt S hC2
 397  unfold TTBlochSymbolIs
 398  have hconst := hbridge.const_mul (2 / (N : ℝ) ^ (3 : ℕ))
 399  refine hconst.congr' ?_
 400  filter_upwards with t
 401  unfold ttSecondDifference
 402  rw [← hk, ← hS, mul_div_assoc]
 403
 404/-- Companion existence form: there IS a real number `H` with
 405`TTBlochSymbolIs N E m H` — the fixed-`N` symbol object is non-vacuous for
 406every polarization and wave vector. -/
 407theorem planeWave_TTBlochSymbol_exists (E : Fin 3 → Fin 3 → ℝ)
 408    (m : Fin 3 → ℤ) :
 409    ∃ H : ℝ, TTBlochSymbolIs N E m H :=
 410  ⟨_, planeWave_TTBlochSymbolIs_secondVariation N E m⟩
 411
 412end
 413
 414end ReggeTTLocalSymbolExistence
 415end Analysis
 416end Gravity
 417end IndisputableMonolith
 418