slotOrbitDeficitKer
plain-language theorem explainer
For each hinge orbit type and lattice slot (s,t), the slot orbit deficit kernel is the orbit seed star-deficit covector pushed forward by the first S₄ covering permutation that realizes that slot. Gravity analysts cite it when assembling all-orbit Bloch m² coefficients, local incidence means, and phased deficit contractions. The body is a one-line composition of the transported deficit with the covering index.
Claim. Fix a hinge orbit type $\tau$ and a lattice slot $(s,t)$ with $s\in\{0,\ldots,23\}$ and tetrahedron index $t\in\{0,\ldots,9\}$. The slot orbit deficit kernel is the map $\mathrm{Fin}\,15\to\mathbb{R}$ equal to the orbit seed deficit kernel of $\tau$ pushed forward by the first $S_4$ covering permutation of $(s,t)$ relative to the orbit representative.
background
The module builds a continuum-facing multi-orbit 4D Bloch fold for Regge gravity. Hinge configurations fall into lattice orbit types under coordinate permutation (the inductive family with labels such as $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$). Each orbit carries a seed star-deficit kernel in the 15-dimensional class space of edge variations; transport along $S_4$ is by the covering pushforward that reindexes that kernel.
The covering index for a slot $(s,t)$ is the first $S_4$ element that realizes the slot relative to the orbit representative (fallback $0$ only off realizable slots). The transported deficit is exactly that seed kernel pushed by a chosen covering element. The module warns against the older factorized transport on 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$.
Local theoretical setting: uniform covering pushforward of assembly area covectors and star deficit kernels for every orbit, with $(1,1)$ recovery of the classical single-orbit fold.
proof idea
Definitional one-liner. Evaluate the transported orbit deficit at the covering permutation of the given slot: compose the pushforward of the orbit seed kernel with the first $S_4$ cover of $(s,t)$. No tactics, no lemmas beyond that composition.
why it matters
This is the slot-level deficit leg of the all-orbit transported fold. Downstream it feeds the full and truncated transported $m^2$ slot coefficients (and their quadratic homogeneity), the collapsed phased deficit contraction used when cube-offset tables are absent, and the local-incidence identities that scale mean local kernels and slot terms by the inverse orbit star size.
It sits inside the gravity analysis chain that compares covering-based transport to factorized folds (lesson that non-$(1,1)$ orbits must not use the older transport). Status-wise it supports proved $(1,1)$ recovery and the raw all-orbit $m^2=-5/2$ evaluation on the TT-plus/symbol direction, while the open continuum targets remain all-orbit $m^2$ Tendsto and EH isotropy (still needing 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.