pith. sign in
module module high

IndisputableMonolith.Complexity.ComputationBridge

show as:
view Lean formalization →

ComputationBridge introduces dual complexity parameters Tc and Tr to characterize recognition-complete problems. Researchers resolving P versus NP via Recognition Science cite it to link RS constraints with vertex cover instances. The module assembles imported definitions from VertexCover, RSVC, and Recognition without internal theorems.

claimRecognition-complete complexity is characterized by the dual parameters $T_c$ and $T_r$.

background

The module sits in the Complexity domain. It imports VertexCover, which supplies complexity pairs as functions of input size, and RSVC, which maps RS constraint instances to edges to be covered. LedgerUnits provides the subgroup of integers generated by delta, specialized to delta equals 1 for an order isomorphism, while Core.Recognition supplies the underlying recognition structures.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the dual parameters Tc and Tr that feed CellularAutomata. That module constructs local gadgets for Boolean operations and shows SAT evaluation by cellular automata runs in O(n to the 1/3 log n) time, advancing the P versus NP resolution.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (14)