reggeActionFirstVariationInput_of_edgeSlotPartition
plain-language theorem explainer
From an incidence-consistent 3D triangulation that is flat and carries an edge-slot partition (each local tetrahedral edge slot represented by exactly one global edge), one obtains the named first-variation input package asserting criticality of the nonlinear Regge action at the zero conformal potential. Gravity constructions on periodic Freudenthal tori cite this to discharge that analytic hypothesis. The body is a one-line composition through the bookkeeping intermediate.
Claim. Given an incidence-consistent 3-dimensional triangulation $K$, a flat configuration on $K$, and an edge-slot partition of its incidence data (every local tetrahedral edge slot $(\tau,f)$ is represented by exactly one global edge, and the incidence map hits that slot iff the global edge is that representative), there exists a first-variation input package for $K$ whose sole content is the assertion that the nonlinear Regge action is critical at the zero conformal potential.
background
This module targets vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric engine is Schläfli cancellation together with zero deficit; the module records the exact analytic statement and the named input required until the derivative calculation is expanded from closed-form local Schläfli identities.
An edge-slot partition is the concrete incidence class in which every local tetrahedral edge slot $(\tau,f)$ is represented by exactly one global edge, and the incidence map hits that slot if and only if the global edge is that representative. From such a partition one builds edge-slot bookkeeping (matching of weighted sums over local slots versus global edges). The first-variation input structure packages a single proposition: criticality of the Regge action at the zero conformal potential on a flat configuration. The intended lower-level proof differentiates the hinge-length factor and local dihedral factors, uses zero deficit for the hinge term, then applies the global Schläfli identity for the dihedral term.
proof idea
One-line wrapper. Convert the given edge-slot partition into edge-slot bookkeeping via the partition-to-bookkeeping constructor, then feed that bookkeeping record into the existing bookkeeping-to-first-variation-input constructor. No new analytic work occurs at this layer; the definition only tightens the incidence hypothesis from abstract bookkeeping to the concrete partition class.
why it matters
Supplies the standard discharge path for the named first-variation input on concrete triangulations that admit an edge-slot partition. Downstream, the canonical periodic first-variation input for the encoded periodic Freudenthal torus is built exactly this way: "The input is discharged by the encoded periodic edge-slot partition." That instance sits in the gravity layer and feeds the Phase-C first-variation theorem, which is conditional on the named analytic input. In the broader Recognition geometry stack this is the bridge from combinatorial incidence data on a 3D triangulation to the analytic hypothesis needed for Regge criticality at flat space, the discrete precursor of Einstein vacuum equations in the Regge calculus setting used by the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.