pith. machine review for the scientific record. sign in
structure definition def or abbrev

GrayCycle

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  53structure GrayCycle (d : Nat) where
  54  /-- Phase-indexed path through patterns (period is fixed to `2^d`). -/
  55  path : Fin (2 ^ d) → Pattern d
  56  /-- No repeats (Hamiltonian cycle candidate). -/
  57  inj : Function.Injective path
  58  /-- Consecutive phases differ in exactly one bit (with wrap-around). -/
  59  oneBit_step : ∀ i : Fin (2 ^ d), OneBitDiff (path i) (path (i + 1))
  60
  61/-- A Gray *cover* with an arbitrary period `T`: adjacency (one-bit steps) plus coverage (surjection). -/

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (22)

Lean names referenced from this declaration's body.