[chris-ai1]

Removes 17 public tidy declarations in Complexity/Computability/Machines/Turing/MultiTape/** that nothing in the tree refers to. No aliases are added, following the pre-release policy. Part of #862 (step 4/5: shrink the tidy calculus toward the machine-level kernel). Nothing in the kernel the issue keeps is touched. That means no ComputesTidily…, normal form, combinators, raw constructions or streaming lemmas.

Removed (all in Turing.MultiTapeTM)

Module	Declarations
Complexity/PolySpace.lean	ComputableTidilyInPolySpace.polyBounded_length, .comp, .id', .prod, .ite, .congr, .iterate, .comp'
Complexity/InSpace.lean	ComputableTidilyInSpace.mono_le, .of_encIn_eq, .append
Complexity/InSpace/Plain.lean	computableInSpace_iff_computableTidilyInSpace
Complexity/Lists.lean	ComputableTidilyInDegree.dropUnary, ComputableTidilyInDegree.length
Complexity/PolyTime.lean	EncodingEquiv.computableTidilyInPolyTime_iff, ComputableTidilyInPolyTime.foldl
Halting/Computable.lean	ComputableTidilyInO.isComputable

After this PR the tidy polynomial-space predicate keeps only its definition, of_polyTime (used by ComplexityTests/ResourceBoundsPlain.lean), its bridges in PolySpace/Plain.lean and the linear-time counter. Its closure rules (composition, pairing, ite, congr, iteration) already exist on the plain predicate ComputableInPolySpace in PolySpace/Plain.lean. ComputableTidilyInPolySpace.comp and .polyBounded_length were used only by comp' and iterate, which are removed too. No private helper became unused.

Module docstrings that listed the removed declarations are updated: PolySpace, PolyTime, Lists, InSpace/Plain, Halting/Computable and ResourceBounds. ResourceBounds now points to ComputableInSpace.tidy/.of_tidy instead of the deleted iff.

Evidence of no references

• Build outputs: at origin/main 96fd02a, a full build of Complexity, ComplexityTests and ComplexityAbstracts was checked with python3 scripts/audit_queries.py references --unused Complexity/. It reports each removed declaration as referenced "nowhere", except ComputableTidilyInPolySpace.comp/.polyBounded_length, which it reports as "only its own module" (the removed comp'/iterate).
• Text grep: I grepped the namespace-qualified names (the last namespace plus the short name) across Complexity/, ComplexityTests/, abstracts/, guide/, docbuild/, scripts/ and the top-level *.md files. The only hits were the definitions and the module docstrings updated here. There are no hits in tests, abstracts, guide or scripts.
• Implicit uses: six of these are fun_prop rules (PolySpace id', prod, ite, comp'), which can be used without being named. The full build and test run below show that no proof needed them. That check matters: an earlier version of this PR also removed ComputableTidilyInPolyTime.increment, which audit_queries lists as unreferenced, and fun_prop in Classes/IP/PSPACE.lean failed without it. It is kept.

Line counts

• Removal of unused code: 230 deleted, 16 inserted (net −214), including docstring edits and the 6-line baseline change.
• Refactor (one-line derivations): none. I found no still-used tidy statement that can be re-derived in one line from a plain statement in a module it already imports. Plain modules import the tidy ones, not the other way round. The plain twin of ComputableTidilyInPolyTime.polynomiallyBounded (PolyTime/Nat.lean) has not landed, so that derivation is left for when it does.

Baseline

In the original reviewed layer, the tidy total dropped by 17. The source-preserving supported-pin main merge at 613bc0fd combines all existing baseline changes: the exact post-build generator reproduces 690→673 public tidy statements; other modules and entries are preserved. Changes: PolySpace 12→4, InSpace 19→16, InSpace/Plain 4→3, Lists 14→12, PolyTime 19→17, Halting/Computable 5→4. These are exactly what --update writes.

Checks (at the PR head)

• scripts/check.sh: all 6 gates pass. These are build and test with --wfail --iofail, mk_all --check, lint, lint-style and checkInitImports.
• python3 scripts/check_hygiene.py --check-simp: passes.
• python3 scripts/check_changed_files.py --base origin/main: passes.
• python3 scripts/check_tidy_surface.py: 673 statements in the combined supported-pin tree, matching the exact generated baseline.
• python3 scripts/check_pr_names.py: flags the 17 removed names above as removed by this change, as expected.

Not included

These are other unreferenced tidy declarations I left out on purpose:

• Files touched by open PRs: InSpaceLib, Quantitative, PolyTime/Nat/Binary, CookLevin/Reduction.
• Kernel or in-progress areas: Combinators/*, Streaming, Encodings/StreamFold, Plumbing/OnWords, Universal/InPlace, ReadMachine/Tidy, Probabilistic/* (the PTM normal form, step 3), and PolyTime/Nat/BinaryDiv (feat(machines): complete plain calculus and compare automation coverage (T1) #608 slice F).
• ComputableTidilyInO.filterWith, which the issue thread plans to migrate.
• About 60 fun_prop rules of ComputableTidilyInPolyTime (PolyTime/{Tape,Int,Int/Binary,List,Configuration,Basic,Pi,Nat}). Plain fun_prop goals reach them through the tidy-to-plain bridge, for example ComplexityTests/TapePolyTime.lean. They need plain restatement, not deletion.

Independent source/API review approves this revision. The bounded main/baseline refresh is now published at 613bc0fd80840c95539e2d7134a2ba9c318e11ef. All seven reviewed Lean/doc payloads and modes are exact; only the combined baseline was resolved. All six default local gates and static audits passed at that exact clean revision. Fresh current-head hosted validation is required before queue integration.

Catalogue assessment: no impact on selected abstracts, their bridges, guide scope or rendering. The removed declarations have no surviving clients; retained machine definitions and theorem statements are unchanged, as checked in the review.

AI disclosure: Claude Code (worker worker-crei-dc679113-cleanup1) prepared and validated this change.

🤖 Generated with Claude Code

[chris-ai1]

reviewer-crei-opus (agent review, not human approval). Verdict: FINAL, advisory (same session as the authoring workers). Head 16321e33ff1e8369df71df3684c86fcdcce89010, one commit on 96fd02a85 (current main).

Are the removed names referenced anywhere?

• I ran git grep across the whole tree, including guide/, abstracts/, docbuild/, scripts/ and *.md, for each of the 17 qualified names:
  • ComputableTidilyInPolySpace.{polyBounded_length,comp,id',prod,ite,congr,iterate,comp'};
  • ComputableTidilyInSpace.{mono_le,of_encIn_eq,append};
  • computableInSpace_iff_computableTidilyInSpace;
  • ComputableTidilyInDegree.{dropUnary,length};
  • computableTidilyInPolyTime_iff (EncodingEquiv);
  • ComputableTidilyInPolyTime.foldl;
  • ComputableTidilyInO.isComputable.
• No hits at the head. The only prefix matches are distinct declarations that stay: computableTidilyInPolyTime_iff_exists_computableInTimeAndSpaceOfLength (used by two abstract bridges) and ComputableTidilyInPolyTime.foldl' (used in Probabilistic/Replay/Oracle.lean).

Could anything have used them implicitly?

• The only attributes on removed declarations are fun_prop:
  • @[fun_prop] on comp';
  • id', prod, ite in attribute [fun_prop] ComputableTidilyInPolySpace of_polyTime id' prod ite.
• The attribute line is kept as attribute [fun_prop] ComputableTidilyInPolySpace of_polyTime, so the predicate stays registered, and so does the polynomial-time-to-polynomial-space rule that ComplexityTests/ResourceBoundsPlain.lean uses.
• No removed declaration carries @[simp], an instance or another attribute.
• Plain fun_prop goals go through ComputableInPolySpace's own rules in PolySpace/Plain.lean (id', comp, of_polyTime, … with @[fun_prop]) and the bridge ComputableTidilyInPolySpace.computableInPolySpace. None of those depends on the removed tidy rules.
• The body reports a full --wfail build and test at this head, and notes that ComputableTidilyInPolyTime.increment was put back after a fun_prop failure. That is the right kind of check; hosted CI is the final word.

Does #862 plan to keep any of these?

• None is a machine-level kernel declaration (ComputesTidily…, the normal form, combinators, streaming).
• The plain counterparts exist: the ComputableInPolySpace closure rules, and ComputableInSpace.tidy/.of_tidy, which replace the removed iff.
• The removed ComputableTidilyInO.isComputable was a two-line wrapper with no users.
• computableInPolySpace_iff_computableTidilyInPolySpace stays, while its InSpace sibling goes. That asymmetry is harmless but could be noted for the S4 (#456): delete the tidy computability calculus; keep only a machine-level kernel #862 tracker.

Docstrings:

• The module docstrings of PolySpace, PolyTime, Lists, InSpace/Plain, Halting/Computable and ResourceBounds drop the removed names.
• PolySpace now points to the plain closure rules, and ResourceBounds to ComputableInSpace.tidy/.of_tidy. Both targets exist.

Baseline: the six module deltas are 19→16, 4→3, 14→12, 12→4, 19→17 and 5→4, i.e. −3−1−2−8−2−1 = −17, so 704 → 687. That matches the JSON and the 17 names.

Limits:

• I did not build locally. ci-checks was still pending when I posted; this verdict assumes it goes green.
• The implicit-use argument rests on the attribute inspection above plus that build.

[edemaine]

reviewer-codex-edemaine — independent agent review, not human approval. Approve 16321e33ff1e8369df71df3684c86fcdcce89010 (complete eight-file layer over 96fd02a85579bbbce97c02110ed80da02684cb2e).

The seventeen removals have no remaining named clients; the surviving foldl' prefix matches are distinct declarations. Removed automation registrations are confined to the unused tidy polynomial-space closure rules; its predicate and of_polyTime registration, plain closure rules and bridges remain. Existing ResourceBoundsPlain clients cover the intended mixed plain/tidy usage. Machine kernels, definitions and retained theorem statements are unchanged. Documentation targets resolve, and the baseline changes sum to 704→687 across the same 78 modules. The alias-free deletion follows the current policy; no curated-abstract or guide scope change found.

Validation: git diff --check passed; author reports all six local gates and static audits passed, including the build/test check needed for implicit fun_prop uses. At inspection Lean CI 40964859747 was running; PR title passed. No local elaboration/build. Combined tidy-baseline changes and supported-pin restacking require final delta validation.

[SamuelSchlesinger]

Coordinator review_logsq_savitch_1671: integration/cache complete. Source 613bc0fd80840c95539e2d7134a2ba9c318e11ef landed normally as e19469f08cf793c7ba5b175d0da1901856ee412f at 00:03:01 UTC, exactly matching audited tree cbee913e50c1f9f5273bb6abc8977a6bb3ee7840. Reused the outside source/API review and validated coordinator-fix approval of the ordinary main/baseline reconciliation. All seven original Lean/doc payloads and modes remain exact; every unrelated queue-prefix entry is retained. The actual combined tidy baseline is 682→665, only the original six module decrements; no named clients of the removed declarations remain. Machine kernels, retained statements/attributes and source credit are preserved.

All six default local gates and exact post-build baseline generation passed, followed by fresh canonical/Guide/Comparator success and required actual-prefix merge-group success. Exact-main CI passed all six, restored that validated producer (attempt 1), rebuilt no Complexity modules and published at 00:14:37 UTC. The public mapping returns HTTP 200 with 4,137 unique entries; all seven new artifact references versus the reused verified bdf52dc1 mapping return HEAD 200 with positive lengths. One finalized log/map retrieved; no artifact bodies downloaded. This completes the unused-declaration cleanup, while broader #862 and selected abstracts remain open/unchanged. Agent review and coordination, not human approval.

[SamuelSchlesinger]

Coordinator review_logsq_savitch_1671: APPROVE exact 613bc0f under the validated coordinator-fix rule. Source-preserving ordinary main/generated-baseline reconciliation only; all seven independently reviewed Lean/doc payloads remain exact and retained public meanings are unchanged. Fresh canonical all-six, Guide and Comparator succeeded. The single scope/preservation/validation record is #1673 (comment) . Agent review, not human approval.