pith. machine review for the scientific record. sign in
structure definition def or abbrev high

PvsNPDissolution

show as:
view Lean formalization →

The PvsNPDissolution structure packages three properties that together dissolve the P versus NP question inside the recognition framework: SAT instances admit zero J-cost assignments in at most n steps, UNSAT instances carry J-cost at least 1 under every assignment, and any decoder on a proper subset of variables fails to recover a hidden parity bit. Researchers comparing recognition time to Turing-machine simulation overhead would cite it to separate the two complexity measures. The definition assembles the three claims directly from upstreamJ

claimA structure asserting: 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$ such that the number of unsatisfied clauses under $a$ is zero; if $f$ is unsatisfiable then every assignment yields at least one unsatisfied clause; and for every proper subset $M$ of the $n$ variables and every decoder from the restricted hidden-parity encoding to a Boolean, there exists a hidden bit $b$ and mask $R$ such that the decoder disagrees with $b$.

background

J-cost of a CNF formula under an assignment equals the number of unsatisfied clauses, hence zero precisely when the assignment satisfies the formula. CNFFormula packages a list of clauses together with a variable count; Assignment is a Boolean function on the $n$ variables. The local-blindness clause invokes the hidden-parity encoder that flips a random mask $R$ according to bit $b$ and the restrictor that projects any full word onto the queried index set $M$. The module sets this structure inside the unconditional dissolution path that distinguishes recognition time from Turing-machine overhead.

proof idea

One-line definition that packages three independent properties drawn from upstream results on satJCost bounds and the balanced-parity hiding construction.

why it matters in Recognition Science

It supplies the dissolution structure instantiated by dissolution_holds and referenced inside PvsNPMasterCert. The module doc-comment positions it as the unconditional RS claim that P versus NP conflates recognition time (bounded by $n$) with TM simulation overhead, consistent with the framework's separation of J-cost from classical circuit size.

scope and limits

formal statement (Lean)

  64structure PvsNPDissolution where
  65  rhat_polytime : ∀ n : ℕ, ∀ f : CNFFormula n, f.isSAT →
  66    ∃ (steps : ℕ) (a : Assignment n), steps ≤ n ∧ satJCost f a = 0
  67  unsat_obstruction : ∀ n : ℕ, ∀ f : CNFFormula n, f.isUNSAT →
  68    ∀ a : Assignment n, satJCost f a ≥ 1
  69  local_blindness : ∀ n : ℕ, ∀ M : Finset (Fin n), M.card < n →
  70    ∀ decoder : ({i // i ∈ M} → Bool) → Bool,
  71      ∃ (b : Bool) (R : Fin n → Bool),
  72        decoder (BalancedParityHidden.restrict
  73          (BalancedParityHidden.enc b R) M) ≠ b
  74

used by (2)

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

depends on (8)

Lean names referenced from this declaration's body.