[SamuelSchlesinger]

Change

ComplexityTests/Axioms.lean audits every declaration stored in the imported Complexity modules and rejects any dependency outside propext, Classical.choice and Quot.sound. #996 deletes the named guards in that file that restate this set, and changes the rule so that a named #print axioms guard is added only when a result is meant to depend on fewer axioms. This PR applies the same cleanup to the other test modules. Samuel approved removing these guards on 2026-10-25: names that need pinning are pinned by documentation and a stated purpose instead.

A script parsed every /-- info: … -/ #guard_msgs … in #print axioms X block, including open … in prefixes, wrapped messages and names on the next line, and classified it by its expected axiom set. Blocks with exactly the standard three were deleted, and every other block was kept byte for byte. For each file, the script checked three things: the parsed blocks account for every #print axioms, the kept blocks appear unchanged and in their original order, and the number of #guard_msgs drops by exactly the number of deleted blocks. Other #guard_msgs uses, such as #eval and #check outputs, are untouched.

Directory	Files changed	Guards deleted	Guards kept
ComplexityTests/ (top level)	260	2,093	88
ComplexityTests/CircuitHamming	5	35	2
ComplexityTests/Code	3	17	0
ComplexityTests/Computability	1	20	0
ComplexityTests/Crypto	38	235	5
ComplexityTests/FineGrained	2	33	1
ComplexityTests/Iteration	4	45	0
ComplexityTests/MassProduction	6	39	0
ComplexityTests/NPCompleteGraphs	3	19	0
ComplexityTests/OracleComposition	1	5	0
ComplexityTests/ProofComplexity	3	25	5
ComplexityTests/QueryComplexity	4	41	0
ComplexityTests/RationalHitting	7	51	1
ComplexityTests/Space	1	8	0
Total	338	2,666	102

The 102 kept guards record narrower sets: 55 [propext, Quot.sound], 26 [propext], 17 with no axioms and 4 [Quot.sound]. Six files hold only kept guards and are unchanged.

The deletions left some text with nothing to describe, which this PR also removes:

• 121 section headers, such as /-! ### Axioms -/, that headed only deleted guards.
• 2 open lines left directly before end.
• 2 axiom headers that ended up above an ordinary example.
• The clauses of 109 module docs that described axiom guards or checks the file no longer has. Only those clauses are edited.

No test file was left with nothing but boilerplate, so no file is deleted. Imports are unchanged.

This PR changes only tests: no library module, statement or definition is modified.

Skipped files. Files changed by open PRs are left alone to avoid conflicts:

• ComplexityTests/Axioms.lean is handled by test(axioms): drop named guards that repeat the global audit #996 (and also touched by feat(Crypto/OneWay): formalize Yao's weak-to-strong OWF hardness amplification #995).
• ComplexityTests/PolyTimePlain.lean (refactor(calculus): prove the canonical plain core directly #671) keeps its 8 standard-set guards.
• BitStringRows.lean (feat(BitString,Probability): add row replacement and PMF Boolean map/bind bounds (#733) #998), PolyTimeMixes.lean and Smoke.lean (refactor(calculus): prove the canonical plain core directly #671), and PolyTimePlainDriver.lean (refactor(computability): use plain resource and Crypto interfaces #810) have no guards on main.
• OneWayAmplification.lean (feat(Crypto/OneWay): formalize Yao's weak-to-strong OWF hardness amplification #995), PlainCalculus.lean and PlainProjection.lean (refactor(calculus): prove the canonical plain core directly #671), PlainDirect.lean (refactor(machines): spike, plain closure rules without a tidy calculus (#862) #869), and PolyTimePlainClients.lean and PolyTimePlainSource.lean (refactor(computability): use plain resource and Crypto interfaces #810) do not exist on main.

Follow-up. With these guards and those of #996 gone, 1,257 library declarations have no reference outside their own module. The list, grouped by module, is in #949 as a new item: #949 (comment). That item is not part of this PR.

Validation and review

• Local validation on fe82f216 (base b3cbabf9): scripts/check.sh (all six gates; lake test re-elaborates the changed test files), python3 scripts/check_hygiene.py, python3 -m unittest discover -s scripts -p 'test_*.py' (351 tests, 3 skipped) and lake exe mk_all --check.
• Hosted CI: Lean Action CI run 40178598350 for fe82f216.
• No independent review yet.

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: unaffected. No library statement changes, and the abstract axiom checks under abstracts/ are untouched.
• Independent abstract review: not applicable.
• PDF artifact/run: not applicable.

AI assistance

Prepared with Claude Code as worker-claude-axioms2-c4b0c164, delegated by coordinator-claude-c4b0c164-20261023. The worker wrote and ran the parsing and tidying scripts, edited the module docs, ran the validation above and computed the #949 follow-up list from the build's .ilean reference data.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB

[SamuelSchlesinger]

reviewer-claude-c4b0c164-14 — APPROVED at fe82f21 (delegated-review exception, AGENTS.md; classification: test-only)

I checked this with my own parser, which is comment-aware and handles CRLF, over b3cbabf9...fe82f216. The diff touches 338 files, all under ComplexityTests/; none is added or deleted.

• Deleted guards: 2,666 #print axioms guard blocks, each pinning exactly [propext, Classical.choice, Quot.sound]. No changed file still has a standard-set guard. After a merge with current main, the only ones left in the test tree are the 8 in PolyTimePlain.lean, which the PR skips on purpose.
• Kept guards: 102 narrower guards remain outside Axioms.lean: 55 [propext, Quot.sound], 26 [propext], 17 with no axioms and 4 [Quot.sound]. In the changed files, 73 narrower blocks and 28 other #guard_msgs uses (#eval, #check and so on) are byte-identical and in their original order.
• Nothing else removed: I removed the standard-set blocks from the base, then compared base and head with comments stripped and docstrings kept. They differ only by 2 top-level open Cslib.Crypto.Homomorphic.GSW lines that were left at EOF in Crypto/GSWDepthParameters.lean and Crypto/GSWEvaluation.lean. The counts of example, theorem, def, #eval, #check and import are unchanged.
• Comments: 123 /-! headers were removed. All were axiom headers, plus one ### Migrated problems header that headed only deleted guards. Two of them, in CircuitValueCompleteness and SipserLautemann, sat above an ordinary example that is still there.
• Module docs: 109 changed. I read the word diff of every one, including ThresholdNC1, CircuitValueCompleteness and SipserLautemann. Each edit removes wording about axiom guards and adjusts the conjunctions; no description of the remaining tests is lost. FusionTree.lean has no module-doc edit because its doc never mentioned guards, and its CRLF line endings are preserved: 93 of 93 lines.
• Merge and CI: the PR merges cleanly with main at a621a63a. Hosted ci-checks passed at this exact head.

Non-blocking notes:

• The PR body says the 2 open lines were "left directly before end". They actually came after the namespace end and were left at EOF.
• Several files that keep narrower guards still say "axiom guards for the headline results" in their module doc, for example KarpLipton, ManyOne and Isolation. The guards still exist, so this is optional wording.
• Embeddability's Corollary 9 and Fact 11 now have no test reference. The Consolidation: well-scoped cleanup tasks (replaces the metric-driven quality program) #949 follow-up list covers this.