IncidenceDeficitSeparating
plain-language theorem explainer
Rank/separation condition on a finite 3D triangulation: any real edge-deficit vector orthogonal to every conformal edge-length direction induced by vertex potentials must vanish. Regge and discrete-gravity workers cite it as the nondegeneracy input that converts criticality of the nonlinear conformal Regge action into zero hinge deficit. It is a Prop on the triangulation, not a derived lemma.
Claim. A finite 3D triangulation $K$ is incidence-deficit separating when every edge vector $\delta\in\mathbb{R}^{E(K)}$ that pairs to zero against all conformal edge-length directions coming from vertex potentials $\eta$ (i.e. $\sum_e \delta_e\,\partial_\eta\ell_e=0$ for every $\eta$) necessarily satisfies $\delta=0$.
background
The module treats the discrete vacuum Einstein equation for the nonlinear conformal Regge action on a finite 3D triangulation $K$. Vacuum means zero angular deficit at every hinge. Forward implication (zero deficit implies criticality) uses Schläfli cancellation on flat backgrounds; the reverse needs a global rank condition on the conformal edge-incidence map.
Vertex potentials are real assignments $\eta:V(K)\to\mathbb{R}$. Each $\eta$ generates a conformal edge-length variation whose directional coefficients appear in the first variation of the Regge action. The incidence pairing is the sum $\sum_e\delta_e$ times those coefficients. Separating says the only deficit vector annihilated by every such pairing is zero.
As the doc-comment stresses, this is a genuine condition on $K$, not automatic from local tetrahedron nondegeneracy.
proof idea
Definitional Prop, not a proved theorem. The body is the universal quantification: for every edge vector $\delta$, if the pairing of $\delta$ against directionalLengthCoefficient of every VertexPotential vanishes, then $\delta=0$. No tactics or lemmas are applied; the declaration simply names that rank/kernel condition.
why it matters
This Prop is the reverse-direction nondegeneracy input for the discrete vacuum Einstein package. It is consumed by zero_deficit_of_critical_of_variationFormula_of_separating (criticality plus first-variation formula plus separating yields zero deficit at flat) and by discreteVacuumEinsteinInput_of_variationFormula_of_separating, which packages the old vacuum-Einstein input from an explicit first-variation formula, flat first-variation, and this separation condition.
A stronger recovery certificate IncidenceDeficitRecovering implies separating via incidenceDeficitSeparating_of_recovering; RecoveringIncidenceTriangulation packages that class and projects to separating. In the broader RS gravity stack this closes the reverse half of the Regge vacuum equivalence without axiomatizing it, keeping the rank hypothesis explicit and dischargeable on concrete triangulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.