def
definition
Window
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.CellularAutomata on GitHub at line 50.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
78 -- AND gate: both inputs must be One
79 | .One, .Gate, .One => .One
80 | .One, .Gate, .Zero => .Zero