slotOrbitDeficitPhase2EdgeOrigins
plain-language theorem explainer
Sums phase-2 star-edge contributions for one hinge-orbit slot after seed edges are transported by the covering S4 permutation and the hinge-base origin. Gravity analysts cite it when building the position-resolved m² truncation coefficient on non-t11 orbits. The body is a one-line map-then-sum over the seed edge list for the orbit type.
Claim. For a hinge orbit type $\tau$, a $4\times 4$ real matrix $H$, a wave direction $v\in\mathbb{R}^4$, and slot indices $(s,t)\in\{0,\ldots,23\}\times\{0,\ldots,9\}$, the position-resolved phase-2 orbit deficit is $\sum_e C^{(2)}(\pi_{\tau}(s,t),\,b(s,t),H,v;e)$, the sum of phase-2 edge contributions of every seed star edge $e$ of $\tau$, each evaluated after the covering $S_4$ permutation $\pi_{\tau}(s,t)$ and the hinge-base origin $b(s,t)$.
background
This module repairs the 4D Regge–Bloch fold by making star-edge origins position-resolved. Seed star edges carry lattice origins; covering permutations transport both class index and origin into the deficit phase for non-t11 hinge orbits. The Python gate banks gauges to zero and keeps TT plus=cross=-1/4 on the symbol direction, leaving t11 untouched.
Mat4 is a $4\times 4$ real matrix and Wave4 a map $\mathrm{Fin},4\to\mathbb{R}$. The hinge base $b(s,t)$ is the masked coordinate of the first triangle-vertex mask at slot $(s,t)$. The covering permutation $\pi_\tau(s,t)$ is the first $S_4$ index that covers the orbit slot relative to the orbit representative (fallback 0 only if unrealizable).
Seed edge contributions are typed triples (class index, weight, origin) listed per orbit type. Phase-2 edge contribution folds those data with $H$ and the wave direction after transport.
proof idea
Pure definition, not a proof. Take the finite list of seed edge contributions for the orbit type, map each through the phase-2 edge contribution evaluated at the covering permutation of $(s,t)$, the hinge base of $(s,t)$, the matrix $H$, and the wave direction, then sum the resulting reals. No lemmas are invoked in the body.
why it matters
This is the deficit-phase factor inside the position-resolved m² truncation slot coefficient for non-t11 orbits: that coefficient multiplies the area-covariance weighted class sum by $-\tfrac12$ times this deficit when the slot lies on the orbit, else zero.
Downstream evaluation theorems identify the quantity on symbol direction with explicit radical prefactors times integer slot-Kpp edge sums: $\sqrt{2}/16$ for t12 and t21, $\sqrt{3}/48$ for t13 and t31, and $1/16$ for t22. Those equalities discharge the fold-position-resolved star-phase blocker for the banked gauges.
In the Recognition gravity stack this is local 4D Regge–Bloch analysis (eight-tick / D=3 scaffolding sits upstream), not a T0–T8 forcing step. It does not touch gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.