module module

`IndisputableMonolith.Complexity.CellularAutomata`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Complexity.ComputationBridge module_import

declarations in this module (23)

inductive CellState L37
def Tape L47
def Window L50
def radius L55
structure Neighborhood L58
def extractNeighborhood L64
def localRule L70
def step L95
theorem ca_is_local L101
theorem ca_k_local L105
theorem dependency_cone L108
structure ClauseGadget L132
def encodeClause L143
structure SATGadget L157
def sat_eval_time L172
def H_SATCARuntime L185
structure TMSimulator L195
def tm_simulation_time L204
theorem tm_simulation_bound L208
def H_SATTMRuntime L218
theorem sat_computation_time L233
theorem sat_recognition_time L245
theorem computation_recognition_separation L260