IndisputableMonolith.Complexity.ComputationBridge
The ComputationBridge module defines dual complexity parameters Tc and Tr that mark recognition-complete problems. It assembles constraints from RSVC edge coverings and VertexCover pairs into a single bridge object. Researchers building cellular automata for SAT evaluation cite this module to link recognition costs to computation time. The module itself contains only definitions and imports, with no internal proofs.
claimDual complexity parameters \(T_c\) and \(T_r\) for recognition-complete instances, where \(T_c\) tracks computational cost and \(T_r\) tracks recognition cost on vertex-cover pairs derived from RS constraint edges.
background
The module operates inside the Complexity domain and imports five supporting modules. VertexCover supplies complexity pairs expressed as functions of input size. RSVC maps an RS constraint instance onto a set of edges that must be covered. LedgerUnits supplies the subgroup of (\mathbb{Z}) generated by (\delta), specialized to (\delta=1) for an order isomorphism. BalancedParityHidden and Core.Recognition supply the remaining recognition primitives. The DOC_COMMENT states the module's purpose as recognition-complete complexity via the pair ((T_c, T_r)).
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the dual parameters required by the downstream CellularAutomata module. That module constructs local CA gadgets for Boolean operations, proves that SAT evaluates under local rules, and obtains the time bound (O(n^{1/3} \log n)) while preserving the bound under TM simulation. The bridge therefore closes the recognition-to-computation link needed for the P-versus-NP argument inside the Recognition framework.
scope and limits
- Does not contain theorem declarations or Lean proofs.
- Does not implement algorithms or run simulations.
- Does not reference phi-ladder mass formulas or the eight-tick octave.
- Does not resolve P versus NP; only supplies the complexity bridge.
- Does not define numerical constants or alpha-band bounds.
used by (1)
depends on (5)
declarations in this module (14)
-
structure
RecognitionComplete -
structure
TuringModel -
structure
LedgerComputation -
structure
SATLedger -
structure
RecognitionScenario -
def
demoRecognitionScenario -
theorem
Turing_incomplete -
theorem
P_vs_NP_resolved -
structure
ClayBridge -
theorem
clay_bridge_theorem -
theorem
ledger_forces_separation -
structure
Validation -
structure
CompleteModel -
theorem
main_resolution