`Tape`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.CellularAutomata
domain: Complexity
line: 47 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Complexity.CellularAutomata on GitHub at line 47.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  44  deriving DecidableEq, Repr
  45
  46/-- The CA tape is an infinite sequence of cells, but we work with finite windows -/
  47def Tape := ℤ → CellState
  48
  49/-- Finite window of a tape -/
  50def Window (n : ℕ) := Fin n → CellState
  51
  52/-! ## Local Update Rules -/
  53
  54/-- Neighborhood radius for the CA -/
  55def radius : ℕ := 1
  56
  57/-- Local neighborhood: cells at positions i-1, i, i+1 -/
  58structure Neighborhood where
  59  left   : CellState
  60  center : CellState
  61  right  : CellState
  62
  63/-- Extract neighborhood from tape at position i -/
  64noncomputable def extractNeighborhood (tape : Tape) (i : ℤ) : Neighborhood :=
  65  { left := tape (i - 1)
  66  , center := tape i
  67  , right := tape (i + 1) }
  68
  69/-- The local update rule -/
  70def localRule (n : Neighborhood) : CellState :=
  71  match n.left, n.center, n.right with
  72  -- Signal propagation: Signal moves right
  73  | _, .Signal, .Wire => .Signal
  74  | _, .Signal, .Blank => .Signal
  75  -- Wire carries signal
  76  | .Signal, .Wire, _ => .Signal
  77  | .Signal, .Blank, _ => .Blank  -- Signal consumed

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.