Gravity Analysis Regge Ttsymbol Preflight Frozen Identification Stencil

The frozen identification

In numerical relativity, the Regge action is a way of writing gravity on a lattice of tetrahedra: each edge has a squared length, and the action sums the square root of each length times a deficit angle, a measure of how much space fails to be flat around that edge. The Recognition Science framework's machine-checked library of formal theorems defines this true nonlinear action on a periodic three-dimensional torus and proves that at the perfectly flat assignment, where every edge has its background squared length, the action is exactly zero.

The declaration frozen_identification_stencil concerns a restricted family of edge fields called conformal, where each edge length is the flat value times an exponential factor built from values at the two endpoints. Along this family, the theorem states that the true action splits into a quadratic part plus a remainder: S = (1/2)·Q_frozen + R. The library is explicit that this decomposition is a definitional tautology, because the remainder is defined as the action minus the quadratic part, so the equation holds for any quadratic form Q and does not single out the graph-Laplacian model on its own.

The real content sits in two other results. First, the theorem reggeAction_conformal_eq proves that the older conformal-ansatz action is exactly equal to the true action when evaluated on these conformal edge fields, a genuine identity between two independently defined expressions. Second, a stage-1 theorem identifies Q_frozen with an anisotropic seven-class stencil energy carrying a specific moment tensor. The frozen identification therefore means: restrict the true action to conformal fields, which is proved, and postulate the graph-Laplacian as its quadratic model, which is a definitional choice, not a theorem.

What the declaration does not claim is equally important. The transverse-traceless plane-wave perturbations used in the numerical probe are not of the conformal form, so the frozen model's anisotropy and the numerically observed isotropy of the true action can coexist. The existence and value of the continuum TT Bloch symbol, expected to be -(1/4) from numerical evidence, remains a named open target with status flag false. The flat value of the action is proved, but first-order derivatives along the plane-wave family are not attempted in this file.

/-- 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 TRUE NONLINEAR 3D REGGE ACTION on the side-`N` periodic Freudenthal
torus, as a function of the edge squared-length field:
`S(ℓ) = Σ_e √(ℓ_e) · deficit_e`.  This is the object whose TT Bloch symbol
the C10 probe measured. -/
def trueReggeAction (ℓ : EdgeField N) : ℝ :=
  ∑ e : PeriodicEdge N N N, Real.sqrt (ℓ e) * deficitOfField N ℓ e

/-- THE TRUE NONLINEAR 3D REGGE ACTION on the side-`N` periodic Freudenthal
torus, as a function of the edge squared-length field:
`S(ℓ) = Σ_e √(ℓ_e) · deficit_e`.  This is the object whose TT Bloch symbol
the C10 probe measured. -/
def trueReggeAction (ℓ : EdgeField N) : ℝ :=
  ∑ e : PeriodicEdge N N N, Real.sqrt (ℓ e) * deficitOfField N ℓ e

What this page does not claim

The frozen identification does not prove that the graph-Laplacian is the correct quadratic model for the true action. The declaration does not establish the value -(1/4) for the continuum TT Bloch symbol. No claim is made about differentiability of the action along the plane-wave family.

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: