mortonOctantFamily_size_bound
plain-language theorem explainer
The Morton octant family collects all octant parity XOR systems across subdivision levels up to maxOctantLevel(n). Researchers bounding the size of geometric XOR families for SAT encodings cite this result. The proof unfolds the family definition, applies a per-level length bound of 2(n+1), invokes the flatMap length lemma, and uses the level count inequality maxOctantLevel(n) ≤ n to reach the quadratic upper bound.
Claim. Let $M(n)$ be the Morton octant family of XOR systems for parameter $n$. Then $|M(n)| ≤ 2(n+1)^2$.
background
The module defines the geometric XOR family as the linear mask family extended by Morton-curve octant constraints. The Morton octant family is the flatMap over levels 0 to maxOctantLevel(n) of octantsAtLevel(n, level), where maxOctantLevel(n) = floor(log2(n+1)/3). Each level contributes at most 2(n+1) systems because min(8^level, n+1) octants each generate two systems. This construction relies on the flatMap length bound lemma, which states that if each of m functions produces lists of length at most bound then the flatMapped list has length at most m times bound. The level count is controlled by the lemma maxOctantLevel(n) ≤ n.
proof idea
The proof first unfolds the family to expose the flatMap structure. It introduces a hypothesis that every octantsAtLevel list is bounded by 2(n+1) using the dedicated length bound lemma. The flatMap length bound lemma is applied to obtain a product bound of (maxOctantLevel(n)+1) times 2(n+1). The maxOctantLevel_le lemma supplies maxOctantLevel(n) + 1 ≤ n + 1, after which multiplication and ring simplification yield the target bound 2(n+1)^2.
why it matters
This bound is used in geoFamily_poly_bound to show that the full geometric family has size at most 4(n+1)^2. It completes the polynomial size claim for the geometric XOR family in the SAT complexity module. In the Recognition framework this supports controlling the resource requirements of geometric constraint families, aligning with the need for polynomial bounds in complexity analyses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.