maxOctantLevel
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not enumerate the octant masks at each level.
- Does not incorporate the phi constant or other Recognition Science primitives.
- Does not apply outside natural-number inputs.
- Does not prove any upper or lower bounds on its output value.
Lean usage
List.range (maxOctantLevel n + 1).flatMap fun level => octantsAtLevel n levelformal statement (Lean)
54def maxOctantLevel (n : Nat) : Nat :=
proof body
Definition body.
55 Nat.log2 n.succ / 3
56
57/-- Morton octant mask family: all octants at all levels. -/