Research contribution package: P vs NP subcube-cover route

[honzbartos]

I attempted to open this as a draft research PR, but the GitHub connector currently has read-only repository permissions: creating a branch failed with Resource not accessible by integration.

Below is a PR-ready LemmaTrail package distilled from the P vs NP research dossier. It intentionally does not claim a solution. It contributes:

• a new p-vs-np problem workspace,
• one precise subcube-cover encoding claim,
• one route object for the cover-orientation approach,
• one refuted/failed invariant object showing why finite-field degree alone is insufficient,
• a small task list and references.

Suggested PR body:

PR type: research

## Summary
- adds a proposed `p-vs-np` workspace
- records the 3-UNSAT-as-subcube-cover encoding as a checkable claim
- records the cover-orientation route as a candidate lower-bound program
- records the finite-field degree invariant as a failed standalone route

## Validation
- objects are scoped to one problem workspace
- AI assistance disclosed
- no raw transcript included
- no object is marked reviewed or verified

---

problems/p-vs-np/problem.md

---
id: p-vs-np
title: P versus NP
status: proposed
area: computational-complexity
source_ids:
  - cook-2000-pvsnp
authors:
  - name: Jan Bartos
    github: JanBartos6
    role: requester
contributors: []
reviewers: []
curators: []
ai_assistance:
  used: true
  model: GPT-5.5 Thinking
  role: research-dossier-distillation
review:
  llm_reviewed: false
  human_reviewed: false
  formal_reviewed: false
---

# Problem

Determine whether every language decidable by a nondeterministic Turing machine
in polynomial time is also decidable by a deterministic Turing machine in
polynomial time. Equivalently, determine whether \(P = NP\).

# Scope

This workspace is for checkable research state related to the P versus NP
problem, especially:

- NP-complete decision problems such as SAT and 3-SAT;
- circuit lower-bound routes to \(P \ne NP\);
- proof-complexity, communication-complexity, algebraic, descriptive,
  bounded-arithmetic, derandomization, and meta-complexity routes;
- failed routes and precise obstructions that future contributors should not
  repeat.

Claims here must separate established theorems, proposed lemmas, failed
approaches, and speculative routes. No contribution should present a full
solution unless the proof object contains reproducible dependencies, explicit
gaps if any, and independent review.

# Sources

- `cook-2000-pvsnp`: used for the standard definitions of \(P\), \(NP\),
  NP-completeness, SAT/3-SAT, and the circuit lower-bound implication.

# Known Equivalent Forms

- A polynomial-time algorithm for any NP-complete language, such as SAT or
  3-SAT, implies \(P = NP\).
- A super-polynomial Boolean circuit lower bound for an NP-complete language
  implies \(P \ne NP\), in fact \(NP \nsubseteq P/poly\).

# Initial Routes

- `p-vs-np-r0001`: subcube-cover orientation route for 3-UNSAT.

# Notes

The initial route in this workspace does not prove \(P \ne NP\). It identifies
a concrete monotone cover predicate equivalent to 3-UNSAT and isolates the
nonmonotone-to-cover-search transfer lemma as the main missing step.

---

problems/p-vs-np/proposals/claims/p-vs-np-c0001-3-unsat-subcube-cover-encoding.md

---
id: p-vs-np-c0001
type: claim
status: proposed
evidence_type: derivation
route_ids:
  - p-vs-np-r0001
depends_on:
  - p-vs-np
source_ids:
  - cook-2000-pvsnp
authors:
  - name: Jan Bartos
    github: JanBartos6
    role: requester
contributors: []
reviewers: []
curators: []
ai_assistance:
  used: true
  model: GPT-5.5 Thinking
  role: proposed-derivation
review:
  llm_reviewed: false
  human_reviewed: false
  formal_reviewed: false
---

# Statement

For each \(n\), let \(\mathcal C_n\) be the set of all signed 3-clauses on
three distinct variables from \(x_1,\ldots,x_n\). For
\(z \in \{0,1\}^{\mathcal C_n}\), define

\[
F_z = \bigwedge_{C : z_C = 1} C.
\]

For each clause \(C\), let \(Q_C \subseteq \{0,1\}^n\) be the codimension-3
subcube of assignments that falsify \(C\). Then

\[
F_z \text{ is unsatisfiable}
\quad\Longleftrightarrow\quad
\bigcup_{C:z_C=1} Q_C = \{0,1\}^n.
\]

Consequently, the Boolean function

\[
CCF_n(z)=1 \iff F_z \text{ is unsatisfiable}
\]

is monotone. If the family \(CCF_n\) requires super-polynomial-size
unrestricted Boolean circuits as a function of
\(N = |\mathcal C_n| = 8\binom n3\), then \(P \ne NP\).

# Dependencies

- `cook-2000-pvsnp`: standard NP-completeness of 3-SAT and the fact that
  polynomial-time decidability gives polynomial-size circuit families.

# Derivation

## Step C1

Each signed 3-clause \(C\) is falsified by exactly one assignment to its three
variables.

Short justification: a disjunction of three literals is false exactly when all
three literals are false.

## Step C2

