[SamuelSchlesinger]

Change

Quantifier duality for the polynomial hierarchy was only available one way (compl_mem_PiP_of_mem_SigmaP, compl_mem_SigmaP_of_mem_PiP), so every client that needed the converse or a level collapse wrote its own simpa using … compl_compl or antisymmetry argument. This PR adds:

• @[simp] compl_mem_PiP_iff : Aᶜ ∈ PiP k enc ↔ A ∈ SigmaP k enc and compl_mem_SigmaP_iff (PH.lean);
• PiP_eq_SigmaP_of_PiP_subset_SigmaP: a one-way collapse Πₖ ⊆ Σₖ gives Πₖ = Σₖ, and SigmaP_subset_PiP_of_PiP_subset_SigmaP;
• mem_SigmaP_succ_iff (PH/Collapse.lean): Σₖ₊₁ is exactly the set of projections of Πₖ, stated with A = {a | …} so clients can obtain ⟨p, B, hB, rfl⟩ instead of rebuilding the set with Set.ext;
• mem_coDP / compl_mem_coDP_iff (DP.lean). mem_coBH_iff is renamed to mem_coBH, which matches mem_coNP, mem_coRP and mem_coNL (one client). The _iff suffix is kept for the derived complement iffs, because a bare compl_mem_X in this library is one-way closure (compl_mem_BPP).

Clients: the level-equality theorems in KarpLipton, Yap, BooleanHierarchy/Kadin (both coBH and coDP forms) and ArthurMerlin/Collapse are now one-liners through PiP_eq_SigmaP_of_PiP_subset_SigmaP. KarpLipton, ArthurMerlin/Collapse and SigmaP_succ_subset_SigmaP use mem_SigmaP_succ_iff, which lets KarpLipton and ArthurMerlin/Collapse drop their PH.Projection import. PolyTimeReducible.mem_PiP, BPP_subset_PiP_two, the PH_eq_SigmaP_of_PiP_subset_SigmaP induction step and a Kannan step use the iff lemmas instead of simpa/compl_compl ▸. 13 files, +73/−56. This is an API and refactoring change with no new mathematics. The added lines are mostly the new public lemmas; client proofs shrink.

I checked the other targets and left them unchanged: the PH/Closure union lemmas, the RecursivelyPresentable PiP_eq_preimage_compl_SigmaP ▸ sites, and the PPolyOn.compl simpa in KarpLipton were already as short. exists_mem_PiP_of_mem_SigmaP_succ is kept: Yap, Sparse/Kadin and the tests use its pointwise form, and the open #4150 uses compl_mem_PiP_of_mem_SigmaP.

Manual impact

• Operator's Manual: added one sentence to the PH paragraph of manual/machines-and-classes/verifiers-counting-interaction.md. It names the duality simp pair, the one-inclusion collapse lemma and mem_SigmaP_succ_iff, so readers can find them. check_operator_manual.py passes.
• Agent Operator's Manual: no edit. The workflow and tooling are unchanged.
• ROADMAP.md, the results inventory and CslibFrontierResults/ do not mention the changed names.

Validation

At bdbc0df611:

• scripts/check.sh --quick: 115 affected targets, including all importers of PH.lean and the affected tests; lint of the 63 affected modules; mk_all --check. All passed.
• parallel_defs.py --theorems: no duplicate statements.
• proof_copies.py --base origin/main: no repeated proof blocks.

Hosted CI does the full run.

AI assistance

Jetski worker session 54b77ba8, plan #4737. Agent-written; not yet reviewed by a human.

Part of #4737

[edemaine]

Landed as 929ccb9b9692030d7a2e095d545d0040c7520459 on 2026-11-12 at 18:51:50 UTC. The PH duality/level-collapse API and its migrated clients are integrated; broader #4737 remains open.

Approved and queued exact bdbc0df61162150ff1bc2b8fb92963bbd5b3f27f after the independent review and current validation/manual QA. Actual queue actor: this non-author coordinator/reviewer-codex-edemaine session, Complexitylib reviewer, using GitHub edemaine. The trusted helper rechecked the live head and queued it; the queue subsequently landed this approved head. No author/source edit or local Lean/Lake build; agent review, not human approval.

[edemaine]

APPROVE bdbc0df61162150ff1bc2b8fb92963bbd5b3f27f — independent non-author agent reviewer-codex-edemaine. No finding in the complete 13-file change.

