conditional_separation
plain-language theorem explainer
Conditional separation establishes that under the SpectralTuringBridgeHypothesis any Turing-machine simulation of recognition-based SAT solving incurs quadratic time while the recognition process itself converges in linear steps. Complexity researchers working on the P versus NP question inside Recognition Science would cite this when quantifying simulation overhead between local circuits and global J-cost gradients. The proof extracts the respective bounds directly from the hypothesis fields via obtains and exact packaging.
Claim. Assuming the SpectralTuringBridgeHypothesis (positive spectral gap for the SAT J-cost Laplacian, $O(n)$ convergence of $R̂$, and $Ω(n)$ TM tape operations per recognition step) together with the CircuitSeparation structure, for every natural number $n$ there exist natural numbers $T_{TM}$ and $T_R$ such that $T_{TM} ≥ n · (n/2)$ and $T_R ≤ n + 1$.
background
The module treats Boolean circuits as feed-forward sub-ledgers lacking global J-cost coupling across the full Z³ lattice; each gate sees only O(1) parents, so Z-capacity is bounded by twice the gate count. CircuitSeparation supplies three proved pieces: R̂ reaches zero satJCost in ≤ n steps on satisfiable formulas, UNSAT formulas carry a defect moat of width ≥ 1, and no fixed-view decoder over fewer than n variables can certify the moat. SpectralTuringBridgeHypothesis is the open-gap structure whose fields encode the spectral gap positivity, the rhat_convergence bound T_R ≤ n + 1, and the simulation_cost_per_step lower bound that produces the TM time claim.
proof idea
Term-mode proof: introduce n, obtain T_TM and its inequality from the tm_time_lower_bound field of the supplied bridge hypothesis, obtain T_R and its inequality from the rhat_convergence field of the same hypothesis, then return the triple with exact.
why it matters
The declaration packages the simulation-overhead consequence of the SpectralTuringBridgeHypothesis, thereby populating the CircuitLedgerCert bundle and completing one concrete step in the module’s four-stage reduction of the P versus NP gap to circuit versus global-gradient reach. It directly implements the doc-comment claim that TM time is Ω(n²) while R̂ needs only O(n) steps, and it isolates the remaining open piece (spectral gap positivity and the precise Ω(n) per-step cost) that would turn the conditional separation into an unconditional result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.