ConformalSchlaefliIncidenceBookkeeping
plain-language theorem explainer
Defines the global incidence identity that converts an edge-indexed deficit variation into a double sum of local tetrahedral Schläfli terms under the conformal ansatz. Anyone assembling the first variation of the nonlinear Regge action at the flat potential cites this Prop as the required bookkeeping hypothesis. It is a pure definition of a predicate; discharge comes from edge-slot reindexing elsewhere.
Claim. For an incidence-consistent 3D triangulation $K$ and a package $A$ of local dihedral directional derivatives under the conformal ansatz, the incidence bookkeeping property holds if, for every vertex potential $\eta$, $$\sum_e m_e(0)\,\delta'_e(\eta)=-\sum_\tau\sum_{f=0}^{5}\sqrt{s_{\tau,f}}\,A_{\tau,f}(\eta),$$ where $m_e(0)$ is the hinge measure at the zero potential, $\delta'_e(\eta)$ is the directional derivative of the deficit angle on edge $e$, $s_{\tau,f}$ is the squared length of local edge slot $f$ in tetrahedron $\tau$, and $A_{\tau,f}(\eta)$ is the corresponding local dihedral directional derivative.
background
This module targets the vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric route is Schläfli cancellation plus zero deficit; until the closed-form local identities are fully expanded, the module records exact analytic statements and named input packages.
A triangulation $K$ is incidence-consistent when global edges and local tetrahedral edge slots match without duplication. The conformal ansatz deforms edge lengths via a vertex potential $\eta$ along the line $t\mapsto$ linePotential$(\eta,t)$, evaluated at the zero potential for the flat background. The structure LocalDihedralDirectionalDerivativePackage packages, for each tetrahedron and each of its six edge slots, the directional derivative of the dihedral angle under that conformal flow, together with a HasDerivAt witness at $t=0$.
Hinge measures and deficit directional derivatives are the global, edge-indexed counterparts of those local angle derivatives. The bookkeeping Prop equates the two presentations of the first-order variation.
proof idea
No proof: this is a definition of a Prop. The body is the universal quantification over vertex potentials of the equality between (i) the sum over global edges of hinge measure at zero potential times the deficit directional derivative built from the local angle package, and (ii) the negated double sum over tetrahedra and six local slots of edge length times the packaged angle derivative. Downstream, the identity is discharged from a coarser edge-slot reindexing hypothesis by intro and reindexing, not by analytic work inside this declaration.
why it matters
Schläfli cancellation for the conformal Regge first variation needs the deficit variation rewritten as a sum of local tetrahedral Schläfli sums; this Prop is exactly that rewrite. It is consumed by conformalSchlaefliCancellation_of_lengthChain_of_bookkeeping (cancellation once a length-chain package and this bookkeeping hold) and by reggeActionFirstVariationInput_of_incidenceBookkeeping (assembly of the full first-variation input bundle). It is produced from IncidenceEdgeSlotBookkeeping via conformalSchlaefliIncidenceBookkeeping_of_edgeSlotBookkeeping, so the analytic load sits on incidence partition rather than on new derivative estimates. In the module's target theorem, this is the combinatorial half of "Schläfli cancellation plus zero deficit" at the flat conformal potential; it does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law, but it is the geometric bookkeeping step those continuum limits presuppose when Regge calculus is the discrete skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.