[chris-ai1]

Item 8 of #949, area Computability.Complexity. This is documentation and visibility only: no statement or definition changes.

Scope. The 12 declarations in this area marked † but not ‡ in the item-8 list. The ‡ entries (CookLevin.Encoding, Clique, IndependentSet, TSP, ThreeSAT polytime rules) are left alone, per the scope note.

Made private (proof plumbing, used only in their own file; #926):

• Classes/PCP/NP.lean: PCPVerifier.isPolyTime_queryTable
• Problems/MonotoneCircuitValue/Completeness.lean: MonotoneCircuitValue.encMonotoneCircuitValue_dualTableauInstance

API: Main entries added

• AverageCase.lean: MildlyHardOnAverageToOneSidedApproxDet.mildlyHardOnAverageToApproxDet
• Classes/ArthurMerlin/Collapse.lean: PiP_two_subset_SigmaP_two_of_coNP_subset_AM
• Classes/DP.lean: mem_coDP_iff_union
• Classes/Hierarchy/Time.lean: computableInO_timeDiagonal
• Classes/MIP/NEXP.lean: MIP.exists_checkCert_of_detProver, MIP.exists_detProver_of_checkCert. The first one's docstring described only the length bound; it now states the completeness claim (the statement is unchanged).
• Classes/UP.lean: coUP_subset_coNP
• Fagin/Ordered.lean: ESODefinable.of_powerLanguage
• FineGrained/Sparsification.lean: Sparsify.decidableInExpTime_search
• Problems/MonotoneCircuitValue/Completeness.lean: MonotoneCircuitValue.logSpaceReducible_of_mem_P

Validation. Hosted CI: Lean Action CI run 40180976498.

Agent/session: worker-crei-dc679113 (Claude Code, Claude Opus 5.5).

🤖 Generated with Claude Code

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-18 (agent review) at b89f20e.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-18 — CHANGES REQUESTED at b89f20e

Agent review. Hosted ci-checks is green at this head (run 40180976498). The scope matches the 12 entries marked † but not ‡. The ten Main entries are accurate, and every documented declaration has a docstring stating its purpose. The rewritten exists_checkCert_of_detProver docstring now states the completeness claim. Making encMonotoneCircuitValue_dualTableauInstance private is fine: it is the writer-correctness step for dualSpec, which is local to the module.

Blocking:

1. Classes/PCP/NP.lean:82, PCPVerifier.isPolyTime_queryTable, should stay public, because doc(contributing): privatize by intent, not by current usage #926 keeps bounds on public definitions public. queryTable is listed under the module's Main definitions, and this lemma is its polynomial-time certificate, the same kind of result as the public isPolyTime_tableVerifier. Remove the private and add a Main entry.

Nonblocking:

• The statement of exists_checkCert_of_detProver is existential. "Some certificate passes checkCert (the proof builds the canonical one from D)" would be more exact than "the canonical certificate built from D passes".

[SamuelSchlesinger]

Coordinator fix (coordinator-claude-c4b0c164-20261023, AGENTS.md coordinator-fix rule; maintainer edits allowed on this branch). This applies reviewer-claude-c4b0c164-18's blocking item in one commit on top, keeping your commit and credit:

• PCPVerifier.isPolyTime_queryTable, the polynomial-time bound of the Main definition queryTable, stays public (doc(contributing): privatize by intent, not by current usage #926).
• It gets a Main results entry.
• encMonotoneCircuitValue_dualTableauInstance stays private, as the review agreed.

A full build, check_changed_files.py and check_hygiene.py pass locally.

coordinator-claude-c4b0c164-20261023 — APPROVED at c93caab (coordinator fix on top of reviewer-claude-c4b0c164-18's review).