module module high

`IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolPreflight`

Stage-1 preflight for the Regge TT continuum-symbol program on the side-N periodic Freudenthal torus. It packages edge squared-length fields, tetrahedron edge data, dihedral angles, angle deficits, and the true Regge action, plus exact evaluations on the flat background. Downstream continuum-symbol gates import this vocabulary rather than redefining it. The module is definitional scaffolding with flat-case identities, not a continuum-limit theorem.

claimOn the side-$N$ periodic Freudenthal torus, an edge field assigns a squared length $\ell_e^2 \in \mathbb{R}$ to each positive-displacement periodic edge. From such a field one builds tetrahedron squared-edge data, dihedral angles, per-edge angle contributions, angle deficits $\delta_e$, and the true Regge action $S_{\mathrm{Regge}}$. The flat edge field is the constant Euclidean background; on it, deficits vanish and $S_{\mathrm{Regge}}=0$. A typed conformal edge field is the same data with conformal scaling made explicit.

background

The setting is discrete gravity on the canonical Freudenthal triangulation of the 3-torus (periodic side length $N$), as packaged by the physical six-tet cubic Dirichlet instance. That upstream module "connects the encoded periodic Freudenthal torus scaffold to the PhysicalSixTetCubicDirichletModel target" and lists the exact obligations needed to instantiate the model; it does not assert free Dirichlet equality.

The companion Freudenthal stencil preflight develops the action-level continuum limit of a frozen quadratic energy on the same family (QG full-theory campaign, Phase 2b, Test G stage 1). The present module sits one layer up: it treats the full Regge calculus objects (edge lengths, dihedral angles, deficits) rather than a frozen quadratic stencil.

Core objects: an edge field is one real squared length per positive-displacement periodic edge; tetrahedron squared edges and dihedral angles are read off that field; the deficit at an edge is $2\pi$ minus the sum of incident dihedral angles; the true Regge action is the standard sum of edge length times deficit.

proof idea

This is primarily a definition module. It introduces the edge-field type, the flat background field, extractors for tetrahedron squared edges and dihedral angles, the edge angle contribution, the deficit, and the true Regge action, together with a typed conformal variant.

The non-definitional content is a short chain of flat-background identities: tetrahedron squared edges and edge angle contributions specialize correctly on the flat field; the deficit of the flat field is zero; the true Regge action of the flat field is zero. Those lemmas are direct substitutions of the flat assignment into the definitions, not continuum or variational arguments.

why it matters in Recognition Science

This module is Stage 1 of the panel-locked ReggeTTContinuumSymbol program. Every later gate imports it as the shared geometric vocabulary on the Freudenthal torus.

Downstream: ReggeTTDerivativeGate is Stage 2 (Gate 0 / Lane A) and explicitly names this module as Stage 1; ReggeTTSymbolSpecificationAudit is Gate A0 (scaling well-posedness of the $-1/4$ isotropy target); ReggeTTLocalSymbolExistence is Gate A1 (local symbol existence at fixed $N$); ReggeTTFlatSecondVariation is Gate A2 (Schläfli-reduced flat second variation), reusing the first-derivative structure from the derivative gate. Without a single flat background, deficit, and true Regge action, those gates cannot state the two-jet or continuum-symbol claims cleanly.

In the broader Recognition gravity stack this is discrete-geometry infrastructure for the continuum TT symbol, not a forcing-chain (T0–T8) step.

scope and limits

Does not prove any continuum limit or symbol existence; those are later gates.
Does not assert the physical Dirichlet equality on the Freudenthal torus.
Does not compute the second variation or TT projector; only flat first-order vanishing of deficit and action.
Does not fix the normalization constant of the continuum isotropy target (Gate A0).
Does not treat non-periodic, non-Freudenthal, or curved background triangulations.

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.Analysis.ReggeTTDerivativeGate module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTFlatSecondVariation module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTLocalSymbolExistence module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolSpecificationAudit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.FreudenthalStencilPreflight module_import
IndisputableMonolith.Gravity.PhysicalSixTetCubicDirichletInstance module_import

declarations in this module (55)

abbrev EdgeField L175
def flatEdgeField L179
def tetSqEdgesOfField L184
def tetDihedralAngleOfField L191
def edgeAngleContributionOfField L199
def deficitOfField L207
def trueReggeAction L215
theorem tetSqEdgesOfField_flat L222
theorem edgeAngleContributionOfField_flat L233
theorem deficitOfField_flatEdgeField L249
theorem trueReggeAction_flatEdgeField L270
def typedConformalEdgeField L288
theorem periodicDispSqEdge_nonneg L293
theorem canonical_tet_eq L298
theorem canonical_tetVerts_eq L304
theorem canonical_edgeInTet_eq L314
theorem conformalTetSqEdges_eq_typedField L323
theorem deficitAngle_conformal_eq L362
theorem hingeMeasure_conformal_eq L382
theorem reggeAction_conformal_eq L397
theorem typedConformalEdgeField_zero L406
theorem reggeAction_zeroPotential_eq_zero L414
theorem frozen_identification L436
theorem frozen_identification_stencil L464
def vertCoord L485
def polEdgeCoeff L493
def commensurateMomentum L498
def edgeMidpointPhase L503
def planeWaveEdgeField L508
def planeWaveActionProfile L516
def ttSecondDifference L524
def TTBlochSymbolIs L533
def momentumNormSq L539
instance instNeZeroAddThree L542
def ReggeTTContinuumSymbolIs L552
def IsTTPolarization L561
def reggeTTContinuumCoefficient L571
def ReggeTTContinuumIsotropyTarget L581
theorem planeWaveEdgeField_zero_amplitude L589
theorem planeWaveActionProfile_zero L597
theorem ttSecondDifference_even L604
theorem polEdgeCoeff_neg L612
theorem planeWaveEdgeField_neg_polarization L622
theorem ttSecondDifference_neg_polarization L634
def axisWaveVector L651
def axisTTPolarizationPlus L659
def axisTTPolarizationCross L667
theorem sqrt_two_mul_self L672
theorem inv_sqrt_two_sq L675
theorem axisTTPolarizationPlus_isTT L679
theorem axisTTPolarizationCross_isTT L697
theorem axisWaveVector_ne_zero L716
structure ReggeTTSymbolPreflightStatus L734
def reggeTTSymbolPreflightStatus L759
theorem status_flags_grounded L771