OctantIndex
plain-language theorem explainer
OctantIndex names the natural numbers that label octants at each level inside the Morton-curve geometric XOR family. Definitions of octant variables, constraints, and locality statements cite it directly. The declaration is a one-line type alias to Nat carrying no proof obligations.
Claim. $OctantIndex := Nat$, the type of indices ranging from 0 to $8^ℓ-1$ that label the octants at level $ℓ$ in the geometric family.
background
The module defines the geometric XOR family $H_geo(n)$ that augments linear mask families with Morton-curve-aligned octant parity constraints. OctantIndex is the companion index type to OctantLevel; together they parameterize the partition of $n$ variables into $8^ℓ$ octants. The downstream definitions octantVars, octantConstraint, and inOctant all take an OctantIndex argument to select the relevant subset of variables or to test membership.
proof idea
The declaration is a one-line abbreviation that directly aliases the natural-number type.
why it matters
OctantIndex supplies the uniform index type required by every octant-specific construction in the module, including octantVars, octantConstraint, octantSystems, inOctant, and the mortonLocality theorem. It therefore forms the indexing layer for the full geoFamily used in geometric SAT encodings. No core Recognition Science chain step (T0-T8 or RCL) is invoked here; the abbreviation simply closes the interface for the complexity-side geometric family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.