GenuineReggeHessianTarget
plain-language theorem explainer
Incidence consistency of a finite 3D triangulation is enough to produce nonempty concrete second-order Regge Hessian data. The declaration is the Prop-level closure target that packages that existence claim. Anyone wiring a conformal Regge action into the shared Hessian interface cites it. The body is a pure universal quantification over triangulations and consistency proofs; no analytic work lives here.
Claim. For every finite 3D triangulation $K$ that is incidence-consistent, the type of concrete second-order Regge data on $(K)$ is nonempty: one can build edgewise conformal second variations, deficit angles, and the associated Hessian package from incidence data alone.
background
The module isolates the last analytic step of a finite 3D Regge triangulation under a conformal edge ansatz. A concrete action package supplies the Regge action and its second variation; the goal is to feed that package into the existing shared Hessian interface rather than invent a parallel one.
Incidence consistency means the combinatorial gluing of tetrahedra, hinges, and edges is coherent enough for dihedral angles and deficit angles to be well-defined. Concrete second-order data then packages the Taylor decomposition of the Regge action (quadratic Hessian term plus remainder) under conformal rescaling of squared edge lengths.
Sibling constructions in the same file define the conformal local squared-edge map, tetrahedron dihedral angles under that map, local deficit contributions, hinge measures, and the second-order remainder. The present definition does not compute those objects; it only asserts that, once incidence holds, some such package exists.
proof idea
There is no proof: the declaration is a definition of a proposition. Its body is the universal statement that every incidence-consistent triangulation $K$ yields a nonempty type of concrete second-order Regge data. Discharge happens downstream by exhibiting a canonical constructor; conversion into the shared Hessian interface is a separate one-line transport.
why it matters
This Prop is the hinge between concrete conformal Regge calculus and the abstract Hessian interface used elsewhere in the geometry stack. The theorem that discharges it builds canonical second-order incidence data for every consistent $K$. A companion theorem then shows that any witness of the target produces nonempty shared Hessian data via the second-order-to-interface converter.
In the broader Recognition geometry program this closes the analytic second-variation step for finite 3D Regge triangulations, the discrete curvature setting tied to the forced $D=3$ spatial dimension (forcing chain T8) and the eight-tick combinatorial octave. It does not itself derive continuum Einstein equations; it only guarantees that the discrete Hessian package is inhabited once incidence is granted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.