GrayCodeFacts
plain-language theorem explainer
GrayCodeFacts packages the classical left-inverse, bound-preservation, and single-bit-flip properties of the binary-reflected Gray code for naturals below 2^64. Discrete mathematicians and implementers of combinatorial encodings cite these facts when discharging bit-manipulation lemmas. The declaration is a direct class definition that lists the five properties as fields, leaving verification to external references or future bitwise infrastructure.
Claim. A typeclass asserting the following for the binary-reflected Gray code map on natural numbers: the inverse operation recovers the original value from its encoded form for all inputs below $2^{64}$; the forward map recovers the encoded form from the inverse; the inverse map sends values below $2^d$ (with $d$ at most 64) to values below $2^d$; any $d$-bit pattern converts to an integer strictly less than $2^d$; and any two consecutive integers below $2^d$ have encodings differing in exactly one bit position.
background
The module declares well-known Gray code properties as a hypothesis interface pending full bitwise formalization. The binary-reflected Gray code uses the forward map that XORs a number with its right shift by one; the inverse applies cumulative XOR shifts. Pattern is the abbrev for a finite window of length $d$, represented as a function from Fin $d$ to Bool whose integer value is the sum of selected powers of two.
proof idea
The declaration is a class definition that enumerates the five properties as fields. Downstream theorems such as grayToNat_inverts_natToGray and gray_code_one_bit_property obtain their conclusions by direct projection from an instance of the class. No internal tactics or reductions occur; the module doc notes the blocker is missing bitwise induction lemmas for Nat.
why it matters
The class supplies the interface consumed by grayToNat and the inversion theorems inside GrayCodeAxioms, which in turn support brgcPath_injective in GrayCycleGeneral. It fills the documented combinatorial gap for pattern encodings while the module awaits bitwise formalization. The properties remain independent of the core forcing chain steps T5 through T8 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.