Encyclopedia Gravity Gravity Analysis Regge Ttflat Second Variation Deriv Action Profile Eventually E

ARTICLE 4 claims 4 theorems

Gravity Analysis Regge Ttflat Second Variation Deriv Action Profile Eventually E

A machine-checked result shows that near flat space, the complicated derivative of a gravitational action collapses to a much simpler expression, without yet computing any number.

Verify this page

A local simplification

In the Regge calculus, a discrete approach to general relativity, spacetime is built from flat tetrahedral blocks, and the gravitational action is a sum over their edge lengths and the angles between faces. The framework's machine-checked library of formal theorems analyzes a one-parameter family of such geometries, a plane wave whose amplitude is controlled by a parameter t. At t = 0 the geometry is flat. The declaration deriv_actionProfile_eventuallyEq_reduced (the framework uses a ledger, a discrete record of events, for such statements) proves that the derivative of the action profile with respect to t is, throughout a small neighborhood of t = 0, equal to a reduced expression that drops an entire class of terms.

That reduced expression keeps only the part of the derivative that comes from how the square roots of edge lengths change, multiplied by the angle deficits at each edge. The dropped terms involve how the angles themselves change; the theorem shows they sum to zero identically near flat space, by a geometric identity named for Schläfli. The result is local: it holds for t in a neighborhood of 0, not at that point alone, and it requires the geometry to be well behaved there, with positive edge lengths and nondegenerate tetrahedra. The library proves these conditions hold automatically at t = 0 and in a neighborhood of it.

The payoff is structural. The second variation of the true nonlinear Regge action at flat space, the quantity that governs linearized gravitational waves in this discrete setting, becomes a finite sum of first-derivative data: flat edge-slopes times flat angle-Jacobian contractions. No second derivative of an arccosine appears anywhere in the final expression. That deletion is proved, not assumed, and it removes a whole block of analytic complexity from the critical path of the framework's gravity program.

The theorem does not compute any number. It does not evaluate the reduced sum, and it makes no claim about the continuum limit as the lattice spacing goes to zero. The target value of the second variation in that limit, the continuum value −(1/4), remains open. The declaration is a kernel-checked identity between two expressions, not an evaluation of either.

THEOREM deriv_actionProfile_eventuallyEq_reduced · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean
deriv_actionProfile_eventuallyEq_reduced · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean:748 
/-- `deriv S` agrees with the reduced first variation on a neighborhood of
flat. -/
theorem deriv_actionProfile_eventuallyEq_reduced (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) :
    deriv (planeWaveActionProfile N E k) =ᶠ[nhds (0 : ℝ)]
      reducedFirstVariation N E k := by
  filter_upwards [eventually_pathGoodAt N E k] with t hgood
  rw [(hasDerivAt_planeWaveActionProfile N E k t hgood).deriv]
  exact firstVariationIntegrand_eq_reduced N E k t hgood
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 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 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)

What this page does not claim

No numerical value of the second variation is computed or claimed. The continuum limit of the reduced sum is not established. The theorem does not prove that the Regge action reproduces general relativity in any limit.

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