Gravity Analysis Regge Ttsymbol Preflight Regge Action Zero Potential Eq Zero

The flat point of the action

In lattice gravity, the Regge action is a discrete sum that assigns a number to a triangulated space, built from the edge lengths and the angles between tetrahedra. The declaration reggeAction_zeroPotential_eq_zero is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It proves that when the edge lengths of the lattice are set to their flat, regular values, the entire Regge action evaluates to exactly zero. This is the expected baseline: a perfectly flat space has no curvature, so its action, which measures total curvature, vanishes.

The theorem is a corollary of a more basic result, trueReggeAction_flatEdgeField, which shows that every individual angle deficit at every edge is zero in this flat configuration. The action is a sum of terms, each an edge length times its deficit, so if every deficit is zero, the sum is zero. The proof is fully formal and checked by the kernel of the proof assistant. The declaration also inherits a specific axiom footprint, including the standard logical axioms and two compiler-trust axioms that enter through an earlier, certified angle-sum result, not through this file itself.

What this theorem does not do is as important as what it does. It does not establish anything about the behavior of the action when the edge lengths are perturbed away from flatness. In particular, it does not prove that the action is differentiable at the flat point, nor does it compute any derivatives. The existence and value of the continuum limit of the transverse-traceless (TT) Bloch symbol, a quantity that would describe how the action responds to plane-wave perturbations, remains an open target, named ReggeTTContinuumIsotropyTarget. The theorem only pins down the value at the single flat point, a necessary but preliminary step in the larger program of analyzing gravitational fluctuations on this lattice.

/-- FLAT POINT, action form (THEOREM): the true Regge action vanishes at
the flat edge assignment. -/
theorem trueReggeAction_flatEdgeField :
    trueReggeAction N (flatEdgeField N) = 0 := by
  unfold trueReggeAction
  refine Finset.sum_eq_zero fun e _ => ?_
  rw [deficitOfField_flatEdgeField N e, mul_zero]

/-- FLAT POINT, action form (THEOREM): the true Regge action vanishes at
the flat edge assignment. -/
theorem trueReggeAction_flatEdgeField :
    trueReggeAction N (flatEdgeField N) = 0 := by
  unfold trueReggeAction
  refine Finset.sum_eq_zero fun e _ => ?_
  rw [deficitOfField_flatEdgeField N e, mul_zero]

/-- FLAT POINT, deficit form (THEOREM): at the flat edge assignment every
deficit angle vanishes.  Reuses the certified periodic angle-sum chain
(`canonicalPeriodicDirectTypedEdgeAngleSumTarget_holds`); the geometry is
not re-derived here. -/
theorem deficitOfField_flatEdgeField (e : PeriodicEdge N N N) :
    deficitOfField N (flatEdgeField N) e = 0 := by
  unfold deficitOfField
  have hsum :
      (∑ cellTet : PeriodicTet N N N,
        edgeAngleContributionOfField N (flatEdgeField N) e cellTet) =
        2 * Real.pi := by
    calc
      (∑ cellTet : PeriodicTet N N N,
          edgeAngleContributionOfField N (flatEdgeField N) e cellTet)
          = ∑ cellTet : PeriodicTet N N N,
              canonicalPeriodicTypedEdgeAngleContribution e cellTet :=
        Finset.sum_congr rfl fun cellTet _ =>
          edgeAngleContributionOfField_flat N e cellTet
      _ = 2 * Real.pi :=
        canonicalPeriodicDirectTypedEdgeAngleSumTarget_holds N N N e
  rw [hsum]
  ring

What this page does not claim

The theorem does not prove differentiability of the action at the flat point. The theorem does not establish the existence or value of any continuum limit for the TT Bloch symbol. The theorem does not claim that the flat configuration is a minimum of the action.

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/ReggeTTSymbolPreflight.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: