transportedOrbitDeficit
plain-language theorem explainer
For each hinge orbit type and covering permutation, the transported star-deficit kernel is the pushforward of that orbit's assembly seed kernel onto the 15 edge-difference classes. Gravity analysts cite it when building all-orbit Bloch folds and slot-local m² coefficients beyond the (1,1) sector. The body is a one-line composition of the seed kernel with the covering pushforward.
Claim. Given a hinge orbit type $\tau$ and a covering permutation index $p\in\{0,\ldots,23\}$, the transported orbit deficit is the class covector $K_{\tau,p}:\{0,\ldots,14\}\to\mathbb{R}$ obtained by pushing the orbit seed star-deficit kernel of $\tau$ forward under $p$: $K_{\tau,p}(d)=\sum_{d_0}\mathbf{1}_{\pi_p(d_0)=d}\,K^{\mathrm{seed}}_\tau(d_0)$.
background
This module builds the continuum-facing multi-orbit 4D Bloch fold. Each slot transports its orbit's seed area covector and star deficit kernel by the covering permutation orbitCoveringPerm (the first $S_4$ cover of the orbit representative). The module status explicitly warns against using the older factorized transport for non-$(1,1)$ orbits: measured all-orbit $m^2$ along the symbol direction on the TT-plus axis is $-5/2$ raw, not the factorized $0$.
Hinge orbit types are the six lattice orbits under coordinate permutation: $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$. The seed star-deficit kernel assigns to each type its assembly commitment (full star-class kernels for $(1,1)$, $(1,2)$, $(1,3)$; dedicated kernels for $(2,1)$ and $(3,1)$). Pushforward of a class covector $v$ by a covering permutation $p$ reindexes $v$ by summing contributions whose permuted class lands on the target difference class.
The ambient setting is Regge calculus on 4D hinges: class covectors live on the 15 edge-difference slots, and covering permutations run over the 24 elements of $S_4$.
proof idea
One-line definitional wrapper. Evaluate the seed star-deficit kernel at the given orbit type, then apply the covering pushforward at the given permutation index. No lemmas or tactics; the meaning is entirely compositional.
why it matters
This is the deficit half of the transported all-orbit infrastructure. Downstream, every slot-orbit deficit kernel is obtained by specializing the covering permutation to orbitCoveringPerm ty s t, and the mean-local kernel identity scales that result by the inverse orbit star size. The $(1,1)$ recovery theorem shows the construction collapses exactly to the classical transported deficit on the $(1,1)$ orbit, tying the multi-orbit fold back to the already-proved single-orbit Bloch fold and $m^2$ symbol.
Sibling M2Eval certificates for $(1,2)$, $(1,3)$, and $(2,1)$ slot coefficients unfold through this definition when matching integer certificates along the symbol and $e_0$ directions. In the Recognition gravity stack it supplies the deficit side of the continuum-facing fold whose raw all-orbit $m^2$ evaluates to $-5/2$ on axis-TT-plus; open items remain all-orbit $m^2$ Tendsto and continuum Einstein-Hilbert isotropy (the residual $2/N^4$ cell-sum dictionary). It does not touch gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.