exactDeficitDot_smul
plain-language theorem explainer
The exact flat-background deficit derivative is homogeneous of degree one in the strain matrix: scaling the strain by a real constant scales the deficit side by the same factor. Gravity analysts assembling the continuum Regge Hessian cross-term cite this when reducing quadratic scaling of each hinge slot. The proof case-splits on hinge orbit type and discharges both branches by the corresponding phased-deficit smul lemmas.
Claim. For every real scalar $c$, hinge orbit type $\tau$, strain matrix $H\in M_4(\mathbb{R})$, wavevector $m\in\mathbb{R}^4$, and hinge indices $s\in\{0,\ldots,23\}$, $t\in\{0,\ldots,9\}$, the exact deficit derivative satisfies $\dot{\delta}_\tau(cH,m,s,t)=c\,\dot{\delta}_\tau(H,m,s,t)$.
background
This module builds the exact flat cross-term continuum symbol for 4D Regge calculus on the Freudenthal torus. At a flat background the deficits vanish, so the Schläfli identity reduces the second variation to the cross term $S''=\sum_h(dA_h)(d\delta_h)$. The deficit factor of each slot is packaged as an orbit-typed exact deficit derivative on plane-wave class strains.
Mat4 is a real $4\times 4$ matrix (the strain); Wave4 is a real 4-vector (the Bloch wavevector). Hinge orbits under coordinate permutation split into six types: type $(1,1)$ keeps star-member cube offsets, while $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, and $(2,2)$ use per-edge transported origins. The exact deficit derivative dispatches on that type to the corresponding phased deficit map.
Upstream, the type-$(1,1)$ branch already has a scalar-homogeneity lemma, and the edge-origin family has its own smul theorem obtained by factoring the plane-wave sum.
proof idea
Case-split on the six hinge orbit constructors. On type $(1,1)$, unfold the exact deficit derivative and apply the resolved type-$(1,1)$ phased-deficit smul lemma (itself a short unfold plus phasedClassDot_smul and sum factoring). On the five remaining orbits, unfold and apply the edge-origins phased-deficit smul theorem, which reduces to a list-sum map of the plane-wave contribution. Both branches finish by simp.
why it matters
Structural homogeneity is required before the flat cross-term slot can be shown quadratic in the strain. The immediate parent is the slot-level smul theorem in the same module, which multiplies area and deficit sides to obtain a $c^2$ factor on each hinge contribution to $S''$.
That slot feeds the exact flat cross-term fold and the finite exact Regge symbol used as the continuum-symbol sequence in preflight. The module's oracle target is the true Regge Hessian on the Freudenthal torus (vertex-gauge annihilation and normalized TT eigenvalue $-1/4$ on the banked symbol directions). Homogeneity lemmas sit in the THEOREM tier of structural facts; they do not close the open continuum Tendsto or ledger $S_{RS}$ inhabit questions, but they keep the discrete bookkeeping package algebraically clean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.