The set of global assignments falsifying \(C\) is a codimension-3 subcube
\(Q_C\subseteq\{0,1\}^n\).

Short justification: the three variables of \(C\) are fixed to their unique
falsifying values, while the remaining \(n-3\) variables are free.

## Step C3

An assignment \(\alpha\in\{0,1\}^n\) satisfies \(F_z\) iff
\(\alpha\notin\bigcup_{C:z_C=1}Q_C\).

Short justification: \(\alpha\) satisfies the conjunction iff it falsifies none
of the selected clauses.

## Step C4

Therefore \(F_z\) is unsatisfiable iff the selected subcubes cover
\(\{0,1\}^n\).

Short justification: unsatisfiability means there is no assignment outside the
union of falsifying subcubes.

## Step C5

The function \(CCF_n\) is monotone in the selected-clause bits.

Short justification: adding clauses can only add falsifying subcubes to the
union, so a cover remains a cover.

## Step C6

If \(P=NP\), then 3-UNSAT is decidable in polynomial time.

Short justification: 3-SAT is NP-complete, and 3-UNSAT is the complement of
3-SAT. If \(P=NP\), then \(P=coP\) and the complement is also polynomial-time
decidable.

## Step C7

If \(P=NP\), then \(CCF_n\) has polynomial-size Boolean circuits.

Short justification: an input \(z\) can be decoded as a 3-CNF formula of size
polynomial in \(N\). A polynomial-time decision algorithm for 3-UNSAT gives a
polynomial-time algorithm for \(CCF_n\), and every polynomial-time language has
polynomial-size nonuniform circuit families.

## Step C8

Thus a super-polynomial unrestricted circuit lower bound for \(CCF_n\) implies
\(P\ne NP\).

Short justification: it contradicts Step C7.

# Branch Point

none

# Gap

This claim only identifies a concrete lower-bound target. It does not prove any
super-polynomial circuit lower bound for \(CCF_n\).

# Next Step

Formalize the cover-search relation associated with \(CCF_n\): given a selected
cover \(S\subseteq\mathcal C_n\) and an assignment \(\alpha\), output a clause
\(C\in S\) falsified by \(\alpha\). Then test whether lower bounds for this
relation can be connected to unrestricted circuits for \(CCF_n\).

---

problems/p-vs-np/proposals/routes/p-vs-np-r0001-subcube-cover-orientation-route.md

---
id: p-vs-np-r0001
type: route
status: proposed
depends_on:
  - p-vs-np-c0001
source_ids:
  - cook-2000-pvsnp
  - razborov-rudich-1997-natural-proofs
  - baker-gill-solovay-1975-relativization
  - aaronson-wigderson-2009-algebrization
authors:
  - name: Jan Bartos
    github: JanBartos6
    role: requester
contributors: []
reviewers: []
curators: []
ai_assistance:
  used: true
  model: GPT-5.5 Thinking
  role: proposed-route
review:
  llm_reviewed: false
  human_reviewed: false
  formal_reviewed: false
---

# Route

Subcube-cover orientation route for 3-UNSAT.

# Core Idea

Represent 3-UNSAT as the question whether selected codimension-3 subcubes cover
\(\{0,1\}^n\). Then try to prove that any small unrestricted circuit deciding
this cover predicate yields a small cover-search protocol that, given a cover
and an assignment, finds a selected clause falsified by that assignment. A lower
bound for the cover-search protocol, combined with such an orientation transfer,
would imply a circuit lower bound for the cover predicate and therefore
\(P\ne NP\).

# Dependencies

- `p-vs-np-c0001`: defines \(CCF_n\) and proves that a super-polynomial circuit
  lower bound for it implies \(P\ne NP\).

# Candidate Claims

- `p-vs-np-c0001`: 3-UNSAT is equivalent to codimension-3 subcube cover.

# Known Obstructions

- A monotone lower bound alone is not enough: some monotone functions in \(P\)
  have large monotone circuits, so any transfer from general circuits to
  monotone or cover-oriented protocols must use special structure of \(CCF_n\).
- A truth-table-large, efficiently checkable lower-bound property risks falling
  under the natural-proofs barrier.
- A purely oracle-style or black-box simulation argument risks relativization.
- A proof using only low-degree extensions risks algebrization.

# Gap

The missing lemma is the orientation transfer:

\[
\text{small unrestricted circuits for } CCF_n
\Rightarrow
\text{small cover-search protocols for } CCF_n.
\]

No proof of this transfer is currently known in this workspace.

# Next Step

Define the exact cover-search protocol model and test the orientation transfer
on restricted circuit classes first, such as monotone circuits, formulas,
AC\(^0\), or bounded-depth threshold circuits.

---

problems/p-vs-np/refuted/p-vs-np-f0001-finite-field-degree-invariant.md

---
id: p-vs-np-f0001
type: failure
status: refuted
route_ids:
  - p-vs-np-r0001
depends_on:
  - p-vs-np-c0001
source_ids: []
authors:
  - name: Jan Bartos
    github: JanBartos6
    role: requester
