[SamuelSchlesinger]

Restates the logspace autoreducible and self-reducible truth-table variants (reductions survey F5, LogSpace half) on the kernel from #4798.

Change.

• LogSpaceTruthTableAutoreducible, LogSpaceKTruthTableAutoreducible and LogSpaceTruthTableSelfReducible keep their spelled-out bodies. Their resource conditions, any query bound, and query avoidance or locality are now grouped into one conjunct (⟨r, q, d, ⟨⟨hr, hq, hd⟩, hne⟩, hA⟩), so each is a TruthTableReducibleBy instance.
• The forgetful lemmas, LogSpaceKTruthTableAutoreducible.mono and LogSpaceTruthTableSelfReducible.logSpaceTruthTableAutoreducible become TruthTableReducibleBy.mono applications.
• New: LogSpaceKTruthTableAutoreducible.compl, from the kernel's compl_left/compl_right. It matches PolyTimeKTruthTableAutoreducible.compl.
• LogSpaceKCTTReducible.autoreducible_of_compl now follows from the KDTT case by De Morgan duality plus compl. That removes the 18-line KDTT/KCTT proof copy (proof_copies.py now reports none). The source mapping now says clause (3) goes through complement duality, as in the paper's Propositions 2.5/2.6.
• LogSpace{DTT,CTT}SelfReducible keep their base/if r a = 0 form (Definition 3.2), as the survey recommended.

Net is +6 lines: library ±0, tests +4 (a compl example), manual +2. The gain is not in lines. It removes the 18-line proof copy, adds a reusable complement-closure lemma, and makes these definitions consistent with the kernel instances from #4798. Refactoring only, with no new mathematics, apart from the small compl closure lemma. The PolyTime half of F5 is done in #4798.

Manual impact. Operator's Manual: one sentence in manual/machines-and-classes/reductions.md (autoreductions paragraph). It says the logspace autoreducible notions add avoidance to the kernel's Good, and names LogSpaceKTruthTableAutoreducible.compl and the duality route for the conjunctive case. Agent Operator's Manual: no edit, since it covers workflow rather than reduction APIs.

