pith. sign in
module module moderate

IndisputableMonolith.Complexity.CellularAutomata

show as:
view Lean formalization →

This module defines the core objects for Boolean cellular automata including cell states, tapes, neighborhoods and local evolution rules. It supports exploratory work on dual complexity measures in the Complexity domain. The module contains only definitions and basic properties with no theorems or proofs.

claimLet $CellState$ denote the Boolean type. A $Tape$ is a map $\mathbb{Z} \to CellState$. For radius $r$, a $Neighborhood$ is the local window extracted from a tape; $localRule$ maps neighborhoods to cell states and $step$ evolves the tape under that rule. Properties such as locality of the rule and dependency cones are recorded.

background

The module resides in the Complexity domain and imports Mathlib together with ComputationBridge. The upstream ComputationBridge module is explicitly marked as a scaffold that explores a hypothetical ledger-style dual complexity framework for P versus NP; it lies outside the verified certificate chain. The definitions introduced here supply the concrete cellular-automaton substrate (CellState, Tape, Window, Neighborhood, extractNeighborhood, localRule, step, ca_is_local, dependency_cone, ClauseGadget) on which that scaffold can be exercised.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the cellular-automaton vocabulary required by the scaffold explorations in ComputationBridge. It feeds no parent theorems in the verified chain (used_by count is zero) and does not close any step in the T0-T8 forcing chain or the Recognition Composition Law. It touches the open question of whether local CA rules can be related to recognition cost without leaving the scaffold layer.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (23)