inductive
definition
CellState
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Complexity.CellularAutomata on GitHub at line 37.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
34/-! ## CA Cell State -/
35
36/-- Cell states for the Boolean CA -/
37inductive CellState
38 | Zero -- Boolean 0
39 | One -- Boolean 1
40 | Signal -- Propagating signal
41 | Gate -- AND/OR/NOT gate marker
42 | Wire -- Passive wire
43 | Blank -- Empty cell
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) }