DiscreteVacuumEinsteinInput
plain-language theorem explainer
Packages the discrete vacuum Einstein equivalence for a consistent 3D Regge triangulation with a flat analytic background: criticality of the nonlinear Regge action at the flat potential is equivalent to vanishing edge deficits. Gravity workers cite it when discharging Phase-F vacuum equations without treating the biconditional as an axiom. It is a one-field structure; instances are built from incidence-rank or recovery hypotheses.
Claim. For a finite 3D Regge triangulation $K$ with incidence consistency and a flat analytic configuration, a discrete vacuum Einstein input is a proof that the nonlinear Regge action is critical at the flat potential if and only if the Regge deficit angle vanishes on every global edge.
background
The module treats the discrete vacuum Einstein equation for the conformal nonlinear Regge action. Classically, the Regge vacuum equation is zero deficit at every hinge. Here the action is the nonlinear conformal version on a finite triangulation $K$ (vertex, edge, and tetrahedron counts with abstract incidence and nondegenerate squared-edge data per tet).
Incidence consistency supplies global squared edge lengths, local-to-global edge matching up to orientation, and the local closed-form Schläfli identity needed for global cancellation. A flat configuration adds the arccos endpoint condition, zero-deficit flatness at the base point, and the smoothness needed for Taylor expansion of the full nonlinear action.
Two local propositions are packaged: criticality of the nonlinear action at the flat (zero) potential, and vanishing of the deficit angle on every global edge of that potential. The module records their equivalence as a named input rather than an axiom: the forward direction uses zero deficit plus global Schläfli; the reverse needs a rank/nondegeneracy condition on the conformal edge-incidence derivative.
proof idea
No proof body: this is a structure definition with a single field, the biconditional between criticality at the flat potential and zero edge deficits. Callers discharge it by constructing an instance (for example from a first-variation formula plus incidence separation, or from a recovering-incidence triangulation), then project the field. The companion one-line theorem simply returns that field.
why it matters
Phase-F discrete vacuum Einstein equivalence in the gravity stack. The companion theorem reggeAction_critical_iff_zero_deficit is literally the field projection, so every vacuum-equation citation routes through an instance of this input.
Downstream constructors build instances from: an explicit first-variation formula plus incidence deficit separation; recovering-incidence triangulations; and restricted incidence recovery on a deficit subspace. The doc-comment flags the nontrivial reverse arrow as the incidence-rank theorem: if all conformal first variations vanish, each edge deficit is zero.
In the broader Recognition geometry program this is the discrete stand-in for the vacuum Einstein equation on a Regge scaffold (zero curvature deficits), kept as a named hypothesis package so the module never axioms the rank step. It does not itself invoke the forcing chain (T0–T8) or the J-cost; it sits in the gravity/Regge layer that those foundations eventually feed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.