Gravity Analysis Regge Ttflat Second Variation

/-- **GATE A2(b) HEADLINE (THEOREM): the Schläfli-reduced second variation
of the true Regge action at flat, as a kernel equation.**

`S''(0) = −Σ_τ Σ_f L'_{τf}(0) · θ'_{τf}(0)`

with `L'_{τf}(0) = v_{τf}/(2√a*_f)` and `θ'_{τf}(0) = Σ_g v_{τg}·J_{fg}`
(flat angle Jacobian of the derivative gate).  NO second derivative of
`arccos` appears: near flat, `S'` equals the deficit group alone because
the Schläfli group vanishes identically on the good neighborhood
(pathwise Schläfli kill); differentiating the deficit group at flat and
using `δ_e(0) = 0` leaves exactly the displayed contraction.  The
explicit-G Hessian stage is thereby deleted from the critical path. -/
theorem trueReggeAction_secondVariation_flat_schlaefli
    (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ) :
    iteratedDeriv 2 (planeWaveActionProfile N E k) 0 =
      -∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
        flatSlotSqrtDeriv N E k τ f * flatSlotAngleDeriv N E k τ f := by
  rw [show (2 : ℕ) = 1 + 1 from rfl, iteratedDeriv_succ, iteratedDeriv_one]
  rw [Filter.EventuallyEq.deriv_eq
    (deriv_actionProfile_eventuallyEq_reduced N E k)]
  rw [(hasDerivAt_reducedFirstVariation_flat N E k).deriv]
  exact sum_edgeSqrtDeriv_deficitDeriv_flat N E k

/-- THE PATHWISE SCHLÄFLI KILL (THEOREM): at every good amplitude the
ENTIRE second group `Σ_e √l_e(t)·δ'_e(t)` vanishes.  Regrouped per
tetrahedron it is a sum of per-tet Schläfli contractions.  This holds
identically on the good neighborhood of flat — not just at flat — and is
what removes every arccos second derivative from the second variation. -/
theorem sum_sqrt_deficitDeriv_eq_zero (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) (t : ℝ) (hgood : PathGoodAt N E k t) :
    (∑ e : PeriodicEdge N N N,
      Real.sqrt (planeWaveEdgeField N E k t e) * deficitDeriv N E k e t) = 0 := by
  have hstep : ∀ e : PeriodicEdge N N N,
      Real.sqrt (planeWaveEdgeField N E k t e) * deficitDeriv N E k e t =
        -∑ τ : PeriodicTet N N N,
          (match canonicalEdgeSlot? e τ.1 τ.2 with
            | some f => Real.sqrt (planeWaveEdgeField N E k t e) *
                slotAngleDeriv N E k τ f t
            | none => 0) := by
    intro e
    unfold deficitDeriv
    rw [mul_neg, Finset.mul_sum]
    congr 1
    refine Finset.sum_congr rfl fun τ _ => ?_
    unfold contribDeriv
    exact slotMatch_mul _ _ _
  calc
    (∑ e : PeriodicEdge N N N,
        Real.sqrt (planeWaveEdgeField N E k t e) * deficitDeriv N E k e t)
        = ∑ e : PeriodicEdge N N N,
            -∑ τ : PeriodicTet N N N,
              (match canonicalEdgeSlot? e τ.1 τ.2 with
                | some f => Real.sqrt (planeWaveEdgeField N E k t e) *
                    slotAngleDeriv N E k τ f t
                | none => 0) :=
          Finset.sum_congr rfl fun e _ => hstep e
    _ = -∑ e : PeriodicEdge N N N, ∑ τ : PeriodicTet N N N,
            (match canonicalEdgeSlot? e τ.1 τ.2 with
              | some f => Real.sqrt (planeWaveEdgeField N E k t e) *
                  slotAngleDeriv N E k τ f t
              | none => 0) := by
          rw [← Finset.sum_neg_distrib]
    _ = -∑ τ : PeriodicTet N N N, ∑ e : PeriodicEdge N N N,
            (match canonicalEdgeSlot? e τ.1 τ.2 with
              | some f => Real.sqrt (planeWaveEdgeField N E k t e) *
                  slotAngleDeriv N E k τ f t
              | none => 0) := by
          rw [Finset.sum_comm]
    _ = -∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
            Real.sqrt (planeWaveEdgeField N E k t (localEdgeOf τ.1 τ.2 f)) *
              slotAngleDeriv N E k τ f t := by
          congr 1
          refine Finset.sum_congr rfl fun τ _ => ?_
          exact sum_edges_slotMatch N τ.1 τ.2
            (fun e f => Real.sqrt (planeWaveEdgeField N E k t e) *
              slotAngleDeriv N E k τ f t)
    _ = 0 := by
          rw [neg_eq_zero]
          refine Finset.sum_eq_zero fun τ _ => ?_
          exact sum_sqrt_slotAngleDeriv_eq_zero N E k τ t
            (fun j => ((hgood.2 τ).2 j).1) (hgood.2 τ).1

/-- **GATE A2(a) (THEOREM): the first variation of the true Regge action
vanishes at the flat point along every plane-wave direction.**
`S'(0) = Σ_e (l'_e/(2√l_e))·δ_e(0) + Σ_e √l_e(0)·δ'_e(0)`; the first group
dies because every flat deficit is zero (Stage-1 kernel theorem), the
second regroups per tetrahedron and dies by the proved Schläfli
identity. -/
theorem trueReggeAction_firstVariation_flat_eq_zero (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) :
    deriv (planeWaveActionProfile N E k) 0 = 0 := by
  have hS := hasDerivAt_planeWaveActionProfile N E k 0 (pathGoodAt_zero N E k)
  rw [hS.deriv]
  exact firstVariationIntegrand_zero N E k

/-- GATE A2(c) (THEOREM): the reduced formula applies verbatim to the
preregistered axis instance — its `S''(0)` IS the named `Finset` sum.
Cross-check hook for the (non-proof) numerics lane; no value claimed. -/
theorem axisReducedSecondVariation_applies :
    iteratedDeriv 2
      (planeWaveActionProfile 3 axisTTPolarizationPlus
        (commensurateMomentum 3 axisWaveVector)) 0 =
      axisReducedSecondVariation :=
  trueReggeAction_secondVariation_flat_schlaefli 3 axisTTPolarizationPlus
    (commensurateMomentum 3 axisWaveVector)