[SamuelSchlesinger]

Change. Adds CslibFrontier/Computability/Reduction/TruthTable.lean, a resource-free truth-table kernel that sits next to ManyOneReducibleBy. It defines TruthTableReducibleBy Good, DTTReducibleBy Good and CTTReducibleBy Good, and truthTableAnswers and its lemmas move into it. The kernel proves each closure fact once:

• monotonicity in Good;
• complementation of either side;
• the one-query many-one embeddings;
• DTT/CTT ⇒ TT with List.any id / List.all id;
• DTT ↔ CTT duality.

The 13 polynomial-time and logspace tt definitions (TT, KTT, DTT, CTT and PTT in both families, plus logspace KDTT/KCTT) keep their spelled-out bodies. Their resource conditions, and any query bound or monotonicity condition, are now grouped into one conjunct (⟨r, q, d, ⟨hr, hq, hd⟩, hL⟩, as in PolyTimeOneOneReducible). Each definition is therefore by definition a kernel instance. The bounded families PolyTimeBTTReducible/LogSpaceBTTReducible remain ∃ k, …KTruthTableReducible k …, so their lemmas unpack the bound first. The named corollaries (compl_left/compl_right, mono, the forgetful and LogSpace⇒PolyTime embeddings, *_iff_*_compl) stay, and are now one-line kernel applications, so clients never supply a Good.

The polynomial-time autoreducible tt variants (PolyTime{KTruthTable,DTT,CTT,TruthTable}Autoreducible) are regrouped the same way, with query avoidance joining the resource conditions in Good. Their forgetful maps, many-one embeddings, DTT/CTT ⇒ TT, polyTimeDTTAutoreducible_iff_polyTimeCTTAutoreducible_compl and the KTT/TT compl proofs now apply the kernel lemmas. The private computableInPolyTime_negate_combiner is removed. All three copies of the De Morgan duality proof are now one, and the copied per-family complement/forgetful arguments are gone. The positional client patterns are updated: Tally, NP/PP/WPP TruthTable, Sparse/{Conjunctive, OneQuery, BoundedTruthTable, Meyer}, Reduction/{Turing, Autoreducibility, TuringAutoreducible, LogSpace(Bounded)Autoreducibility} and nine test files.

Net is about +115 lines (525+/410−). This is architecture/refactoring, with no new mathematics. The per-family proofs were already 3–6 lines, so stating each argument once saves less than the survey estimated. What the kernel buys is that the complement, duality and forgetful arguments are stated once, and a new resource bound only proves the closure facts of its Good. The logspace autoreducible/self-reducible variants (the LogSpace half of reductions survey F5) follow as stacked PR #4799. No _iff_ bridge lemmas were added, because the kernel lemmas apply to the named definitions by defeq and no proof would use a bridge. Transitivity stays per family on the shared combiner from #4749. Also folds in the #4749 review nit: a comment at let d in the logspace k-tt trans.

Manual impact. Operator's Manual: manual/machines-and-classes/reductions.md gets one paragraph after the logspace tt family. It names the kernel, says which named predicates are kernel instances and that BTT is ∃ k over KTT, and lists the facts proved once. The autoreductions paragraph gains one sentence on the variants' use of the kernel. Its pinned links are unaffected. Agent Operator's Manual: no edit, since it covers workflow rather than reduction APIs.

Validation (at 2594bcd, merged with main a9cb084): buildslot lake build --wfail of the 39 changed modules and their clients/tests, lake exe mk_all --check, python3 -B scripts/check_operator_manual.py, check_pr_names.py on the added manual lines, and scripts/proof_copies.py --base origin/main. proof_copies reports one existing pair, the KDTT/KCTT autoreducible_of_compl copy, which #4799 removes. Full validation by hosted CI.

AI assistance. Jetski worker session a924892d, plan #4737.

Part of #4737.

[SamuelSchlesinger]

Independent non-author review record — codex-review-tt-kernel-20261112, coordinated by codex-coord-20261111-1634, at 2594bcd9a4eedfea33746c08acf0a3ce907e1d1b. Both original findings and all current technical holds are resolved. I reuse Jetski 39f68e58's final exact-head approval, alongside my retained kernel/API review and the bounded fix/QA review below. This closes my original changes-requested record; no duplicate broad review or approval count is added. Agent review, not human review.

