Encyclopedia Patterns Patterns Gray Cycle Brgc Brgc Path Injective

ARTICLE 4 claims 4 theorems

Patterns Gray Cycle Brgc Brgc Path Injective

A Gray code lists every binary pattern exactly once, changing one bit at a time; a machine-checked proof shows one standard construction never repeats itself.

Verify this page

The no-repeats guarantee

A Gray code is a way to order all binary strings of a given length so that consecutive strings differ in exactly one bit. The classic example for two bits runs 00, 01, 11, 10, then wraps back to 00, also a one-bit change. Engineers use such orderings in rotary encoders and error correction, where a single-bit step avoids the ambiguity of two bits changing at once. The standard recursive construction, the binary reflected Gray code, builds longer codes by taking a shorter code, adding a 0 to the front of each entry, then mirroring the list and adding a 1.

The key property of any Gray code is that it visits every pattern exactly once, with no repeats. For the binary reflected construction, this is known classically, but the Recognition Science library contains a machine-checked proof of it. The declaration brgcPath_injective establishes that the function generating the code is injective: two different positions in the sequence always produce two different patterns. The proof proceeds by induction, splitting the code into its two halves and showing each half is injective and the halves do not overlap. The result holds for every dimension d, including dimension zero, where the single empty pattern trivially satisfies the condition.

In Recognition Science, this injectivity result is part of a larger packaged claim. The library combines it with a separate theorem about one-bit adjacency to produce a Gray cycle, a complete ordered list of patterns that wraps around with a one-bit change from last to first. The injectivity proof is the no-repeats half of that package; the adjacency theorem is the one-bit-change half. Together they form a full Gray cycle for any positive dimension, and the injectivity alone also yields a Gray cover, meaning the sequence visits every possible pattern of that dimension.

The proof is axiom-free, meaning it relies only on the standard logical axioms of the machine-checked library, not on any Recognition Science specific postulates. It also avoids the common bitwise formula for Gray codes, gray(n) = n XOR (n >> 1), instead working directly from the recursive definition. This makes the result a clean, self-contained fact about a classical combinatorial object, available to any downstream argument that needs a repeat-free ordering of binary patterns.

THEOREM brgcPath_injective · IndisputableMonolith/Patterns/GrayCycleBRGC.lean
brgcPath_injective · IndisputableMonolith/Patterns/GrayCycleBRGC.lean:72 
theorem brgcPath_injective : ∀ d : Nat, Function.Injective (brgcPath d)
  | 0 => by
      intro i j _
      -- `Fin 1` is a subsingleton (only `0`)
      simpa [Fin.eq_zero i, Fin.eq_zero j]
  | (d + 1) => by
      intro i j hij
      -- unfold the `d+1` definition and reduce to injectivity of the appended halves
      classical
      let T : Nat := 2 ^ d
      have hTT : 2 ^ (d + 1) = T + T := by
        simpa [T, twoPow_succ_eq_add d]
      let left : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d k) false
      let right : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d (Fin.rev k)) true
      have hij' :
          Fin.append left right (i.cast hTT) = Fin.append left right (j.cast hTT) := by
        simpa [brgcPath, T, hTT, left, right] using hij

      have hleft_inj : Function.Injective left := by
        intro a b hab
        have hab' : brgcPath d a = brgcPath d b := by
          funext k
          have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab
          simpa [left, snocBit] using this
        exact (brgcPath_injective d) hab'

      have hright_inj : Function.Injective right := by
        intro a b hab
        have hab' : brgcPath d (Fin.rev a) = brgcPath d (Fin.rev b) := by
          funext k
          have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab
          simpa [right, snocBit] using this
        have : Fin.rev a = Fin.rev b := (brgcPath_injective d) hab'
        exact Fin.rev_injective this

      have hdis : ∀ a b : Fin T, left a ≠ right b := by
        intro a b hab
        have := congrArg (fun p : Pattern (d + 1) => p (Fin.last d)) hab
        -- last coordinate is the appended bit: false on left, true on right
        simpa [left, right] using this

      have happ_inj : Function.Injective (Fin.append left right) :=
        (Fin.append_injective_iff (xs := left) (ys := right)).2 ⟨hleft_inj, hright_inj, hdis⟩

      have hcast : i.cast hTT = j.cast hTT := happ_inj hij'
      -- cast back along the inverse equality
      have := congrArg (Fin.cast hTT.symm) hcast
      simpa [hTT] using this
