module module high

`IndisputableMonolith.Geometry.ReggeActionConcrete`

Concrete Regge action on a finite 3D triangulation under the vertex-conformal ansatz. Defines squared-edge scaling, dihedral and deficit angles, hinge measures, the action, and its second-order Taylor split about the flat potential. Gravity and curvature-cost modules cite it for the Hessian quadratic and remainder. Mostly definitions plus algebraic Taylor identities built on the dihedral-derivative and Hessian interfaces.

claimUnder the vertex-conformal ansatz, a local edge $f=(u,v)$ in tetrahedron $\tau$ has squared length scaled by $e^{\xi_u+\xi_v}$. The module defines the induced dihedral angles, hinge measures, deficit angles $\delta_h$, the Regge action $S=\sum_h \delta_h A_h$, the quadratic Taylor term at vanishing conformal potential $\xi=0$, and the remainder $S-S^{(2)}$.

background

Regge calculus replaces continuum curvature by deficit angles on hinges of a triangulation. In 3D the hinges are edges; the action is the sum of deficit angle times hinge measure. This module works on incidence-consistent finite 3D triangulations (from Triangulation3DConsistency), which supply the local Schläfli data needed for global cancellation identities.

The deformation is the vertex-conformal ansatz: each vertex carries a potential $\xi$, and every edge scales by the product of endpoint factors. DihedralDerivatives isolates the analytic step from Cayley-Menger cosine to angle, $d\theta=-(1/\sqrt{1-\cos^2}),d(\cos\theta)$. ReggeHessian3D is the abstract Hessian interface: a concrete action, its Hessian matrix, and the claim that the quadratic Taylor coefficient is that matrix.

Sibling objects cover local squared edges, tetrahedron edge tuples, dihedral angles under the conformal chart, local deficit contributions, global deficit, hinge measure, the action, second-order piece, remainder, and the zero-potential Hessian quadratic.

proof idea

Definition-heavy module, not a single theorem. It instantiates the ReggeHessian3D interface with explicit conformal formulas: edge lengths from $\exp(\xi_u+\xi_v)$, dihedrals via the upstream arccos derivative chain, deficits as $2\pi$ minus incident dihedrals (or the local contribution form), and hinge measures from the conformal edge data.

The Taylor package is algebraic: reggeAction_taylor_decomposition splits $S=S^{(2)}+R$, hessianQuadratic_zeroPotential identifies the quadratic form at $\xi=0$ with the Hessian matrix, and reggeActionRemainder_zero records that the remainder vanishes to second order at the flat point. Smoothness and cone nondegeneracy are left to downstream modules.

why it matters in Recognition Science

Closes the concrete geometric side of the 3D Regge action so comparison and continuum-limit work can cite a single action object rather than abstract placeholders.

Downstream: CurvatureCostForm uses it as the M2B bridge from Regge/Dirichlet quadratics toward the J-curvature cost form (living plan Regge_To_JCurv_CostForm). ReggeActionSmoothness takes the nonlinear action and demands the conformal chart stay in the nondegenerate tetrahedral cone with arccos away from $\pm 1$. ReggeComponentTheorem3DProof turns the geometric dual-weight computation into ReggeComponentComparison. FreudenthalStencilPreflight imports it for the frozen quadratic energy on the Freudenthal family in the QG continuum-limit campaign.

In the broader RS chain this is geometry infrastructure for curvature cost, not a direct T0-T8 forcing step; it supplies the discrete action whose continuum and cost-form limits feed gravity modules.

scope and limits

Does not prove continuum limit of the Regge action to Einstein-Hilbert.
Does not establish smoothness of the nonlinear action away from the flat potential.
Does not derive the J-cost or curvature cost form; only supplies Regge input.
Does not treat dimension other than 3 or non-conformal edge variations.
Does not discharge global Schläfli cancellation; that lives in triangulation consistency.

used by (4)

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

IndisputableMonolith.Constants.CurvatureCostForm module_import
IndisputableMonolith.Geometry.ReggeActionSmoothness module_import
IndisputableMonolith.Gravity.Analysis.FreudenthalStencilPreflight module_import
IndisputableMonolith.Gravity.ReggeComponentTheorem3DProof module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.DihedralDerivatives module_import
IndisputableMonolith.Geometry.ReggeHessian3D module_import
IndisputableMonolith.Geometry.Triangulation3DConsistency module_import

declarations in this module (45)

def conformalLocalSqEdge L29
def conformalTetSqEdges L37
def tetDihedralAngleUnderConformal L45
def localDeficitAngleContribution L51
def deficitAngle L59
def hingeMeasureUnderConformal L65
def reggeAction L73
def reggeActionSecondOrder L83
def reggeActionRemainder L91
theorem hessianQuadratic_zeroPotential L98
theorem reggeAction_taylor_decomposition L106
theorem reggeActionRemainder_zero L119
theorem reggeActionSecondOrder_secondVariation L128
def canonicalEdgePairWeight L142
def canonicalDualWeight L152
theorem canonicalEdgePairWeight_symm L157
theorem canonicalDualWeight_symm L177
theorem canonicalDualWeight_nonneg L184
def canonicalReggeHessian L198
theorem canonicalReggeHessian_symm L204
theorem canonicalReggeHessian_row_sum_zero L215
theorem canonicalReggeHessian_offDiag_eq_neg_weight L235
def canonicalDirichletEnergy L245
theorem canonicalDirichletEnergy_nonneg L251
theorem canonicalReggeHessian_quadratic_expanded L263
theorem canonicalDirichletEnergy_expanded L285
theorem canonicalReggeHessian_quadratic_eq_dirichlet L384
theorem canonicalReggeHessian_quadratic_nonneg L392
def canonicalEdgeStencilDirichletEnergy L401
def CanonicalDirichletEqualsEdgeStencilTarget L408
def CanonicalEdgePairWeightReindexTarget L417
def NoSelfLoopEdges L425
theorem canonicalEdgePairWeightReindex_of_noSelfLoop L428
def CanonicalEdgeStencilSumCommTarget L527
theorem canonicalEdgeStencilSumComm L536
theorem canonicalDirichletEqualsEdgeStencil_of_sumComm_and_reindex L561
theorem canonicalEdgeStencilDirichletEnergy_nonneg L583
structure ConcreteReggeSecondOrderData L595
def canonicalReggeSecondOrderData L607
structure ConcreteReggeActionData L619
def GenuineReggeHessianTarget L630
theorem genuineReggeHessianTarget L636
def reggeHessianData_of_concrete L641
def reggeHessianData_of_secondOrder L654
theorem genuine_regge_hessian_of_concrete L665