conformalSchlaefliIncidenceBookkeeping_of_edgeSlotBookkeeping
plain-language theorem explainer
Edge-slot incidence bookkeeping upgrades to the conformal Schläfli incidence identity: the edge-sum of hinge measure times deficit angle derivative equals minus the sum of local edge lengths times angle derivatives over tetrahedral slots. Cited when assembling the first variation of the nonlinear Regge action at the flat conformal potential. Proof is a two-step calc: zero-potential hinges become global lengths, then sum_match reindexes.
Claim. Let $K$ be a 3D triangulation with consistent incidence, and let $A$ package local dihedral-angle directional derivatives under the conformal ansatz. If summing a local edge-slot weight over global edges and tetrahedra equals the direct sum over local tetrahedral edge slots (with matching flat edge lengths), then for every vertex potential $\eta$, $\sum_e \ell_e(0)\,\delta'_e(\eta)=-\sum_\tau\sum_{f=1}^{6}\sqrt{s_{\tau,f}}\,A(\eta,\tau,f)$, where $\ell_e(0)$ is the hinge measure at zero potential and $\delta'_e$ is the deficit directional derivative from $A$.
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 plus zero deficit; until closed-form local Schläfli identities are fully expanded, the module records exact analytic statements and named input packages.
A local dihedral directional-derivative package supplies, for each tetrahedron and each of its six edge slots, the directional derivative of the conformal dihedral angle along a line of vertex potentials, with a HasDerivAt certificate at $t=0$. The hinge measure under the conformal ansatz is the edge length $\sqrt{s_e}\exp((\xi_u+\xi_v)/2)$. At the zero potential this collapses to the bare global edge length.
Incidence edge-slot bookkeeping is the partition certificate: summing a weight $w(\tau,f)$ against global edge lengths via the incidence match equals summing $\sqrt{s_{\tau,f}} w(\tau,f)$ directly over all local slots. Existence of a global edge per local slot comes from incidence consistency; uniqueness and no-duplication are packaged so reindexing is exact.
proof idea
Fix a vertex potential $\eta$. Unfold the deficit directional derivative (the negative sum of local angle derivatives over tetrahedra incident to each edge). The first calc step unfolds hinge measure at the zero potential and global edge length, pulls out the overall minus via Finset.sum_neg_distrib, and simplifies pointwise so each hinge factor becomes the bare global edge length.
The second step applies the bookkeeping sum_match identity to the weight $w(\tau,f)$ equal to the packaged angle derivative at $(\eta,\tau,f)$. That reindexes the double sum from global edges (with incidence matching) to a pure sum over tetrahedra and their six local edge slots, weighted by $\sqrt{s_{\tau,f}}$. The result is exactly the right-hand side of conformal Schläfli incidence bookkeeping.
why it matters
This lemma bridges combinatorial incidence data to the global form of the first variation. Downstream, the first-variation input builder from edge-slot bookkeeping assembles a full package from flatness plus this identity, and the gravity side uses it inside the canonical periodic deficit-derivative package for the periodic Freudenthal torus (Track 1.B), so the deficit package is no longer an arbitrary hypothesis.
In the module program, the target is vanishing of the Regge first variation at the flat conformal potential via Schläfli cancellation. The identity converts the edge-indexed deficit variation into a sum of local tetrahedral Schläfli sums, the algebraic shape needed before local angle derivatives cancel against edge-length variations. It sits in the geometry layer that feeds discrete gravity, not in the T0-T8 forcing chain itself, but it is load-bearing for stationarity of the nonlinear Regge action on flat conformal backgrounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.