octantConstraint
plain-language theorem explainer
The octantConstraint definition builds an XORConstraint record whose variable list is exactly the subset belonging to one Morton octant at a chosen subdivision depth. Researchers constructing geometric SAT instances or parity systems aligned with spatial octants cite this as the atomic generator inside the geoFamily. The definition is a direct one-line record constructor that delegates the variable filter to octantVars and attaches the supplied parity bit.
Claim. For natural numbers $n$, subdivision depth $l$, octant index $o$, and parity bit $p$, the constraint is the pair $(V, p)$ where $V$ is the list of variables $v < n$ satisfying the octant-membership test $v / (n / 8^l) = o$ (with the usual conventions for level 0 and boundary cases).
background
The Geometric XOR Family module defines the family of Morton-aligned XOR systems that extend ordinary linear masks. OctantLevel is simply a natural number counting successive 8-way subdivisions of the variable index space; level 0 is the entire interval while level $l$ produces $8^l$ subregions. OctantIndex is the corresponding coordinate running from 0 to $8^l-1$ inside that partition.
proof idea
The definition is a one-line wrapper that applies octantVars to obtain the filtered variable list for the given level and octant, then packages the list together with the supplied parity into an XORConstraint record.
why it matters
octantConstraint is the generator consumed by the downstream octantSystems definition, which assembles the two parity instances for each octant and thereby populates the geometric family H_geo(n). This construction supplies the spatial-octant layer of the SAT encoding used to probe complexity bounds inside the Recognition Science framework, where the eight-tick octave and D=3 geometry are expected to appear as structural constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.