Encyclopedia Gravity Gravity Analysis Regge Ttflat Second Variation Has Deriv At Reduced First Variat

ARTICLE 3 claims 2 theorems 1 open

Gravity Analysis Regge Ttflat Second Variation Has Deriv At Reduced First Variat

A machine-checked proof that the slope of a gravity action's first variation at a flat starting point can be written as a finite sum of simple edge data, with no angle second derivatives.

Verify this page

The reduced first variation

In the Recognition Science framework's study of a discrete model of gravity, the action of a plane wave on a periodic lattice of tetrahedra is a function of a single amplitude parameter t. The first variation of this action is its derivative with respect to t. The declaration hasDerivAt_reducedFirstVariation_flat proves that this derivative, at the flat starting point t = 0, equals a finite sum over the lattice edges. Each term in that sum is the product of two pieces of first-derivative data: the rate at which the square root of an edge length changes, and the rate at which a deficit angle changes. This is a THEOREM in the machine-checked library of formal theorems.

The force of the result is that it removes a whole class of complicated terms. In the full expression for the derivative of the action, there are two groups of contributions. One group involves the square root of edge lengths times the derivative of deficit angles. The other group involves the square root of edge lengths times the derivative of the angles themselves. The theorem proves that this second group vanishes identically near the flat point, by a geometric identity known as the Schläfli identity for tetrahedra. This means the derivative of the action near flat is entirely captured by the first group alone, which is exactly what the reduced first variation expresses.

What the declaration does not claim is equally important. It does not evaluate the sum to a number, and it makes no statement about the continuum limit as the lattice becomes infinitely fine. The value of the second variation at flat, and its limit as N tends to infinity, remain OPEN targets. The reduced formula is a kernel identity, not a numerical evaluation. The specific continuum target of -1/4 is not proved. The result also does not claim that the Schläfli identity holds at degenerate configurations, only at points where all tetrahedra are nondegenerate with positive edge lengths and interior cosines.

THEOREM hasDerivAt_reducedFirstVariation_flat · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean
hasDerivAt_reducedFirstVariation_flat · IndisputableMonolith/Gravity/Analysis/ReggeTTFlatSecondVariation.lean:777 
/-- Derivative of the reduced first variation at flat: only the
`L'_e(0)·δ'_e(0)` group survives (the other product-rule term carries the
vanishing flat deficit). -/
theorem hasDerivAt_reducedFirstVariation_flat (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) :
    HasDerivAt (reducedFirstVariation N E k)
      (∑ e : PeriodicEdge N N N,
        edgeSqrtDeriv N E k e 0 * deficitDeriv N E k e 0) 0 := by
  have hterm : ∀ e : PeriodicEdge N N N,
      HasDerivAt
        (fun t : ℝ => edgeSqrtDeriv N E k e t *
          deficitOfField N (planeWaveEdgeField N E k t) e)
        (edgeSqrtDeriv N E k e 0 * deficitDeriv N E k e 0) 0 := by
    intro e
    have hu : HasDerivAt (fun t : ℝ => edgeSqrtDeriv N E k e t)
        (deriv (fun t : ℝ => edgeSqrtDeriv N E k e t) 0) 0 :=
      (edgeSqrtDeriv_differentiableAt N E k e).hasDerivAt
    have hv : HasDerivAt
        (fun t : ℝ => deficitOfField N (planeWaveEdgeField N E k t) e)
        (deficitDeriv N E k e 0) 0 :=
      hasDerivAt_deficit N E k e 0 (pathGoodAt_zero N E k)
    have hprod := hu.mul hv
    have hδ0 : deficitOfField N (planeWaveEdgeField N E k 0) e = 0 :=
      deficit_planeWave_zero N E k e
    rw [hδ0, mul_zero, zero_add] at hprod
    exact hprod
  have hall : ∀ e ∈ (Finset.univ : Finset (PeriodicEdge N N N)),
      HasDerivAt
        (fun t : ℝ => edgeSqrtDeriv N E k e t *
          deficitOfField N (planeWaveEdgeField N E k t) e)
        (edgeSqrtDeriv N E k e 0 * deficitDeriv N E k e 0) 0 :=
    fun e _ => hterm e
  have hsum := HasDerivAt.fun_sum hall
  unfold reducedFirstVariation
  exact hsum
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

What this page does not claim

The value of the second variation at flat is not evaluated to a number. The continuum limit of the reduced formula is not established. The Schläfli identity is not claimed to hold at degenerate configurations.

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