TuringBridgeCert
plain-language theorem explainer
TuringBridgeCert bundles four components into a single certificate for the R-hat to Turing-machine complexity bridge. It records the faithful SAT-to-J-cost encoding, the non-natural character of the R-hat certificate, the linear size of the landscape, and the explicit identification of the remaining open gap. Complexity theorists working on P versus NP via recognition operators would cite this structure as the current status summary. The definition is assembled directly from the four referenced facts with no additional reasoning steps.
Claim. A certificate consisting of (i) the statement that a J-cost landscape has minimum cost zero precisely when its encoded SAT instance is satisfiable, (ii) a certificate asserting that the R-hat operator acts on the full lattice and is not a natural property, (iii) the inequality $n + m ≥ n$ for any SAT instance with $n$ variables and $m$ clauses, and (iv) an OpenGap record marking the simulation-cost overhead from lattice minimization to Turing-tape steps as unknown.
background
JCostLandscape is the structure that attaches a SATInstance to a landscape whose size is $n + m$ and whose minimum cost is zero exactly when the instance is satisfiable. RHatCertificate records that the recognition operator operates on the full Z³ lattice rather than on polynomial-size circuits and is therefore not a natural property in the Razborov-Rudich sense. SATInstance simply packages positive integers $n$ and $m$ for the number of variables and clauses. OpenGap is the stub that flags the missing translation from spectral-gap convergence (O(1/λ₂) octaves) to Turing-machine steps.
proof idea
The declaration is a bare structure definition whose four fields are populated by direct reference to the sibling facts encoding_faithful, rhat_is_non_natural, landscape_linear, and the_open_gap. No tactics or reductions are applied; the construction is a one-line wrapper that merely assembles the already-proved or already-stated components.
why it matters
The structure supplies the single object consumed by turingBridgeCert, which in turn is the top-level summary of the P-vs-NP bridge described in the module documentation. It records the three established pieces (faithful encoding, non-naturality, linear size) while explicitly naming the open spectral-to-Turing translation gap that remains after the contractivity results. The surrounding framework treats R-hat minimization on Z³ as the native recognition step whose polynomial versus superpolynomial cost would decide P = NP once the tape-simulation overhead is bounded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.