IndisputableMonolith.Complexity.CellularAutomata
This module introduces the core data structures for Boolean cellular automata, including cell states, tapes, neighborhoods, and local evolution rules. It supports exploratory work on computational complexity in Recognition Science. Researchers examining local rule systems or dual complexity measures would reference these definitions. The module contains only definitions and no proofs.
claimDefines CellState as the set {0,1}, Tape as maps from integers to CellState, Window and Neighborhood as local extracts of radius r, extractNeighborhood as the map from Tape and position to Neighborhood, localRule as a function from Neighborhood to CellState, and step as the global evolution map on Tape.
background
The module sits in the Complexity domain and supplies discrete dynamical systems with strictly local update rules. It introduces CellState for binary cell values, Tape for the configuration space, Neighborhood for dependency cones of finite radius, and the functions extractNeighborhood, localRule, and step that implement one-step evolution. It imports the ComputationBridge module, whose documentation states it explores a hypothetical P versus NP resolution framework based on ledger-style dual complexity separating computation from recognition and lies outside the verified certificate chain.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The structures supply the cellular automata primitives that support the exploratory P versus NP analysis in the ComputationBridge module. They contribute to Recognition Science complexity investigations by furnishing a concrete local-computation model, though they remain disconnected from the main certificate chain such as UltimateClosure or CPMClosureCert.
scope and limits
- Does not contain theorems or proofs.
- Does not connect to the verified certificate chain.
- Does not simulate specific automata or compute invariants.
- Does not reference the phi-ladder, forcing chain, or physical constants.
depends on (1)
declarations in this module (23)
-
inductive
CellState -
def
Tape -
def
Window -
def
radius -
structure
Neighborhood -
def
extractNeighborhood -
def
localRule -
def
step -
theorem
ca_is_local -
theorem
ca_k_local -
theorem
dependency_cone -
structure
ClauseGadget -
def
encodeClause -
structure
SATGadget -
def
sat_eval_time -
def
H_SATCARuntime -
structure
TMSimulator -
def
tm_simulation_time -
theorem
tm_simulation_bound -
def
H_SATTMRuntime -
theorem
sat_computation_time -
theorem
sat_recognition_time -
theorem
computation_recognition_separation