reggeActionFirstVariationInput_of_conformalSchlaefliCancellation
plain-language theorem explainer
Packages a flat 3D triangulation together with conformal Schläfli cancellation into the named first-variation input for the nonlinear Regge action. Anyone establishing criticality of the zero conformal potential cites this constructor. Proof is a one-line wrapper that feeds the flat local-dihedral package into the local-angles builder.
Claim. Let $K$ be a 3D triangulation with consistent incidence and a flat configuration. Suppose the conformal Schläfli cancellation identity holds for the local dihedral directional-derivative package built from that flat data: for every vertex potential $\eta$, the edge sum of hinge measure (at zero potential) times deficit directional derivative vanishes. Then one obtains the named first-variation input asserting that the Regge action is critical at the zero 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 statement is recorded here until the closed-form local Schläfli identities are fully expanded into derivatives.
A flat configuration means the triangulation sits at zero deficit in the conformal gauge. The local dihedral directional-derivative package of a flat configuration supplies, for each tetrahedron face and each vertex potential $\eta$, the ordinary derivative at $t=0$ of the dihedral angle along the line potential $t\mapsto$ conformal deformation by $t\eta$.
Conformal Schläfli cancellation is the global identity that the edge-sum of hinge measure (evaluated at zero potential) times those deficit directional derivatives is identically zero for every $\eta$. The named first-variation input is a structure whose sole field is the proposition that the Regge action is critical at zero.
proof idea
One-line wrapper. It applies the sibling constructor that builds the first-variation input from an arbitrary local-dihedral package plus a cancellation hypothesis, specializing the package to the flat one obtained from the given flat configuration. No extra algebra is performed; the cancellation hypothesis is passed through unchanged.
why it matters
The module's target theorem is criticality of the nonlinear Regge action at the flat conformal potential. This definition is the thin interface that turns a proved (or assumed) conformal Schläfli cancellation into the exact input structure required by that criticality statement. Downstream work that expands the full derivative calculation from closed-form local Schläfli identities will discharge the cancellation hypothesis and then invoke this constructor. In the broader Recognition geometry stack it sits under the discrete curvature / Regge side of the forcing chain (spatial dimension $D=3$, eight-tick discrete structure), packaging the variational step that identifies flat conformal data as a critical point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.