mortonIndex
plain-language theorem explainer
MortonIndex encodes three natural-number coordinates into one index via the linear combination x + 1000 y + 1000000 z. Researchers building geometric SAT families for three-dimensional constraint problems would reference this encoding when generating octant parity masks. The definition is supplied directly as an arithmetic expression.
Claim. The coordinate encoding function is defined by $m(x,y,z) = x + 1000 y + 10^6 z$ for natural numbers $x,y,z$.
background
The module defines the geometric XOR family as an extension of linear mask families that adds Morton-curve-aligned octant parity constraints. MortonIndex supplies the coordinate-to-index map used to label octant subdivisions in three dimensions. No upstream lemmas are required; the definition stands alone within the SAT.GeoFamily module.
proof idea
The definition expands directly to the arithmetic expression x + y * 1000 + z * 1000000.
why it matters
This definition supplies the indexing primitive for the geometric XOR family in the SAT complexity module. It supports construction of octant systems that extend linear masks toward three-dimensional geometric constraints. No parent theorems or downstream uses are recorded, leaving its precise role in larger Recognition Science complexity arguments open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.