swap23Mask_bounds
plain-language theorem explainer
For every edge class index in the 15-class 4D stencil, the bit-mask obtained by swapping axes 2 and 3 stays inside {1,…,15}. Anyone building the induced class map under that swap cites this bound. The proof is exhaustive case analysis on Fin 15 with decide.
Claim. For every edge class $d \in \{0,\ldots,14\}$, if $m = d+1$ is its bit-mask and $m'$ is the mask after exchanging coordinate bits 2 and 3, then $0 < m' \le 15$.
background
The module builds the combinatorial skeleton of a Freudenthal/Kuhn 4-cube hinge for 4D Regge calculus, importing the fixed 15-class edge stencil rather than redefining it. Edge classes are indexed by Fin 15; each class $d$ has bit-mask $m = d+1 \in {1,\ldots,15}$, encoding which of the four axis bits are set in the 0/1 displacement.
The axis swap $2 \leftrightarrow 3$ acts on masks by exchanging bits 2 and 3 while leaving bits 0 and 1 fixed. That map is the local definition used here. The seed hinge (vertices $0$, $e_0$, $e_0+e_1$) is fixed by this swap, so incidence symmetry under the swap is a natural combinatorial check in the campaign.
The bound is the arithmetic gate needed before one can reindex the swapped mask back into Fin 15.
proof idea
Term-mode proof by exhaustive case split: fin_cases d runs over all fifteen class indices, and decide discharges the concrete numeric inequalities $0 < \mathrm{swap23Mask}(d+1) \le 15$ in each case. No intermediate lemmas are invoked beyond the definitions of the mask and the swap.
why it matters
Feeds the definition of the induced class map under axis swap $2 \leftrightarrow 3$, which subtracts one from the swapped mask and packages the result as an element of Fin 15; the bound supplies the proof obligation that the result is in range. That class map is the carrier for the THEOREM that seed-hinge incidence is invariant under the swap fixing the seed triangle.
In the module's honest scope this is a small A-shaped combinatorial gate inside deliverable B (incidence support, nonvacuity, symmetry, decoys). It does not touch the OPEN per-hinge deficit/area kernels, the flat Hessian of the 4D Regge action, or S_RS_converges_EH_4d. It sits in the gravity analysis track that prepares discrete curvature data for later Recognition-scale continuum limits, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.