OctantIndex
OctantIndex is the natural-number type labeling octants at a fixed level of the Morton curve, with values running from 0 to 8^level minus one. Researchers constructing locality-preserving XOR systems for geometric SAT encodings cite it when partitioning variables into octant-aligned parity groups. The declaration is a direct type alias to Nat and carries no proof obligations.
claimAn octant index is any natural number $k$ used to label one of the $8^ell$ subregions at level $ell$ in the Morton ordering.
background
The module introduces the geometric XOR family that augments linear mask families by adding parity constraints aligned with Morton-curve octants. Octant indices label the eight spatial subregions at each level, while the companion OctantLevel type tracks the subdivision depth. Downstream definitions such as octantVars filter variables whose Morton indices fall inside a chosen octant, and octantConstraint packages those variables with a required parity bit.
proof idea
The declaration is a one-line abbreviation that directly equates the octant index type to Nat.
why it matters in Recognition Science
OctantIndex parameterizes inOctant, octantVars, octantConstraint, octantSystems, and mortonLocality, which together assemble the geoFamily of XOR systems. These systems encode spatial locality for SAT reductions that respect the Morton curve. The construction supplies the geometric layer needed to bound locality in complexity arguments within the Recognition Science framework.
scope and limits
- Does not embed the upper bound 8^level minus one into the type.
- Does not define arithmetic or conversion operations on indices.
- Does not reference J-cost, defect distance, or the phi-ladder.
- Does not connect to the T0-T8 forcing chain or Recognition Composition Law.
formal statement (Lean)
27abbrev OctantIndex := Nat
proof body
Definition body.
28
29/-- Check if a Morton index falls within a given octant at a given level. -/