localRule

formal source

  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
  89  | .Signal, .Zero, _ => .One
  90  | .Signal, .One, _ => .Zero
  91  -- Default: preserve state
  92  | _, c, _ => c
  93
  94/-- Apply local rule globally to create successor tape -/
  95noncomputable def step (tape : Tape) : Tape :=
  96  fun i => localRule (extractNeighborhood tape i)
  97
  98/-! ## Locality Proof -/
  99
 100/-- The CA is local: each cell depends only on its radius-1 neighborhood -/