octantVars
plain-language theorem explainer
octantVars selects the list of variable indices whose Morton positions fall inside a chosen octant at a given subdivision depth. Researchers constructing geometric SAT encodings with locality constraints cite this selector to populate octant parity systems. The definition is a direct filter over the finite range of indices that applies scaled integer division to test membership.
Claim. For $n, k, i : Nat$ with $k$ the subdivision depth and $i$ the octant index, the octant variables are the list of $v : Fin n$ such that if $k=0$ the condition holds for every $v$, otherwise $v / max(1, n/8^k) = i mod min(n, 8^k)$.
background
OctantLevel is a natural number giving the depth of octant subdivision (0 covers the whole space; positive $k$ yields $8^k$ subregions). OctantIndex names one subregion within that partition. The module introduces the geometric XOR family that augments linear masks with Morton-curve-aligned octant parity constraints. Variables are drawn from the CNF module as indices of type Fin n.
proof idea
The definition is a one-line wrapper that applies List.filter to List.finRange n. The predicate returns true for every index when the level is zero and otherwise compares the scaled index (via integer division by the level-adjusted block size) against the given octant index using modulo.
why it matters
octantVars supplies the variable lists required by octantConstraint to form XOR parity systems and by mortonLocality to assert spatial closeness under the Morton ordering. It completes the variable-grouping step that extends the linear mask family to octant-based constraints, supporting the geometric family construction inside the SAT complexity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.