remainderAnalyticClosed
plain-language theorem explainer
Packages the full analytic-remainder closure certificate for cubic Taylor expansion of the Regge action on incidence-consistent 3D triangulations. Downstream agents cite it for third-derivative remainder bounds and the nonlinear cubic Taylor endpoint without importing the broad progress audit. Proof is a one-field structure instance pointing at the canonical certificate.
Claim. There is a lane-local certificate asserting: for every incidence-consistent 3D Regge triangulation $K$, the canonical analytic remainder closure holds. That closure packages, from any flat configuration and the standard first- and second-variation remainder jet inputs, the continuity, quadratic-vanishing, and third-derivative bound targets needed for the cubic Taylor remainder of the Regge action.
background
Track 1B-REM concerns analytic control of the remainder after the quadratic (Hessian) term in the Regge action, expanded about a flat configuration on a 3D triangulation. The broad progress audit pulls in finite-Freudenthal combinatorics; this module isolates the analytic-remainder branch so it builds independently.
RemainderAnalyticClosed is the proof surface required downstream: every local analytic remainder target must follow from a flat configuration plus the usual first- and second-variation remainder jet inputs. The concrete certificate lives in ReggeActionCubicTaylorBound as canonicalRemainderAnalyticClosureCert, which supplies line contDiff-from-flat, quadratic-zero-from-jets, and the third-derivative bound fields.
Regge calculus here is the discrete Einstein–Hilbert action on edge lengths of a triangulation; the cubic Taylor remainder is the obstacle to matching continuum curvature expansions and to J-cost local correspondence later in the geometry lane.
proof idea
One-field structure instance. The single field closure is definitionally set equal to canonicalRemainderAnalyticClosureCert from ReggeActionCubicTaylorBound. No new proof obligations are discharged here; the definition merely re-exports that certificate under the lane-local RemainderAnalyticClosed interface so sibling theorems can project individual targets without importing the full audit graph.
why it matters
Gives Track 1B-REM a thin, buildable handle on analytic remainder closure separate from combinatorial Freudenthal machinery. Downstream, canonicalRemainderLineThirdDerivBound_closed projects the third-derivative bound via (remainderAnalyticClosed.closure K hK).line_third_deriv_bound_from_flat, and nonlinearReggeCubicTaylorTheorem_closed uses the same package for the full cubic Taylor endpoint under first- and second-variation inputs.
In the Recognition geometry lane this is scaffolding toward nonlinear Regge–J-cost local correspondence and the strongest true Regge–J-cost replacement (sibling closed forms in the same audit). It sits under the D=3 / eight-tick forcing context (T7–T8) only insofar as the ambient triangulation type is 3D; the certificate itself is pure discrete-geometry analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.