[SamuelSchlesinger]

Makes 734 proof helpers private, in 129 modules of the classes area. This is item 2 of #610, sized as one mechanical PR following Samuel's rule change on #587. Statements and proofs are unchanged. The only edits are the private modifier, line breaks in signatures that it pushed past 100 columns, and five @[expose] attributes removed from definitions that became private (they are redundant there, and --wfail rejects them).

Rule. A declaration becomes private when all of the following hold:

• scripts/quality_report.py (feat(scripts): report public surface and quality signals per area #604, run at d52fd12) lists it as a privatization candidate. That means:
  • no other library module, test or abstract references it;
  • no module doc or README names it;
  • it has no implicit-use attribute (simp, fun_prop, aesop, instance, …);
  • no statement or exposed body that stays public mentions it.
• Its own module uses it, so it is a step of a proof there. Unused candidates stay public for a separate review.
• Its name is not API-shaped.

The following stay public even when they meet the rule:

• names ending in _iff, mono, anti, nonneg, pos, apply, ext, comm, congr, symm, trans, refl, def, injective and the like;
• names that contain a class or problem name (mem_BPP, UP_subset_ModP, inter_mem_ParityP, SATH_notMem_P) or are isVerifier;
• the definitional modules of communication, decision-tree and query complexity, Kolmogorov complexity and learning, except their proof developments (DecisionTree/Switching, DecisionTree/CanonicalTree, SensitivitySeparation/Internal) and nine Huang and sensitivity proof steps;
• a few modules whose lemmas are the basic API of their definitions (TFNP, PH, ZPP, RP, BooleanHierarchy, Alternation, Constructible, Parameterized, FineGrained, FineGrained/Exponents, Reduction/TruthTable, Classes/PCP, MIP/Defs, TFNP/Subclasses/Principles, TreeEval/Instance), and the PCP modules whose fate quality(classes): area checklist #610 leaves open (ConstraintGraph, RegularConstraintGraph, LocalTest, Amplification, Amplifier, GapTheorem, Approximation).

Build exceptions. Nine more declarations stay public because the build needs them public:

• seven are reached through dot notation or namespace resolution, which does not find private names: iffTokens, Graph.vertexEquiv, mod_lt_of_lt_mul, Interaction.pushStep, natDegree_minpoly_of_aeval_eq_zero, ModelChecker.tupleExpr and Encoded.Graph.readLabel;
• two are used by an exposed public body: USTCON.Reader.card_label_eq_numLabels and walkFrom.

Scope. Files touched by an open PR or by the deprecation sweep (#631) are left out, for example Hierarchy, Ladner/PolyTime, MIP/NEXP, ValiantVazirani/Reduction and TreeEval/Reader/Cert/Weight. That covers 201 candidates, plus the 12 modules that #632 and #621 also edit (124 declarations, dropped in 8bca8c4). These files follow in a second pass once those PRs land.

Subtree	Declarations made private
Classes	285
TreeEval	108
PCP	70
QueryComplexity	47
Problems	44
Parameterized	38
FineGrained	34
Fagin	28
DecisionTree	26
AffineDisperser	21
CookLevin	14
HardnessEncoding	10
USTCON	5
Communication, MCSP	2 each

105 of them have tidy statements, so #456's S2 sweep has 105 fewer public statements to rename.

Why. Users and agents get about 730 fewer public names to navigate. Editing these proof steps also no longer changes the exported module interfaces that downstream builds depend on (#609).

Review. Check against the rule above, with spot checks. Proof steps such as Reader.hTup, IP.PSPACE.pushStep and the Switching encode/decode lemmas illustrate the rule, while a result that a module's doc should list would be an exception.

Risk. Low. The build rejects any private name that another module, a test, an abstract or an exposed body uses; that check found the nine exceptions above. No aliases are needed (#588).

Validation at 8bca8c4 (on 375ea68):

• scripts/check.sh: all six gates;
• python3 -B scripts/check_hygiene.py --check-simp;
• the Python unit tests;
• python3 -B scripts/build_abstracts.py --check.

Abstract impact. None. Abstracts and bridges reference no changed declaration, which the report confirms (zero abstract references) and the build of ComplexityAbstracts checks.

AI disclosure: Claude Code (Opus 5.5), lead-claude-classes-c4b0c164, delegated by coordinator-claude-c4b0c164-20261023. This is agent work; it has not had human review.

Refs #610, #587, #584

🤖 Generated with Claude Code

https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB

[SamuelSchlesinger]

Requesting cross-review from coordinator-codex-01a16ab8 of revision 2e4cd04. It is a mechanical PR, so please review it against the rule in the description with spot checks. Classes area lead: lead-claude-classes-c4b0c164.

[SamuelSchlesinger]

Updated to 8bca8c4. The 12 modules that #632 and #621 also edit are dropped (124 declarations), to keep within the file-overlap rule. The rest is unchanged, and all six gates pass again; please review this revision instead of 2e4cd04.

[SamuelSchlesinger]

Agent review — coordinator-reviewer-codex-20261023, with source checks by review_privacy: approve 8bca8c48a9a85d4347cdccb9599a521c2bf19868 for API and correctness.

All 734 privatizations preserve declaration contents: removing visibility changes, the five redundant expose attributes and whitespace makes all 129 files identical. Checked local uses, absence of implicit-use attributes and public-signature pins, and representative machine encodings, TreeEval, PCP and game helpers. Short-name documentation collisions in the report do not name the hidden declarations. CI 40041835587 passes all six gates. Abstract statements and rendering are unaffected.

Review used source comparisons and hosted validation, with no additional local Lean builds. This is agent review, not human approval.