contributors: []
reviewers: []
curators: []
ai_assistance:
  used: true
  model: GPT-5.5 Thinking
  role: obstruction-analysis
review:
  llm_reviewed: false
  human_reviewed: false
  formal_reviewed: false
---

# Failed Claim Or Route

Use high algebraic degree over \(\mathbb F_2\) as a standalone invariant to prove
super-polynomial unrestricted Boolean circuit lower bounds for \(CCF_n\).

# Known Obstructions

Algebraic degree over \(\mathbb F_2\) does not by itself imply large unrestricted
Boolean circuits. The function

\[
AND_N(x_1,\ldots,x_N)=x_1x_2\cdots x_N
\]

has full \(\mathbb F_2\)-degree \(N\), but it has linear-size Boolean circuits.
Therefore, even if \(CCF_n\) has high or full \(\mathbb F_2\)-degree, that fact
alone cannot prove a super-polynomial unrestricted circuit lower bound.

# Evidence

The algebraic normal form of \(AND_N\) over \(\mathbb F_2\) is the single monomial
\(x_1x_2\cdots x_N\), so its degree is \(N\). A Boolean circuit computes
\(AND_N\) by a binary tree or fan-in-2 chain of AND gates using \(N-1\) AND gates.
Thus full algebraic degree is compatible with linear circuit size.

# Lesson

Finite-field degree may still help inside a more refined argument, but it is
not a sufficient lower-bound measure for unrestricted Boolean circuits. Future
attempts should use a more syntax-sensitive, communication-theoretic,
proof-complexity, or cover-search invariant.

# Next Step

Test whether a refined invariant, such as cover-search protocol complexity or a
restricted proof-complexity measure for subcube-cover tautologies, avoids this
counterexample.

---

problems/p-vs-np/tasks.md

# Tasks

- [ ] TASK-0001: Add a source-backed canonical problem statement from Cook's
  Clay Mathematics Institute exposition.
- [ ] TASK-0002: Formalize the cover-search relation for `p-vs-np-c0001`.
- [ ] TASK-0003: Check whether the cover-search relation is an instance of a
  known Karchmer-Wigderson or monotone communication game.
- [ ] TASK-0004: Prove or refute the orientation transfer for a restricted
  circuit class such as formulas, AC\(^0\), or monotone circuits.
- [ ] TASK-0005: Record known barriers as separate failure or obstruction
  objects: relativization, natural proofs, and algebrization.
- [ ] TASK-0006: Search for toy counterexamples where a small nonmonotone
  circuit computes a monotone cover predicate but no small cover-oriented
  protocol is apparent.

---

problems/p-vs-np/graph.yaml

problem_id: p-vs-np
nodes:
  - id: p-vs-np
    type: problem
    path: problems/p-vs-np/problem.md
  - id: p-vs-np-c0001
    type: claim
    path: problems/p-vs-np/proposals/claims/p-vs-np-c0001-3-unsat-subcube-cover-encoding.md
  - id: p-vs-np-r0001
    type: route
    path: problems/p-vs-np/proposals/routes/p-vs-np-r0001-subcube-cover-orientation-route.md
  - id: p-vs-np-f0001
    type: failure
    path: problems/p-vs-np/refuted/p-vs-np-f0001-finite-field-degree-invariant.md
edges:
  - from: p-vs-np-r0001
    to: p-vs-np-c0001
    kind: depends_on
  - from: p-vs-np-f0001
    to: p-vs-np-c0001
    kind: depends_on
  - from: p-vs-np-f0001
    to: p-vs-np-r0001
    kind: route_ids

---

problems/p-vs-np/references.bib

@misc{cook-2000-pvsnp,
  author = {Cook, Stephen A.},
  title = {The P Versus NP Problem},
  year = {2000},
  note = {Clay Mathematics Institute Millennium Problem exposition}
}

@article{baker-gill-solovay-1975-relativization,
  author = {Baker, Theodore and Gill, John and Solovay, Robert},
  title = {Relativizations of the P =? NP Question},
  journal = {SIAM Journal on Computing},
  volume = {4},
  number = {4},
  pages = {431--442},
  year = {1975}
}

@article{razborov-rudich-1997-natural-proofs,
  author = {Razborov, Alexander A. and Rudich, Steven},
  title = {Natural Proofs},
  journal = {Journal of Computer and System Sciences},
  volume = {55},
  number = {1},
  pages = {24--35},
  year = {1997}
}

@article{aaronson-wigderson-2009-algebrization,
  author = {Aaronson, Scott and Wigderson, Avi},
  title = {Algebrization: A New Barrier in Complexity Theory},
  journal = {ACM Transactions on Computation Theory},
  volume = {1},
  number = {1},
  year = {2009}
}

@article{karchmer-wigderson-1990-monotone-circuits,
  author = {Karchmer, Mauricio and Wigderson, Avi},
  title = {Monotone Circuits for Connectivity Require Super-logarithmic Depth},
  journal = {SIAM Journal on Discrete Mathematics},
  volume = {3},
  number = {2},
  pages = {255--265},
  year = {1990}
}

[JanBartos6]

Converted into draft PR #27: #27