CanonicalRemainderZeroSecondVariationTheorem
plain-language theorem explainer
Names the proposition that the canonical nonlinear remainder of the 3D Regge action has vanishing second directional derivative at the flat potential, in every vertex-potential direction. Cited by anyone packaging that vanishing into the remainder second-variation input for the nonlinear Hessian. One-line definitional alias of the upstream remainder-zero predicate; no new mathematics.
Claim. For an incidence-consistent finite 3D Regge triangulation $K$, the statement that for every vertex potential $\xi$, the map $t \mapsto$ (canonical nonlinear remainder of the Regge action along the flat potential plus $t\xi$) has second derivative zero at $t=0$.
background
The module isolates the hard endpoint of the nonlinear Regge calculation: the second directional derivative of the full action at the flat potential must match the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
A Triangulation3D is a finite abstract 3D Regge complex (vertices, edges, tets) with nondegenerate squared-edge data on each tetrahedron. IncidenceConsistent strengthens this with global edge matching and a local closed-form Schläfli field so global Schläfli needs no caller-supplied data.
Upstream, CanonicalRemainderSecondVariationZero is exactly the Prop that the canonical nonlinear remainder has zero second variation at the flat potential. The present declaration is a named equivalent formulation of that same Prop, phrased for the nonlinear-Hessian interface.
proof idea
Definitional one-liner: the body is literally the upstream predicate CanonicalRemainderSecondVariationZero K hK. No tactics, no lemmas applied, no calculation. It exists only as a stable name in the nonlinear Hessian proof interface.
why it matters
Sits on the last mile of the nonlinear Regge Hessian chain. Downstream, reggeActionRemainderSecondVariationInput_of_theorem consumes a proof of this Prop and builds ReggeActionRemainderSecondVariationInput by setting remainder_secondVariation_zero := h. That input is what closes the module's stated goal: second directional derivative at the flat potential equals the canonical incidence Hessian, after which the ordinary ReggeActionSecondVariationInput follows. In the broader Recognition geometry stack this is scaffolding for discrete gravity / Regge dynamics on the forced $D=3$ lattice (T8), not a new physical law. It does not itself discharge the hard second-variation calculation; it only names the target Prop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.