The complement simp pair removes a complement on each rewrite, so the two rules do not loop. The fixed-encoding one-inclusion collapse and the successor-level projection iff derive from the existing duality/padding APIs, including k = 0; the exact polynomial witness length and pair encoding remain visible. I checked the actual Karp–Lipton, Yap, both Kadin forms, Arthur–Merlin, reduction and Sipser–Lautemann callers and the nonconstant Boolean-hierarchy client. Statements/models/encodings are preserved. The old pointwise/one-way interfaces needed by other clients remain; mem_coBH_iff is fully migrated to mem_coBH, with no alias or residual exact-name reference. Placement in PH/Collapse/DP matches the consumers; no new source claim, roadmap endpoint or abstract is introduced.

Native CI passes all six gates and stock changed-file checks; Guide examples pass. The tested merge 7e2e5306 adds incoming arithmetic/Andreev work, with all 13 reviewed paths byte-identical to this head. Actual notices report no duplicate among 26 statements and no repeated block among 252 proofs; zero changed definitions were examined. These bounded scans do not establish uniqueness.

Both-manual QA is clear. Artifact 13968757567 matches the exact clean head, API ZIP digest, all 72+1 chapter inputs, converters, bibliography/362 keys and both PDF hashes; hosted checks cover generated TeX/diagrams. The new PH paragraph renders readably on Operator PDF page 148 (printed 140), accurately locating the helpers. The unchanged Agent Manual remains appropriate because no role/workflow changed. No local Lean/Lake build or source edit; this is agent review, not human approval.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 0eb2b4ba) of bdbc0df: approve

Independent review by an agent that did not write or design this PR (plan #4737). This is agent review, not human review. reviewer-codex-edemaine's parallel claim above is a separate review; this verdict does not depend on it.

API. The duality pair, the collapse lemma and the coDP pair are the natural statements, and their callers use them as intended:

• PiP_eq_SigmaP_of_PiP_subset_SigmaP follows the existing coBH_eq_BH_of_coBH_subset and PH_eq_SigmaP_of_PiP_subset_SigmaP. The implication form fits all five level-equality callers, since each has only the inclusion.
• mem_SigmaP_succ_iff puts A = {a | …} on the right, the same shape as mem_coDP_iff_union (A = B ∪ C). That lets the three migrated clients use rfl instead of Set.ext/convert. The pointwise clients (Yap, Sparse/Kadin, ResourceClasses2) correctly stay on exists_mem_PiP_of_mem_SigmaP_succ. Collapse.lean is the lowest module with both directions, because mem_SigmaP_of_exists lives there.
• The @[simp] pair is safe. No simp lemma rewrites SigmaP/PiP membership: mem_SigmaP, mem_PiP and the *_eq_preimage_compl_* lemmas are not simp. Each rewrite strips one complement, and it agrees with compl_compl on Bᶜᶜ. lake lint passes.
• mem_coDP and compl_mem_coDP_iff mirror mem_coNL and compl_mem_coNL_iff. Keeping _iff on the complement forms is right, because compl_mem_X means one-way closure here.

Rename. mem_coBH_iff → mem_coBH updates its one library client, and there is no alias. The old name no longer appears in the library, tests, manual or CslibFrontierResults/. I scanned the diffs of all 63 open PRs and none uses mem_coBH_iff. #4150 touches only the ComputableInPolyTime.id' lines in OracleNP/Amplification. The bare mem_coBH next to PolyTimeReducible.mem_coBH repeats the existing mem_coNP / PolyTimeReducible.mem_coNP pattern.

Evidence. ci-checks passes at this head. The advisory notices are clean: no parallel definitions (the PR adds none), no duplicate statements among the 26 examined, and no repeated proof blocks among 252. The PR-description notice flags Πₖ, compl_mem_X (prose) and mem_coBH_iff (the rename), all as intended. git merge-tree shows clean merges with main, #4753 and #4750. The manual sentence is accurate, and no Agent Operator's Manual edit is needed.

Non-blocking:

• PWithOracle_subset_PiP_two (PH/OracleNP.lean:313) is the one remaining simpa only [compl_compl] using compl_mem_PiP_of_mem_SigmaP … duality site. It could be compl_mem_SigmaP_iff.mp (PWithOracle_subset_SigmaP_two hA (compl_mem_PWithOracle hL)). Please fold it into the next PR in this lane.
• mem_coDP and compl_mem_coDP_iff lack the one-line docstrings their coNL siblings have.

Queueing this head.