127theorem pattern_to_nat_bound : 128 ∀ (d : ℕ) (p : Pattern d), 129 (∑ k : Fin d, if p k then 2^(k.val) else 0) < 2^d :=
proof body
Term-mode proof.
130 GrayCodeFacts.pattern_to_nat_bound 131 132/-- **Classical Result**: Consecutive Gray codes differ in one bit. 133 134For any n < 2^d - 1, gray(n) and gray(n+1) differ in exactly one bit position. 135 136**Proof**: 137- gray(n) XOR gray(n+1) = [n XOR (n>>1)] XOR [(n+1) XOR ((n+1)>>1)] 138- This simplifies to a single power of 2 (bit at position of least significant 0 in n) 139 140**References**: 141- Savage (1997), Theorem 2.1 142- Knuth (2011), Theorem 7.2.1.1.A 143 144**Status**: Defining property of Gray codes 145-/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.