IndisputableMonolith.Geometry.ReggeActionSmoothness
Smoothness and continuity layer for the nonlinear Regge action on a finite 3D triangulation under the conformal ansatz. It builds local analytic flat charts, proves nonvanishing of dihedral denominators, and continuity of squared dihedral cosines near nondegenerate configurations. Global zero-deficit flatness is treated as an assembled-triangulation condition, not a local tetrahedron property. First-variation work cites this module. The argument is local chart construction plus denominator control for cofactor ratios.
claimFor a finite 3D Regge triangulation with conformal squared edge lengths, the local dihedral denominator polynomials are positive (hence nonzero) on a neighborhood of any nondegenerate tetrahedron, so squared dihedral cosines are continuous there and the conformal Regge action is $C^\infty$ via a local analytic flat chart. Global zero deficit at a flat configuration is an assembled-triangulation condition and does not follow from local nondegeneracy of each tetrahedron alone.
background
Regge calculus replaces smooth curvature by deficit angles on a piecewise-flat triangulation. In three dimensions the elementary cells are tetrahedra; dihedral angles are recovered from edge lengths via Cayley-Menger determinants and cofactor ratios. The Recognition geometry stack works under a conformal ansatz on squared edge lengths, so the action is a function of a scalar potential on the edges.
Upstream, AffineIndepInterior supplies the strict interior step: linearly independent adjacent face normals have normalized dot product strictly in $(-1,1)$, which keeps dihedral angles away from $0$ and $\pi$. CofactorDerivatives exposes derivative hooks for Cayley-Menger cofactors and the dihedral cofactor ratio. ReggeActionConcrete isolates the concrete action package and Hessian target under the same conformal ansatz.
This module sits between those analytic primitives and the first-variation theorem. Its doc-comment states the key geometric distinction: global zero-deficit flatness is an assembled-triangulation condition and does not follow from local nondegeneracy of each tetrahedron.
proof idea
The module is a chain of local analytic lemmas, not a single theorem. It defines flat configurations and local analytic flat charts, then proves that a local chart with zero deficit yields a flat configuration. Positivity (hence nonvanishing) of the cubic dihedral denominator polynomial is established on the local chart; continuity of the denominator and of squared dihedral cosine follow at points where the denominator is nonzero. ContDiff of conformal local squared edge maps is recorded, and the Regge action is shown ContDiff by transporting through the local chart. Global zero-deficit-at-flat is packaged as a separate assembled condition rather than deduced tetrahedron-by-tetrahedron.
why it matters in Recognition Science
The immediate consumer is ReggeActionFirstVariation: vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential, whose geometric proof is Schläfli cancellation plus zero deficit. That module needs a precise analytic neighborhood of the flat configuration where dihedral data and the action are differentiable, and a clean statement that zero deficit is available globally at flatness.
Without denominator nonvanishing and local charts, the first variation cannot even be written as a classical derivative. The module also closes the gap between local tetrahedron nondegeneracy (from AffineIndepInterior and cofactor calculus) and the triangulation-level flatness hypothesis that first variation and Hessian targets assume. In the broader RS geometry program this is the smoothness gate before curvature-response and forcing-chain geometry can be treated variationally.
scope and limits
- Does not prove vanishing of the first variation; that lives in ReggeActionFirstVariation.
- Does not derive global zero deficit from local tetrahedron nondegeneracy alone.
- Does not complete symbolic Hessian simplifications left downstream of CofactorDerivatives.
- Does not treat non-conformal edge variations or dimensions other than 3D tetrahedral Regge calculus.
- Does not assert analyticity of the action away from nondegenerate local charts.
used by (1)
depends on (3)
declarations in this module (30)
-
def
GlobalZeroDeficitAtFlat -
structure
LocalAnalyticFlatChart -
structure
ReggeActionContDiffFromLocalChart -
structure
FlatConfiguration -
def
flatConfiguration_of_localChart_zeroDeficit -
theorem
local_dihedralDenom3Poly_pos -
theorem
local_dihedralDenom3Poly_ne_zero -
theorem
local_dihedralDenom3_ne_zero -
theorem
dihedralDenom3_continuousAt -
theorem
dihedralCos3Sq_continuousAt_of_den_ne_zero -
theorem
local_dihedralCos3Sq_continuousAt -
theorem
conformalLocalSqEdge_contDiff -
theorem
conformalLocalSqEdge_contDiffAt_zero -
theorem
conformalTetSqEdges_contDiff -
theorem
conformalTetSqEdges_zero -
theorem
dihedralCos3Sq_conformal_continuousAt_zero -
theorem
cmCofactor3_conformal_contDiff -
theorem
cmCofactor3_conformal_contDiffAt_zero -
theorem
dihedralDenom3_conformal_contDiffAt_zero -
theorem
dihedralCos3Sq_conformal_contDiffAt_zero -
theorem
tetDihedralAngleUnderConformal_contDiffAt_zero -
theorem
localDeficitAngleContribution_contDiffAt_zero -
theorem
deficitAngle_contDiffAt_zero -
theorem
hingeMeasureUnderConformal_contDiff -
theorem
hingeMeasureUnderConformal_contDiffAt_zero -
theorem
reggeAction_contDiffAt_zero_of_endpoint_free -
theorem
reggeAction_contDiffAt_zero_of_localChart -
def
reggeActionContDiffFromLocalChart_of_localChart -
theorem
reggeAction_contDiff_at_zero -
theorem
deficitAngle_zero_of_flat