ConformalSchlaefliCancellation
plain-language theorem explainer
Defines the exact global Schläfli cancellation identity required for the conformal first variation of the 3D Regge action: the edge-sum of hinge length times deficit directional derivative vanishes for every vertex-potential direction. Anyone assembling the first-variation input package from local dihedral derivatives cites this predicate. It is a pure Prop definition, not a proved theorem.
Claim. For an incidence-consistent 3D triangulation $K$ and a package $A$ of local dihedral-angle directional derivatives under the conformal ansatz, the following holds: for every vertex potential direction $\eta$, $$\sum_e \ell_e(0)\,\partial_\eta\delta_e = 0,$$ where $\ell_e(0)$ is the hinge measure (edge length) at the zero potential and $\partial_\eta\delta_e$ is the directional derivative of the angle deficit at edge $e$, assembled from the local tetrahedral angle derivatives in $A$.
background
The module targets the vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric engine is classical Schläfli cancellation together with zero deficit on a flat configuration.
In 3D Regge calculus the hinge measure is the edge length. Under the vertex-conformal ansatz, that length is $\sqrt{q_e},\exp((\xi_u+\xi_v)/2)$. The deficit at a hinge is $2\pi-\sum\theta$, assembled from dihedral angles of incident tetrahedra. The package $A$ supplies, for each tetrahedron and each of its six edges, the directional derivative of the conformal dihedral angle along a line of vertex potentials, with a HasDerivAt witness at $t=0$.
The deficit directional derivative is then the negative sum of those local angle derivatives over tetrahedra that contain the global edge. The present definition packages the global weighted sum of those deficit derivatives against the zero-potential hinge measures into a single cancellation predicate.
proof idea
No proof: this is a definition of a proposition. The body is the universal quantification over vertex potentials $\eta$ of the vanishing of $\sum_e \ell_e(0),\partial_\eta\delta_e$, with $\ell_e(0)$ given by hingeMeasureUnderConformal at the zero potential and $\partial_\eta\delta_e$ given by deficitDirectionalDerivFromLocalAngles built from the local package $A$. Downstream constructors discharge the predicate from incidence bookkeeping plus local Schläfli identities.
why it matters
This predicate is the exact analytic gate between local dihedral derivatives and the global first-variation input. Downstream, deficitPackage_of_conformalSchlaefliCancellation turns a witness into a deficit-angle directional-derivative package; reggeActionFirstVariationInput_of_conformalSchlaefliCancellation and reggeActionFirstVariationInput_of_localAngles feed that package into the full first-variation input at a flat configuration. The companion theorem conformalSchlaefliCancellation_of_lengthChain_of_bookkeeping produces witnesses from a length-chain-rule package plus incidence bookkeeping.
In the Recognition geometry stack this is the 3D discrete avatar of Schläfli cancellation that makes the conformal Regge action stationary at flat space, consistent with the forcing of $D=3$ (T8) and the eight-tick discrete structure. It does not itself prove stationarity; it names the cancellation hypothesis the stationarity proof consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.