Encyclopedia Gravity Gravity Analysis Regge Ttflat Second Variation Sum Edge Sqrt Deriv Deficit Deriv

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Ttflat Second Variation Sum Edge Sqrt Deriv Deficit Deriv

A machine-checked proof shows that the second variation of a discrete gravity action at flat space reduces to a sum of first-derivative terms, eliminating a complicated angle-derivative block.

Verify this page

The flat-space simplification

In Regge calculus, gravity is approximated by a triangulated space where edge lengths are the dynamical variables and the action is a sum over triangular hinges of their deficit angles. The question of whether a particular configuration is stable, a local minimum of the action, turns on the second variation: how the action responds to small perturbations. Computing this directly requires differentiating the arccosine functions that define the dihedral angles, a messy symbolic chore.

The declaration sum_edgeSqrtDeriv_deficitDeriv_flat in the framework's machine-checked library of formal theorems proves a clean identity at the flat configuration, where all deficit angles are zero. It states that a sum over edges of the product of the derivative of the square-root of the edge length and the derivative of the deficit angle equals a negative sum over tetrahedra of the product of two flat-space derivative terms. This is not a numerical evaluation; it is an exact algebraic equality between two finite sums, holding for any grid size N and any wave vector.

The importance is that this identity, combined with the pathwise Schläfli kill theorem, removes the entire block of second derivatives of arccosine from the second variation. The second variation at flat space becomes a sum of first-derivative data only: the slopes of the square-root edge lengths times the contractions of the flat angle Jacobian. This makes the stability analysis tractable and is a necessary step toward evaluating the continuum limit of the Regge action.

In Recognition Science, this result is part of a campaign to derive the continuum limit of the Regge action from first principles. The framework models the universe as a discrete ledger, a record of recognition events, and this theorem is a technical step in showing that the discrete gravity action has the correct flat-space behavior. The proof is machine-checked, meaning it is verified by a computer program that checks every logical step, and it carries no new axioms beyond the standard ones.

What this result does not claim is a specific numerical value for the second variation, nor does it establish the continuum limit. The target value of -(1/4) for the continuum second variation remains open, and the numerical evidence from the C10 probe is not cited as proof. The theorem provides the algebraic structure of the second variation at flat space, not its final numerical outcome.

THEOREM sum_edgeSqrtDeriv_deficitDeriv_flat · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean
sum_edgeSqrtDeriv_deficitDeriv_flat · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean:673 
/-- The deficit-group first variation regrouped at flat:
`Σ_e L'_e(0)·δ'_e(0) = −Σ_τ Σ_f L'_{τf}(0)·θ'_{τf}(0)`. -/
theorem sum_edgeSqrtDeriv_deficitDeriv_flat (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) :
    (∑ e : PeriodicEdge N N N,
      edgeSqrtDeriv N E k e 0 * deficitDeriv N E k e 0) =
      -∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
        flatSlotSqrtDeriv N E k τ f * flatSlotAngleDeriv N E k τ f := by
  have hstep : ∀ e : PeriodicEdge N N N,
      edgeSqrtDeriv N E k e 0 * deficitDeriv N E k e 0 =
        -∑ τ : PeriodicTet N N N,
          (match canonicalEdgeSlot? e τ.1 τ.2 with
            | some f => edgeSqrtDeriv N E k e 0 * slotAngleDeriv N E k τ f 0
            | 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,
        edgeSqrtDeriv N E k e 0 * deficitDeriv N E k e 0)
        = ∑ e : PeriodicEdge N N N,
            -∑ τ : PeriodicTet N N N,
              (match canonicalEdgeSlot? e τ.1 τ.2 with
                | some f => edgeSqrtDeriv N E k e 0 *
                    slotAngleDeriv N E k τ f 0
                | 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 => edgeSqrtDeriv N E k e 0 *
                  slotAngleDeriv N E k τ f 0
              | 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 => edgeSqrtDeriv N E k e 0 *
                  slotAngleDeriv N E k τ f 0
              | none => 0) := by
          rw [Finset.sum_comm]
    _ = -∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
            edgeSqrtDeriv N E k (localEdgeOf τ.1 τ.2 f) 0 *
              slotAngleDeriv N E k τ f 0 := by
          congr 1
          refine Finset.sum_congr rfl fun τ _ => ?_
          exact sum_edges_slotMatch N τ.1 τ.2
            (fun e f => edgeSqrtDeriv N E k e 0 * slotAngleDeriv N E k τ f 0)
    _ = -∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
            flatSlotSqrtDeriv N E k τ f * flatSlotAngleDeriv N E k τ f := by
          congr 1
          refine Finset.sum_congr rfl fun τ _ => ?_
          refine Finset.sum_congr rfl fun f _ => ?_
          rw [edgeSqrtDeriv_localEdge_zero, slotAngleDeriv_zero]
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 · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean
axisReducedSecondVariation · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean:843 
/-- The reduced second-variation value for the axis instance at `N = 3`,
as a `Finset` sum expression (`#eval`-free; MODEL-level named quantity —
its VALUE is not computed or claimed anywhere in this development). -/
def axisReducedSecondVariation : ℝ :=
  -∑ τ : PeriodicTet 3 3 3, ∑ f : Fin 6,
    flatSlotSqrtDeriv 3 axisTTPolarizationPlus
        (commensurateMomentum 3 axisWaveVector) τ f *
      flatSlotAngleDeriv 3 axisTTPolarizationPlus
        (commensurateMomentum 3 axisWaveVector) τ f

What this page does not claim

No numerical value for the second variation is established. No continuum limit claim is made; the target remains open. No new axioms are introduced beyond the standard ones and the inherited disclosure.

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