reggeActionFirstVariationInput_of_edgeSlotBookkeeping
plain-language theorem explainer
Constructs the named first-variation input for a 3D triangulation from an incidence edge-slot bookkeeping certificate at a flat configuration. Anyone establishing criticality of the nonlinear Regge action at the flat conformal potential cites this builder. The body is a pure composition: flat local-angle derivatives, length chain rule, dihedral directional derivatives, conformal Schläfli incidence bookkeeping, then the incidence-bookkeeping input constructor.
Claim. Given an incidence-consistent 3D triangulation $K$, a flat edge-length configuration, and a certificate that sums of local tetrahedral edge-slot weights reindex exactly against global edges (with matching flat lengths), produce the named first-variation input package whose content is the vanishing of the first variation of the Regge action at the zero conformal potential.
background
This module targets the vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric engine is Schläfli cancellation plus zero deficit; the analytic work is packaged as named input structures until the closed-form local identities are fully expanded into derivatives.
The output structure is the named first-variation input: it packages the statement that the Regge action is critical at zero conformal potential on an incidence-consistent triangulation in a flat configuration. Its intended lower-level proof differentiates the hinge-length factor and local dihedral factors, uses zero deficit on the hinge term, then applies the global Schläfli identity on the dihedral term.
The key hypothesis is the incidence edge-slot bookkeeping certificate: summing a local edge-slot weight over global edges and tetrahedra equals summing it directly over local tetrahedral edge slots, with matching flat edge lengths. Existence of a global edge per local slot comes from incidence consistency; uniqueness and no-duplication are recorded here so reindexing is exact.
proof idea
One-line composition wrapper. Start from the flat configuration to obtain the local angle-versus-squared-edge chain-rule package. Lift that to the local angle-versus-length chain-rule package, then to the local dihedral directional-derivative package. Feed that package together with the edge-slot bookkeeping certificate into the conformal Schläfli incidence-bookkeeping constructor. Finally pass the resulting incidence bookkeeping into the incidence-bookkeeping first-variation input builder, which yields the required named input.
why it matters
Sits on the assembly path toward the module target: vanishing of the first variation of the nonlinear Regge action at the flat conformal potential (Schläfli cancellation plus zero deficit). Downstream, the edge-slot-partition constructor is a one-line wrapper around this definition, so every partition-based criticality proof routes through it.
In the Recognition geometry stack this is the bookkeeping bridge between local tetrahedral edge slots and global edges needed before the global Schläfli identity can cancel the dihedral contribution. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is pure discrete-geometry infrastructure for the Regge criticality claim on 3D triangulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.