Encyclopedia Gravity Gravity Analysis Regge Ttflat Second Variation True Regge Action Second Variatio

ARTICLE 4 claims 4 theorems

Gravity Analysis Regge Ttflat Second Variation True Regge Action Second Variatio

A machine-checked proof shows that the second derivative of a discrete gravity action at flat space is a finite sum of first-derivative data, with the hardest angle terms eliminated by a classical identity.

Verify this page

The second variation at flat

In the discrete geometry approach to gravity called Regge calculus, space is built from flat tetrahedra joined along triangular faces, and the gravitational action is a sum over the edges of the lattice. The quantity in question is the second variation of this action: how the action responds when the edge lengths are perturbed away from a flat, regular configuration by a small plane wave. In the Recognition Science framework, a machine-checked library of formal theorems has proved that this second variation, at the flat point, reduces to a finite sum of first-derivative terms.

The theorem, named trueReggeAction_secondVariation_flat_schlaefli, states that the second derivative of the action profile at zero amplitude equals a negative sum over tetrahedra and their six edges of a product: the derivative of the square-root of the edge length at flat, times the derivative of the dihedral angle at flat. The key structural result is that the entire second group of terms, which would contain second derivatives of the arccos function appearing in the angle formula, vanishes identically near the flat point. This is achieved by the Schläfli identity, a classical relation among the derivatives of the dihedral angles of a tetrahedron, which the library proves in closed form.

What this establishes is a significant simplification: the second variation of the true nonlinear Regge action at flat is now a kernel-checked finite sum of first-derivative data, with the arccos second-derivative block eliminated by the proved Schläfli identity, not by any symbolic differentiation of arccos compositions. The theorem also provides a named reduced formula for a specific axis direction and polarization at lattice size N=3, as a finite sum expression, and proves that this reduced formula computes that instance's second variation.

What the theorem does not claim is equally important. It does not provide a numerical value for the second variation, nor does it make any continuum claim. The reduced formula is a kernel identity, not an evaluation. The target value of -(1/4) for the continuum limit remains open, and the probe that suggests it is numerical evidence, never cited as proof. The remaining open work is the evaluation of the reduced finite sum and its limit as N goes to infinity.

THEOREM trueReggeAction_secondVariation_flat_schlaefli · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean
trueReggeAction_secondVariation_flat_schlaefli · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean:813 
/-- **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
THEOREM sum_sqrt_deficitDeriv_eq_zero · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean
sum_sqrt_deficitDeriv_eq_zero · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean:539 
/-- 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
THEOREM axisReducedSecondVariation_applies · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean
axisReducedSecondVariation_applies · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean:853 
/-- 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)
THEOREM trueReggeAction_secondVariation_flat_schlaefli · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean
trueReggeAction_secondVariation_flat_schlaefli · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean:813 
/-- **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

What this page does not claim

No numeric value of the second variation is claimed or evaluated. No continuum limit is claimed; the target -(1/4) remains open. The C10 probe is numerical evidence, not a proof.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND