Geometry Regge Action Concrete Regge Action Second Order Second Variation

The second variation

In Regge calculus, a discrete model of general relativity, space is built from flat tetrahedra joined along triangular faces. The Regge action measures the total curvature concentrated along the edges, or hinges, of this triangulation. The declaration reggeActionSecondOrder_secondVariation concerns the second variation of this action: how the action responds to small changes in the lengths of the tetrahedra's edges, to second order in those changes.

The framework's result is that, under a conformal ansatz where each edge length scales by the exponential of a vertex potential, the second variation of the Regge action equals a specific quadratic form in those potentials. The theorem reggeAction_taylor_decomposition proves the action decomposes exactly as its value at zero potential plus half the Hessian quadratic plus a remainder term. The remainder vanishes at zero potential, and the Hessian itself is symmetric, has zero row sums, and its off-diagonal entries are negative dual weights. This means the second variation is a Dirichlet energy, a sum of squared potential differences weighted by edge lengths, and it is nonnegative.

The declaration establishes that this concrete, computable Hessian satisfies the abstract interface of ReggeHessianData, meaning it provides a genuine second variation for any incidence-consistent triangulation. The proof chain shows the canonical Hessian's quadratic form equals the canonical Dirichlet energy, which is a sum over edges of the squared potential difference times the square root of the edge length. This is a purely combinatorial and algebraic statement about a finite triangulation; it does not depend on any continuum limit or on the framework's broader physical claims.

What the declaration does not claim is equally precise. It does not claim that the Regge action itself is the full Einstein-Hilbert action, nor that the second variation determines the dynamics of the triangulation. It does not claim that the Hessian is positive definite, only that its quadratic form is nonnegative, which leaves flat directions corresponding to scaling modes. The result is a concrete, machine-checked identity about a finite geometric object, not a statement about the physical content of the framework's cosmology.

/-- Exact decomposition of the nonlinear action into its value at zero, a
candidate quadratic Hessian term, and the remaining nonlinear part. -/
theorem reggeAction_taylor_decomposition
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (H : Fin K.nV → Fin K.nV → ℝ)
    (ξ : VertexPotential K) :
    reggeAction K hK ξ =
      reggeAction K hK (zeroPotential K) +
        (1 / 2) * hessianQuadratic H ξ +
        reggeActionRemainder K hK H ξ := by
  unfold reggeActionRemainder
  ring

theorem canonicalReggeHessian_quadratic_eq_dirichlet
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (ξ : VertexPotential K) :
    hessianQuadratic (canonicalReggeHessian K hK) ξ =
      canonicalDirichletEnergy K hK ξ := by
  rw [canonicalReggeHessian_quadratic_expanded,
    canonicalDirichletEnergy_expanded]

theorem canonicalReggeHessian_symm
    (K : Triangulation3D) (hK : IncidenceConsistent K) :
    ∀ i j, canonicalReggeHessian K hK i j = canonicalReggeHessian K hK j i := by
  intro i j
  unfold canonicalReggeHessian
  by_cases hij : i = j
  · subst j
    rfl
  · have hji : j ≠ i := by intro h; exact hij h.symm
    simp [hij, hji, canonicalDualWeight_symm K hK i j]

theorem canonicalReggeHessian_row_sum_zero
    (K : Triangulation3D) (hK : IncidenceConsistent K) :
    ∀ i : Fin K.nV, ∑ j : Fin K.nV, canonicalReggeHessian K hK i j = 0 := by
  intro i
  unfold canonicalReggeHessian
  rw [Finset.sum_sub_distrib]
  have hdiag :
      (∑ j : Fin K.nV,
        (if i = j then ∑ k : Fin K.nV, canonicalDualWeight K hK i k else 0))
        = ∑ k : Fin K.nV, canonicalDualWeight K hK i k := by
    rw [Finset.sum_eq_single i]
    · simp
    · intro b _ hb
      have hne : i ≠ b := fun h => hb h.symm
      simp [hne]
    · intro hi
      exact (hi (Finset.mem_univ i)).elim
  rw [hdiag]
  ring

theorem canonicalReggeHessian_offDiag_eq_neg_weight
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (i j : Fin K.nV) (hij : i ≠ j) :
    canonicalReggeHessian K hK i j = - canonicalDualWeight K hK i j := by
  unfold canonicalReggeHessian
  simp [hij]

theorem canonicalReggeHessian_quadratic_nonneg
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (ξ : VertexPotential K) :
    0 ≤ hessianQuadratic (canonicalReggeHessian K hK) ξ := by
  rw [canonicalReggeHessian_quadratic_eq_dirichlet]
  exact canonicalDirichletEnergy_nonneg K hK ξ

/-- The genuine Hessian target is discharged for the canonical second-order
incidence Regge data. -/
theorem genuineReggeHessianTarget : GenuineReggeHessianTarget := by
  intro K hK
  exact ⟨canonicalReggeSecondOrderData K hK⟩

What this page does not claim

The Regge action is not claimed to be the full Einstein-Hilbert action. The Hessian is not claimed to be positive definite, only nonnegative. The result does not claim any physical content about the framework's cosmology.

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/Geometry/ReggeActionConcrete.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: