orbitCoveringPerm_spec
plain-language theorem explainer
When a hinge slot's orbit type is fixed as ty, the orbit-covering S4 index for that slot maps the orbit representative's difference pair exactly onto the slot's two difference masks. Anyone transporting Regge-Bloch data across all orbit classes (not just (1,1)) cites this packaging lemma. The proof substitutes the type hypothesis into the exhaustive covering theorem and unfolds the Boolean cover test.
Claim. Let $ty$ be a hinge orbit type and let $(s,t)\in\mathrm{Fin}\,24\times\mathrm{Fin}\,10$ be a lattice slot with $\mathrm{hingeOrbitType}(s,t)=ty$. Write $p$ for the first $S_4$ index that covers the slot relative to the orbit representative of $ty$. Then applying the coordinate permutation of $p$ to the representative difference pair yields exactly the slot difference masks $(\mathrm{diffMaskA}(s,t),\mathrm{diffMaskB}(s,t))$.
background
This module builds orbit-covering coordinate permutations for 4D Regge-Bloch hinge transport. Each lattice slot $(s,t)$ carries two difference masks (XOR of successive triangle vertex masks) and an orbit type under the $S_4$ action on axes. The orbit representative of a type is a fixed pair of masks; transport is the first permutation $p\in\mathrm{Fin},24$ (in permAxes order) such that permuting that representative recovers the slot's masks.
The Boolean predicate coversOrbitSlot decides exactly that equality after applying coordPermOf p. The definition orbitCoveringPerm searches the finite list of all 24 indices and returns the first hit (falling back to 0 only if none exists, which never happens on realizable slots). The upstream theorem orbitCoveringPerm_covers states that every slot is covered by the covering index built from its own orbit type: the cover test returns true after exhaustive fin_cases and decide.
The hand table used historically for $(1,1)$ slots must not be reused on other orbits; the covering construction is the uniform transport for all types.
proof idea
One-line packaging of the exhaustive covering result. Obtain orbitCoveringPerm_covers s t, which asserts that the Boolean cover test holds for (hingeOrbitType s t, s, t) at the covering index. Substitute the hypothesis hingeOrbitType s t = ty so the type argument becomes ty. Then simpa unfolds coversOrbitSlot (and decide_eq_true_iff) to turn the Boolean equality into the propositional identity of permuted representative masks with (diffMaskA s t, diffMaskB s t).
why it matters
Uniform Bloch transport across every hinge orbit class depends on knowing that the covering permutation really solves the difference-mask equation once the orbit type is known. This lemma is the typed packaging of that fact: callers who already classified the slot as ty can invoke the covering equation without re-deriving the type. The module doc marks covering existence on every slot (and agreement with the legacy $(1,1)$ table) as the THEOREM tier of this file; the present statement is the form used when the type is an explicit parameter rather than recomputed.
In the broader Recognition gravity stack this sits inside 4D Regge hinge analysis: difference masks label triangle geometry on the lattice, and $S_4$ axis permutations implement discrete transport of those labels. No downstream consumers are wired yet in the graph, so the lemma is presently a stable API edge for later fold and curvature assemblies. It closes no open scaffold; it is fully proved by finite decision from the covering theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.