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

IndisputableMonolith.Complexity.ComputationBridge

show as:
view Lean formalization →

The ComputationBridge module defines recognition-complete complexity via dual parameters Tc and Tr. Researchers addressing the P versus NP question inside Recognition Science would cite it when connecting vertex-cover instances to cellular-automaton simulations. The module assembles five imported submodules to supply the required bridge definitions without internal theorems.

claimDual complexity parameters $T_c$ (computational time) and $T_r$ (recognition time) for recognition-complete problems, obtained by mapping RS constraints to vertex-cover edges.

background

The module resides in the Complexity domain and imports VertexCover, which treats complexity as a pair of functions of input size, and RSVC, which maps an RS constraint instance to a set of edges that must be covered. BalancedParityHidden supplies the parity gadget, while LedgerUnits contributes the subgroup of integers generated by a fixed delta specialized to delta equals 1. Core.Recognition supplies the underlying recognition framework whose J-cost and defect measures are used to label the complexity parameters.

proof idea

This is a definition module with no proofs. It structures the argument solely by importing BalancedParityHidden, RSVC, VertexCover, Core.Recognition, and LedgerUnits, thereby exposing the dual parameters Tc and Tr for use in downstream constructions.

why it matters in Recognition Science

The module feeds the CellularAutomata module, which constructs local gadgets for Boolean operations and establishes that SAT evaluation runs in O(n to the 1/3 log n) time under a cellular-automaton simulation. It therefore supplies the complexity bridge required for the Recognition Science resolution of P versus NP.

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)