feat(complexity): prove P is contained in NP - #84
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 0cbaedf0f7
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| import ComplexityTheory.Computability.ConditionalIdentity.Output | ||
| import ComplexityTheory.ComplexityClasses.P | ||
| import ComplexityTheory.ComplexityClasses.NP | ||
| import ComplexityTheory.ComplexityClasses.NP.FromP |
There was a problem hiding this comment.
The new public module ComplexityTheory.Computability.PairFirstComposition.Correctness is only reachable transitively through NP.FromP, but the root aggregate still skips it in the PairFirstComposition section. If downstream import audits or users rely on ComplexityTheory.lean enumerating public modules directly, this public theorem module is omitted; add a direct import next to the other PairFirstComposition imports.
Useful? React with 👍 / 👎.
|
|
||
| import ComplexityTheory.Computability.PairFirstComposition.Clock | ||
|
|
||
| /-! |
There was a problem hiding this comment.
This new correctness module specializes Mathlib's Turing.initList/haltList configurations and StateTransition.EvalsToInTime.trans, but the module docstring does not record the borrowed source/version for those definitions and results. That leaves proof provenance incomplete for the public wrapper theorem; add a Mathlib citation here, as the neighboring conditional-identity proof modules do.
Useful? React with 👍 / 👎.
1 participant
What does this change?
Proves the pair-first wrapper computes the source Boolean function on the first component with its explicit polynomial clock. It packages that theorem as the exact specialized composition principle needed by an empty-witness verifier and proves
ComplexityClass.p_subset_np : P ⊆ NPunconditionally in the repository's concrete multitape-machine model.This formalizes Arora and Barak, Computational Complexity: A Modern Approach, Claim 2.3 while avoiding mathlib's unresolved generic polynomial-time composition obligation. This is stack layer 8 of 8.
How was it tested?
lake build --wfailpasseslake lintpassessorryor new axioms, or this PR does not change Lean proofs