Gravity Analysis Regge Ttsymbol Preflight Edge Angle Contribution Of Field Flat

The edge angle contribution

In lattice gravity, space is chopped into tetrahedra, and the total action is built from the angles where these tetrahedra meet. The declaration edgeAngleContributionOfField picks out, for a given edge and a given tetrahedron, the dihedral angle at that edge, computed from the squared lengths of the tetrahedron's six edges via the standard Cayley-Menger formula. If the edge is not part of that tetrahedron, the contribution is zero. This is a definition, not a theorem: it names the object of study.

The theorem deficitOfField_flatEdgeField then proves a concrete fact about this object. When every edge squared length is set to its flat, periodic value (the value it would have in a regular, uncurved lattice), the angle contribution at every edge and every incident tetrahedron sums to exactly 2π. That means the deficit, defined as 2π minus the sum of incident angles, is zero at every edge. The flat lattice is genuinely flat: no curvature, no deficit, at any edge. This is a proved statement, audited to the standard axioms of the logical kernel.

What this does not claim is just as important. The theorem says nothing about what happens when the edge lengths are perturbed away from flat. It does not prove that the action is differentiable at the flat point, nor that the second variation (the Hessian) has any particular form. The existence and value of the continuum limit of the transverse-traceless Bloch symbol, which would connect this lattice model to linearized Einstein gravity, is a separate, explicitly open target. The numerical evidence for that limit, reported by an independent probe, is not a proof and is not claimed as one here.

In plain terms: this declaration and its theorem establish the base point of the model. They verify that the flat configuration is a genuine stationary point of the action, with zero deficit everywhere. The next step, understanding how the action responds to small wiggles around that base point, is precisely what remains open. The theorem is the foundation; the house is not yet built.

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

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 value of the continuum Bloch symbol. The numerical evidence for isotropy is 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/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: