octantSystems
plain-language theorem explainer
The definition builds the pair of even- and odd-parity XOR systems for one Morton octant at a fixed subdivision level. Researchers encoding SAT problems with geometric Morton constraints cite this when populating the octant family. The body is a literal two-element list that calls the single-octant constraint constructor once for each parity.
Claim. For natural number $n$, octant level $k$, and index $i$, the value is the list consisting of the even-parity XOR constraint and the odd-parity XOR constraint on the variables of the $i$-th octant at level $k$.
background
The module introduces the geometric XOR family that augments linear masks with Morton-curve octant parity constraints. Octant level is the natural number counting recursive subdivisions of space into octants. Octant index selects one of the $8^k$ regions at level $k$. XOR system denotes a list of XOR constraints, each a set of variables together with a parity bit.
proof idea
The definition directly returns the list containing the false-parity single-octant constraint followed by the true-parity single-octant constraint.
why it matters
It serves as the generator for the function assembling all octants at one level, which supports the length bounds for that function and for the per-octant length. This fills the geometric extension of the XOR family described in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.