Complexity lab / SAT diagonalization
P != NP as a question of compression, witness space, and self-reference.
This room reconstructs the uploaded preprint series as an academic working model: a proposed proof route through SAT solution-space incompressibility, not a claim of settled community acceptance.
Independent preprint Expert review required Six uploaded PDFs
assume f phi_f exclude f(enc(phi_f)) SAT remains?
Problem
P vs NP frame
If SAT is solvable in polynomial time, then P = NP; if no such polynomial-time procedure exists, P != NP.
Formal object
P = NP iff SAT in P Function in argument
Sets the target problem through the standard Cook-Levin equivalence.
standard backgroundInteractive instrument
Compress a witness space, then watch the diagonal formula avoid it.
This finite model demonstrates the mechanism behind the uploaded papers: a small candidate list is selected, the formula adds one exclusion clause per candidate, and the remaining Boolean cube is inspected for witnesses. It visualizes the diagonal exclusion step; the full preprint additionally requires the fixed-point, constructivity, and barrier arguments.
Mode toy verifier Shows the construction logic; it is not a substitute for the full proof.
Boolean cube 16 assignments
Remaining witnesses 11
Generated formula
phi_f excludes exactly the candidate set.
The compressor selected five assignments. The generated CNF forbids those five points and leaves other assignments available as witnesses.
f candidate excluded by phi_f remaining satisfying witness first available witness
Review cockpit
A world-class version must expose the proof obligations, not hide them.
Selected audit node 01
Compressibility equivalence
What this page demonstrates
The page models a compressor as a finite candidate selector over {0,1}^n.
What the PDF must prove
Prove the precise equivalence between a polynomial hitting-set compressor for SAT witnesses and a polynomial-time SAT decision/search procedure.
Failure mode to rule out
If CH is weaker or stronger than P = NP, the diagonal contradiction may miss the target theorem.
Status Review target
Uploaded P != NP corpus
Six documents are treated as one reviewable argument system.
Part I 7 pages
Refutation of the Compressibility Hypothesis
Defines CH for SAT and introduces the diagonal self-referential formula phi_f.
- Contribution
- Frames P != NP as the failure of a universal polynomial-size solution-space compressor.
- Review posture
- Presented on the site as an independent preprint proposing a proof.
Part II 7 pages
Polynomial construction and barriers
Replaces reliance on a fixed-point theorem with an explicit polynomial construction program.
- Contribution
- Moves the argument from abstract self-reference toward a constructive algorithmic object.
- Review posture
- The polynomial constructivity claim remains a key verification target.
Part III 8 pages
Practical verification and specificity
Adds PySAT-style computational checks and compares the behavior against 2SAT.
- Contribution
- Introduces an empirical layer for satisfiability, exclusion, and NP-complete specificity.
- Review posture
- Experiments illustrate the construction; they do not replace a formal proof.
Part IV 9 pages
Formalization and exhaustive validation
Restates CH, fixed-point convergence, satisfiability, exclusion, and edge cases.
- Contribution
- Collects the proof obligations into a more explicit checklist.
- Review posture
- The site keeps these as obligations for independent mathematical review.
Part V 8 pages
Equivalence proof, gap closure, barrier analysis
Strengthens the equivalence between CH and P = NP and addresses review gaps.
- Contribution
- Turns the sequence into a single audit trail: equivalence, construction, exclusion, barriers.
- Review posture
- Claims are displayed as the author's preprint architecture, not a settled theorem.
Extended Part V 106 pages
Measure-growth theorem and barrier resilience
Develops structural diagonalization, a syntactic gadget, and a measure-growth invariant.
- Contribution
- Adds a large methodological defense against relativization, natural proofs, and algebrization.
- Review posture
- Best treated as the main verification dossier for experts.
Parsed corpus / evidence layer
The PDF series is now treated as a structured proof dossier.
The six uploaded PDFs have been extracted into text and analyzed as one connected argument: SAT compression, polynomial self-reference, diagonal exclusion, barrier resilience, and formal verification targets. This block separates the public claim from the exact proof obligations that an expert reviewer would inspect first.
Standardize the hypothesis
Unify CH / IH / CH1 into one precise statement: a polynomial-time SAT witness candidate-set compressor whose output intersects the satisfying assignments of every satisfiable CNF.
Prove equivalence to P = NP
Show both directions: SAT in P gives the compressor by search self-reduction, and the compressor decides SAT by checking its polynomial-size output list.
Make phi_f constructive
The self-referential formula must be produced by an explicit polynomial-time construction, not by an informal appeal to fixed-point intuition.
Preserve satisfiability
The diagonal clauses must exclude the candidates returned by f while leaving at least one satisfying witness after all encoding and gadget constraints.
Isolate the 2SAT boundary
The construction should be presented as a SAT / 3SAT mechanism; 2SAT must be treated as a boundary case, not as proof that known P problems are paradoxical.
Keep experiments in their lane
PySAT traces and finite simulations are valuable reproducibility artifacts, but the asymptotic separation must rest on the formal construction.
Corpus files
Open the extracted text and the review map.
These files make the proof corpus auditable. The Markdown analysis records the argument architecture, strengths, likely expert objections, and the next formal work needed before peer-facing presentation.
Proof obligations
The site should make the argument inspectable, not merely impressive.
The strongest version of this page is a verification cockpit: every major claim becomes a node, every node has a formula, and every formula has an audit question.
- CH equivalence to P = NP is stated with an explicit candidate-set function.
- phi_f must be constructible within polynomial bounds for every admissible f.
- The exclusion clauses must forbid f's candidates without destroying satisfiability.
- The satisfiability margin must survive encoding overhead and boundary cases.
- The argument must not be a disguised relativizing, naturalizing, or algebrizing method.
- Empirical checks should be treated as reproducibility evidence, not as final proof.
Public dossier link
How the work remains academically cautious on the site.
SSRN card: preprint posted May 6, 2025 and revised May 7, 2025, presenting an archived argument around SAT, formal complexity, and compressibility.
Open formal dossierThe relation between finding a solution and verifying a solution
SAT solution spaces and whether their structure can be compressed
Diagonalization and incompressibility are treated as pressure points
Displayed as a formal map of limits, not as an unreviewed final theorem