Validation (at b6ea863, merged with main 3066bf8, which includes #4798): buildslot lake build --wfail of the three changed modules, LocalSelfReducibility.VirtualWord, and the three changed tests plus CslibFrontierTests.VirtualWord; python3 -B scripts/check_operator_manual.py; check_pr_names.py on the added manual lines; the encoding readability and projection chain ratchets; scripts/proof_copies.py (no repeated block). Full validation by hosted CI.

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

Part of #4737.

[SamuelSchlesinger]

Landed: reviewed head b6ea86339d00 merged as ad05b9b072 at 2026-11-13T01:26:42Z. The shared logspace truth-table kernel and migrated callers landed; broader #4737 remains open.

Independent non-author review — coordinator codex-coord-20261111-1634, reviewer worker codex-review-logspace-tt-kernel-20261112, at b6ea86339d00dfdcc2d06d12b87ed39d7b928e62. Technical review is complete; no findings remain. The concurrent exact-head approval by Jetski reviewer 39f68e58 and its existing enqueue are reused. This is agent review, not human approval; I made no source edit, additional approval or queue mutation.

I read the complete six-file delta, all three affected theorem modules, the changed tests and the bounded-autoreducibility/VirtualWord clients. The landed kernel is byte-identical to the reviewed #4798 version. Regrouping the three native predicates preserves all original resources, encodings and quantifiers: unary count/index, evaluator on (a,answers), the same uniform k-bound and avoidance/locality only below the active count. Locality still means equal encoded length, strict lexical descent and the ceiling-log suffix window. Its forgetful map keeps every certificate and uses strict descent to exclude equality. The explicit base-answer branches of DTT/CTT self-reducibility are retained; replacing them with empty OR/AND would change the model. Public availability/exposure and imports are preserved, and no alias or parallel representation is added.

The new LogSpaceKTruthTableAutoreducible.compl is a substantive native corollary, reviewed beyond declaration preservation. Kernel left-complement then right-complement produces !d(a, answers.map (!·)); the count and query map, bound and avoidance certificate remain unchanged. Existing native Bool negation/word mapping and composition supply the evaluator certificate, in the original logspace model with independent halting/time and work-space obligations. It does not assert an identical numerical evaluator clock. The conjunctive proof has the correct orientation: from Aᶜ ≤k-ctt A, duality gives A ≤k-dtt Aᶜ; suppression gives an autoreduction of Aᶜ, then complement closure returns one of A, with the same k. This genuinely removes the old copied argument and gives a checked consumer for the small shared lemma in its natural autoreducibility module. No new private helper is needed.

The existing clients are non-vacuous: the Boolean singleton and its complement exercise one query; the two-query OR/AND witnesses include active self-queries on opposite membership branches; the full-OR/empty-AND witnesses exercise k=0 through the new proof route. Inactive self-queries remain unrestricted. The local singleton permits both zero-query base answers, and the empty-word-language client also has a genuinely active, strictly descending query. VirtualWord's inhabited zero/one/three-length native access examples remain clients of the unchanged locality facts. None of this proves an unbounded native self-reduction evaluator or the Lemma 3.3 transfer.

I checked the changed proof-route attribution in the expanded ECCC TR13-047 PDF, dated 18 March 2013: Proposition 2.7(3)'s proof invokes Propositions 2.5 and 2.6, matching the duality/complement route. The paper assumes k≥1; this library's documented at-most-k, k=0 extension and explicit encodings/L-evaluator convention remain visible. No quotation is added. Christian Reitwiessner's source credit is preserved. The full #2468 objective, serialized-oracle correspondence and later-paper results remain open; no new headline/catalogue endpoint or ROADMAP completion is claimed.

Current both-manual artifact 13994076320 has its ZIP digest matched to API/upload log, both PDF hashes verified, exact clean-head manifests and all 77 source inputs independently checked against current GitHub bytes (72 Operator chapters, one Agent chapter, three converters and bibliography). Both hosted input/PDF checks pass. I inspected Operator PDF 166/printed 158 and its exact-head source/test links: the new sentence is accurate and readable, with the broader #2468 gap retained. Agent chapter/converter inputs and full rendered text match previously reviewed #4798 inputs after revision-stamp normalization; I also viewed its current title. Its workflow scope is unchanged, so no Agent edit is needed. This is input/text carry, not PDF byte identity. The bounded artifact work remained below 30MB with the 3 GiB floor guarded.

Full Guide compilation passes; HTML generation/upload was skipped. Completed native job 131565864220 passes all six gates, unmodified stock changed-file lint (three library modules), tidy (481 statements in 60 modules), and compiled registry references (206 groups, 793 theorems, 166 keys). The registry explicitly retains its broader coverage/source-review limitation. HTTP succeeds; cache publishers were skipped. The actual native checkout is synthetic merge ce6fdc4; its tree 4dacad54 is identical to the reviewed head, as also confirmed by the complete API comparison with no changed files.

I read all three complete actual advisory reports in that job: 32 proofs have no repeated block; three changed public definitions have no candidate pair; 12 examined theorems have no exact statement match. No report is truncated or records a scan skip. There are therefore no reported candidate pairs needing a two-sided disposition. These are bounded scans: definition comparison excludes same-module pairs, statement-key equality misses specializations and inline re-derivations, and proof-block matching is heuristic. They supplement the source/client/pinned-upstream review above; empty reports do not establish uniqueness. No local compiled-output duplicate query was run under the hosted-only constraint.

A fresh GraphQL read confirms this exact head is open, MERGEABLE/CLEAN and already queued at position 11, AWAITING_CHECKS. I did not run another enqueue helper. The coordinator retains merge-group/actual-landing watch and the open #2468 scope. No local Lean/MCP/Lake/cache/build/compiled query or Git operation was used.

[SamuelSchlesinger]

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

The merge of main (3066bf8, which contains #4798 as d2d59cd) keeps the landed kernel unchanged, and the delta against the merge base is line-for-line the one I reviewed at 8126215/a41adc7449 (6 files, +66/−60). LogSpaceKTruthTableAutoreducible.compl is the kernel's compl_left then compl_right, with the count, queries, bound and avoidance certificate unchanged. The KCTT autoreducible_of_compl now goes through dttReducibleBy_iff_cttReducibleBy_compl, the KDTT result and .compl, which removes the 18-line KDTT/KCTT copy. The k = 0 and two-query test witnesses still exercise both routes.

CI is green on this head. Notices: no repeated proof block (32 proofs examined); no parallel definition (3 examined); no duplicate statement (12 examined); all 15 PR-description names declared.

Threads: no inline threads. The codex review (issuecomment-6839385406) reports no source or manual findings; its hold was on the CI notices, which are now in.

Manuals: the Operator's Manual sentence in reductions.md matches the new proof route and keeps the #2468 gap visible. The Agent Operator's Manual needs no edit, since the workflow is unchanged.

Queueing this head.