Neighborhood

formal source

  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
  78  -- AND gate: both inputs must be One
  79  | .One, .Gate, .One => .One
  80  | .One, .Gate, .Zero => .Zero
  81  | .Zero, .Gate, .One => .Zero
  82  | .Zero, .Gate, .Zero => .Zero
  83  -- OR gate: either input is One
  84  | .One, .Wire, .One => .One
  85  | .One, .Wire, .Zero => .One
  86  | .Zero, .Wire, .One => .One
  87  | .Zero, .Wire, .Zero => .Zero
  88  -- NOT gate: invert center when activated