reggeActionRemainderSecondVariationInput_of_flat_directionalHessian
plain-language theorem explainer
From a flat configuration on an incidence-consistent 3D triangulation together with the nonlinear Regge directional Hessian theorem, one obtains the remainder second-variation input for the Regge action. Cubic-Taylor and discrete-gravity developments cite this packaging step when assembling jet data for the remainder. The proof is a one-line term wrapper into the Hessian-proof module's matching constructor.
Claim. Let $K$ be an incidence-consistent three-dimensional triangulation. If $K$ admits a flat configuration and the nonlinear Regge directional Hessian theorem holds for $K$, then the remainder second-variation input for the Regge action on $K$ is available.
background
The module isolates the final analytic Taylor theorem needed once the nonlinear Hessian of the Regge action has been identified. The heavy content is a local third-order bound on the remainder in the finite-dimensional space of vertex potentials.
A flat configuration means the discrete geometry sits at the zero-curvature background about which the remainder is expanded. The directional Hessian theorem supplies the second-variation jet of that remainder along admissible potential lines. The remainder second-variation input is the structured hypothesis bundle that later steps consume when they force the quadratic Taylor term to vanish and close the cubic estimate.
Upstream, the matching constructor lives in the nonlinear Hessian proof module; this declaration re-exports it under the cubic-Taylor-bound namespace so the cascade can stay local.
proof idea
One-line term wrapper. It applies reggeActionRemainderSecondVariationInput_of_flat_nonlinearHessian from the nonlinear Hessian proof module to the given triangulation, incidence hypothesis, flat configuration, and directional Hessian theorem, and returns the second-variation input structure.
why it matters
This is the second-variation leg of the jet-input chain for the cubic Taylor bound on the nonlinear Regge remainder. Downstream, canonicalRemainderLineQuadraticTaylorZero_of_flat_first_and_directionalHessian consumes it (with the first-variation input) to obtain the quadratic-Taylor-zero target. The composite canonicalRemainderLineTaylorData_of_jetInputs_chainRule_and_localNorm then assembles ContDiff, quadratic vanishing, chain rule, and local-norm bound into full line-Taylor data.
In gravity, canonicalPeriodicEdgeStencilLocalCorrespondence_of_flat_first_and_directionalHessian uses the same package: the Hessian theorem supplies the remainder second-variation jet, and the closed line-Taylor cascade supplies the cubic remainder bound on the periodic Freudenthal torus. Within RS geometry this is scaffolding closure for the discrete-action expansion that feeds continuum correspondence, not a new forcing-chain step (T5–T8 already fix J, phi, the eight-tick octave, and D = 3).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.