Patterns Gray Cycle Gray Cycle3 Surjective

The 3-bit Gray cycle

A Gray code is a way to list all binary strings of a fixed length so that any two neighboring entries differ in exactly one bit. For three bits there are eight strings, and the classic order is 000, 001, 011, 010, 110, 111, 101, 100. The sequence wraps around: the last entry, 100, differs from the first, 000, in exactly one bit as well. This wrap-around property makes the list a cycle rather than just a path.

The machine-checked library of formal theorems proves that this eight-entry list visits every three-bit string exactly once. The declaration grayCycle3_surjective establishes that the list covers all eight possibilities, meaning no three-bit string is left out. A companion result proves the list has no repetitions, and together they show the list is a complete tour of the three-bit space. The proof is fully explicit: it checks each of the eight positions by direct computation, so no hidden assumptions or axioms are needed for this fact.

The ledger, a discrete record of events, uses such cycles to model how a system can pass through all its possible states while changing only one feature at a time. For three features, the eight-step cycle matches the framework's eight-tick recognition cycle, the unit of counting that the framework derives from its cost function. The Gray cycle gives a concrete, adjacency-respecting picture of that counting: not merely that eight states exist, but that they can be visited in a single closed loop of minimal steps.

What the declaration does not claim is broader than what it proves. It does not say that this cycle is unique, nor that it is the only way to order the eight states. It does not assert anything about cycles for other numbers of bits, though the same construction generalizes by the standard recursive method. And it does not connect the cycle to the framework's cost function or to the derivation of the eight-tick cycle; that connection remains a separate, unformalized step. The declaration is a precise combinatorial fact, and its value is in the exactness of the coverage it certifies.

theorem grayCycle3_surjective : Function.Surjective grayCycle3Path :=
  (grayCycle3_bijective).2

theorem grayCycle3_injective : Function.Injective grayCycle3Path := by
  intro i j hij
  have h0 : gray8At i = gray8At j := pattern3_injective (by simpa [grayCycle3Path] using hij)
  exact gray8At_injective h0

theorem grayCycle3_bijective : Function.Bijective grayCycle3Path := by
  classical
  -- card(Fin 8) = 8
  have hFin : Fintype.card (Fin 8) = 8 := by simp
  -- card(Pattern 3) = 2^3 = 8
  have hPat' : Fintype.card (Pattern 3) = 2 ^ 3 := by
    simpa using (Patterns.card_pattern 3)
  have hPow : (2 ^ 3 : Nat) = 8 := by decide
  have hPat : Fintype.card (Pattern 3) = 8 := by simpa [hPow] using hPat'
  have hcard : Fintype.card (Fin 8) = Fintype.card (Pattern 3) := by
    -- rewrite both sides to 8
    calc
      Fintype.card (Fin 8) = 8 := hFin
      _ = Fintype.card (Pattern 3) := by simpa [hPat]
  -- injective + card equality ⇒ bijective
  exact (Fintype.bijective_iff_injective_and_card grayCycle3Path).2 ⟨grayCycle3_injective, hcard⟩

/-- A rigorous Gray cycle for 3-bit patterns (the “8-tick” cycle). -/
def grayCycle3 : GrayCycle 3 :=
{ path := grayCycle3Path
, inj := grayCycle3_injective
, oneBit_step := grayCycle3_oneBit_step
}

What this page does not claim

The declaration does not prove that the Gray cycle is unique among all possible eight-step tours. It does not assert anything about cycles for bit lengths other than three. It does not connect the cycle to the framework's cost function or the derivation of the eight-tick cycle.

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/GrayCycle.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: