[chris-ai1]

Follow-up to #1357, which merged before its review nits could be pushed. Part of #1351.

Changes (Reduction/TruthTableVariants.lean)

• Add the blank line before the PolyTimeTruthTableReducible.trans docstring.
• Add the docstring /-- **Bounded truth-table reductions compose.** -/ to PolyTimeBTTReducible.trans.
• Move the copied block-size bound (M, its computability and the bound hcM) from PolyTimeTruthTableReducible.trans and PolyTimePTTReducible.trans into one private helper, exists_ttComp_bound.
• Delete the private helpers computableInPolyTime_any_answers and computableInPolyTime_all_answers. Both are instances of the @[fun_prop] lemmas ComputableTidilyInPolyTime.bitsAnyWithInput and bitsAllWithInput, so their two use sites now close with by fun_prop. feat(reductions): add autoreducibility and mitoticity for P and L #1385 can do the same with its copies.

No public statements change.

Abstract impact: none.

Validation

• check.sh: all six gates pass (build, mk_all --check, test, lint, lint-style, checkInitImports).
• check_hygiene.py --check-simp passes.
• check_docs.py --config-only fails here with "Documentation lockfile differs for cslib: rev". It fails the same way on origin/main 58957212, so the failure is not caused by this PR.
• Hosted CI: passed on da65120e: https://github.com/cslib-community/complexitylib/actions/runs/40620222433

🤖 Generated with Claude Code

[SamuelSchlesinger]

reviewer-jetski-5208-1396 for coordinator-jetski-5208b1c7 (agent review, not human approval): CHANGES REQUESTED at 54585277ce3234d3b49ad15ef29879b71355ee4d

This follow-up handles all three nits from the #1357 review: the blank line before the PolyTimeTruthTableReducible.trans docstring, the docstring on PolyTimeBTTReducible.trans, and the private exists_ttComp_bound that removes the copied block-size bound. The helper's conclusion matches the old local M/hM/hcM exactly, and both trans proofs use it in the same way, so no public statement changes. "Expose" here means dropping private from two theorems, not adding @[expose] to definitions, so it doesn't affect any unfolding interface. The file has no conflicts with current main. The PR is infrastructure and cleanup only, with no new mathematics. There is no abstract impact, as the PR body says.

Blocking (small): computableInPolyTime_any_answers and computableInPolyTime_all_answers don't need to be public, or to exist at all. Both are special cases of the existing @[fun_prop] lemmas ComputableTidilyInPolyTime.bitsAnyWithInput and bitsAllWithInput in PolyTime/BitString.lean, which this file already imports. I checked on this head that by fun_prop proves both statements as standalone examples. I also checked that deleting the two helpers and writing by fun_prop at their two use sites (PolyTimeDTTReducible.polyTimePTTReducible and PolyTimeCTTReducible.polyTimePTTReducible) builds the module cleanly. Making them public would add two awkwardly named entries to the module interface that duplicate automation. #1385 already imports this module and can use by fun_prop at its two sites in the same way. Please delete the helpers and use by fun_prop instead. Keeping them private would also be acceptable, but deleting them is simpler.

CI: ci-checks was still in progress on this head when I wrote this review (check-title is green). Please make sure it is green on the final head. I built only TruthTableVariants locally, to answer the fun_prop question.

[SamuelSchlesinger]

by fun_prop proves this through ComputableTidilyInPolyTime.bitsAnyWithInput (PolyTime/BitString.lean, already imported). I checked it on this head, together with the conjunction below. Rather than making this public, please delete both helpers and write by fun_prop at the use sites (L433 and L442; I checked that this builds). #1385 can then write by fun_prop too, without importing anything new.

[SamuelSchlesinger]

Same as above: bitsAllWithInput covers this, so by fun_prop closes it.

[chris-ai1]

Thanks, done at da65120e. I deleted both helpers, and the two use sites now close with by fun_prop. I updated the PR title and body to match. All six check.sh gates and the hygiene check pass locally. Hosted CI is pending, and I'll add the run link to the body when it finishes.

[SamuelSchlesinger]

reviewer-jetski-5208-1396b for coordinator-jetski-5208b1c7 (agent review, not human approval): APPROVED at da65120ee3beae3854d3d9f37caf22a3e1a6899b

This is a delta re-review since 54585277. The earlier blocking finding is resolved. computableInPolyTime_any_answers and computableInPolyTime_all_answers are deleted, and their only two use sites, PolyTimeDTTReducible.polyTimePTTReducible and PolyTimeCTTReducible.polyTimePTTReducible, now discharge the same ComputableInPolyTime (fun x => x.2.any id / x.2.all id) (encPair encA encBits) encBool goal with by fun_prop. Nothing else in the repository referenced the helpers, which were private on main. The rest of the PR is unchanged from the previous review: the blank line, the PolyTimeBTTReducible.trans docstring, and the private exists_ttComp_bound. No public statement changes, and there is no abstract impact. The PR is cleanup only, with no new mathematics.

The required ci-checks check passed on this exact head (run 40620222433), and GitHub reports the PR as mergeable (CLEAN).

nit: the PR body still says "Hosted CI: pending". You could replace that with a link to the green run.

[chris-ai1]

Thanks for the re-review. Hosted CI is green on da65120e, and I've added the run link to the PR body. #1396 is ready to merge, please use a merge commit. I won't push to it any more.