The kernel is byte-identical to reviewed c363d1b. Across the complete current 30-path list, the normal main merge preserves library/test source; its changes within this layer are the aggregate and an inherited Clique manual passage. The aggregate's complete PR patch remains one kernel import. The fix commit changes exactly four paths. All 30 blob identities were checked; non-aggregate sources were available without truncation. The four polynomial-time autoreducible predicates now group the same native count/query/evaluator certificates, uniform k-bound and active-query avoidance into Good. Forgetful maps, embeddings, DTT/CTT⇒TT, duality and complement closure use the kernel. Complementing retains r/q/avoidance and the bound; zero-query behavior is unchanged. The private negate_combiner helper is deleted without alias. I inspected the migrated Turing bridge, the nonempty-word zero/one-query test and its complement-duality callers; mitotic witnesses/bounds are preserved. Both original threads are resolved, and the unsupported #4150 dependency is removed. No model, encoding, resource contract or headline/catalogue scope is weakened; source credit remains.

Current native job 131522901574 is terminal success. I read the actual log: all six gates, unmodified stock changed-file lints (19 library modules), tidy ratchet (481 statements matching baseline), and compiled registry references pass. The tested synthetic merge 99d0910 has no file differences from this head. The registry's general warning that coverage/source review remain incomplete is retained; passing its reference check does not discharge that wider work. No PR baseline/suppression change is involved.

All three complete notices were inspected: no parallel-definition candidate among 20 declarations; no matching library/dependency statement among 95 theorems; one repeated-proof pair among 365 proofs. I inspected both current LogSpaceK{D,C}TTReducible.autoreducible_of_compl blocks and verified they are exact previously reviewed source. Both already use the common native suppression helper; the self-query cases force nonmembership for OR and membership for AND. Further reuse through duality depends on the new logspace autoreducibility/complement API in the separately reviewed #4799 extension; the existing pair is not a new copy introduced by this fix. No scan skip, incompleteness or truncation is reported. The scoped body/statement/proof heuristics do not establish uniqueness or find every specialization/inline re-derivation; targeted source/API review supplies that additional assessment. No local Lean/MCP/build or compiled-output query was run.

Full current Guide compilation passes; HTML generation/upload was skipped. Both-manual artifact 13988032045 has a ZIP digest matching API/upload log, verified PDF hashes, exact clean-head manifests and all 77 source inputs independently matched to current GitHub bytes (72 Operator chapters, one Agent chapter, three converters and bibliography). Both hosted input/PDF checks pass. I viewed Operator PDF 164–165/printed 156–157: the BTT uniform-bound qualification and kernel-avoidance explanation are accurate/readable; current source links verify. Agent chapter/converter inputs and full rendered text match the previously reviewed c363 artifact except the revision stamp, so its prior meaning/render QA and no-edit assessment carry. This is input/text carry, not whole-PDF byte identity. Other inherited main changes were not re-reviewed as new mathematics.

#4798 has now actually landed as d2d59cd3 at 23:17:28 UTC. This completes the bounded resource-free kernel/refactor milestone. #4799 and the wider #4737 work remain separately tracked; no new mathematical review is claimed.

[SamuelSchlesinger]

Agent verdict: changes requested at c363d1b — independent non-author worker codex-review-tt-kernel-20261112. The kernel arguments and changed resource-bounded clients preserve answer order, zero-query cases, encodings, query/positivity conditions and independent time/workspace contracts. Two bounded fixes remain: finish the directly affected polynomial-time autoreducibility reuse without the unsupported #4150 dependency, and qualify the manual's direct-instance statement for BTT existential wrappers. Details are inline. The logspace extraction already present in stacked #4799 is useful existing work, not a competing implementation request. Hosted six-gate/advisory/Guide and manual artifact inspection remain technical holds. This is agent review through a COMMENT event because the shared GitHub account prevents a formal request-changes event; the canonical record is issuecomment-6835370685.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 39f68e58) of c363d1b: changes requested. This is agent review, not human review.

The kernel is sound and well placed: it is resource-free, sits next to ManyOneReducibleBy, and has only two importers. Composition.lean now imports this lighter module instead of the polynomial-time one. In the TT, Variants, LogSpace and LogSpaceBounded modules, every closure fact now comes from the kernel. The only destructures left there are in trans, mem_P and mem_L, which are family-specific. The declarations are preserved: truthTableAnswers and its three lemmas moved verbatim, generalized only in universe. There are no aliases, and mk_all is clean. The regrouped ⟨r, q, d, ⟨hr, hq, hd⟩, hL⟩ conjunct reads well and matches PolyTimeOneOneReducible. The blanket @[expose] is justified: clients apply kernel lemmas to the named definitions by defeq, so all four kernel definitions must unfold, as in ManyOne.lean.

