OctantLevel
plain-language theorem explainer
OctantLevel is the natural number counting recursive octant subdivisions in the Morton curve for the geometric XOR family. Researchers encoding geometric SAT instances cite it when building locality-preserving parity systems over octants. The declaration is a direct type abbreviation of Nat carrying no further axioms or computation.
Claim. Let $k$ be a natural number denoting octant level, where $k=0$ corresponds to the undivided domain and level $k$ partitions the space into $8^k$ subregions aligned with the Morton curve.
background
The Geometric XOR Family module constructs the family 𝓗_geo(n) by adjoining Morton-curve octant parity constraints to linear mask families. OctantLevel supplies the depth parameter used by sibling definitions such as inOctant, octantVars, octantConstraint, and mortonLocality. These definitions filter variables and impose XOR parities within each octant at the chosen subdivision depth.
proof idea
The declaration is a direct abbreviation of the natural numbers type, supplying a named alias for subdivision depth with no additional structure or lemmas applied.
why it matters
OctantLevel parameterizes every octant-based construction in the module, including octantSystems, octantsAtLevel, and the locality predicate mortonLocality. It thereby supports the geometric extension of the XOR family described in the module header. The alias feeds the seven downstream uses that realize Morton-aligned SAT encodings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.