maxOctantLevel_le
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish a tighter bound such as log8(n).
- Does not apply when n is zero or negative.
- Does not address real-valued subdivision counts.
- Does not interact with the Recognition Composition Law.
formal statement (Lean)
108lemma maxOctantLevel_le (n : Nat) : maxOctantLevel n ≤ n := by
proof body
Term-mode proof.
109 unfold maxOctantLevel
110 have h1 : Nat.log2 n.succ / 3 ≤ Nat.log2 n.succ := Nat.div_le_self _ _
111 have h2 : Nat.log2 n.succ ≤ n := log2_succ_le n
112 omega
113
114/-- Auxiliary: flatMap length bound. -/