natToGray_inverts_grayToNat
plain-language theorem explainer
The declaration establishes that the forward binary-reflected Gray code map inverts the inverse Gray code operation for every input below 2^64. Discrete mathematicians and hardware designers working with bit-reversal encodings would cite this left-inverse property when verifying round-trip correctness. The proof is a one-line term that directly invokes the corresponding field of the GrayCodeFacts class.
Claim. For every natural number $g$ satisfying $g < 2^{64}$, if $n$ denotes the inverse Gray code of $g$, then $n$ XOR $(n$ right-shifted by 1$)$ equals $g$.
background
The module declares standard properties of the binary-reflected Gray code as axioms pending complete bitwise formalization. The inverse operation grayInverse recovers the original binary integer by repeated XOR with successive right shifts of the input. GrayCodeFacts is the class that bundles the two inversion statements together with the bound-preservation lemma.
proof idea
The proof is a direct term-mode reference to the natToGray_inverts_grayToNat field of the GrayCodeFacts class.
why it matters
This supplies the left-inverse half of the pair required by the GrayCodeFacts class, which the module uses to support pattern-to-natural-number conversions and bound checks. It implements the classical bijectivity step described in the module documentation on Gray code properties. The result leaves open the question of discharging the axiom class with fully verified bitwise lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.