GrayCodeFacts
GrayCodeFacts packages five standard properties of the binary-reflected Gray code into one hypothesis class for the Patterns layer. Discrete mathematicians and Recognition Science users working on combinatorial encodings cite it to access inversion, bound preservation, and single-bit transition facts. The declaration is a direct class definition that states the properties as fields, with justification drawn from external literature rather than an internal proof.
claimThe class asserts: the cumulative-XOR inverse satisfies $grayInverse(n XOR (n >> 1)) = n$ for all $n < 2^{64}$; the forward map inverts the inverse for all $g < 2^{64}$; $grayInverse(g) < 2^d$ whenever $g < 2^d$ and $d ≤ 64$; the integer value of any $d$-bit pattern is strictly less than $2^d$; and consecutive Gray codes differ in exactly one bit position.
background
The GrayCodeFacts class acts as a hypothesis envelope for classical Gray code properties inside the Patterns.GrayCodeAxioms module. The binary-reflected Gray code is the map $n ↦ n XOR (n >> 1)$, with its inverse recovered by cumulative XOR shifts. Pattern is the abbreviation PatternLayer.Pattern $n$ from the Measurement module, representing finite bit windows of length $n$.
proof idea
The declaration is a class definition whose body consists of five field declarations. Each field states a quantified property directly; no Lean tactics or upstream lemmas are invoked inside the definition. Justification rests on the external references to Knuth and Savage supplied in the module documentation.
why it matters in Recognition Science
GrayCodeFacts supplies the combinatorial facts required by eight downstream declarations, including grayToNat, gray_code_one_bit_property, grayToNat_inverts_natToGray, and pattern_to_nat_bound. It implements the classical results cited in the module documentation to Savage (1997) and Knuth (2011). In the Recognition framework it supports pattern encoding for eight-tick octave structures, though it lies outside the core T0-T8 forcing chain.
scope and limits
- Does not derive Gray code inversion from the Recognition Composition Law.
- Does not verify the properties for bit widths exceeding 64.
- Does not supply a constructive algorithm for the inverse beyond the stated bounds.
- Does not connect the one-bit property to Berry creation thresholds or Z_cf values.
formal statement (Lean)
49class GrayCodeFacts where
50 grayToNat_inverts_natToGray :
51 ∀ n : ℕ, n < 2^64 → grayInverse (n ^^^ (n >>> 1)) = n
52 natToGray_inverts_grayToNat :
53 ∀ g : ℕ, g < 2^64 →
54 let n := grayInverse g
proof body
Definition body.
55 n ^^^ (n >>> 1) = g
56 grayToNat_preserves_bound :
57 ∀ g d : ℕ, g < 2^d → d ≤ 64 → grayInverse g < 2^d
58 pattern_to_nat_bound :
59 ∀ (d : ℕ) (p : Pattern d),
60 (∑ k : Fin d, if p k then 2^(k.val) else 0) < 2^d
61 gray_code_one_bit_property :
62 ∀ (d n : ℕ), n + 1 < 2^d →
63 ∃! k : ℕ, k < d ∧
64 ((n ^^^ (n >>> 1)).testBit k ≠ ((n+1) ^^^ ((n+1) >>> 1)).testBit k)
65
66variable [GrayCodeFacts]
67
68/-- **Classical Result**: Gray code inverse is a left inverse.
69
70The inverse Gray code operation (cumulative XOR) correctly inverts the forward
71Gray code transformation.
72
73**Proof**: Induction on bit positions with XOR algebra
74
75**References**:
76- Knuth (2011), Exercise 7.2.1.1.4
77- Savage (1997), Section 2.1
78
79**Formalization Blocker**: Requires bitwise induction infrastructure for Nat
80
81**Status**: Standard result in discrete mathematics
82-/