grayToNat_preserves_bound
plain-language theorem explainer
The declaration states that Gray code to natural conversion preserves the d-bit bound: for natural numbers g and d, g less than 2 to the d and d at most 64 together imply that the decoded value grayInverse g is also less than 2 to the d. Pattern modelers in Recognition Science cite the bound when embedding combinatorial objects into discrete ladders or spectral counts. The proof is a one-line term that directly applies the corresponding field from the GrayCodeFacts hypothesis class.
Claim. For all natural numbers $g$ and $d$, if $g < 2^d$ and $d ≤ 64$, then the Gray-code inverse satisfies grayInverse($g$) < $2^d$.
background
The module Patterns.GrayCodeAxioms registers standard combinatorial facts about binary-reflected Gray codes as axioms while a full bitwise Lean development remains pending. The binary-reflected Gray code maps a natural n to n XOR (n right-shift 1); its inverse recovers n by successive XORs of right-shifts. The local setting treats these maps as elementary discrete objects whose published proofs (Savage 1997, Knuth Vol. 4A) and numerical checks already suffice for the Recognition Science pattern layer.
proof idea
The proof is a one-line term that invokes the grayToNat_preserves_bound field of the GrayCodeFacts class. This delegates the bound preservation to the hypothesis envelope that collects the elementary bitwise properties.
why it matters
The result supplies one of the bounding facts required by the GrayCodeFacts class, the hypothesis envelope that collects all classical Gray-code properties for the Patterns module. It is referenced by GrayCodeFacts itself and by the sibling pattern_to_nat_bound. In the Recognition framework the bound anchors discrete pattern manipulations that later feed the eight-tick octave and phi-ladder constructions, although the lemma itself remains a classical import rather than a derived Recognition Science statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.