ReggeActionRemainderSecondVariationInput
plain-language theorem explainer
Packages the analytic hypothesis that the canonical nonlinear Regge remainder has vanishing second variation at the flat potential, for every line of vertex potentials. Downstream cubic-Taylor closures in the Regge geometry stack take this structure as a named jet input. It is a one-field input bundle wrapping the corresponding Prop, not a proved identity.
Claim. For a finite 3D Regge triangulation $K$ with incidence consistency, an input record asserting that the canonical remainder action $R$ (full nonlinear Regge action minus the quadratic form of the canonical Hessian) satisfies $\partial_t^2|_{t=0} R(\phi_0 + t\xi) = 0$ for every vertex potential direction $\xi$, i.e. has second derivative zero at the flat configuration along every straight line of potentials.
background
The module fixes second-variation and cubic-remainder targets for the nonlinear Regge action in a form usable before the full Cayley-Menger/arccos chain-rule expansion is complete. Analytic facts that the expansion must eventually supply live in named input structures rather than as axioms.
A Triangulation3D is a finite abstract 3D Regge complex (vertices, edges, tets) with nondegenerate squared-edge data on each tetrahedron. IncidenceConsistent strengthens that scaffold: local tet edge slots match global endpoints (up to orientation) and supplies the local closed-form Schläfli data needed for a global Schläfli identity.
CanonicalRemainderSecondVariationZero is the Prop that, for every vertex potential $\xi$, the real function $t \mapsto$ (canonical remainder of the Regge action along the line potential $\phi_0 + t\xi$) has second derivative zero at $t = 0$. The remainder is the nonlinear action minus the quadratic form built from the canonical Regge Hessian. This structure simply packages that Prop as a field.
proof idea
No proof body: the declaration is a structure (definitional input bundle). Its single field is exactly the Prop CanonicalRemainderSecondVariationZero K hK. Callers construct an instance by supplying a proof of that universal second-derivative statement; consumers project the field. Sibling first-variation input structures play the same packaging role one order lower.
why it matters
This is the second-order jet input in the cascade that closes the cubic Taylor theorem for the canonical remainder. Downstream, CanonicalRemainderCubicTaylorFromJetInputsTarget isolates the finite-dimensional analytic claim: given flat configuration plus first- and second-variation remainder inputs, the remainder is $O(|\xi|^3)$. Concrete closures include canonicalRemainderLineQuadraticTaylorZero_of_jetInputs (degree-2 Taylor polynomial of the line-restricted remainder vanishes at $t=1$), iteratedDerivWithin_two_canonicalRemainderLine_of_jetInputs (second iterated derivative along the line is zero), and the assembly theorems canonicalRemainderLineTaylorData_of_flat_and_remainderJets and nonlinearReggeCubicTaylorTheorem_of_flat_and_remainderJets / CanonicalRemainderAnalyticClosureCert.
In the Recognition geometry stack this is the missing second-order vanishing needed so the nonlinear Regge action near flat space is controlled by a cubic remainder, matching the continuum Einstein-Hilbert second-variation picture on a discrete 3D complex. It does not itself invoke T0-T8 or the RCL; it is pure discrete-geometry scaffolding for the Regge side of the program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.