def
definition
binaryReflectedGray
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Patterns.GrayCode on GitHub at line 34.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
31
32/-- Binary-reflected Gray code as a function from Fin (2^d) to Pattern d
33 We use the standard bit-extraction to convert Gray code to pattern -/
34def binaryReflectedGray (d : ℕ) (i : Fin (2^d)) : Pattern d :=
35 fun j => (natToGray i.val).testBit j.val
36
37/-- Inverse Gray code: converts Gray code back to binary -/
38def grayToNat (g : ℕ) : ℕ :=
39 -- Inverse Gray code: repeatedly XOR with shifted versions
40 -- g XOR (g >> 1) XOR (g >> 2) XOR ...
41 -- For bounded values, this terminates
42 let rec aux (shift : ℕ) (acc : ℕ) (fuel : ℕ) : ℕ :=
43 match fuel with
44 | 0 => acc
45 | fuel' + 1 =>
46 let shifted := g >>> shift
47 if shifted = 0 then acc
48 else aux (shift + 1) (acc ^^^ shifted) fuel'
49 aux 0 0 64 -- 64 shifts is enough for any practical number
50
51-- Properties and classical results are provided via
52-- `IndisputableMonolith.Patterns.GrayCodeAxioms.GrayCodeFacts`.
53-- This module remains axiom-free and parametric over those facts.
54
55end Patterns
56end IndisputableMonolith