Gravity Analysis Regge Ttsymbol Preflight True Regge Action Flat Edge Field

The flat point of the action

In lattice quantum gravity, the Regge action is a way to write down the gravitational action on a discretized spacetime. Instead of a smooth manifold, one takes a triangulated space, a collection of flat tetrahedra glued together along their faces. The action is then a sum over the edges of the space, where each edge contributes its length times a measure of how much the surrounding geometry is curved. That curvature measure is the deficit angle: the amount by which the sum of the dihedral angles around an edge falls short of the full 2π.

The declaration trueReggeAction_flatEdgeField is a theorem in the framework's machine-checked library of formal theorems. It states that when the edge lengths are assigned in a very specific way, the one that corresponds to a perfectly flat, regular lattice, every deficit angle is zero. Consequently, the entire action, which is a sum of terms each containing a deficit angle, is exactly zero. This is a proof, not a numerical observation: the theorem is derived from the definitions of the action and the flat edge field, and it holds for any lattice size N.

The flat point is the starting point for studying small fluctuations. The framework's library defines a family of plane wave perturbations away from this flat configuration, and the theorem planeWaveActionProfile_zero shows that at zero amplitude, the action along this family is also zero. This is a necessary consistency check for any perturbative analysis. The definitions of the TT Bloch symbol, the object that would describe how these fluctuations propagate, are also set up in the same file, but their actual values are not derived here.

What the theorem does not claim is as important as what it proves. It does not prove that the action is differentiable at the flat point, nor does it compute any derivatives. It does not establish the value of the TT Bloch symbol, which is the next step in the analysis. That value, conjectured to be -1/4, remains an explicitly named open target. The theorem is a foundational anchor: it proves the action has the correct zero point, which is a prerequisite for any meaningful study of the dynamics around it.

/-- 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

/-- 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]

/-- The action profile vanishes at amplitude `0` (flat point of the
family). -/
theorem planeWaveActionProfile_zero (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) :
    planeWaveActionProfile N E k 0 = 0 := by
  unfold planeWaveActionProfile
  rw [planeWaveEdgeField_zero_amplitude, trueReggeAction_flatEdgeField]

What this page does not claim

The theorem does not prove the action is differentiable at the flat point, nor does it compute any derivatives. The theorem does not establish the value of the TT Bloch symbol, which remains an open target. The theorem does not claim that the frozen graph-Laplacian model is the correct quadratic approximation to the true 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: