mortonLocality
plain-language theorem explainer
The mortonLocality definition encodes the property that every variable selected for a given octant at subdivision level ell satisfies a Morton-order locality condition via integer division by powers of eight. Researchers constructing geometric SAT encodings or Morton-curve XOR families cite this predicate when verifying that octant constraints act only on spatially local variables. It is introduced as a direct predicate that restates the membership test already computed inside the octantVars filter.
Claim. Let $n$ be a natural number, let $ell$ be an octant level, and let $o$ be an octant index. The predicate mortonLocality$(n,ell,o)$ asserts that for every variable $v$ belonging to the list octantVars$(n,ell,o)$, if $ell=0$ then the statement holds vacuously, otherwise $v/(n/8^ell)$ equals $o$ modulo $8^ell$ (with the usual max and min adjustments for boundary cases).
background
The Geometric XOR Family module defines the geometric family H_geo(n) by extending linear mask families with parity constraints aligned to the Morton space-filling curve. OctantLevel is the natural number counting recursive octant subdivisions of the n-variable space (level 0 is the undivided space). OctantIndex is the natural number labeling one of the 8^ell subregions at that level.
proof idea
This declaration is a direct definition of the locality predicate. Its body states a universal quantifier over the output of octantVars together with a level-zero conditional that returns true. No lemmas are invoked; the predicate simply reproduces the integer-division filter already present inside octantVars.
why it matters
The definition supplies the predicate discharged by the theorem mortonLocality_holds, which confirms the locality property by unfolding the filter and applying simp. It forms part of the infrastructure for the geometric XOR family H_geo(n) in the module, enabling later constructions such as octantConstraint and geoFamily to impose Morton-aligned constraints. Within Recognition Science this supports complexity analyses that may connect to the forcing chain or recognition composition law, though no explicit link is asserted here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.