mortonIndex
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not implement bit-interleaving Morton order.
- Does not accept negative or non-natural inputs.
- Does not define octant subdivision or parity logic itself.
- Does not guarantee uniqueness for coordinates larger than the implicit base-1000 separation.
formal statement (Lean)
20def mortonIndex (x y z : Nat) : Nat :=
proof body
Definition body.
21 x + y * 1000 + z * 1000000
22
23/-- Octant level: how many octant subdivisions (0 = whole space, k = 8^k subregions). -/