octantsAtLevel_length_bound
plain-language theorem explainer
The bound states that at any fixed level the geometric octant family for n variables contains at most 2(n+1) systems. Complexity theorists bounding the size of Morton-curve XOR families cite this when proving the overall family remains quadratic. The argument unfolds the flatMap definition of octantsAtLevel, observes that each of the min(8^level, n+1) octants contributes two parity systems, and invokes the trivial min inequality together with omega arithmetic.
Claim. For natural numbers $n$ and level, if $O(n, level)$ denotes the list of XOR systems generated by octants at the given level for $n$ variables, then $|O(n, level)| ≤ 2(n + 1)$.
background
The module constructs the geometric XOR family by aligning parity constraints along Morton curves in octant subdivisions of the variable space. The definition octantsAtLevel n level produces the list of all such systems at a given subdivision level by flat-mapping octantSystems over the first min(8^level, n+1) octants. Each octantSystems entry returns exactly two systems, one for each parity of the octantConstraint.
proof idea
The proof unfolds octantsAtLevel, rewrites via List.length_flatMap, establishes that every octantSystems list has length exactly two, simplifies the resulting sum of constants over the range, and reduces the claim to min(8^level, n+1) ≤ n+1 via a short calculation and the omega tactic.
why it matters
This per-level bound is invoked directly in mortonOctantFamily_size_bound to establish that the complete Morton octant family has size O(n²). It therefore supplies the key cardinality estimate in the geometric extension of the linear mask family for SAT instances. The 8^level subdivision connects to the eight-tick octave structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.