maxOctantLevel_le
plain-language theorem explainer
The lemma shows that maxOctantLevel n is at most n for every natural number n. Analysts deriving size bounds on geometric SAT families cite this control on subdivision depth. The argument unfolds the definition, records the division bound on log2, invokes the upstream log2 inequality, and closes with omega.
Claim. For every natural number $n$, $Nat.log2(n+1)/3$ is at most $n$.
background
The module defines the geometric XOR family via Morton-curve octant masks that extend linear parity constraints. maxOctantLevel n counts the admissible subdivision levels and equals the integer division of log2(n+1) by 3. The upstream lemma log2_succ_le states that log2(n+1) is at most n for all n.
proof idea
Unfold maxOctantLevel to expose the division. Record that the quotient by 3 is bounded by the dividend itself via div_le_self. Apply log2_succ_le to replace the log term by n. Finish with omega to combine the two inequalities.
why it matters
The bound is invoked inside the proof that mortonOctantFamily has length at most 2(n+1)^2. It therefore supports the claim that the geometric family remains polynomially sized, which is the central size result of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.