def definition def or abbrev

`natToGray`

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

formal statement (Lean)

  30def natToGray (n : ℕ) : ℕ := n ^^^ (n >>> 1)

proof body

Definition body.

  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 -/

used by (6)

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

binaryReflectedGray in IndisputableMonolith.Patterns.GrayCode decl_use
grayToNat_inverts_natToGray in IndisputableMonolith.Patterns.GrayCodeAxioms decl_use
brgc_oneBit_step in IndisputableMonolith.Patterns.GrayCycleGeneral decl_use
brgcPath_injective in IndisputableMonolith.Patterns.GrayCycleGeneral decl_use
brgc_wrap_oneBitDiff in IndisputableMonolith.Patterns.GrayCycleGeneral decl_use
natToGray_testBit_false_of_ge in IndisputableMonolith.Patterns.GrayCycleGeneral decl_use

depends on (6)

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
Pattern in IndisputableMonolith.Measurement decl_use
Pattern in IndisputableMonolith.Patterns decl_use
Pattern in IndisputableMonolith.Streams decl_use
Pattern in IndisputableMonolith.Streams.Blocks decl_use