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

IndisputableMonolith.Complexity.TuringBridge

show as:
view Lean formalization →

The TuringBridge module introduces SAT instances and their mapping to J-cost structures inside the Recognition Science framework. It defines SATInstance with n variables and m clauses, plus supporting objects such as JCostLandscape, ResolutionTime, and RHatCertificate. Complexity researchers would cite these to encode classical decision problems into the J-cost formalism. The module contains only definitions and basic relations, with no theorems or proofs.

claimAn SAT instance is a pair $(n, m)$ of positive integers together with a collection of $m$ clauses over $n$ boolean variables, written $SATInstance(n,m)$. The associated J-cost landscape is the function $JCostLandscape : SATInstance(n,m) → ℝ$ that assigns to each assignment its total J-cost.

background

The module sits in the Complexity domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the core J-cost definitions from JcostCore. It introduces SATInstance as the basic object for encoding satisfiability problems, JCostLandscape as the cost surface over the 2^n assignments, ResolutionTime as the number of ticks needed to reach a satisfying assignment, and auxiliary notions such as NaturalProperty and RHatCertificate. These objects prepare the ground for relating classical NP questions to the J-uniqueness and phi-ladder structures of Recognition Science.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the encoding layer that later results on separation claims, open gaps, and TuringBridgeCert rely upon. It translates SAT instances into the J-cost language so that downstream arguments can invoke the Recognition Composition Law and the eight-tick octave without leaving the RS-native setting. No parent theorems are listed in the dependency graph, yet the definitions close the interface between classical complexity and the forcing chain T0–T8.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)