mortonOctantFamily
plain-language theorem explainer
mortonOctantFamily assembles the complete collection of Morton octant XOR systems for n variables by ranging over subdivision levels from 0 to maxOctantLevel n and concatenating the systems produced at each level. Researchers bounding the size of geometric SAT encodings or analyzing XOR constraint families in complexity theory would cite this construction when forming the full geoFamily. The definition is a direct flatMap of octantsAtLevel over the integer range up to the maximum level.
Claim. Let $H_{morton}(n)$ be the Morton octant family for $n$ variables, given by the concatenation over levels $0$ to $maxOctantLevel(n)$ of the list of XOR systems produced by octantsAtLevel at that level, where each such system encodes parity constraints aligned to an octant subdivision of the $n$-variable space.
background
The module constructs the geometric XOR family $H_{geo}(n)$ by adjoining Morton-curve-aligned octant parity constraints to the linear mask family. maxOctantLevel(n) returns the largest subdivision depth, computed as floor(log2(n+1)/3) and described as the number of log_8(n) levels of subdivision. octantsAtLevel(n, level) returns the list of all octant systems at a fixed level by ranging over octant indices up to min(8^level, n+1) and invoking octantSystems for each. XORSystem(n) is an abbreviation for a list of XOR constraints on n variables.
proof idea
The definition is a one-line wrapper that applies List.range to (maxOctantLevel n + 1) and flatMaps the octantsAtLevel function over each level index.
why it matters
This definition supplies the Morton component that geoFamily concatenates with the linear family, enabling the subsequent size-bound lemma that shows the full geometric family has length O(n^2). It fills the geometric-construction step in the SAT complexity module, supporting polynomial-size families used to analyze constraint systems within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.