log2_succ_le
plain-language theorem explainer
The lemma establishes that the base-two logarithm of n plus one is at most n for every natural number n. Researchers bounding subdivision depth in Morton octant families for SAT encodings cite this result to control the size of geoFamily instances. The argument rewrites the logarithm, invokes the power inequality succ_le_two_pow inside a short chain, and closes with omega.
Claim. For every natural number $n$, $log_2(n+1) leq n$.
background
The Geometric XOR Family module constructs Morton-curve-aligned octant parity constraints that extend linear mask families for SAT encodings. The maximum octant level is defined as the floor division of log2(n+1) by three. This lemma supplies the auxiliary bound log2(n+1) leq n required to cap that level at n. It depends on the successor definition from ArithmeticFromLogic, the log2 function from Information.Compression, and the power bound succ_le_two_pow proved by induction on n.
proof idea
The tactic proof rewrites Nat.log2 to the Nat.log form with base two. It introduces 1 < 2 and n.succ neq 0, then applies Nat.log_lt_iff_lt_pow to reduce the goal to n.succ < 2^{n.succ}. This comparison follows from succ_le_two_pow via the chain n.succ < n.succ.succ leq 2^{n.succ}. Omega discharges the resulting inequality.
why it matters
The result is invoked by maxOctantLevel_le to conclude that the maximum octant level is at most n. That parent lemma ensures octantSystems and geoFamily remain inside the n-variable regime for the SAT instance. In the Recognition framework it supports the geometric family component of complexity analyses tied to the eight-tick octave and spatial dimension constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.