octantsAtLevel
The function that collects all octants at a given level assembles the list of XOR constraint systems for each octant subdivision in an n-variable instance. Researchers building geometric SAT encodings or proving size bounds on the Morton family in Recognition Science cite it when constructing the full geoFamily. It is realized by flat-mapping the octant systems generator over the initial segment of octant indices up to min(8 to the power level, n plus one).
claimLet $L(n,k)$ be the list of all XOR systems at octant level $k$ for an $n$-variable instance. Then $L(n,k)$ is obtained by flattening the output of the octant systems function over the first $m = min(8^k, n+1)$ octant indices, where each index yields a pair of even-parity and odd-parity systems.
background
The Geometric XOR Family module defines Morton-curve-aligned octant parity constraints that extend the linear mask family. OctantLevel is the natural number $k$ counting subdivision depth, with $k=0$ the undivided space and $k$ producing $8^k$ subregions. The sibling octantSystems produces, for each octant index, the two XOR systems enforcing the respective parities inside that octant; XORSystem itself is the type of lists of XOR constraints.
proof idea
This is a direct definition that computes the list by taking List.range up to min(8^level, n+1) and then flatMapping the octantSystems function over those indices. It relies only on the prior sibling definition of octantSystems together with standard List operations from Mathlib. No lemmas or tactics appear in the body.
why it matters in Recognition Science
This definition supplies the per-level generator for mortonOctantFamily, which aggregates across all levels up to maxOctantLevel and thereby populates the geometric component of the full geoFamily. It is invoked directly in the proof of the O(n^2) size bound for the Morton family. In the Recognition Science setting it enumerates the octant constraints that align with the eight-tick octave structure and the three-dimensional spatial partitioning.
scope and limits
- Does not generate systems for octants beyond the min(8^level, n+1) cutoff.
- Does not define the formulas inside individual XOR constraints.
- Does not compute or prove any length or complexity bounds on its output.
- Does not incorporate the linear mask family components.
formal statement (Lean)
49def octantsAtLevel (n : Nat) (level : OctantLevel) : List (XORSystem n) :=
proof body
Definition body.
50 (List.range ((8 ^ level).min (n + 1))).flatMap fun octant =>
51 octantSystems n level octant
52
53/-- Maximum octant level: log_8(n) levels of subdivision. -/