succ_le_two_pow
plain-language theorem explainer
The auxiliary lemma proves that n + 1 ≤ 2^n holds for every natural number n. Researchers deriving logarithmic bounds inside SAT encodings for geometric XOR families cite this result. The proof proceeds by induction on n, invoking the standard inequality 1 ≤ 2^n in the successor step and closing the chain with algebraic simplification.
Claim. For all natural numbers $n$, $n + 1 ≤ 2^n$.
background
The Geometric XOR Family module defines the geometric XOR family 𝓗_geo(n) which extends the linear mask family with Morton-curve-aligned octant parity constraints. This auxiliary inequality supports bounding arguments needed for those encodings. It draws on the successor operation from ArithmeticFromLogic, where successor is one more application of the generator, and connects to the log base 2 definition from Information.Compression used in the immediate downstream bound.
proof idea
Proof by induction on n. The base case n = 0 simplifies directly. The successor case applies the known fact 1 ≤ 2^n, then uses a calculation chain with omega to show the inequality lifts to n + 2 ≤ 2^{n+1}.
why it matters
This lemma directly supports the log2_succ_le auxiliary that bounds log2(n + 1) ≤ n inside the same module. It contributes to complexity estimates for the geometric XOR family in Recognition Science, aiding information-compression arguments that feed into the phi-ladder and eight-tick octave structures. The result closes a small scaffolding step for logarithmic control in the SAT encoding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.