pattern_to_nat_bound
plain-language theorem explainer
Any d-bit pattern converts to an integer strictly below 2^d. Discrete mathematicians and computer scientists working with Gray code encodings cite this bound when limiting pattern enumerations. The proof is a one-line wrapper delegating to the GrayCodeFacts hypothesis envelope.
Claim. For every natural number $d$ and every pattern $p$ of length $d$, the sum over $k=0$ to $d-1$ of $2^k$ if the $k$-th bit of $p$ is set (else 0) satisfies the inequality strictly less than $2^d$.
background
The module declares well-known Gray code properties as axioms pending full bitwise formalization. The binary-reflected Gray code uses the standard construction gray(n) = n XOR (n >> 1), with multiple published proofs in the discrete mathematics literature. The local setting treats these as classical results with O(log n) algorithms and extensive use in digital systems.
proof idea
One-line wrapper that applies GrayCodeFacts.pattern_to_nat_bound.
why it matters
This bound supports the GrayCodeFacts class that envelopes classical properties for pattern handling. It fills the elementary combinatorics step noted in the module doc-comment on Gray code axioms. The declaration touches the open question of completing the bitwise formalization referenced in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.