reggeActionRemainderSecondVariationInput_of_theorem
plain-language theorem explainer
Packages a proof that the canonical nonlinear remainder has vanishing second directional variation into the structure expected by the Regge second-variation interface. Anyone connecting the nonlinear Hessian chain to ReggeActionSecondVariation cites this. The body is a one-line field assignment from the equivalent theorem-shaped Prop.
Claim. Let $K$ be a finite 3D Regge triangulation with incidence consistency. If the canonical nonlinear remainder of the Regge action has zero second variation in every direction at the flat potential, then the remainder-second-variation input bundle is inhabited: its sole field is that vanishing statement.
background
The module isolates the hard endpoint of the nonlinear Regge Hessian: the second directional derivative of the full action at the flat potential must match the canonical incidence Hessian. Once that calculation is in hand, the existing second-variation input follows immediately.
A Triangulation3D is a finite abstract 3D Regge complex (vertices, edges, tets, incidence, nondegenerate squared-edge data). IncidenceConsistent strengthens that scaffold with global squared-edge lengths, local-to-global edge agreement up to orientation, and the local closed-form Schläfli data needed for a global Schläfli identity.
CanonicalRemainderZeroSecondVariationTheorem is the Prop form: the canonical nonlinear remainder has zero second variation in every direction. ReggeActionRemainderSecondVariationInput is the matching structure with a single field recording that same vanishing. This definition is the trivial bridge between those two presentations.
proof idea
One-line structure constructor. The hypothesis h already has type CanonicalRemainderSecondVariationZero K hK (via the theorem-shaped alias), which is exactly the type of the structure field remainder_secondVariation_zero, so the field is filled by h with no further proof work.
why it matters
Closes the packaging step between the convenient theorem-shaped formulation of remainder vanishing and the structure that the second-variation API consumes. The module doc states the target is not a new assumption but the endpoint of the second chain-rule calculation; once that calculation supplies the Prop, this definition yields ReggeActionRemainderSecondVariationInput immediately.
No downstream consumers are wired yet (used_by is empty). In the broader geometry stack it is the last glue before the nonlinear directional Hessian can be identified with the canonical incidence Hessian on a consistent 3D Regge triangulation. It does not itself touch T0–T8 or the Recognition Composition Law; it is pure discrete-geometry interface hygiene for the Regge action expansion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.