IndisputableMonolith.Gravity.Analysis.ReggeTTFlatSecondVariation
IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean · 887 lines · 37 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolPreflight
2import IndisputableMonolith.Gravity.Analysis.ReggeTTDerivativeGate
3import IndisputableMonolith.Gravity.Analysis.ReggeTTLocalSymbolExistence
4
5/-!
6# Regge TT flat second variation, Schläfli-reduced (Gate A2)
7
8QG full-theory campaign, `ReggeTTContinuumSymbol` program, Crux-1(c) lane,
9Gate A2 of the panel-locked protocol "Normalization-Gated Schläfli Two-Jet"
10(Gate A0 is `ReggeTTSymbolSpecificationAudit`, Gate A1 is
11`ReggeTTLocalSymbolExistence`; the first-derivative structure at flat is
12`ReggeTTDerivativeGate`, reused here, never re-proved).
13
14## What this module proves (all THEOREM)
15
16* Regrouping bijection (`sum_edges_slotMatch`): for every cell/tet and
17 every summand family, the edge-sum of `canonicalEdgeSlot?`-matched values
18 equals the slot-sum over the tet's six local edges. This is the
19 incidence involution "edge-sum of incident-tet hits = tet-sum of slot
20 values", proved from `canonicalEdgeSlot_eq_some_implies` +
21 `canonicalPeriodicLocalEdgeNoDup`.
22* Derivative of the profile at every good amplitude
23 (`hasDerivAt_planeWaveActionProfile`): at every `t` where all edge values
24 are positive and all tetrahedra are nondegenerate with interior cosines,
25 `S'(t) = Σ_e [ (l'_e/(2√l_e))·δ_e + √l_e·δ'_e ]` with every primed object
26 in explicit closed form (`edgeSqrtDeriv`, `deficitDeriv`,
27 `slotAngleDeriv`).
28* PATHWISE SCHLÄFLI KILL (`sum_sqrt_deficitDeriv_eq_zero`): at every good
29 amplitude the ENTIRE second group `Σ_e √l_e·δ'_e` vanishes — regrouped
30 per tetrahedron it is `−Σ_τ Σ_g v_g·(Σ_f √a_f·∂θ_f/∂a_g) = 0` by the
31 proved tetrahedral Schläfli identity (`tetraSchlaefliSixEdgeClosedForm`)
32 at the (nondegenerate) path point. This holds IDENTICALLY near `0`, not
33 just at `0`, and is what deletes every arccos second derivative from the
34 second variation.
35* GATE A2(a) (`trueReggeAction_firstVariation_flat_eq_zero`):
36 `deriv (planeWaveActionProfile N E k) 0 = 0`. At `t = 0` the first
37 group dies (flat deficits vanish, Stage-1 kernel theorem) and the second
38 group dies by the Schläfli kill at flat.
39* GATE A2(b) (`trueReggeAction_secondVariation_flat_schlaefli`):
40 `iteratedDeriv 2 (planeWaveActionProfile N E k) 0
41 = −Σ_τ Σ_f L'_{τf}(0) · θ'_{τf}(0)`
42 with `L'_{τf}(0) = v_{τf}/(2√a*_f)` (`flatSlotSqrtDeriv`) and
43 `θ'_{τf}(0) = Σ_g v_{τg}·J_{fg}` the flat angle Jacobian contraction
44 (`flatSlotAngleDeriv`, `J = flatAngleJacobian` of the derivative gate).
45 NO second derivative of `arccos` appears anywhere: `S'` agrees near `0`
46 with `Σ_e (l'_e/(2√l_e))·δ_e` alone (the `√l·δ'` group is identically
47 zero near `0` by the pathwise Schläfli kill), so `S''(0)` is the
48 `t`-derivative of the FIRST group only, and `δ_e(0) = 0` reduces it to
49 `Σ_e L'_e(0)·δ'_e(0)`, regrouped per tetrahedron.
50* GATE A2(c) (`axisReducedSecondVariation` +
51 `axisReducedSecondVariation_applies`): the reduced formula instantiated
52 at the preregistered axis direction `m = (1,0,0)` with polarization
53 `axisTTPolarizationPlus` at `N = 3`, as a named `Finset`-sum expression
54 and the kernel equation that the reduced formula computes that
55 instance's `S''(0)`. NO numeric value is claimed or evaluated.
56
57## Consequence for the campaign (PASS report)
58
59The explicit-G Hessian stage is deleted from the critical path: the
60second variation of the TRUE nonlinear Regge action at flat is now a
61kernel-checked finite sum of first-derivative data (flat sqrt-edge slopes
62times flat angle-Jacobian contractions), with the arccos second-derivative
63block eliminated by the proved Schläfli identity, not by any symbolic
64differentiation of `arccos` compositions.
65
66## What this module does NOT prove (binding scope disclosure)
67
68* No VALUE of `S''(0)` and no continuum claim: the reduced formula is a
69 kernel identity, not an evaluation. The `-(1/4)` continuum target stays
70 OPEN with status flag `false`; the C10 probe remains NUMERICAL EVIDENCE
71 and is never cited as proof.
72* Combined with Gate A1's bridge, the fixed-`N` symbol equals
73 `(2/N³)·S''(0)` with `S''(0)` given by the reduced formula here; the
74 remaining OPEN work toward the continuum target is the evaluation of the
75 reduced finite sum and its `N → ∞` limit.
76
77## Inherited axiom footprint (disclosure)
78
79Gate A2(a) uses the Stage-1 flat-deficit theorem
80(`deficitOfField_flatEdgeField`), which rides the certified periodic
81angle-sum chain and therefore carries `Lean.ofReduceBool` /
82`Lean.trustCompiler` in addition to the standard trio — inherited
83disclosure, not new axioms. Gate A2(b) also passes through the flat
84point (`δ_e(0) = 0`), so it carries the same inherited pair. No new
85axioms; no `sorry`, no `admit`, no `native_decide` in this file.
86-/
87
88namespace IndisputableMonolith
89namespace Gravity
90namespace Analysis
91namespace ReggeTTFlatSecondVariation
92
93open Geometry.PeriodicFreudenthalTorus
94open Geometry.CayleyMengerPolynomial (SqEdges cm3)
95open Geometry.DihedralCayleyMenger (dihedralCos3Sq)
96open Geometry.DihedralDerivatives (dihedralAngle3Sq dihedralAngle3SqClosedFormDeriv)
97open Geometry.FreudenthalCubeTriangulation (freudenthalTetSqEdges freudenthalTet)
98open ReggeTTSymbolPreflight
99open ReggeTTLocalSymbolExistence
100
101noncomputable section
102
103variable (N : ℕ) [NeZero N]
104
105/-! ## §1. Edge-level closed-form derivative data -/
106
107/-- The affine slope of a single plane-wave edge value:
108`c_e = polEdgeCoeff E d_e · cos(k·x_mid(e))`. On matched slots this is
109definitionally `planeWaveTetVelocity`. -/
110def edgeCoeff (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
111 (e : PeriodicEdge N N N) : ℝ :=
112 polEdgeCoeff E e.disp * Real.cos (edgeMidpointPhase N k e)
113
114/-- The closed-form derivative of the sqrt hinge factor:
115`L'_e(t) = c_e / (2·√(l_e(t)))`. -/
116def edgeSqrtDeriv (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
117 (e : PeriodicEdge N N N) (t : ℝ) : ℝ :=
118 edgeCoeff N E k e / (2 * Real.sqrt (planeWaveEdgeField N E k t e))
119
120/-- Each plane-wave edge value is differentiable in the amplitude with
121derivative its affine slope. -/
122theorem hasDerivAt_edgeValue (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
123 (e : PeriodicEdge N N N) (t₀ : ℝ) :
124 HasDerivAt (fun t : ℝ => planeWaveEdgeField N E k t e)
125 (edgeCoeff N E k e) t₀ := by
126 have h : (fun t : ℝ => planeWaveEdgeField N E k t e) =
127 fun t : ℝ => periodicDispSqEdge e.disp + t * edgeCoeff N E k e := by
128 funext t
129 simp only [planeWaveEdgeField, edgeCoeff]
130 ring
131 rw [h]
132 simpa using ((hasDerivAt_id t₀).mul_const (edgeCoeff N E k e)).const_add
133 (periodicDispSqEdge e.disp)
134
135/-- Derivative of the sqrt hinge factor at any amplitude where the edge
136value is nonzero. -/
137theorem hasDerivAt_sqrtEdge (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
138 (e : PeriodicEdge N N N) (t₀ : ℝ)
139 (hne : planeWaveEdgeField N E k t₀ e ≠ 0) :
140 HasDerivAt (fun t : ℝ => Real.sqrt (planeWaveEdgeField N E k t e))
141 (edgeSqrtDeriv N E k e t₀) t₀ := by
142 have hsq : HasDerivAt Real.sqrt
143 (1 / (2 * Real.sqrt (planeWaveEdgeField N E k t₀ e)))
144 (planeWaveEdgeField N E k t₀ e) :=
145 Real.hasDerivAt_sqrt hne
146 have hcomp := hsq.comp t₀ (hasDerivAt_edgeValue N E k e t₀)
147 have hval : edgeSqrtDeriv N E k e t₀ =
148 1 / (2 * Real.sqrt (planeWaveEdgeField N E k t₀ e)) * edgeCoeff N E k e := by
149 unfold edgeSqrtDeriv
150 ring
151 rw [hval]
152 exact hcomp
153
154/-! ## §2. The directional angle derivative at a general nondegenerate point -/
155
156/-- Directional derivative of one dihedral angle along an affine
157squared-edge path through ANY nondegenerate tetrahedron with interior
158cosine (generalization of the derivative gate's flat-point lemma; same
159proof route: `C¹` Fréchet derivative + the six proved coordinate
160partials). -/
161theorem hasDerivAt_angle_directional
162 (T : Geometry.ReggeRigorousFoundation.NonDegenerateTet) (f : Fin 6)
163 (hEnd : dihedralCos3Sq T.sqEdge f ≠ -1 ∧ dihedralCos3Sq T.sqEdge f ≠ 1)
164 (v : Fin 6 → ℝ) :
165 HasDerivAt
166 (fun t : ℝ => dihedralAngle3Sq (fun j : Fin 6 => T.sqEdge j + t * v j) f)
167 (∑ g : Fin 6, v g * dihedralAngle3SqClosedFormDeriv T.sqEdge f g) 0 := by
168 have hC : ContDiffAt ℝ 1 (fun x : SqEdges => dihedralAngle3Sq x f) T.sqEdge :=
169 Geometry.ReggeActionFirstVariation.dihedralAngle3Sq_contDiffAt_nonDegenerate
170 T f 1 hEnd
171 have hDiff : DifferentiableAt ℝ (fun x : SqEdges => dihedralAngle3Sq x f)
172 T.sqEdge :=
173 hC.differentiableAt (by simp)
174 have hF : HasFDerivAt (fun x : SqEdges => dihedralAngle3Sq x f)
175 (fderiv ℝ (fun x : SqEdges => dihedralAngle3Sq x f) T.sqEdge)
176 T.sqEdge :=
177 hDiff.hasFDerivAt
178 have hγ : HasDerivAt
179 (fun t : ℝ => (fun j : Fin 6 => T.sqEdge j + t * v j)) v 0 := by
180 rw [hasDerivAt_pi]
181 intro j
182 simpa using
183 ((hasDerivAt_id (0 : ℝ)).mul_const (v j)).const_add (T.sqEdge j)
184 have hF' : HasFDerivAt (fun x : SqEdges => dihedralAngle3Sq x f)
185 (fderiv ℝ (fun x : SqEdges => dihedralAngle3Sq x f) T.sqEdge)
186 (fun j : Fin 6 => T.sqEdge j + (0 : ℝ) * v j) := by
187 simpa using hF
188 have hcomp := HasFDerivAt.comp_hasDerivAt (x := (0 : ℝ))
189 (f := fun t : ℝ => (fun j : Fin 6 => T.sqEdge j + t * v j))
190 hF' hγ
191 have hvalue :
192 (fderiv ℝ (fun x : SqEdges => dihedralAngle3Sq x f) T.sqEdge) v =
193 ∑ g : Fin 6, v g * dihedralAngle3SqClosedFormDeriv T.sqEdge f g := by
194 rw [Geometry.ReggeActionFirstVariation.continuousLinearMap_apply_eq_sum_single]
195 refine Finset.sum_congr rfl fun g _ => ?_
196 exact congrArg (fun z => v g * z)
197 (Geometry.ReggeActionFirstVariation.fderiv_dihedralAngle3Sq_apply_single
198 T f g hEnd)
199 rw [hvalue] at hcomp
200 simpa [Function.comp_def] using hcomp
201
202/-! ## §3. Slot-level derivative data along the plane wave -/
203
204/-- Closed-form slot angle derivative along the plane wave:
205`θ'_{τf}(t) = Σ_g v_{τg} · ∂θ_f/∂a_g (a_τ(t))`. -/
206def slotAngleDeriv (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
207 (τ : PeriodicTet N N N) (f : Fin 6) (t : ℝ) : ℝ :=
208 ∑ g : Fin 6,
209 planeWaveTetVelocity N E k τ g *
210 dihedralAngle3SqClosedFormDeriv
211 (tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ) f g
212
213/-- Derivative of one slot angle along the plane wave at any amplitude
214where the tetrahedron is nondegenerate with interior cosine (shift of the
215directional lemma to base point `t₀` — the path is affine, so it is the
216same affine path re-based at `a_τ(t₀)`). -/
217theorem hasDerivAt_slotAngle (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
218 (τ : PeriodicTet N N N) (f : Fin 6) (t₀ : ℝ)
219 (hpos : ∀ j : Fin 6,
220 0 < tetSqEdgesOfField N (planeWaveEdgeField N E k t₀) τ j)
221 (hcm : 0 < cm3 (tetSqEdgesOfField N (planeWaveEdgeField N E k t₀) τ))
222 (hEnd :
223 dihedralCos3Sq (tetSqEdgesOfField N (planeWaveEdgeField N E k t₀) τ) f ≠ -1 ∧
224 dihedralCos3Sq (tetSqEdgesOfField N (planeWaveEdgeField N E k t₀) τ) f ≠ 1) :
225 HasDerivAt
226 (fun t : ℝ => tetDihedralAngleOfField N (planeWaveEdgeField N E k t) τ f)
227 (slotAngleDeriv N E k τ f t₀) t₀ := by
228 set T : Geometry.ReggeRigorousFoundation.NonDegenerateTet :=
229 ⟨tetSqEdgesOfField N (planeWaveEdgeField N E k t₀) τ, hpos, hcm⟩ with hT
230 have hgen := hasDerivAt_angle_directional T f hEnd
231 (planeWaveTetVelocity N E k τ)
232 have hshift : HasDerivAt (fun t : ℝ => t - t₀) 1 t₀ :=
233 (hasDerivAt_id t₀).sub_const t₀
234 have hcomp := HasDerivAt.comp_of_eq t₀ hgen hshift (sub_self t₀).symm
235 have hfuneq :
236 (fun t : ℝ => dihedralAngle3Sq
237 (fun j : Fin 6 => T.sqEdge j + (t - t₀) * planeWaveTetVelocity N E k τ j) f)
238 = fun t : ℝ =>
239 tetDihedralAngleOfField N (planeWaveEdgeField N E k t) τ f := by
240 funext t
241 unfold tetDihedralAngleOfField
242 congr 1
243 funext j
244 show tetSqEdgesOfField N (planeWaveEdgeField N E k t₀) τ j +
245 (t - t₀) * planeWaveTetVelocity N E k τ j =
246 tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ j
247 rw [planeWaveTetSqEdges_apply N E k τ t₀ j,
248 planeWaveTetSqEdges_apply N E k τ t j]
249 ring
250 have hcomp' : HasDerivAt
251 (fun t : ℝ => dihedralAngle3Sq
252 (fun j : Fin 6 => T.sqEdge j + (t - t₀) * planeWaveTetVelocity N E k τ j) f)
253 ((∑ g : Fin 6, planeWaveTetVelocity N E k τ g *
254 dihedralAngle3SqClosedFormDeriv T.sqEdge f g) * 1) t₀ := by
255 simpa [Function.comp_def] using hcomp
256 rw [hfuneq] at hcomp'
257 simpa [slotAngleDeriv, hT] using hcomp'
258
259/-! ## §4. Contribution and deficit derivatives -/
260
261/-- Closed-form derivative of one edge-tet angle contribution (the slot
262match, `none` branch constant `0`). -/
263def contribDeriv (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
264 (e : PeriodicEdge N N N) (τ : PeriodicTet N N N) (t : ℝ) : ℝ :=
265 match canonicalEdgeSlot? e τ.1 τ.2 with
266 | some f => slotAngleDeriv N E k τ f t
267 | none => 0
268
269/-- Derivative of one edge-tet angle contribution at a good amplitude. -/
270theorem hasDerivAt_contrib (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
271 (e : PeriodicEdge N N N) (τ : PeriodicTet N N N) (t₀ : ℝ)
272 (hpos : ∀ j : Fin 6,
273 0 < tetSqEdgesOfField N (planeWaveEdgeField N E k t₀) τ j)
274 (hcm : 0 < cm3 (tetSqEdgesOfField N (planeWaveEdgeField N E k t₀) τ))
275 (hEnd : ∀ f : Fin 6,
276 dihedralCos3Sq (tetSqEdgesOfField N (planeWaveEdgeField N E k t₀) τ) f ≠ -1 ∧
277 dihedralCos3Sq (tetSqEdgesOfField N (planeWaveEdgeField N E k t₀) τ) f ≠ 1) :
278 HasDerivAt
279 (fun t : ℝ =>
280 edgeAngleContributionOfField N (planeWaveEdgeField N E k t) e τ)
281 (contribDeriv N E k e τ t₀) t₀ := by
282 unfold edgeAngleContributionOfField contribDeriv
283 cases h : canonicalEdgeSlot? e τ.1 τ.2 with
284 | none => simpa [h] using hasDerivAt_const t₀ (0 : ℝ)
285 | some f =>
286 simpa [h] using
287 hasDerivAt_slotAngle N E k τ f t₀ hpos hcm (hEnd f)
288
289/-- Closed-form deficit derivative:
290`δ'_e(t) = −Σ_τ (matched θ'_{τf}(t))`. -/
291def deficitDeriv (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
292 (e : PeriodicEdge N N N) (t : ℝ) : ℝ :=
293 -∑ τ : PeriodicTet N N N, contribDeriv N E k e τ t
294
295/-- The goodness predicate for an amplitude: all edge values positive, all
296tetrahedra nondegenerate with strictly interior cosines. -/
297def PathGoodAt (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ) (t : ℝ) : Prop :=
298 (∀ e : PeriodicEdge N N N, 0 < planeWaveEdgeField N E k t e) ∧
299 ∀ τ : PeriodicTet N N N,
300 0 < cm3 (tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ) ∧
301 ∀ f : Fin 6,
302 0 < tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ f ∧
303 (-1 < dihedralCos3Sq
304 (tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ) f ∧
305 dihedralCos3Sq
306 (tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ) f < 1)
307
308/-- The flat amplitude is good: edge values are the positive displacement
309classes, every tetrahedron is the Freudenthal tetrahedron (`cm3 = 8 > 0`),
310and every flat cosine is strictly interior. -/
311theorem pathGoodAt_zero (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ) :
312 PathGoodAt N E k 0 := by
313 constructor
314 · intro e
315 simp only [planeWaveEdgeField, zero_mul, add_zero]
316 exact periodicDispSqEdge_pos e.disp
317 · intro τ
318 rw [planeWaveTetSqEdges_zero]
319 refine ⟨?_, ?_⟩
320 · rw [Geometry.FreudenthalCubeTriangulation.cm3_freudenthalTetSqEdges]
321 norm_num
322 · intro f
323 exact ⟨freudenthalTet.sqEdge_pos f,
324 ReggeTTDerivativeGate.flatCos_bounds f⟩
325
326/-- Goodness persists on a neighborhood of the flat amplitude
327(continuity of the affine paths + the derivative gate's flat neighborhood
328nondegeneracy). -/
329theorem eventually_pathGoodAt (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ) :
330 ∀ᶠ t in nhds (0 : ℝ), PathGoodAt N E k t := by
331 have hedges : ∀ᶠ t in nhds (0 : ℝ),
332 ∀ e : PeriodicEdge N N N, 0 < planeWaveEdgeField N E k t e := by
333 rw [Filter.eventually_all]
334 intro e
335 have hcont : Filter.Tendsto (fun t : ℝ => planeWaveEdgeField N E k t e)
336 (nhds 0) (nhds (planeWaveEdgeField N E k 0 e)) :=
337 ((planeWaveEdgeValue_contDiff N E k e 0).continuous).continuousAt
338 have hpos : 0 < planeWaveEdgeField N E k 0 e :=
339 (pathGoodAt_zero N E k).1 e
340 exact hcont.eventually (eventually_gt_nhds hpos)
341 have htets : ∀ᶠ t in nhds (0 : ℝ),
342 ∀ τ : PeriodicTet N N N,
343 0 < cm3 (tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ) ∧
344 ∀ f : Fin 6,
345 0 < tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ f ∧
346 (-1 < dihedralCos3Sq
347 (tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ) f ∧
348 dihedralCos3Sq
349 (tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ) f < 1) := by
350 rw [Filter.eventually_all]
351 intro τ
352 have h0 : ContinuousAt
353 (fun t : ℝ => tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ) 0 :=
354 (planeWaveTetSqEdges_contDiff N E k τ 0).continuous.continuousAt
355 have hcont : Filter.Tendsto
356 (fun t : ℝ => tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ)
357 (nhds 0)
358 (nhds (tetSqEdgesOfField N (planeWaveEdgeField N E k 0) τ)) :=
359 h0.tendsto
360 rw [planeWaveTetSqEdges_zero] at hcont
361 have hflat := ReggeTTDerivativeGate.flat_nondegeneracy_eventually
362 have hev := hcont.eventually hflat
363 refine hev.mono fun t ht => ⟨ht.1, fun f => ?_⟩
364 exact ⟨(ht.2 f).1, (ht.2 f).2.2⟩
365 filter_upwards [hedges, htets] with t h1 h2
366 exact ⟨h1, h2⟩
367
368/-- Derivative of one edge deficit at a good amplitude. -/
369theorem hasDerivAt_deficit (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
370 (e : PeriodicEdge N N N) (t₀ : ℝ) (hgood : PathGoodAt N E k t₀) :
371 HasDerivAt (fun t : ℝ => deficitOfField N (planeWaveEdgeField N E k t) e)
372 (deficitDeriv N E k e t₀) t₀ := by
373 have hall : ∀ τ ∈ (Finset.univ : Finset (PeriodicTet N N N)),
374 HasDerivAt
375 (fun t : ℝ =>
376 edgeAngleContributionOfField N (planeWaveEdgeField N E k t) e τ)
377 (contribDeriv N E k e τ t₀) t₀ := by
378 intro τ _
379 exact hasDerivAt_contrib N E k e τ t₀
380 (fun j => ((hgood.2 τ).2 j).1) (hgood.2 τ).1
381 (fun f => ⟨ne_of_gt ((hgood.2 τ).2 f).2.1,
382 ne_of_lt ((hgood.2 τ).2 f).2.2⟩)
383 have hsum := HasDerivAt.fun_sum hall
384 have h := hsum.const_sub (2 * Real.pi)
385 unfold deficitOfField deficitDeriv
386 exact h
387
388/-! ## §5. The profile derivative at every good amplitude -/
389
390/-- The explicit first-variation integrand:
391`T(t) = Σ_e [ L'_e(t)·δ_e(t) + √l_e(t)·δ'_e(t) ]`. -/
392def firstVariationIntegrand (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
393 (t : ℝ) : ℝ :=
394 ∑ e : PeriodicEdge N N N,
395 (edgeSqrtDeriv N E k e t *
396 deficitOfField N (planeWaveEdgeField N E k t) e +
397 Real.sqrt (planeWaveEdgeField N E k t e) * deficitDeriv N E k e t)
398
399/-- THE PROFILE DERIVATIVE (THEOREM): at every good amplitude,
400`S'(t) = Σ_e [ (l'_e/(2√l_e))·δ_e + √l_e·δ'_e ]` — every primed object in
401explicit closed form. -/
402theorem hasDerivAt_planeWaveActionProfile (E : Fin 3 → Fin 3 → ℝ)
403 (k : Fin 3 → ℝ) (t₀ : ℝ) (hgood : PathGoodAt N E k t₀) :
404 HasDerivAt (planeWaveActionProfile N E k)
405 (firstVariationIntegrand N E k t₀) t₀ := by
406 have hfun : planeWaveActionProfile N E k =
407 fun t : ℝ => ∑ e : PeriodicEdge N N N,
408 Real.sqrt (planeWaveEdgeField N E k t e) *
409 deficitOfField N (planeWaveEdgeField N E k t) e := by
410 funext t
411 rfl
412 rw [hfun]
413 unfold firstVariationIntegrand
414 have hall : ∀ e ∈ (Finset.univ : Finset (PeriodicEdge N N N)),
415 HasDerivAt
416 (fun t : ℝ => Real.sqrt (planeWaveEdgeField N E k t e) *
417 deficitOfField N (planeWaveEdgeField N E k t) e)
418 (edgeSqrtDeriv N E k e t₀ *
419 deficitOfField N (planeWaveEdgeField N E k t₀) e +
420 Real.sqrt (planeWaveEdgeField N E k t₀ e) *
421 deficitDeriv N E k e t₀) t₀ := by
422 intro e _
423 exact (hasDerivAt_sqrtEdge N E k e t₀ (ne_of_gt (hgood.1 e))).mul
424 (hasDerivAt_deficit N E k e t₀ hgood)
425 exact HasDerivAt.fun_sum hall
426
427/-! ## §6. The regrouping bijection (edge-sum ↔ tet-slot-sum) -/
428
429/-- Constant multiplication distributes through the slot match. -/
430theorem slotMatch_mul (c : ℝ) (m : Option (Fin 6)) (G : Fin 6 → ℝ) :
431 (c * match m with | some f => G f | none => 0) =
432 match m with | some f => c * G f | none => 0 := by
433 cases m with
434 | none => simp
435 | some f => rfl
436
437/-- THE REGROUPING BIJECTION (THEOREM): for every cell/tet and every
438family `F`, the edge-sum of `canonicalEdgeSlot?`-matched values equals the
439slot-sum over the tet's six local edges. This is the incidence
440involution reused by every regrouped Regge sum. -/
441theorem sum_edges_slotMatch (cell : Vertex N N N) (tet : Fin 6)
442 (F : PeriodicEdge N N N → Fin 6 → ℝ) :
443 (∑ e : PeriodicEdge N N N,
444 match canonicalEdgeSlot? e cell tet with
445 | some f => F e f
446 | none => 0) =
447 ∑ f : Fin 6, F (localEdgeOf cell tet f) f := by
448 have hnodup : ∀ f g : Fin 6,
449 localEdgeOf cell tet f = localEdgeOf cell tet g → f = g :=
450 fun f g h => canonicalPeriodicLocalEdgeNoDup N N N cell tet f g h
451 have hstep : ∀ e : PeriodicEdge N N N,
452 (match canonicalEdgeSlot? e cell tet with
453 | some f => F e f
454 | none => 0) =
455 ∑ f : Fin 6, if e = localEdgeOf cell tet f then F e f else 0 := by
456 intro e
457 cases h : canonicalEdgeSlot? e cell tet with
458 | none =>
459 symm
460 refine Finset.sum_eq_zero fun f _ => ?_
461 rw [if_neg]
462 intro heq
463 have hsome := canonicalEdgeSlot_eq_some_of_noDup hnodup heq
464 rw [h] at hsome
465 simp at hsome
466 | some f0 =>
467 have he : e = localEdgeOf cell tet f0 :=
468 canonicalEdgeSlot_eq_some_implies h
469 symm
470 rw [Finset.sum_eq_single f0]
471 · rw [if_pos he]
472 · intro g _ hg
473 rw [if_neg]
474 intro heq
475 apply hg
476 have h2 : localEdgeOf cell tet g = localEdgeOf cell tet f0 := by
477 rw [← heq, ← he]
478 exact hnodup g f0 h2
479 · intro hmem
480 exact absurd (Finset.mem_univ f0) hmem
481 calc
482 (∑ e : PeriodicEdge N N N,
483 match canonicalEdgeSlot? e cell tet with
484 | some f => F e f
485 | none => 0)
486 = ∑ e : PeriodicEdge N N N, ∑ f : Fin 6,
487 if e = localEdgeOf cell tet f then F e f else 0 :=
488 Finset.sum_congr rfl fun e _ => hstep e
489 _ = ∑ f : Fin 6, ∑ e : PeriodicEdge N N N,
490 if e = localEdgeOf cell tet f then F e f else 0 :=
491 Finset.sum_comm
492 _ = ∑ f : Fin 6, F (localEdgeOf cell tet f) f := by
493 refine Finset.sum_congr rfl fun f _ => ?_
494 rw [Finset.sum_ite_eq' Finset.univ (localEdgeOf cell tet f)
495 (fun e => F e f)]
496 rw [if_pos (Finset.mem_univ _)]
497
498/-! ## §7. The pathwise Schläfli kill -/
499
500/-- Per-tet Schläfli against the affine velocity at any nondegenerate path
501point: `Σ_f √(a_f(t)) · θ'_{τf}(t) = 0`. The proved tetrahedral Schläfli
502identity holds in every coordinate direction; contracting with the
503velocity kills the whole block. -/
504theorem sum_sqrt_slotAngleDeriv_eq_zero (E : Fin 3 → Fin 3 → ℝ)
505 (k : Fin 3 → ℝ) (τ : PeriodicTet N N N) (t : ℝ)
506 (hpos : ∀ j : Fin 6,
507 0 < tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ j)
508 (hcm : 0 < cm3 (tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ)) :
509 (∑ f : Fin 6,
510 Real.sqrt (tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ f) *
511 slotAngleDeriv N E k τ f t) = 0 := by
512 set a : SqEdges := tetSqEdgesOfField N (planeWaveEdgeField N E k t) τ with ha
513 have hschl : ∀ g : Fin 6,
514 (∑ f : Fin 6,
515 Real.sqrt (a f) * dihedralAngle3SqClosedFormDeriv a f g) = 0 :=
516 fun g =>
517 Geometry.SchlaefliTetrahedronProof.tetraSchlaefliSixEdgeClosedForm
518 ⟨a, hpos, hcm⟩ g
519 calc
520 (∑ f : Fin 6, Real.sqrt (a f) * slotAngleDeriv N E k τ f t)
521 = ∑ f : Fin 6, Real.sqrt (a f) *
522 (∑ g : Fin 6, planeWaveTetVelocity N E k τ g *
523 dihedralAngle3SqClosedFormDeriv a f g) := by
524 refine Finset.sum_congr rfl fun f _ => ?_
525 unfold slotAngleDeriv
526 rw [← ha]
527 _ = ∑ g : Fin 6, planeWaveTetVelocity N E k τ g *
528 (∑ f : Fin 6, Real.sqrt (a f) *
529 dihedralAngle3SqClosedFormDeriv a f g) := by
530 simp_rw [Finset.mul_sum]
531 rw [Finset.sum_comm]
532 refine Finset.sum_congr rfl fun g _ => ?_
533 refine Finset.sum_congr rfl fun f _ => ?_
534 ring
535 _ = 0 := by
536 refine Finset.sum_eq_zero fun g _ => ?_
537 rw [hschl g, mul_zero]
538
539/-- THE PATHWISE SCHLÄFLI KILL (THEOREM): at every good amplitude the
540ENTIRE second group `Σ_e √l_e(t)·δ'_e(t)` vanishes. Regrouped per
541tetrahedron it is a sum of per-tet Schläfli contractions. This holds
542identically on the good neighborhood of flat — not just at flat — and is
543what removes every arccos second derivative from the second variation. -/
544theorem sum_sqrt_deficitDeriv_eq_zero (E : Fin 3 → Fin 3 → ℝ)
545 (k : Fin 3 → ℝ) (t : ℝ) (hgood : PathGoodAt N E k t) :
546 (∑ e : PeriodicEdge N N N,
547 Real.sqrt (planeWaveEdgeField N E k t e) * deficitDeriv N E k e t) = 0 := by
548 have hstep : ∀ e : PeriodicEdge N N N,
549 Real.sqrt (planeWaveEdgeField N E k t e) * deficitDeriv N E k e t =
550 -∑ τ : PeriodicTet N N N,
551 (match canonicalEdgeSlot? e τ.1 τ.2 with
552 | some f => Real.sqrt (planeWaveEdgeField N E k t e) *
553 slotAngleDeriv N E k τ f t
554 | none => 0) := by
555 intro e
556 unfold deficitDeriv
557 rw [mul_neg, Finset.mul_sum]
558 congr 1
559 refine Finset.sum_congr rfl fun τ _ => ?_
560 unfold contribDeriv
561 exact slotMatch_mul _ _ _
562 calc
563 (∑ e : PeriodicEdge N N N,
564 Real.sqrt (planeWaveEdgeField N E k t e) * deficitDeriv N E k e t)
565 = ∑ e : PeriodicEdge N N N,
566 -∑ τ : PeriodicTet N N N,
567 (match canonicalEdgeSlot? e τ.1 τ.2 with
568 | some f => Real.sqrt (planeWaveEdgeField N E k t e) *
569 slotAngleDeriv N E k τ f t
570 | none => 0) :=
571 Finset.sum_congr rfl fun e _ => hstep e
572 _ = -∑ e : PeriodicEdge N N N, ∑ τ : PeriodicTet N N N,
573 (match canonicalEdgeSlot? e τ.1 τ.2 with
574 | some f => Real.sqrt (planeWaveEdgeField N E k t e) *
575 slotAngleDeriv N E k τ f t
576 | none => 0) := by
577 rw [← Finset.sum_neg_distrib]
578 _ = -∑ τ : PeriodicTet N N N, ∑ e : PeriodicEdge N N N,
579 (match canonicalEdgeSlot? e τ.1 τ.2 with
580 | some f => Real.sqrt (planeWaveEdgeField N E k t e) *
581 slotAngleDeriv N E k τ f t
582 | none => 0) := by
583 rw [Finset.sum_comm]
584 _ = -∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
585 Real.sqrt (planeWaveEdgeField N E k t (localEdgeOf τ.1 τ.2 f)) *
586 slotAngleDeriv N E k τ f t := by
587 congr 1
588 refine Finset.sum_congr rfl fun τ _ => ?_
589 exact sum_edges_slotMatch N τ.1 τ.2
590 (fun e f => Real.sqrt (planeWaveEdgeField N E k t e) *
591 slotAngleDeriv N E k τ f t)
592 _ = 0 := by
593 rw [neg_eq_zero]
594 refine Finset.sum_eq_zero fun τ _ => ?_
595 exact sum_sqrt_slotAngleDeriv_eq_zero N E k τ t
596 (fun j => ((hgood.2 τ).2 j).1) (hgood.2 τ).1
597
598/-! ## §8. Gate A2(a): the first variation vanishes at flat -/
599
600/-- Flat deficits vanish along the plane-wave family at `t = 0`
601(re-export of the Stage-1 kernel theorem through the family). -/
602theorem deficit_planeWave_zero (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
603 (e : PeriodicEdge N N N) :
604 deficitOfField N (planeWaveEdgeField N E k 0) e = 0 := by
605 rw [planeWaveEdgeField_zero_amplitude]
606 exact deficitOfField_flatEdgeField N e
607
608/-- The first-variation integrand vanishes at flat: the deficit group dies
609because flat deficits vanish, the Schläfli group dies by the pathwise
610kill. -/
611theorem firstVariationIntegrand_zero (E : Fin 3 → Fin 3 → ℝ)
612 (k : Fin 3 → ℝ) :
613 firstVariationIntegrand N E k 0 = 0 := by
614 unfold firstVariationIntegrand
615 rw [Finset.sum_add_distrib]
616 have h1 : (∑ e : PeriodicEdge N N N,
617 edgeSqrtDeriv N E k e 0 *
618 deficitOfField N (planeWaveEdgeField N E k 0) e) = 0 := by
619 refine Finset.sum_eq_zero fun e _ => ?_
620 rw [deficit_planeWave_zero, mul_zero]
621 have h2 : (∑ e : PeriodicEdge N N N,
622 Real.sqrt (planeWaveEdgeField N E k 0 e) * deficitDeriv N E k e 0) = 0 :=
623 sum_sqrt_deficitDeriv_eq_zero N E k 0 (pathGoodAt_zero N E k)
624 rw [h1, h2, add_zero]
625
626/-- **GATE A2(a) (THEOREM): the first variation of the true Regge action
627vanishes at the flat point along every plane-wave direction.**
628`S'(0) = Σ_e (l'_e/(2√l_e))·δ_e(0) + Σ_e √l_e(0)·δ'_e(0)`; the first group
629dies because every flat deficit is zero (Stage-1 kernel theorem), the
630second regroups per tetrahedron and dies by the proved Schläfli
631identity. -/
632theorem trueReggeAction_firstVariation_flat_eq_zero (E : Fin 3 → Fin 3 → ℝ)
633 (k : Fin 3 → ℝ) :
634 deriv (planeWaveActionProfile N E k) 0 = 0 := by
635 have hS := hasDerivAt_planeWaveActionProfile N E k 0 (pathGoodAt_zero N E k)
636 rw [hS.deriv]
637 exact firstVariationIntegrand_zero N E k
638
639/-! ## §9. Gate A2(b): the Schläfli-reduced second variation -/
640
641/-- Flat slot sqrt-edge derivative: `L'_{τf}(0) = v_{τf}/(2√a*_f)`. -/
642def flatSlotSqrtDeriv (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
643 (τ : PeriodicTet N N N) (f : Fin 6) : ℝ :=
644 planeWaveTetVelocity N E k τ f / (2 * Real.sqrt (freudenthalTetSqEdges f))
645
646/-- Flat slot angle derivative: `θ'_{τf}(0) = Σ_g v_{τg}·J_{fg}` with `J`
647the shared flat angle Jacobian of the derivative gate. -/
648def flatSlotAngleDeriv (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
649 (τ : PeriodicTet N N N) (f : Fin 6) : ℝ :=
650 ∑ g : Fin 6,
651 planeWaveTetVelocity N E k τ g * ReggeTTDerivativeGate.flatAngleJacobian f g
652
653/-- The edge sqrt-derivative at flat on a matched slot is the flat slot
654sqrt-derivative. -/
655theorem edgeSqrtDeriv_localEdge_zero (E : Fin 3 → Fin 3 → ℝ)
656 (k : Fin 3 → ℝ) (τ : PeriodicTet N N N) (f : Fin 6) :
657 edgeSqrtDeriv N E k (localEdgeOf τ.1 τ.2 f) 0 =
658 flatSlotSqrtDeriv N E k τ f := by
659 unfold edgeSqrtDeriv flatSlotSqrtDeriv edgeCoeff planeWaveTetVelocity
660 simp only [planeWaveEdgeField, zero_mul, add_zero]
661 rw [show periodicDispSqEdge ((localEdgeOf τ.1 τ.2 f).disp) =
662 freudenthalTetSqEdges f from
663 (freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf τ.1 τ.2 f).symm]
664
665/-- The slot angle derivative at flat is the flat Jacobian contraction. -/
666theorem slotAngleDeriv_zero (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
667 (τ : PeriodicTet N N N) (f : Fin 6) :
668 slotAngleDeriv N E k τ f 0 = flatSlotAngleDeriv N E k τ f := by
669 unfold slotAngleDeriv flatSlotAngleDeriv
670 rw [planeWaveTetSqEdges_zero]
671 rfl
672
673/-- The deficit-group first variation regrouped at flat:
674`Σ_e L'_e(0)·δ'_e(0) = −Σ_τ Σ_f L'_{τf}(0)·θ'_{τf}(0)`. -/
675theorem sum_edgeSqrtDeriv_deficitDeriv_flat (E : Fin 3 → Fin 3 → ℝ)
676 (k : Fin 3 → ℝ) :
677 (∑ e : PeriodicEdge N N N,
678 edgeSqrtDeriv N E k e 0 * deficitDeriv N E k e 0) =
679 -∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
680 flatSlotSqrtDeriv N E k τ f * flatSlotAngleDeriv N E k τ f := by
681 have hstep : ∀ e : PeriodicEdge N N N,
682 edgeSqrtDeriv N E k e 0 * deficitDeriv N E k e 0 =
683 -∑ τ : PeriodicTet N N N,
684 (match canonicalEdgeSlot? e τ.1 τ.2 with
685 | some f => edgeSqrtDeriv N E k e 0 * slotAngleDeriv N E k τ f 0
686 | none => 0) := by
687 intro e
688 unfold deficitDeriv
689 rw [mul_neg, Finset.mul_sum]
690 congr 1
691 refine Finset.sum_congr rfl fun τ _ => ?_
692 unfold contribDeriv
693 exact slotMatch_mul _ _ _
694 calc
695 (∑ e : PeriodicEdge N N N,
696 edgeSqrtDeriv N E k e 0 * deficitDeriv N E k e 0)
697 = ∑ e : PeriodicEdge N N N,
698 -∑ τ : PeriodicTet N N N,
699 (match canonicalEdgeSlot? e τ.1 τ.2 with
700 | some f => edgeSqrtDeriv N E k e 0 *
701 slotAngleDeriv N E k τ f 0
702 | none => 0) :=
703 Finset.sum_congr rfl fun e _ => hstep e
704 _ = -∑ e : PeriodicEdge N N N, ∑ τ : PeriodicTet N N N,
705 (match canonicalEdgeSlot? e τ.1 τ.2 with
706 | some f => edgeSqrtDeriv N E k e 0 *
707 slotAngleDeriv N E k τ f 0
708 | none => 0) := by
709 rw [← Finset.sum_neg_distrib]
710 _ = -∑ τ : PeriodicTet N N N, ∑ e : PeriodicEdge N N N,
711 (match canonicalEdgeSlot? e τ.1 τ.2 with
712 | some f => edgeSqrtDeriv N E k e 0 *
713 slotAngleDeriv N E k τ f 0
714 | none => 0) := by
715 rw [Finset.sum_comm]
716 _ = -∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
717 edgeSqrtDeriv N E k (localEdgeOf τ.1 τ.2 f) 0 *
718 slotAngleDeriv N E k τ f 0 := by
719 congr 1
720 refine Finset.sum_congr rfl fun τ _ => ?_
721 exact sum_edges_slotMatch N τ.1 τ.2
722 (fun e f => edgeSqrtDeriv N E k e 0 * slotAngleDeriv N E k τ f 0)
723 _ = -∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
724 flatSlotSqrtDeriv N E k τ f * flatSlotAngleDeriv N E k τ f := by
725 congr 1
726 refine Finset.sum_congr rfl fun τ _ => ?_
727 refine Finset.sum_congr rfl fun f _ => ?_
728 rw [edgeSqrtDeriv_localEdge_zero, slotAngleDeriv_zero]
729
730/-- The reduced first-variation function: near flat, `S'` agrees with the
731deficit group alone (the Schläfli group is identically zero on the good
732neighborhood). -/
733def reducedFirstVariation (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
734 (t : ℝ) : ℝ :=
735 ∑ e : PeriodicEdge N N N,
736 edgeSqrtDeriv N E k e t *
737 deficitOfField N (planeWaveEdgeField N E k t) e
738
739/-- Near flat, the full first-variation integrand equals the reduced
740(deficit-group-only) form. -/
741theorem firstVariationIntegrand_eq_reduced (E : Fin 3 → Fin 3 → ℝ)
742 (k : Fin 3 → ℝ) (t : ℝ) (hgood : PathGoodAt N E k t) :
743 firstVariationIntegrand N E k t = reducedFirstVariation N E k t := by
744 unfold firstVariationIntegrand reducedFirstVariation
745 rw [Finset.sum_add_distrib, sum_sqrt_deficitDeriv_eq_zero N E k t hgood,
746 add_zero]
747
748/-- `deriv S` agrees with the reduced first variation on a neighborhood of
749flat. -/
750theorem deriv_actionProfile_eventuallyEq_reduced (E : Fin 3 → Fin 3 → ℝ)
751 (k : Fin 3 → ℝ) :
752 deriv (planeWaveActionProfile N E k) =ᶠ[nhds (0 : ℝ)]
753 reducedFirstVariation N E k := by
754 filter_upwards [eventually_pathGoodAt N E k] with t hgood
755 rw [(hasDerivAt_planeWaveActionProfile N E k t hgood).deriv]
756 exact firstVariationIntegrand_eq_reduced N E k t hgood
757
758/-- The sqrt-derivative factor is differentiable at flat (needed only for
759the product rule; its derivative value multiplies the vanishing flat
760deficit and never appears in the reduced formula). -/
761theorem edgeSqrtDeriv_differentiableAt (E : Fin 3 → Fin 3 → ℝ)
762 (k : Fin 3 → ℝ) (e : PeriodicEdge N N N) :
763 DifferentiableAt ℝ (fun t : ℝ => edgeSqrtDeriv N E k e t) 0 := by
764 have hpos : 0 < planeWaveEdgeField N E k 0 e := (pathGoodAt_zero N E k).1 e
765 have hsq : HasDerivAt (fun t : ℝ => Real.sqrt (planeWaveEdgeField N E k t e))
766 (edgeSqrtDeriv N E k e 0) 0 :=
767 hasDerivAt_sqrtEdge N E k e 0 (ne_of_gt hpos)
768 have hden : DifferentiableAt ℝ
769 (fun t : ℝ => 2 * Real.sqrt (planeWaveEdgeField N E k t e)) 0 :=
770 (hsq.differentiableAt).const_mul 2
771 have hden_ne : 2 * Real.sqrt (planeWaveEdgeField N E k 0 e) ≠ 0 := by
772 have : 0 < Real.sqrt (planeWaveEdgeField N E k 0 e) :=
773 Real.sqrt_pos.mpr hpos
774 positivity
775 exact (differentiableAt_const (edgeCoeff N E k e)).div hden hden_ne
776
777/-- Derivative of the reduced first variation at flat: only the
778`L'_e(0)·δ'_e(0)` group survives (the other product-rule term carries the
779vanishing flat deficit). -/
780theorem hasDerivAt_reducedFirstVariation_flat (E : Fin 3 → Fin 3 → ℝ)
781 (k : Fin 3 → ℝ) :
782 HasDerivAt (reducedFirstVariation N E k)
783 (∑ e : PeriodicEdge N N N,
784 edgeSqrtDeriv N E k e 0 * deficitDeriv N E k e 0) 0 := by
785 have hterm : ∀ e : PeriodicEdge N N N,
786 HasDerivAt
787 (fun t : ℝ => edgeSqrtDeriv N E k e t *
788 deficitOfField N (planeWaveEdgeField N E k t) e)
789 (edgeSqrtDeriv N E k e 0 * deficitDeriv N E k e 0) 0 := by
790 intro e
791 have hu : HasDerivAt (fun t : ℝ => edgeSqrtDeriv N E k e t)
792 (deriv (fun t : ℝ => edgeSqrtDeriv N E k e t) 0) 0 :=
793 (edgeSqrtDeriv_differentiableAt N E k e).hasDerivAt
794 have hv : HasDerivAt
795 (fun t : ℝ => deficitOfField N (planeWaveEdgeField N E k t) e)
796 (deficitDeriv N E k e 0) 0 :=
797 hasDerivAt_deficit N E k e 0 (pathGoodAt_zero N E k)
798 have hprod := hu.mul hv
799 have hδ0 : deficitOfField N (planeWaveEdgeField N E k 0) e = 0 :=
800 deficit_planeWave_zero N E k e
801 rw [hδ0, mul_zero, zero_add] at hprod
802 exact hprod
803 have hall : ∀ e ∈ (Finset.univ : Finset (PeriodicEdge N N N)),
804 HasDerivAt
805 (fun t : ℝ => edgeSqrtDeriv N E k e t *
806 deficitOfField N (planeWaveEdgeField N E k t) e)
807 (edgeSqrtDeriv N E k e 0 * deficitDeriv N E k e 0) 0 :=
808 fun e _ => hterm e
809 have hsum := HasDerivAt.fun_sum hall
810 unfold reducedFirstVariation
811 exact hsum
812
813/-- **GATE A2(b) HEADLINE (THEOREM): the Schläfli-reduced second variation
814of the true Regge action at flat, as a kernel equation.**
815
816`S''(0) = −Σ_τ Σ_f L'_{τf}(0) · θ'_{τf}(0)`
817
818with `L'_{τf}(0) = v_{τf}/(2√a*_f)` and `θ'_{τf}(0) = Σ_g v_{τg}·J_{fg}`
819(flat angle Jacobian of the derivative gate). NO second derivative of
820`arccos` appears: near flat, `S'` equals the deficit group alone because
821the Schläfli group vanishes identically on the good neighborhood
822(pathwise Schläfli kill); differentiating the deficit group at flat and
823using `δ_e(0) = 0` leaves exactly the displayed contraction. The
824explicit-G Hessian stage is thereby deleted from the critical path. -/
825theorem trueReggeAction_secondVariation_flat_schlaefli
826 (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ) :
827 iteratedDeriv 2 (planeWaveActionProfile N E k) 0 =
828 -∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
829 flatSlotSqrtDeriv N E k τ f * flatSlotAngleDeriv N E k τ f := by
830 rw [show (2 : ℕ) = 1 + 1 from rfl, iteratedDeriv_succ, iteratedDeriv_one]
831 rw [Filter.EventuallyEq.deriv_eq
832 (deriv_actionProfile_eventuallyEq_reduced N E k)]
833 rw [(hasDerivAt_reducedFirstVariation_flat N E k).deriv]
834 exact sum_edgeSqrtDeriv_deficitDeriv_flat N E k
835
836/-! ## §10. Gate A2(c): symbolic cross-check instantiation (axis direction)
837
838The preregistered axis direction `m = (1,0,0)` with the `+`-polarization at
839`N = 3`, stated as a named `Finset`-sum expression plus the kernel equation
840that the reduced formula computes that instance. NO numeric value is
841claimed and nothing is evaluated. -/
842
843/-- The reduced second-variation value for the axis instance at `N = 3`,
844as a `Finset` sum expression (`#eval`-free; MODEL-level named quantity —
845its VALUE is not computed or claimed anywhere in this development). -/
846def axisReducedSecondVariation : ℝ :=
847 -∑ τ : PeriodicTet 3 3 3, ∑ f : Fin 6,
848 flatSlotSqrtDeriv 3 axisTTPolarizationPlus
849 (commensurateMomentum 3 axisWaveVector) τ f *
850 flatSlotAngleDeriv 3 axisTTPolarizationPlus
851 (commensurateMomentum 3 axisWaveVector) τ f
852
853/-- GATE A2(c) (THEOREM): the reduced formula applies verbatim to the
854preregistered axis instance — its `S''(0)` IS the named `Finset` sum.
855Cross-check hook for the (non-proof) numerics lane; no value claimed. -/
856theorem axisReducedSecondVariation_applies :
857 iteratedDeriv 2
858 (planeWaveActionProfile 3 axisTTPolarizationPlus
859 (commensurateMomentum 3 axisWaveVector)) 0 =
860 axisReducedSecondVariation :=
861 trueReggeAction_secondVariation_flat_schlaefli 3 axisTTPolarizationPlus
862 (commensurateMomentum 3 axisWaveVector)
863
864/-! ## §11. Combination with Gate A1: the symbol value in reduced form -/
865
866/-- COMBINED COROLLARY (THEOREM): the fixed-`N` TT Bloch symbol value of
867Gate A1 equals `(2/N³)` times the Schläfli-reduced contraction — existence
868and reduced form together, still with no evaluation and no continuum
869claim. -/
870theorem planeWave_TTBlochSymbolIs_reduced (E : Fin 3 → Fin 3 → ℝ)
871 (m : Fin 3 → ℤ) :
872 TTBlochSymbolIs N E m
873 ((2 / (N : ℝ) ^ (3 : ℕ)) *
874 (-∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
875 flatSlotSqrtDeriv N E (commensurateMomentum N m) τ f *
876 flatSlotAngleDeriv N E (commensurateMomentum N m) τ f)) := by
877 have h := planeWave_TTBlochSymbolIs_secondVariation N E m
878 rwa [trueReggeAction_secondVariation_flat_schlaefli N E
879 (commensurateMomentum N m)] at h
880
881end
882
883end ReggeTTFlatSecondVariation
884end Analysis
885end Gravity
886end IndisputableMonolith
887