transportedDeficit
plain-language theorem explainer
For each of the 24 coordinate permutations, the transported deficit is the pushforward of the committed type-(1,1) star class kernel onto the 15 edge-class slots. Anyone assembling the finite-momentum Bloch fold or the m² slot certificates cites it as the permuted seed weight. The body is a one-line reindexing sum: copy the kernel entry when the permuted class matches the target, else zero.
Claim. Given a coordinate permutation index $p \in \{0,\ldots,23\}$, the transported deficit is the map $d \mapsto \sum_{d_0} K_{\star}(d_0)$ over the fifteen edge classes, retaining only those $d_0$ whose class is sent to $d$ by the permutation action of $p$ on masks; $K_{\star}$ is the committed full-star class kernel of the type-$(1,1)$ hinge.
background
The ambient module builds the exact phase-decorated Bloch fold of the committed true-weight flat Hessian for type-(1,1) triangle hinges in one Kuhn cell, under the midpoint plane-wave convention. Scope is the (1,1) orbit only (72 oriented slots per cell).
Edge classes are indexed by $\mathrm{Fin},15$. The seed weight is the full-star class kernel $K_{\star}:\mathrm{Fin},15\to\mathbb{R}$ from the hinge star-kernel module: sparse real values on a handful of classes (e.g. $\pm 1$ on selected indices). A coordinate permutation $p$ acts on class masks via permClass, sending each source class $d_0$ to a target class.
Transport means: push $K_{\star}$ forward along that class map so every oriented slot can reuse the same seed after the lattice symmetry that places the hinge.
proof idea
Pure definition, no proof obligations. For fixed $p$ and target class $d$, sum over all fifteen source classes $d_0$; contribute $K_{\star}(d_0)$ exactly when permClass $p$ $d_0$ equals $d$, otherwise contribute zero. Equivalently, the value at $d$ is $K_{\star}$ evaluated on the preimage of $d$ under the class permutation (at most one term is nonzero for each $d$ in the cases used downstream).
why it matters
This is the elementary transport step that lets the Bloch fold and the $m^2$ symbol work slot-by-slot without rebuilding the Hessian. Downstream, phasedClassDot_transportedDeficit rewrites a phased dot against the transported kernel as the seed kernel folded through the class permutation; slotDeficitKer specialises transport to each of the 72 oriented slots via the slot transport permutation.
Further parents include the $m^2$ slot-coefficient certificate (m2SlotCoeff_eq_cert), the identification of the (1,1) orbit deficit with this transport (transportedOrbitDeficit_t11), and the corresponding $e_0$-direction $m^2$ evaluation. In the module's campaign list it underwrites the transported phased fold, the integer Bloch symbol at the star wavevector, and the geometric-versus-certificate match on all oriented slots. It does not itself close continuum EH matching or gap-action recovery; those remain later lanes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.