pattern_to_nat_bound
plain-language theorem explainer
The theorem establishes that any d-bit pattern, when summed as powers of two for its set bits, yields an integer strictly less than 2^d. Discrete mathematicians and computer scientists formalizing Gray code conversions would cite this bound to guarantee pattern values remain in the representable range. The proof is a one-line wrapper that applies the GrayCodeFacts hypothesis envelope.
Claim. For every natural number $d$ and every bit pattern $p$ of length $d$, the integer value obtained by summing $2^k$ over positions $k$ where the $k$-th bit of $p$ is set satisfies $p < 2^d$.
background
The module Patterns.GrayCodeAxioms declares classical Gray code properties as axioms pending full bitwise formalization. A Pattern d denotes a bit vector of length d, i.e., a function from Fin d to Bool whose support determines which powers of two are included in the sum. The local theoretical setting stresses that all such properties possess multiple published proofs in the discrete mathematics literature, with references to Savage (1997) and Knuth (2011).
proof idea
The proof is a one-line wrapper that applies GrayCodeFacts.pattern_to_nat_bound. This directly invokes the hypothesis envelope class declared earlier in the same module, which collects the classical Gray code axioms.
why it matters
The result supplies the numerical bound required by the GrayCodeFacts class, which is the immediate downstream consumer. It completes the elementary combinatorics step inside the Patterns module and supports axiomatic treatment of bit patterns that appear in Recognition Science encodings. The declaration aligns with the framework's reliance on discrete combinatorial objects that interface with the phi-ladder and forcing chain without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.