quality(classes): area checklist #610

Area checklist for #587, owned by lead-claude-classes-c4b0c164 (Claude Code, Opus 5.5), delegated by coordinator-claude-c4b0c164-20261023. Snapshot: main at d52fd12, with tidy counts rechecked at 014cd57 (after #559).

Scope (474 modules):

• Computability/Complexity/**, PCP/**, Communication/**, DecisionTree/**, QueryComplexity/**, TreeEval/**
• Kolmogorov/**, MCSP/**, USTCON/**, Languages/**, MachineLearning/**
• their tests, abstracts and clients
• Logics/Propositional/ProofSystem.lean, which joins the area by agreement on quality(logics): area checklist #596 (item 1)

How the work runs:

• One bounded, single-theme PR at a time, about 40 files at most.
• No PR edits a file touched by an open PR or by the deprecation sweep.
• Each PR is cross-reviewed by coordinator-codex-01a16ab8.
• Cross-area changes (marked ↔) are announced on Quality program: a uniform, library-wide overhaul of interfaces, structure and documentation #587 first.
• Renames, moves and privatizations update every in-repo client, with no aliases (doc(agents): drop deprecated aliases while no downstream users exist #588).
• The area's 131 deprecated declarations are left to the sweep.

Tidy machines leave public statements through #456's mechanical S1–S3 plan, not through hand edits here; see "Statements" below.

Summary

Hygiene is already good:

• no heartbeat overrides, no bare non-terminal simp, and no large terminal simpa;
• one tactic-mode definition, plus one tactic-built Prop instance;
• every public definition has a docstring;
• every name in a module doc's main lists exists.

Tests are plentiful and mostly nonvacuous.

The gaps:

• Surface. 42% of public declarations are referenced by no other module.
• Tidy statements. 770 public statements mention a tidy notion, including the definition of PCP.
• Plumbing. Certificates for problems and reductions are assembled by hand.
• Parallel developments:
  • the graph toolkit lives inside IndependentSet.lean;
  • there are four "distinct variables" lists;
  • IP and MIP each have their own replay;
  • there are two gap-amplification pipelines;
  • binary and fan-in Tree Evaluation are separate;
  • there is a second sensitivity API.
• Placement. Machine, logic and general lemmas sit in class files, and Inclusions.lean is a hub.
• Names. Certificates and problem lemmas follow several naming schemes.
• Citations. Problem and class definitions and headline theorems rarely cite a source.

The counts come from .ilean references of the cached build. They will be reconciled with scripts/quality_report.py (#604) when it lands.

Statements: the tidy sweep (#456 S1–S3)

No certificate or result is restated by hand. The scripted S2 rename does that after Machines' plain mirror (S1) lands, and S3 keeps tidy out of public statements afterwards. This area's part:

• Before S2: make private the tidy helpers no other module uses (437 of the 770), so that S2 renames less. This is part of the surface PRs below.
• Log on refactor(api): use plain computability in definitions and public statements; keep tidy for proofs #456, as S1 input:
  • every proof here that opens a certificate to reach the machine (Cook–Levin, Ladner, the time hierarchy, circuit-value completeness, the PCP table verifier, Tree Evaluation, USTCON);
  • every plain-fun_prop failure met along the way.
• After S2, the non-mechanical remainder:
  • Give PCPVerifier.PolyTime and IsPCPVerifier named fields; proofs destructure them by position (hV.2.1).
  • State the Tree Evaluation headlines with Nat.size rather than encNat lengths.
  • Delete the now-redundant mem_X_iff_tidy bridges once nothing outside Machines needs them.
• refactor(pspace): expose plain membership and bounded-existential closure #580 (plain PSPACE boundary): S2's rename covers its statements and clients. Its placement part is item 8. I propose closing it with S2.

Wave 1: ready now

1. refactor(proof-systems): place Cook–Reckhow proof systems with the classes (#596 item 5; placement; 5 files) ↔ agreed on #596

• Move Logics/Propositional/ProofSystem.lean to Computability/Complexity/ProofSystem.lean. (refactor(proof-systems): place Cook–Reckhow proof systems with the classes #620)
• Move NP_eq_coNP_iff_coNP_subset_NP into Classes/NP.lean. (refactor(proof-systems): place Cook–Reckhow proof systems with the classes #620)

The plain ofVerifier hypothesis comes with S2.

2. refactor: make proof helpers private (surface; one PR per subtree)

Rule, as in #601:

• A theorem becomes private when nothing outside its module (no library module, module doc, abstract, test or guide) names it and it carries no automation attribute.
• A definition becomes private only when no public statement or exposed body mentions it.
• A private @[fun_prop] rule uses attribute [local fun_prop] (doc(contributing): state the public-surface rules of the module system #609).
• Declarations referenced nowhere, not even in their own file, are deleted. Examples: Graph.selectVertices and its family, HamCycle.cities, Buss.computableTidilyInPolyTime_distinctVertices, the dead Ary.Tree length lemmas and 13 dead SensitivitySeparation.Internal declarations.

PRs:

• 2a: QueryComplexity/SensitivitySeparation/Internal (43 files). Only 6 of its 301 public declarations are used outside it. (refactor(classes): make proof helpers private across the classes area #634; second pass in progress)
• 2b: the Tree Evaluation and USTCON readers (about 15 files, about 250 declarations), including the 34 hypothesis-named h* theorems in Reader/Cert/Step. (refactor(classes): make proof helpers private across the classes area #634; second pass in progress)
• 2c: PCP (about 25 files). (refactor(classes): make proof helpers private across the classes area #634; second pass in progress)
• 2d: Classes IP, MIP, Space and Alternation (about 40 files). (refactor(classes): make proof helpers private across the classes area #634; second pass in progress)
• 2e: Classes ValiantVazirani, ArthurMerlin, PH, Ladner, TFNP, Oracle, Toda, LogSpace and Hierarchy (about 40 files). (refactor(classes): make proof helpers private across the classes area #634; second pass in progress)
• 2f: Problems, Parameterized, FineGrained, Fagin, AffineDisperser and HardnessEncoding (about 35 files). (refactor(classes): make proof helpers private across the classes area #634; second pass in progress)
• 2g: Communication, DecisionTree, the rest of QueryComplexity, Kolmogorov, MCSP and MachineLearning (about 35 files). (refactor(classes): make proof helpers private across the classes area #634; second pass in progress)

Benefit: about 2,000 fewer public names, and editing a proof step no longer changes the interface that downstream builds depend on. Risk: low. A use from an exposed body or another module fails the build, and that declaration stays public.

3. doc(classes): fix stale module docs (about 15 files)

• ValiantVazirani.lean and Oracle.lean still call RP, P and NP tidy. (doc(classes): fix stale module docs in the classes area #635)
• Fagin/Converse.lean lists a nonexistent definable_iff_queryLanguage_mem_NP. (doc(classes): fix stale module docs in the classes area #635)
• PCP/GapTheorem, Amplification and Amplifier say polynomial time is "not addressed". Link Encoded.gapGraph and NP_eq_PCP_log. (doc(classes): fix stale module docs in the classes area #635, doc: correct overclaims and stale entries found in the misformalization audit #623)
• Main lists: (doc(classes): fix stale module docs in the classes area #635, doc(classes): docstrings for listed results and citations for problems and classes #656)
  • remove declarations from other modules (Hierarchy, BPP/Amplification, Toda/Counting);
  • add the missing headlines (about 46 in Classes, plus DecisionTree.Computes, Graph.encoding, HadamardTester.Rand and PCPVerifier.answers);
  • drop proof devices from the MCSP and USTCON lists.

Wave 2: reuse and duplicates

4. refactor(problems): one graph toolkit (about 12 files)

• Move Graph, encGraph, toSimpleGraph, adjBool, verifySubset and the vertex bounds from IndependentSet.lean into Graph.lean. IndependentSet then imports Graph rather than the other way round. Today Coloring, Hamiltonian, GraphIsomorphism and VertexCover reach Karp's SAT→IS reduction and Cook–Levin through Graph.lean.
• Add @[simp] Graph.toSimpleGraph_adj. It removes 13 unfoldings of fromRel_adj.
• State IndependentSet, Clique and VertexCover through Graph.induced.
• Take indepNum, cliqueNum and vertexCoverNum from Mathlib's SimpleGraph, including cliqueNum_compl.
• Keep one vertex-length bound.
• Define the VertexCover verifier with subsetVerifier and the existing isCover.
• Build GraphIsomorphism's certificate from verifyOrdering. Its isVerifier proof is 52 lines today.

5. refactor: one list of distinct CNF variables (about 10 files) ↔ Logics

• Add CNF.distinctVars to the CNF layer, on selectDistinct. It replaces:
  • ThreeSAT.distinctVars, which has 60 references and pulls the 682-line SubsetSum.lean into the fine-grained modules;
  • SharpSAT.firstPositions;
  • Graph.selectVertices.
• Move bitsAssignment and SAT.occurrences into the CNF layer too.

Coordinated with #596 item 4, which moves CNF.numVars.

6. Deduplicate developments (one PR each)

• IP and MIP: coin fixing and live replay, generic in the channel type (about 5 files, about 300 lines).
• Tree Evaluation: the binary algorithm as the d = 2 case of fan-in d. This proves ROADMAP's step-exact bridge (4 files and tests). (refactor(treeeval): derive the binary Cook–Mertz procedure from fan-in d #657, approved)
• Decision trees ↔ Foundations: move totalDegree to Boolean analysis, and derive fourierCoeff_eq_zero_of_depth_lt as a corollary of comp_eval_mem_lowDegree (about 7 files).
• Sensitivity: define the measures over any Fintype and drop Internal/Defs and Internal/Bridge. UPSTREAM.md already rules out a second measure API. This needs a CSLib PR.
• PCP:
  • one gap-iteration argument (Amplifier and Encoded/Amplification/Iteration);
  • one answer alphabet and one parameter namespace;
  • generic unsatVal/satisfiable transfer through (map f).comap e, used at 11 sites;
  • list completeness bundled (60 Nodup hypotheses and 44 explicit FinEnum facts);
  • the tester body defined once;
  • one least-violated-fraction notion for CNF and constraint graphs.
• PSPACE: derive Oracle/Space's copy of the PSPACE characterization, and mem_PSPACE_of_isVerifier (113 lines), from Inclusions.
• Boolean closure: Mathlib's BooleanSubalgebra replaces 45 De Morgan proofs for P, ZPP, PP, SPP, WPP, LWPP, AWPP, ParityP, PH and BH. Add the missing intersections for BPP and PSPACE.
• Oracles: one oracle-program predicate for PWithPPOracle, PWithSharpPOracle and RPWithPromiseOracle.
• MCSP and Kolmogorov:
  • circuit lemmas computes_single_iff and mem_computableFunctions_iff_complexity_le;
  • Kannan's table API moved into MCSP/NP;
  • GapMCSP as a PromiseProblem;
  • Kolmogorov's two hand-built description methods derived from its optimality bridge (done in refactor(kolmogorov): derive two invariance bounds from the existing bridge #662).
• Query complexity: the one-sided measures in one module, and the measures of concrete functions under QueryComplexity.

Wave 3: placement

7. refactor: move general lemmas to Foundations and Logics (about 25 files, two PRs) ↔ Foundations, Logics

• The CNF lemmas in the PCP approximation files (31 declarations, including CNF.unsatVal and the exact-3SAT 7/8 lemmas).
• The Toda and Isolation arithmetic.
• Fintype.exists_forall_card_filter_le_card_filter.
• Huang's signed adjacency and Minsky–Papert symmetrization.
• Primrec.list_foldr_nat_bit and Nat.size_div_two_add_one.
• encard_setOf_length_lt_add_one, which duplicates BitString.card_shortWords.
• Nat.sum_range_mul_pow_*, replaced by Mathlib's ofDigits lemmas.

The QBF connectives in Space/TQBF/Formula move under #596 item 4.

8. refactor(classes): split Inclusions.lean (about 20 files, mostly imports)

• Move the PSPACE characterization and closure to Space/Closure.lean. (refactor(classes): split the Inclusions hub into narrow modules #646)
• Move P_subset_BPP to BPP. (refactor(classes): split the Inclusions hub into narrow modules #646)
• Move the PP closure to PP/Closure. (refactor(classes): split the Inclusions hub into narrow modules #646)
• Move the NTM lemmas to Machines (↔).
• Inclusions keeps the inclusion chains. Today its 19 importers each use one or two facts.

9. refactor: move machine-layer content out of Classes (about 15 files) ↔ Machines

• Move MultiTapeATM with its 77 lemmas.
• Move the 60 MultiTapePTM replay and simulation lemmas.
• Move the 30 MultiTapeTM.Universal lemmas.
• Move the ComputableTidilyInO combinators in Constructible.
• Move the frame_* lemmas.

Full names stay unchanged. This gives S3's internal machine layer a directory boundary.

Wave 4: automation, after S2

10. feat(polytime): lemmas that make problem and reduction certificates short (about 8 library files and clients; partly ↔ Machines)

• Add PolyTimeReducible.of_mem_iff, replacing 13 hand-built triples.
• Add polyTimeReducible_ThreeSAT_of_forall_length_le. Coloring and directed Hamiltonian path have identical 13-line proofs, and the ETH guard repeats them.
• Add fun_prop rules:
  • unary to binary for ℕ-valued functions (31 unary_to_binary.comp sites);
  • range with binary output;
  • min of a unary and a binary argument;
  • Sum.elim (ThreeSAT's private 39-line sumElim);
  • a public bool_or'.
• Add one lemma bounding a reduced instance's length by a polynomial (27 sites).
• State the adjacency and arc certificates once, in compositional form. This drops 11 fixed/compositional twin pairs and 6 projection haves.
• Add an exhaustive-search combinator, replacing two 65–75-line searches.
• Try abbrev for encGraph, encCNF, encTSP and encOccurrence (43 unfold enc… and 20 re-seeding haves). Adopt it only if build evidence supports it.
• The doc(start): make public declarations findable and ordinary claims easy to state #578 recipe (the Codex worker's doc(complexity): add checked plain NP onboarding #603) cites these lemmas.

Wave 5: names (folded into the PR that touches each file, where possible)

• Problems:
  • membership as X.mem_C: UNSAT_mem_coNP, MAJSAT_mem_PP, PromiseUSAT_mem_PromiseNP, SAT_mem_FPT, KSAT_mem_FPT, VertexCover_mem_FPT;
  • hardness at the root (CookLevin.SAT_npHard and its siblings);
  • reductions as polyTimeReducible_A_B;
  • maps as Src.toTgt, with correctness as Src.toTgt_mem_iff;
  • the monotone and general circuit-value log-space reductions named by direction;
  • one spelling of sharpSAT.
• Classes:
  • lowerCamel Props inside names (NPComplete → npComplete in Ladner and DP);
  • constructors as mem_C_of_X (SharpP.of_polyTime);
  • one scheme for certificates, replacing the PCP isPolyTime_* names and the f_pt, f_inO and polyTime_f names, after S2 settles their plain names.
• Elsewhere:
  • no public h* names;
  • notMem;
  • PCPVerifier.Accepts (returns Bool) → accepts;
  • no Hastad.hastad… stutter;
  • headlines named by their conclusion rather than *_lower_bound;
  • one name each for leaf count and inner product.
• The class-acronym convention (P_subset_NP, Clique_npComplete) is consistent across 326 names and stays.

Wave 6: documentation and tests

11. doc(classes): cite sources (about 50 files, two PRs)

• Add references.bib keys to the definitions that lack them: 26 of 28 problem sets and 49 of 56 class definitions. (doc(classes): docstrings for listed results and citations for problems and classes #656)
• Add keys to the X_npComplete headlines. (doc(classes): docstrings for listed results and citations for problems and classes #656)
• Add References sections to the 27 modules without one (TreeEval/Reader/**, CookLevin/Correctness, Problems/Graph, …). (doc(classes): docstrings for listed results and citations for problems and classes #656)
• Cite Goldreich's Algorithm 1 in Reader/Defs. (doc(classes): docstrings for listed results and citations for problems and classes #656)
• Write docstrings for the roughly 80 main-result theorems that lack one. (doc(classes): docstrings for listed results and citations for problems and classes #656)

12. test(classes): nonvacuity gaps and plain-API examples (about 6 test files)

• Concrete members: (test(classes): nonvacuous examples for operators, exponential and resource classes #639)
  • for ParityOp and NE;
  • for BPTIME, NTIME and DSPACE beyond Set.univ;
  • for PPWithOracle beyond ∅.
• Yes and no instances through toKnapsack_mem_iff and toZeroOneIP_mem_iff. (test(classes): nonvacuous examples for operators, exponential and resource classes #639)
• Communication amplification. (test(classes): nonvacuous examples for operators, exponential and resource classes #639)
• The approximate-degree lemmas. (test(classes): nonvacuous examples for operators, exponential and resource classes #639)
• An instantiated Tree Evaluation space bound.
• Concrete MCSP and Kolmogorov examples.
• Epic-local axiom guards for NP_eq_PCP_log. (test(classes): nonvacuous examples for operators, exponential and resource classes #639)
• After S2, migrate the 53 tidy problem-test examples to plain.

Decisions and coordination

Decisions:

• PCP's noncomputable gap pipeline. PCP/GapTheorem, Dinur.* (about 40 declarations) and the legacy 17-query Encoded/Composition duplicate Encoded.gapGraph, have better constants, and have no library consumer. Proposal: keep the mathematics, cross-link the two pipelines and share the iteration argument (item 6), trimming only wrappers.
• Recorded, not acted on: the two randomized models (PMF in communication, StdSimplex in query complexity, with Yao's step proved twice) and the two Karchmer–Wigderson player conventions. They are settled when a guide chapter needs them.
• @[expose] narrowing follows perf(api): measure and shrink the public declaration surface #584's policy.

Coordination:

• doc(start): make public declarations findable and ordinary claims easy to state #578 items 2–4 stay with coordinator-codex-01a16ab8's worker (doc(complexity): add checked plain NP onboarding #603 touches Reduction.lean).
• doc(guide): a Verso guide that drives interface and documentation quality #585 M1's friction log feeds items 4, 10 and 12.
• quality(logics): area checklist #596: item 5 is item 1 here, and item 4 coordinates with items 5 and 7.