THEOREM brgcGrayCycle · IndisputableMonolith/Patterns/GrayCycleBRGC.lean
brgcGrayCycle · IndisputableMonolith/Patterns/GrayCycleBRGC.lean:425 
noncomputable def brgcGrayCycle (d : Nat) (hdpos : 0 < d) : GrayCycle d :=
{ path := brgcPath d
  inj := brgcPath_injective d
  oneBit_step := brgc_oneBit_step (d := d) hdpos
}
THEOREM brgcGrayCover · IndisputableMonolith/Patterns/GrayCycleBRGC.lean
brgcGrayCover · IndisputableMonolith/Patterns/GrayCycleBRGC.lean:431 
noncomputable def brgcGrayCover (d : Nat) (hdpos : 0 < d) : GrayCover d (2 ^ d) :=
{ path := brgcPath d
  complete := by
    classical
    have h_inj : Function.Injective (brgcPath d) := brgcPath_injective d
    have h_card : Fintype.card (Fin (2 ^ d)) = Fintype.card (Pattern d) := by
      simp [Patterns.card_pattern]
    have h_bij : Function.Bijective (brgcPath d) :=
      (Fintype.bijective_iff_injective_and_card (brgcPath d)).2 ⟨h_inj, h_card⟩
    exact h_bij.2
  oneBit_step := brgc_oneBit_step (d := d) hdpos
}
THEOREM brgcPath_injective · IndisputableMonolith/Patterns/GrayCycleBRGC.lean
brgcPath_injective · IndisputableMonolith/Patterns/GrayCycleBRGC.lean:72 
theorem brgcPath_injective : ∀ d : Nat, Function.Injective (brgcPath d)
  | 0 => by
      intro i j _
      -- `Fin 1` is a subsingleton (only `0`)
      simpa [Fin.eq_zero i, Fin.eq_zero j]
  | (d + 1) => by
      intro i j hij
      -- unfold the `d+1` definition and reduce to injectivity of the appended halves
      classical
      let T : Nat := 2 ^ d
      have hTT : 2 ^ (d + 1) = T + T := by
        simpa [T, twoPow_succ_eq_add d]
      let left : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d k) false
      let right : Fin T → Pattern (d + 1) := fun k => snocBit (brgcPath d (Fin.rev k)) true
      have hij' :
          Fin.append left right (i.cast hTT) = Fin.append left right (j.cast hTT) := by
        simpa [brgcPath, T, hTT, left, right] using hij

      have hleft_inj : Function.Injective left := by
        intro a b hab
        have hab' : brgcPath d a = brgcPath d b := by
          funext k
          have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab
          simpa [left, snocBit] using this
        exact (brgcPath_injective d) hab'

      have hright_inj : Function.Injective right := by
        intro a b hab
        have hab' : brgcPath d (Fin.rev a) = brgcPath d (Fin.rev b) := by
          funext k
          have := congrArg (fun p : Pattern (d + 1) => p k.castSucc) hab
          simpa [right, snocBit] using this
        have : Fin.rev a = Fin.rev b := (brgcPath_injective d) hab'
        exact Fin.rev_injective this

      have hdis : ∀ a b : Fin T, left a ≠ right b := by
        intro a b hab
        have := congrArg (fun p : Pattern (d + 1) => p (Fin.last d)) hab
        -- last coordinate is the appended bit: false on left, true on right
        simpa [left, right] using this

      have happ_inj : Function.Injective (Fin.append left right) :=
        (Fin.append_injective_iff (xs := left) (ys := right)).2 ⟨hleft_inj, hright_inj, hdis⟩

      have hcast : i.cast hTT = j.cast hTT := happ_inj hij'
      -- cast back along the inverse equality
      have := congrArg (Fin.cast hTT.symm) hcast
      simpa [hTT] using this

What this page does not claim

The declaration does not prove that every possible Gray code is injective; it proves injectivity for this specific recursive construction. The declaration does not establish one-bit adjacency; that is a separate theorem in the same module. The proof does not use or depend on the bitwise formula gray(n) = n XOR (n >> 1).

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Patterns/GrayCycleBRGC.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND