Encyclopedia Gravity Gravity Analysis Regge Ttflat Second Variation First Variation Integrand Eq Redu

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Ttflat Second Variation First Variation Integrand Eq Redu

A machine-checked identity shows that the first variation of a discrete gravity action near flat space is far simpler than its full formula suggests.

Verify this page

The reduced first variation

In the Recognition Science framework's study of discrete gravity, the action of a triangulated spacetime is a sum over its tetrahedra, each contributing a term built from edge lengths and dihedral angles. The first variation of this action, the derivative with respect to a small perturbation, is what tells you whether a configuration is stationary. The declaration firstVariationIntegrand_eq_reduced is a theorem in the framework's machine-checked library of formal theorems. It states that, at any point where the geometry is well-behaved, the full first-variation integrand equals a reduced expression that drops an entire class of terms.

The full integrand has two groups. One involves the derivative of the square root of edge lengths times the deficit angle. The other involves the square root of edge lengths times the derivative of the deficit angle. The theorem proves that the second group is identically zero, thanks to a geometric identity known as the tetrahedral Schläfli identity. This holds not just at the flat point, but in a whole neighborhood of it. So the reduced first variation is simply the sum over edges of the edge-sqrt derivative times the deficit angle, with the angle-derivative terms gone.

This is not a numerical evaluation. The theorem does not compute a value for the second variation, nor does it make any claim about the continuum limit. The reduced expression is a kernel identity, a structural simplification. It says that the second variation at flat space can be written as a finite sum of first-derivative data: flat sqrt-edge slopes times flat angle-Jacobian contractions. The arccos second-derivative block is eliminated by the proved Schläfli identity, not by symbolic differentiation.

The consequence for the campaign is that the explicit Hessian stage is deleted from the critical path. The second variation of the true nonlinear Regge action at flat is now a kernel-checked finite sum. The continuum target value of -(1/4) remains open, and the evaluation of the reduced finite sum and its N → ∞ limit is the remaining work. The theorem also inherits a disclosure: it uses a flat-deficit theorem that carries Lean.ofReduceBool and Lean.trustCompiler in addition to the standard trio of axioms. No new axioms are introduced.

THEOREM firstVariationIntegrand_eq_reduced · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean
firstVariationIntegrand_eq_reduced · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean:739 
/-- Near flat, the full first-variation integrand equals the reduced
(deficit-group-only) form. -/
theorem firstVariationIntegrand_eq_reduced (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) (t : ℝ) (hgood : PathGoodAt N E k t) :
    firstVariationIntegrand N E k t = reducedFirstVariation N E k t := by
  unfold firstVariationIntegrand reducedFirstVariation
  rw [Finset.sum_add_distrib, sum_sqrt_deficitDeriv_eq_zero N E k t hgood,
    add_zero]
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)

What this page does not claim

No numerical value for the second variation is established. No claim about the continuum limit or the target value of -(1/4) is made. The theorem does not prove that the reduced expression is the unique simplification.

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