IndisputableMonolith.Patterns.GrayCode

   1import Mathlib
   2import IndisputableMonolith.Patterns
   3import IndisputableMonolith.Patterns.GrayCodeAxioms
   4
   5/-!
   6# Binary-Reflected Gray Code
   7
   8This module provides the binary-reflected Gray code construction.
   9This is a well-known algorithm that generates a Hamiltonian cycle on the
  10d-dimensional hypercube Q_d.
  11
  12The construction uses the recursive definition:
  13- BRGC(0) = [0]
  14- BRGC(n+1) = [0·BRGC(n), 1·BRGC(n)ʳ]
  15  where x·L prepends bit x to each pattern in list L, and Lʳ is L reversed
  16
  17The key properties:
  181. It visits all 2^d vertices exactly once
  192. Consecutive entries differ in exactly one bit
  203. The first and last entries also differ in exactly one bit (forming a cycle)
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Patterns
  25
  26open Function
  27
  28/-- Convert a natural number to its Gray code representation
  29    The standard formula: gray(n) = n XOR (n >> 1) -/
  30def natToGray (n : ℕ) : ℕ := n ^^^ (n >>> 1)
  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
  57