Encyclopedia Gravity Gravity Analysis Regge Ttflat Second Variation Has Deriv At Plane Wave Action Pr

ARTICLE 4 claims 4 theorems

Gravity Analysis Regge Ttflat Second Variation Has Deriv At Plane Wave Action Pr

A machine-checked theorem gives the exact rate of change of a discrete gravity action along a plane wave, and deletes a whole class of difficult terms.

Verify this page

The derivative gate

In the Regge calculus approach to gravity, spacetime is chopped into flat tetrahedral pieces, and the action is a sum over the edges of the triangulation. Each term is the edge length times the deficit angle, the angle by which the flat pieces fail to close around that edge. The Recognition Science framework studies a one-parameter family of such triangulations, where a plane wave of amplitude t is superimposed on a flat background. The object of interest is the action as a function of t, called the plane-wave action profile, a curve that records how the total Regge action changes as the wave amplitude grows.

The theorem hasDerivAt_planeWaveActionProfile states that this curve has a derivative at every amplitude t where the geometry is well behaved: all edge lengths are positive and every tetrahedron is nondegenerate, meaning its interior angles are strictly between zero and a straight angle. At such a point, the derivative is given by an explicit closed-form sum over the edges. The formula has two groups of terms: one involving the rate of change of the edge lengths, and another involving the rate of change of the deficit angles. The theorem proves that both groups are computable from first-derivative data alone, with every primed quantity written out in a finite algebraic expression.

The deeper content is a second theorem, sum_sqrt_deficitDeriv_eq_zero, which shows that the entire second group vanishes identically near the flat point, not just at it. This is a pathwise Schläfli identity: for each tetrahedron, the sum of the square-root edge lengths times the derivative of the dihedral angles cancels exactly, by a proved tetrahedral identity. The consequence is that the second variation of the action at flat, the quantity that controls linearized stability, contains no second derivative of the arccosine function at all. It reduces to a finite sum of first-derivative terms: flat edge slopes times flat angle Jacobian contractions, regrouped per tetrahedron.

What the theorem does not claim is a numeric value. The reduced formula is a kernel identity, not an evaluation. The continuum target of −1/4 for the second variation remains open, and the C10 probe is numerical evidence only, never cited as proof. The framework's machine-checked library of formal theorems proves the structure of the derivative, not the number it takes at any particular amplitude.

THEOREM hasDerivAt_planeWaveActionProfile · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean
hasDerivAt_planeWaveActionProfile · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean:399 
/-- THE PROFILE DERIVATIVE (THEOREM): at every good amplitude,
`S'(t) = Σ_e [ (l'_e/(2√l_e))·δ_e + √l_e·δ'_e ]` — every primed object in
explicit closed form. -/
theorem hasDerivAt_planeWaveActionProfile (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) (t₀ : ℝ) (hgood : PathGoodAt N E k t₀) :
    HasDerivAt (planeWaveActionProfile N E k)
      (firstVariationIntegrand N E k t₀) t₀ := by
  have hfun : planeWaveActionProfile N E k =
      fun t : ℝ => ∑ e : PeriodicEdge N N N,
        Real.sqrt (planeWaveEdgeField N E k t e) *
          deficitOfField N (planeWaveEdgeField N E k t) e := by
    funext t
    rfl
  rw [hfun]
  unfold firstVariationIntegrand
  have hall : ∀ e ∈ (Finset.univ : Finset (PeriodicEdge N N N)),
      HasDerivAt
        (fun t : ℝ => Real.sqrt (planeWaveEdgeField N E k t e) *
          deficitOfField N (planeWaveEdgeField N E k t) e)
        (edgeSqrtDeriv N E k e t₀ *
            deficitOfField N (planeWaveEdgeField N E k t₀) e +
          Real.sqrt (planeWaveEdgeField N E k t₀ e) *
            deficitDeriv N E k e t₀) t₀ := by
    intro e _
    exact (hasDerivAt_sqrtEdge N E k e t₀ (ne_of_gt (hgood.1 e))).mul
      (hasDerivAt_deficit N E k e t₀ hgood)
  exact HasDerivAt.fun_sum hall
THEOREM hasDerivAt_planeWaveActionProfile · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean
hasDerivAt_planeWaveActionProfile · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean:399 
/-- THE PROFILE DERIVATIVE (THEOREM): at every good amplitude,
`S'(t) = Σ_e [ (l'_e/(2√l_e))·δ_e + √l_e·δ'_e ]` — every primed object in
explicit closed form. -/
theorem hasDerivAt_planeWaveActionProfile (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) (t₀ : ℝ) (hgood : PathGoodAt N E k t₀) :
    HasDerivAt (planeWaveActionProfile N E k)
      (firstVariationIntegrand N E k t₀) t₀ := by
  have hfun : planeWaveActionProfile N E k =
      fun t : ℝ => ∑ e : PeriodicEdge N N N,
        Real.sqrt (planeWaveEdgeField N E k t e) *
          deficitOfField N (planeWaveEdgeField N E k t) e := by
    funext t
    rfl
  rw [hfun]
  unfold firstVariationIntegrand
  have hall : ∀ e ∈ (Finset.univ : Finset (PeriodicEdge N N N)),
      HasDerivAt
        (fun t : ℝ => Real.sqrt (planeWaveEdgeField N E k t e) *
          deficitOfField N (planeWaveEdgeField N E k t) e)
        (edgeSqrtDeriv N E k e t₀ *
            deficitOfField N (planeWaveEdgeField N E k t₀) e +
          Real.sqrt (planeWaveEdgeField N E k t₀ e) *
            deficitDeriv N E k e t₀) t₀ := by
    intro e _
    exact (hasDerivAt_sqrtEdge N E k e t₀ (ne_of_gt (hgood.1 e))).mul
      (hasDerivAt_deficit N E k e t₀ hgood)
  exact HasDerivAt.fun_sum hall
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

What this page does not claim

No numeric value for the second variation is established by this module. The continuum limit of the reduced formula is not proved. 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