GrayCodeFacts
plain-language theorem explainer
GrayCodeFacts packages five classical identities of the binary-reflected Gray code and its inverse as a single assumption class. Pattern theorists and combinatorial encoding work in the Recognition framework cite the envelope to invoke inversion, bound preservation, and single-bit adjacency without re-deriving them. The declaration is a class whose fields simply record the standard results from the discrete-mathematics literature.
Claim. Let $G(n)=n⊕(n≫1)$ be the binary-reflected Gray code map on natural numbers and let $G^{-1}$ denote its inverse (cumulative XOR). The class asserts: (i) $G^{-1}(G(n))=n$ whenever $n<2^{64}$; (ii) $G(G^{-1}(g))=g$ whenever $g<2^{64}$; (iii) $G^{-1}(g)<2^{d}$ whenever $g<2^{d}$ and $d≤64$; (iv) the integer value of any $d$-bit pattern is strictly less than $2^{d}$; (v) for any $n+1<2^{d}$ the codes $G(n)$ and $G(n+1)$ differ in exactly one bit position.
background
The module treats the binary-reflected Gray code as a standard combinatorial object whose forward map is $G(n)=n⊕(n≫1)$ and whose inverse is obtained by repeated right-shifts and XOR. Pattern is the type of finite binary windows of length $d$, imported from Measurement.Pattern as an abbreviation for PatternLayer.Pattern. The class GrayCodeFacts therefore supplies the five identities that are known to hold for these maps on bounded naturals but whose Lean proofs would require additional bitwise-induction infrastructure.
proof idea
The declaration is a class whose five fields are the axioms themselves; no proof term is supplied. Each downstream theorem simply projects the corresponding field (one-line wrapper).
why it matters
GrayCodeFacts supplies the classical Gray-code lemmas required by grayToNat, grayToNat_inverts_natToGray, natToGray_inverts_grayToNat, gray_code_one_bit_property and pattern_to_nat_bound. It therefore closes the formalization gap noted in the module documentation until full bitwise induction is available, while keeping the Recognition pattern layer free of unverified bit-manipulation claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.