def definition def or abbrev

`OneBitDiff`

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

formal statement (Lean)

  37def OneBitDiff {d : Nat} (p q : Pattern d) : Prop :=

Definition body.

  38  ∃! k : Fin d, p k ≠ q k
  39

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

coordAtomicStep_oneBitDiff in IndisputableMonolith.LedgerParityAdjacency decl_use
ledgerVecStep_oneBitDiff in IndisputableMonolith.LedgerParityAdjacency decl_use
legalAtomicTick_oneBitDiff in IndisputableMonolith.LedgerPostingAdjacency decl_use
parity_oneBitDiff_of_post in IndisputableMonolith.LedgerPostingAdjacency decl_use
postingStep_oneBitDiff in IndisputableMonolith.LedgerPostingAdjacency decl_use
run_step_oneBitDiff in IndisputableMonolith.LedgerPostingAdjacency decl_use
stepAt_oneBitDiff in IndisputableMonolith.LedgerPostingAdjacency decl_use
GrayCover in IndisputableMonolith.Patterns.GrayCycle decl_use
GrayCycle in IndisputableMonolith.Patterns.GrayCycle decl_use
grayCycle3_oneBit_step in IndisputableMonolith.Patterns.GrayCycle decl_use
OneBitDiff_symm in IndisputableMonolith.Patterns.GrayCycle decl_use
brgc_oneBit_step in IndisputableMonolith.Patterns.GrayCycleBRGC decl_use
oneBitDiff_snocBit_flip in IndisputableMonolith.Patterns.GrayCycleBRGC decl_use
oneBitDiff_snocBit_same in IndisputableMonolith.Patterns.GrayCycleBRGC decl_use
brgc_oneBit_step in IndisputableMonolith.Patterns.GrayCycleGeneral decl_use
brgc_wrap_oneBitDiff in IndisputableMonolith.Patterns.GrayCycleGeneral decl_use

Lean names referenced from this declaration's body.