113theorem grayToNat_preserves_bound : 114 ∀ g d : ℕ, g < 2^d → d ≤ 64 → grayInverse g < 2^d :=
proof body
Term-mode proof.
115 GrayCodeFacts.grayToNat_preserves_bound 116 117/-- **Classical Result**: Pattern to number conversion bound. 118 119Converting a d-bit pattern to a number gives a value < 2^d. 120 121**Proof**: Sum of 2^i for i < d equals 2^d - 1 < 2^d 122 123**References**: Elementary combinatorics 124 125**Status**: Straightforward calculation 126-/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.