ReggeActionCriticalAtZero
plain-language theorem explainer
Names the proposition that the nonlinear 3D Regge action has vanishing Fréchet derivative at the flat (zero) conformal potential. Discrete-gravity and vacuum-Einstein modules cite it as the analytic content of criticality at flat space. It is a one-line Prop abbreviation of that derivative equation, not a proved theorem.
Claim. For an incidence-consistent finite 3D Regge triangulation $K$, write $S$ for the conformal Regge action on vertex potentials. The flat configuration is the zero potential $\xi\equiv 0$. Criticality at flat means the Fréchet derivative vanishes: $DS|_{\xi=0}=0$ as a continuous linear map on the space of vertex potentials.
background
This module fixes the analytic target for the first variation of the full nonlinear Regge action at the flat conformal potential. The intended geometric engine is Schläfli cancellation together with vanishing deficit; until the closed-form local identities are fully expanded, the module records the exact derivative statement and the named input bundle that packages it.
The concrete action is the edge sum $S(\xi)=\sum_e \ell_e(\xi),\delta_e(\xi)$, hinge measure times deficit angle under the vertex-conformal ansatz. The zero potential is the constant-zero assignment on vertices (the flat background). A Triangulation3D supplies finite vertex/edge/tet counts and incidence maps; incidence consistency strengthens that data with global squared-edge lengths, orientation-compatible edge-in-tet matching, and the local closed-form Schläfli package needed for a global identity without caller-supplied Schläfli data.
proof idea
Pure definitional abbreviation: the proposition is definitionally equal to
fderiv ℝ (reggeAction K hK) (zeroPotential K) = 0.
There is no tactic proof and no lemma application. Downstream theorems discharge it by unfolding and either extending a directional-criticality hypothesis or composing a first-variation formula with a global zero-deficit hypothesis at flat.
why it matters
This is the named criticality predicate that the first-variation development aims to establish. Downstream, reggeActionCriticalAtZero_of_directional lifts directional vanishing along all lines to full Fréchet criticality, and reggeActionCriticalAtZero_of_firstVariationFormula_of_zeroDeficit obtains it from a first-variation formula plus global zero deficit at flat. The structure ReggeActionFirstVariationInput packages it as the required firstVariation_zero field under a flat-configuration hypothesis, with the intended lower-level path: differentiate hinge lengths and local dihedrals, kill the hinge term by zero deficit, kill the dihedral term by global Schläfli.
In the gravity layer it is re-exported verbatim as CriticalAtFlat, the vacuum criticality hypothesis used both forward and reverse: criticality plus a variation formula and a separating (or restricted-subspace) incidence condition recovers zero deficit at flat. That reverse implication is the discrete vacuum Einstein content on the conformal Regge scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.