Various NP/coNP Things - #26
Merged
Merged
Conversation
Develop the elementary structural theory of coNP in Classes/NP/CoNP.lean: P is contained in NP ∩ coNP, Karp reductions dualize to complements, coNPHard/coNPComplete with transfer lemmas, NP-completeness dualizes to coNP-completeness of the complement, and P = NP implies NP = coNP (contrapositively, NP ≠ coNP separates P from NP). Dualizing Cook-Levin yields the headline corollary in SAT/CoNP.lean: the complement of the SAT language is coNP-complete (SAT.coNPComplete_compl_language). Index the new headlines in AxiomGuard.
Add to Classes/NP/Reduction.lean: an NP-hard language in P forces P = NP (NPHard.P_eq_NP_of_mem_P), so an NP-complete language lies in P iff P = NP (NPComplete.mem_P_iff_P_eq_NP). Consolidate the Cook-Levin consequences into SAT/CookLevin/Corollaries.lean (replacing SAT/CoNP.lean): the complement of SAT is coNP-complete, and SAT ∈ P iff P = NP (SAT.language_mem_P_iff_P_eq_NP). Index the new headline in AxiomGuard.
…port Add Trace/DetPrefix.lean: NTM.det projects an NTM onto the DTM that always follows one branch; BranchesAgreeAt names pointwise branch agreement; trace_succ_det bridges one non-halted trace step to a det step; and trace_of_det_prefix transports a det-false run through any choice sequence while an agreement invariant holds. This is the generic foundation for machines with a deterministic phase before a nondeterministic one (deterministic preprocessing before an NTM, NP closure under Karp reductions). Also add reachesIn_zero_iff / reachesIn_succ_iff inversion lemmas to the core run API, usable when the machine is a compound expression on which cases cannot abstract the configuration indices.
Replace the step-closed-invariant formulation of trace_of_det_prefix with TM.ReachesInVia, a run whose step sources carry a predicate. A step-closed invariant cannot describe a deterministic prefix, because the final prefix step exits the agreeing region when it enters the nondeterministic phase; annotating sources instead makes the transport apply exactly up to that boundary. Provide the ReachesInVia API: zero/succ inversion, toReachesIn, mono, trans, construction from a step-closed invariant, and reachesInVia_of_stepCommute for phase embeddings with a step-commute lemma. trace_of_det_prefix now consumes an annotated run directly.
…eleton Define NTM.compositionNTM tmF N, the sequential composition of a deterministic function computation with a nondeterministic machine. Branch b of the composite is TM.compositionTM tmF (N.det b): the deterministic composition's state space, start/halt markers, and tape layout do not depend on the second machine's transition function, so the det projections coincide with the deterministic compositions definitionally (compositionNTM_det is rfl). This lets the existing compositionTM simulation lemmas drive the composite's traces through NTM.trace_of_det_prefix. Prove branch agreement on all deterministic-phase states (first computation, raw-output rewind, copy, live virtual-input rewind); the rewind-phase halt state is excluded since its seam enters the placed retargeted phase at N's post-first-transition state, the composite's first branch-dependent step.
Prove that every trace of NTM.compositionNTM tmF N, along any choice sequence, factors through a deterministic-prefix boundary: the first computation, raw-output rewind, copy, and virtual-input rewind run without consulting a single choice bit, ending at the virtual-input rewind's halt state with f x parked at head 1 on the virtual-input tape, blank scratch block and output, and all tapes start-invariant (NTM.compositionNTM_trace_prefix, bound 4*TF(n) + 10). Internally the prefix is a TM.ReachesInVia run annotated with BranchesAgreeAt, assembled from the existing first-phase boundary lemma and the rewind/copy Hoare frames, lifted through the seqTM phase wraps by reachesInVia_of_stepCommute (Composition/Internal/NondetPrefix.lean).
Relate the composite's placed phase to N itself: placedCfg embeds an N-configuration into the composite (frame outside the placed block, real input ignored, N's input tape as the virtual input); placedCfg_step commutes one branch-b composite step with one N.det b step through the retarget, placement, and seqTM phase wraps; placedCfg_trace extends this to whole traces along any choice sequence; and compositionNTM_seam_step shows the single step out of a DetPrefixBoundary configuration enters the placed phase exactly at N's post-first-step configuration (startedCfg) on the virtual input. Combining with the prefix factorization gives the headline correspondence compositionNTM_trace_run: for N not starting halted, every composite trace of length (s+1)+t is the placed embedding of N's own (s+1)-step trace on f x, with the same choice bits.
Assemble the campaign: compositionNTM_decidesInTime composes a polynomial-time function machine with a nondeterministic decider within 4*TF(n) + 11 + TG(TF(n)), aligning the composite's traces with N's through the prefix factorization and the bit-for-bit placed-phase correspondence; a decider that starts halted decides only the empty language, so that degenerate case avoids the composite entirely. Normalizing NP witnesses to polynomial evaluations then gives mem_NP_preimage and MapReducesPoly.mem_NP (NP closed under polynomial-time reductions), dualized to MapReducesPoly.mem_coNP, and the collapse criterion NPComplete.mem_coNP_iff_NP_eq_coNP. Instancing at Cook-Levin: SAT ∈ coNP iff NP = coNP (SAT.language_mem_coNP_iff_NP_eq_coNP). Index the new headlines in AxiomGuard and record the milestone in ROADMAP N3.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Making a PR for visibility.