Concrete complexity problems related to P versus NP

## Campaign scope

The campaign currently has 95 source-backed complexity statements in 19 PRs (only #5413 ready),
with five substantive statements per batch. These are concrete decision, search,
promise and complexity questions related to P versus NP, not 95 independent
conjectures equivalent to P ≠ NP. Helpers and tests are not counted.

Each PR includes a source-to-declaration table, encoding and boundary conventions,
and focused tests. Problem statements are admitted; shared definitions and interface
proofs contain no admissions. Classical machine-based problems use the existing
TM2 polynomial-time definition; RAM-model statements identify their model separately.

The first batch, #5413, concerns clique, vertex cover, graph coloring, and
directed/undirected Hamiltonian cycles. Its source is Karp,
[Reducibility among Combinatorial Problems (1972)](https://doi.org/10.1007/978-1-4684-2001-2_9),
Theorem 3 and Main Theorem items 3, 5, 9, 10, 12, pp.93–95.

## Complexity relationships and source corrections

For an NP-complete problem, the absence of a deterministic polynomial-time decider
is classically equivalent to P ≠ NP. This relationship belongs in the theorem
docstring. Other campaign items require different wording:

| Problem | Relationship of the negative polynomial-time answer to P ≠ NP |
| --- | --- |
| DFA intersection nonemptiness, #5421 | Equivalent to P ≠ PSPACE; implied by P ≠ NP; converse unknown |
| Exact Euclidean TSP, #5422 | NP-hard, not known in NP; its lower bound follows from P ≠ NP; converse unknown |
| Quadratic residuosity, #5423 | A negative answer implies P ≠ NP; converse unknown |
| RSA inversion, #5423 | A negative answer implies P ≠ NP; converse unknown |
| Prime-field discrete logarithm, #5423 | A negative answer implies P ≠ NP; converse unknown |
| Partial MCSP, #5426 | The cited randomized-reduction hardness yields a lower bound from NP ⊄ BPP, not from P ≠ NP alone |

The source passages are Kozen's Definition3.2.2/Lemma3.2.3 for DFA intersection;
Garey–Johnson ND23's non-discretized metric comment for exact TSP;
[HAC Chapter3](https://cacr.uwaterloo.ca/hac/about/chap3.pdf), Definitions3.28/3.31/3.51,
for the three cryptographic problems; and
[Hirahara TR22-119](https://eccc.weizmann.ac.il/report/2022/119/), Theorem8.5,
for partial MCSP's randomized reductions. No proved strict separation between the
cryptographic hardness conjectures and P ≠ NP is asserted.

The HAC declarations now ask two-sided polynomial-time questions, following the
repository's [factoring statement](https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/PolyTimeFunctions.lean).
They concern worst-case classical algorithms, not average-case security.

In #5415, signed subset sum, partition, cut weights and integer-programming
right-hand sides are explicitly labelled generalizations: Karp's Appendix I uses
positive integers and nonnegative right-hand-side vectors. In #5416, signed
one-in-three and NAE SAT cite GJ LO4/LO3. In #5420, the zero-duration processing-
interval convention is explicitly distinguished from GJ's literal ordering clause.

## Review remediation and merge order

The 10 September parallel automated review is being addressed in this order:

1. Campaign-wide title/references-only module docs, complete problem theorem docs,
consistent positive/negative/question shapes, and precise complexity relationships.
Complete and pushed on all19 PRs:95 statements, including7 genuine questions.
All revised modules pass local strict builds and statement-shape checks.
2. Source-fidelity fixes E1–E8, repository-conforming file layout, and removal
of PR-local `scripts/axiom_audits` files: complete and pushed on all 19 PRs.
Local audits remain outside the PRs.
3. One shared infrastructure PR first, then rebase batch01 on it and mark only
batch01 ready. Other batches remain draft while conventions feedback is collected.
4. Close the unused infrastructure PRs #5410/#5411 and replace unpublished batch19's
approach with a light axiomatic PV1/T2/APX1 syntax and derivability presentation.

Batch19 interpreter work is already paused; existing code is preserved. Its five
original source-backed targets remain planned, including the solved parity theorem
with `research solved`. No external Foundation dependency is planned for that PR.

For the connection to the repository's `P_ne_NP`, the current pass uses the classical
relationship in each relevant theorem docstring. It does not present encoding-specific
reductions or machine-model bridges as already proved in Lean. Maintainer feedback on
whether a proved encoding bridge is required before merging is welcome.

The shared base is published as #5539. Batch01 (#5413) is rebased onto it and is
now ready for review; the other18 campaign PRs remain draft. PRs5410/5411 are now closed; their branches and code are preserved.
Light batch19 axiomatic work is next, with the interpreter remaining paused. Revised modules pass local `--wfail` checks; fresh CI is tracked
separately from historical green runs. Codex prepared the code and checks, and a
parallel Claude session supplied automated feedback. No completed human review is claimed.

Fresh CI exposed upstream #5477's rename from `ComplexityClass` to
`DecisionComplexityClass` in batches14/15. The compatibility fix uses the
definitionally identical type `Set DecisionProblem`, without changing any language
class or rebasing ahead of the planned base PR. Both fixes are pushed and pass
strict shared/scoped/regression builds on both the original base and the exact
current-upstream core API.
These core-API checks are not full latest-main merge builds. Fresh remote CI
remains separately tracked; this is not an all-green claim.

Source corrections E1–E8, layout F and audit removal G are now complete on all 19
campaign drafts. Extra API/style cleanups are also pushed for batches 02, 03, 05,
06, 07 and 09–12. Batch 04's meta import is retained because removing it breaks
both guarded evaluations. Optional unused-API pruning and the redundant proof-
simulation length bound remain deferred; they do not change the statements.

The shared base #5539 is built on current upstream main. Its ownership is:
DecisionProblems, SearchProblems, MatrixGraph/Basic, BooleanSatisfiability,
BooleanTruthTable, BooleanCircuit, WordRAM, PromiseProblems, TimeClasses, and the
core Finset encoding. Batch 01 will own MatrixGraphProblems; batch 06 will own
NetworkProblems and its graph-tree decidability support, reused by batch 07.
Other problem-specific modules stay with their current batches.

Merge the base first, then batch 01. Rebase the remaining drafts after conventions
feedback; regenerate the shared import index on each rebase. Their current
main-based diffs still repeat support files until the base lands and rebases finish.

Current upstream AGENTS reserves FormalConjecturesTest for repository tooling.
The base and rebased batch 01 therefore retain regression suites externally,
with useful shared lemmas beside their definitions. Apply this test-layout
adjustment to the other drafts when they are rebased.

The latest exact-head CI snapshot has batches 15–17 green and the others running;
batch 12 has since received another push. No current-head failure was reported in
that snapshot, and no all-green claim is made.

The base passes an8,890-job strict shared build, three external regression suites,
a706-declaration transitive axiom audit and repository tooling tests. Batch01 adds
only178 lines in three files above that base; its8,910-job build,44 kernel examples,
two guards,31-declaration audit and five-statement checks pass. The base also proves
a same-encoding bitstring-language bridge to existing P, not a general encoding
bridge or an NP-completeness reduction. Remote CI for these new heads is pending.

Start with the shared base in PR #5539 and batch 01 in PR #5413, then read the documented ownership, merge order, and remaining CI status. The campaign is complete when the shared base and batch 01 merge cleanly, remaining drafts are rebased after conventions feedback, and their stated builds and checks pass.

Written by the indexing model from the issue text.