CriticalAtFlat
plain-language theorem explainer
Names the statement that the nonlinear Regge action is stationary under conformal edge-length variations at the flat (zero) potential on a 3D triangulation. Gravity and discrete GR workers cite it as the criticality half of the discrete vacuum Einstein equivalence. It is a one-line alias of the upstream first-variation criticality predicate at zero potential.
Claim. For an incidence-consistent 3D triangulation $K$, the predicate "critical at flat" holds precisely when the nonlinear Regge action is critical at the zero (flat) potential configuration on $K$.
background
This module treats the discrete vacuum Einstein equation for the conformal nonlinear Regge action on a 3D triangulation. Classically, the Regge vacuum equation is vanishing angle deficit at every hinge. Here the action is the nonlinear conformal version, so criticality means that all first variations of edge lengths (in the conformal class) vanish at the flat potential.
Upstream geometry supplies ReggeActionCriticalAtZero: the first-variation criticality statement at the zero potential, under an incidence-consistency hypothesis on the triangulation. Flat configurations and zero-deficit predicates live alongside this definition in the same module. The module records the exact criticality $\leftrightarrow$ zero-deficit equivalence as a named input structure rather than an axiom, because the reverse direction needs a rank/nondegeneracy condition on the conformal edge-incidence derivative.
proof idea
Pure definitional alias: the body is exactly the upstream predicate that the Regge action is critical at the zero potential, applied to the same triangulation and incidence-consistency hypothesis. No tactics, no extra hypotheses.
why it matters
This is the criticality side of the Phase-F discrete vacuum Einstein package. The structure DiscreteVacuumEinsteinInput packages the biconditional between criticality at flat and zero deficit at flat; the theorem reggeAction_critical_iff_zero_deficit simply projects that field. Reverse implications such as zero_deficit_of_critical_of_variationFormula_of_separating and the restricted-incidence recovery theorem take criticality at flat as a hypothesis and, given a first-variation formula plus a separating (or restricted-separating) incidence condition, conclude zero deficit.
In the Recognition gravity stack this is the discrete stand-in for the vacuum Einstein equation on the triangulation: stationary nonlinear Regge action at flat geometry. It does not itself force $D=3$ or the eight-tick structure; those enter through the ambient triangulation and forcing chain. The open content sits in discharging the incidence-rank/separating hypotheses that turn criticality into zero deficit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.