pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Complexity.SAT.Runtime

show as:
view Lean formalization →

This module supplies abstract runtime parameters for cellular automaton embeddings within the Recognition Science complexity layer. Researchers analyzing CA-to-TM simulation overheads or 3-SAT reductions cite it to fix the interface before concrete bounds are derived. It introduces parameters such as logical depth and time bounds that later sibling declarations instantiate for specific models.

claimThe module defines abstract runtime parameters $CARuntime(n)$ and $CARuntimeModel$ together with functions $logicalDepth$ and $caTimeBound$ for cellular-automaton embeddings of computational problems.

background

Recognition Science treats cellular automata as an intermediate layer between the J-cost functional equation and discrete computational models. This module supplies the abstract runtime interface for CA embeddings, including the logical depth of a configuration and the time bound required for a CA to simulate a target machine. It sits above the single Mathlib import and below the concrete propositions ca_to_tm_simulation_prop and three_sat_runtime_prop that appear as siblings.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the parameter interface required by the sibling declarations ca_to_tm_simulation_prop and three_sat_runtime_prop, which establish simulation properties and runtime bounds for 3-SAT. It therefore occupies the position of the abstract layer that must be fixed before any concrete complexity claim in the Recognition Science monolith can be stated.

scope and limits

declarations in this module (6)