pith. machine review for the scientific record. sign in
theorem proved term proof high

dissolution_holds

show as:
view Lean formalization →

The dissolution_holds theorem verifies the three axioms of the RS dissolution structure for the P versus NP problem by confirming polynomial recognition time for SAT instances, a positive J-cost obstruction for UNSAT formulas, and local blindness under partial decoders. Complexity researchers working in the Recognition Science framework cite it for the unconditional dissolution route that separates recognition measures from Turing-machine simulation. The proof is a direct term-mode assembly that supplies each field of the target structure from

claimThe dissolution theorem asserts that for every natural number $n$ and CNF formula $f$ on $n$ variables, if $f$ is satisfiable then there exist steps $s$ and assignment $a$ with $s$ at most $n$ and satJCost$(f,a)=0$; if $f$ is unsatisfiable then satJCost$(f,a)$ is at least 1 for every assignment $a$; and for every proper subset $M$ of the $n$ variables and every decoder from the restricted domain to Bool, there exist a hidden bit $b$ and full assignment $R$ such that the decoder disagrees with $b$ on the balanced-parity encoding of $b$ and $R$.

background

In the P vs NP Assembly module the dissolution path supplies an unconditional argument that the classical P versus NP question conflates two distinct complexity measures. The central definitions are satJCost, the natural-number length of unsatisfied clauses after recognition, and the recognition time bound that counts steps until zero J-cost is reached. The structure PvsNPDissolution packages three properties: polynomial-time recognition for satisfiable formulas, a strict positive lower bound on J-cost for unsatisfiable formulas, and local blindness for any decoder that sees only a proper subset of variables.

proof idea

The proof is a term-mode construction that directly populates the three fields of PvsNPDissolution. The rhat_polytime field invokes sat_recognition_time_bound to extract the witness steps and assignment. The unsat_obstruction field applies unsat_cost_lower_bound to obtain the positive J-cost guarantee. The local_blindness field delegates to BalancedParityHidden.adversarial_failure on the given subset and decoder.

why it matters in Recognition Science

This theorem completes the unconditional dissolution path inside the P vs NP assembly and supplies the missing piece for the master certificate pvsNPMasterCert. It realizes the RS claim that recognition time for SAT is linear while Turing-machine simulation incurs structural overhead, thereby dissolving the classical question rather than resolving it via circuit lower bounds. The result sits downstream of the recognition-time and J-cost bounds and upstream of any global complexity certificate that invokes the dissolution route.

scope and limits

formal statement (Lean)

  75theorem dissolution_holds : PvsNPDissolution where
  76  rhat_polytime := fun n f h =>

proof body

Term-mode proof.

  77    let ⟨steps, a, hle, ha⟩ := sat_recognition_time_bound f h
  78    ⟨steps, a, hle, ha⟩
  79  unsat_obstruction := fun _n f h => unsat_cost_lower_bound f h
  80  local_blindness := fun _n M _hM decoder =>
  81    BalancedParityHidden.adversarial_failure M decoder
  82
  83/-! ## Status -/
  84

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.