reggeActionCubicRemainderInput_of_identically_zero
plain-language theorem explainer
Sanity constructor: if the canonical Regge remainder vanishes for every vertex potential on a flat, incidence-consistent 3D triangulation, the named cubic-remainder input is inhabited with zero constant. Cited when discharging Phase-E Taylor input in the degenerate flat case. Proof refines the local cubic bound with radius 1 and constant 0, then rewrites by the zero hypothesis.
Claim. Let $K$ be an incidence-consistent 3D triangulation that is flat. If the canonical Regge action remainder (relative to the canonical graph-Laplacian Hessian) is identically zero on every vertex potential $\xi$, then the named cubic-remainder input holds: the local cubic bound is satisfied with remainder constant $0$.
background
This module packages nonlinear second-variation and cubic-remainder targets for the Regge action so they can be used before the full Cayley-Menger/arccos chain-rule expansion is complete. Analytic obligations sit in named input structures rather than unfinished expansions.
ReggeActionCubicRemainderInput is the Taylor-remainder slot: it packages a LocalCubicRemainderBound that Mathlib's multivariate Taylor theorem (or an IsBigO fallback) is meant to supply. The canonical Hessian is the graph-Laplacian built from incidence dual weights; the remainder is the nonlinear Regge action minus its quadratic Hessian piece.
The hypothesis here is the strongest possible remainder statement: the remainder map is the zero functional on all vertex potentials. Flatness of the configuration is part of the ambient setting for the cubic input.
proof idea
One-line structure constructor. The sole field cubic_bound is filled by refining a LocalCubicRemainderBound witness: radius $1$, constant $0$, with the trivial numeric side conditions (norm_num, le_rfl). For each vertex potential $\xi$, rewrite the remainder by the global zero hypothesis and simplify to obtain the cubic inequality.
why it matters
Closes the cubic-remainder input in the degenerate case where the nonlinear remainder is identically zero, so Phase-E cubic remainder theorems that take ReggeActionCubicRemainderInput as a named hypothesis can fire without waiting on the full Cayley-Menger expansion. The module doc frames this as usable-now scaffolding around unfinished lower-level analysis.
No downstream consumers are wired yet (used_by empty); the declaration is a constructor for the input structure itself. In the broader RS geometry stack it supports second-variation control of the Regge action on discrete 3D triangulations, consistent with the $D=3$ landmark (T8), but it does not itself derive continuum Einstein equations or curvature identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.