maxOctantLevel
plain-language theorem explainer
maxOctantLevel returns the largest subdivision depth for Morton octant masks inside a geometric XOR family of size n. Researchers bounding the constraint count in SAT encodings that incorporate spatial octant parity would cite the value when constructing the full mask list. The definition is realized as a direct arithmetic reduction that takes the integer division of log base 2 of n+1 by 3.
Claim. The maximum octant level for a system of size $n$ is given by $⌊log₂(n+1)/3⌋$.
background
The Geometric XOR Family module defines the geometric XOR family 𝓗_geo(n) as the extension of linear mask families by Morton-curve-aligned octant parity constraints. This construction supports SAT instances whose variables carry three-dimensional geometric relations. maxOctantLevel supplies the depth of subdivision, expressed via the base-2 logarithm imported from Information.Compression and the successor operation from ArithmeticFromLogic.
proof idea
The declaration is a one-line definition that applies Nat.log2 to the successor of the input and then performs integer division by 3. No lemmas or tactics are invoked inside the body.
why it matters
The value is required by mortonOctantFamily to generate the complete list of octant masks and by the subsequent size-bound lemma that shows the family remains polynomial in n. It supplies the level count for the eight-tick octave structure (period 2^3) inside the geometric family, consistent with the forcing-chain derivation of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.