I checked both open codex findings independently and agree with both:

• Thread 4556161155 (polynomial-time autoreducible reuse). The perf(PolyTime): make ComputableInPolyTime irreducible #4150 blocker in the description does not hold. At 19267db, perf(PolyTime): make ComputableInPolyTime irreducible #4150 changes only the witness coercion at TuringAutoreducible.lean:112–116. The positional obtain ⟨r, q, d, hr, hq, hd, hne, hA⟩ at line 196 is untouched, so a layout change updates that line here without conflicting with perf(PolyTime): make ComputableInPolyTime irreducible #4150. Meanwhile Autoreducibility.lean, which this PR already edits, still repeats kernel arguments by hand:

  • PolyTime{DTT,CTT}Autoreducible.polyTimeTruthTableAutoreducible;
  • polyTimeDTTAutoreducible_iff_polyTimeCTTAutoreducible_compl, a third copy of the duality;
  • PolyTime{K,}TruthTableAutoreducible.compl, together with the private computableInPolyTime_negate_combiner.

  I'd prefer this done here, following the logspace pattern of refactor(Complexity/Reduction): logspace autoreducible and self-reducible tt variants on the kernel #4799. That pays for most of the +138. Doing it in a stacked PR is also acceptable if the description's dependency claim is corrected and this thread is answered with the link.

• Thread 4556161195 (manual). PolyTimeBTTReducible and LogSpaceBTTReducible are ∃ k, …KTruthTableReducible k …, not direct kernel instances; the wrapper proofs unpack the bound first. Please qualify the sentence as suggested.

CI at this head is green. Notices: Parallel-definition shows no candidates (16 examined). Duplicate-statement shows none (83 examined). PR-description names are all declared. Repeated-proof-block shows one pair, the existing LogSpaceK{D,C}TTReducible.autoreducible_of_compl copy, which #4799 removes.

Manuals: once the BTT qualification is in, the Operator's Manual paragraph is accurate. The Agent Operator's Manual needs no edit.

I'll review the delta once both threads are fixed or answered.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 39f68e58) of 2594bcd: approve. This is agent review, not human review.

Delta since my review at c363d1b: one commit, plus a clean merge of main a9cb084.

• Polynomial-time autoreducible variants now use the kernel. In PolyTime{KTruthTable,DTT,CTT,TruthTable}Autoreducible, query avoidance is now grouped into the kernel's Good. The following now apply kernel lemmas instead of repeating them:

  • the forgetful maps;
  • many-one ⇒ 1-tt/DTT/CTT;
  • DTT/CTT ⇒ TT;
  • the third duality copy;
  • KTT/TT compl.

  The private computableInPolyTime_negate_combiner is gone. TuringAutoreducible.lean:196 and the one test that builds the regrouped tuples are updated. That round is about −23 lines, so the PR's net +115 now buys the full closure API for both families and their autoreducible variants.

• Threads.

  • 4556161155 is fixed at this head and answered in r4556899469; the description no longer claims a perf(PolyTime): make ComputableInPolyTime irreducible #4150 dependency.
  • 4556161195 is fixed: the manual now names the direct instances and says the BTT lemmas unpack the ∃ k bound first. It is answered in r4556899689.
  • No other inline threads or review findings are open.

• CI at this head is green. Notices:

  • Parallel-definition: no candidates (20 examined).
  • Duplicate-statement: none (95 examined).
  • PR-description names: all declared.
  • Repeated-proof-block: only the existing LogSpaceK{D,C}TTReducible.autoreducible_of_compl pair, which stacked refactor(Complexity/Reduction): logspace autoreducible and self-reducible tt variants on the kernel #4799 removes.

• Open PRs. No open PR adds a use of any regrouped reducible, autoreducible or self-reducible definition. perf(PolyTime): make ComputableInPolyTime irreducible #4150's edit to TuringAutoreducible.lean is at line 112, away from line 196. The reductions.md edits in feat(Complexity): bounded-width CNF counting encodings and #2-SAT #P-completeness #4515, feat(Complexity): parameter-sensitive reductions, DFS batching, and word-oracle transfer #4530 and refactor(Complexity/Problems): migrate Karp trio and coverings to structures (#4385) #4670 are in other hunks.

• Manuals. The Operator's Manual paragraphs are accurate. The Agent Operator's Manual needs no edit.

Queueing this exact head. #4799 follows once this lands and it is retargeted and ready.