pith. sign in
module module low

IndisputableMonolith.Complexity.CellularAutomata

show as:
view Lean formalization →

This module defines core structures for Boolean cellular automata including cell states, tapes, neighborhoods and local rules as part of an exploratory complexity model. Researchers studying discrete dynamical systems or ledger-based dual complexity would reference these definitions. The module consists entirely of type and function definitions with no theorems or proofs.

claimCellState := {0,1}; Tape := ℤ → CellState; Neighborhood := finite window of radius r; localRule : Neighborhood → CellState; step : Tape → Tape applies the rule synchronously.

background

The module sits inside the Complexity domain and imports the ComputationBridge scaffold. That upstream file explicitly states it is a SCAFFOLD MODULE — NOT PART OF CERTIFICATE CHAIN and explores a hypothetical P vs NP resolution framework based on ledger-style dual complexity (computation vs recognition). The present module supplies the concrete Boolean CA objects (CellState, Tape, Window, Neighborhood, extractNeighborhood, localRule, step, ca_is_local, dependency_cone, ClauseGadget) needed to instantiate such models.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the cellular-automaton substrate for the hypothetical dual-complexity framework described in ComputationBridge. No parent theorems in the verified certificate chain (UltimateClosure, CPMClosureCert, etc.) are fed by it; the connection remains exploratory.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (23)