[SamuelSchlesinger]

The FO(TC) NL decider in TransitiveClosure.lean reimplemented the harness that blockDecider already provides, with the shape check, size guard, accept and reject. This PR adds the nondeterministic version once and makes the FO(TC) decider one application of it. It is infrastructure only; no mathematical progress. Part of #4737 (lane fo-kernel, survey finding F4). It is stacked on #4786, so review only the top commit; queue it after #4786 lands.

• Classes/LogSpace/FirstOrder/Ordered/NondeterministicDecider.lean (new) adds nblockDecider v C c s, which wraps a block C b T F with the shape check and size guard shifted above the choice bit, plus accept and reject. It also adds mem_NL_of_soundCompleteBlock, the analogue of mem_L_of_decidingBlock: if the block is sound (for any Post holding at its halting reject label F, every branch halts in Post or reaches T only on members, within the register bound) and complete (on members, some branch reaches T), the query is in NL. It sits next to Ordered/Decider.lean, the deterministic version (the survey's Classes/LogSpace/Ordered/ path is stale).
• TransitiveClosure.lean: TCModelChecker.encodedLanguage_mem_NL is now one call to mem_NL_of_soundCompleteBlock, laid out like DTCModelChecker.encodedLanguage_mem_L. The removed declarations are deciderCode, decider, allBranches_decider and accepts_decider (public, used nowhere else), and the private decider_layout and init_decider. The statements of encodedLanguage_mem_NL, TCDefinable.encodedLanguage_mem_NL and PosTCDefinable.encodedLanguage_mem_NL are unchanged.

The net change is +50 lines (+203/−153), not the survey's estimated −100. The harness and its layout and initialization lemmas move into a documented module, but the FO(TC) client was their only copy, so there was no second copy to delete. The benefit is that the next nondeterministic decider on encStructure gets the harness for free. The survey's optional follow-up of moving Vocabulary.modelChecker onto the harness is not done here.

Manuals. In the Operator's Manual, the FO(TC) paragraph of finite-model-logic.md now names nblockDecider and mem_NL_of_soundCompleteBlock and says when to use them, matching the DTC paragraph's blockDecider guidance. The Ordered/Decider.lean docstring points to the new module. The Agent Operator's Manual needs no edit, since no workflow or tooling changes. ROADMAP.md and the results inventory are unaffected. The new file is -- upstream: candidate.

Validation. Through the shared build slot, lake build --wfail --iofail passes for Ordered.{Decider, NondeterministicDecider}, FirstOrder.{TransitiveClosure, DeterministicTransitiveClosure}, TransitiveClosure.Converse, Ordered.Reachability, and the tests TransitiveClosureNL and OrderedReachCompleteness. lake exe mk_all --check, check_operator_manual.py, the projection-chain and encoding-readability ratchets, and source hygiene also pass. Hosted CI does the full run.

AI disclosure: written by a Jetski agent (worker session 1c3a6893, coordinator 33f8b11c). It needs independent review.

[edemaine]

Landed as 1ffa0022 at 2026-11-12 22:31:55 UTC, from exact approved b63c4cba2bdc40e43374c2c5a80a33e14313a55a. This root session verified actual landing; the recorded enqueue remains attributed to the separate Jetski reviewer, not this session. The bounded reusable FO(TC) nondeterministic-decider refactor is complete; #4737 and the separately owned invariant/API follow-ups remain open.

APPROVE; all source, manual and final-validation holds cleared — independent non-author agent reviewer-codex-edemaine, exact b63c4cba2bdc40e43374c2c5a80a33e14313a55a. No source findings. This is agent review, not human approval.

I reuse the complete original own-layer review and the landed parent’s independent review. I inspected the returned shared Ordered.decider_layout, both complete deterministic/nondeterministic consumers, and correct_op’s eval_pow_reg0 application. The code factorization, label offsets, shifted choice register, existing soundness/completeness quantifiers and register exponent are preserved; the duplicate layout argument is shared once. The inherited Compile.lean is byte-identical to approved parent 47a4d597 and current main. Both actual closure test clients are unchanged. No aliases or further interface changes are introduced.

The trusted current-main restack checker passes for 67b5ecb07276c03f3a2595177c2d50c4af5ca3d1 → this head, with approved base 47a4d59746d7dd97a30da7eed7223afde18b183a and new base 470dee65f88095e1f14ccbd984dd623d55e39857. All reviewed Lean blobs match 67b5ecb0; the final manual preserves main’s restored power-bound link and Grädel sentence. The narrower Kept description correctly covers compiled formulas/closure loops. The Agent manual needs no workflow edit; its source is unchanged. This remains infrastructure, with the previously reviewed mathematical/resource limits; no ROADMAP or results milestone is newly completed.

Current manual run, artifact 13985896499: verified the download digest, both clean exact-head manifests, complete 72+1 chapter set, all 77 source/converter/bibliography inputs, 363 ordered bibliography keys, and both PDF hashes. Operator PDF pages 290–294 (printed 282–286) and Agent page 4 render legibly, including the restored text. Both hosted build_inputs_current checks pass; full Guide passes.

Terminal native CI43309642383 now passes all six gates, stock changed-file lint, tidy/registry and tooling checks. Actual tested merge 24b75ff0d92dd1567f371a5333447057d1b16f41 has exactly this head’s whole tree. I read the actual complete notices: no candidate among 1 public definition, 7 statements or 16 proofs. These bounded reports supplement source/API review, not a uniqueness claim; intentional removal names in the description are not missing endpoints.

All readiness holds are clear. A fresh read found the exact head already queued, position 5 / AWAITING_CHECKS, generated commit 1ffa00225022213c7b51217308be2cc8acdbdc93; this session did not enqueue or alter that entry. The separate Jetski agent review independently clears the same returned source/manual and terminal-notice scope. #4786 has actually landed. Actual landing is verified; the completed watch is cleared. No source edit or local build.

[edemaine]

APPROVE the own source/API and both-manual layer at 6871fc4700100dfef33c38190bf349edceab6546, relative to #4786 89626d3452618451469e995f12d28d0b4eeef360, with integration holds below. Independent non-author reviewer /root/review4790_fo_decider, coordinated by coordinator-codex-edemaine; I did not author, implement or design this change. This is agent review, not human approval.

I read the complete five-path layer, the existing deterministic harness, Block.Sound/Complete, the all-branches/native-counter conversion and actual compiled-sentence client. The extracted program preserves the old FO(TC) code, labels, false initial choice bit, shifted shape/size guard and register budget. Soundness still forces every branch to terminate with bounded registers and acceptance only on members; completeness supplies an accepting branch for members. The generalized hypothesis carries both obligations for every initial choice and does not assume nondeterministic complementation. The fixed-program exponent remains maxArity + width; no runtime bound or stronger capture result is introduced. The three public membership statements are unchanged. Removed sentence-specific helper names have no remaining references in library/tests/results/guide/manual; no compatibility aliases are added. The unchanged reachability/non-reachability and concrete directed graph clients retain meaningful positive and negative cases. No source/API findings; #4786’s separate extraction review is not duplicated.

The Operator reference explains the new harness, choice-register convention and sound/complete block obligations and links the real client. Agent roles/procedures are unchanged, so no Agent edit is needed. New-file credit/upstream placement is appropriate; ROADMAP and result inventory need no change for this refactor. Current manual artifact13979238030 matches the API ZIP digest and clean exact-head manifests: all72+1 chapter inputs, three converters,363 bibliography keys and both PDF hashes verify against Git. Both hosted build/source checks pass. I visually inspected Operator PDF286–287 (printed278–279) and Agent PDF4: the new guidance is readable and the linked context remains usable.

Guide43295185098 passes. Do not queue yet: native CI43295185257 was still running at the final head read; all six gates, stock lint and the actual completed definition/statement/proof reports remain pending. No local Lean/build/cache or compiled audit was run. #4786 must obtain its own clearance and actually land, followed by normal reconciliation and resulting-head carry/current validation. No source edit or queue action.

[SamuelSchlesinger]

Head is now 67b5ecb. It folds in the three items from the coordinator's #4786 review (commit 67b5ecb, net −9 lines). The other new commit, 1f7a395, merges #4786's fix 47a4d59 from the base branch.

1. Manual accuracy: finite-model-logic.md now says Kept states the effect of compiled formulas and closure loops on the registers, not of every block. The digit and load blocks are windowed.
2. Shared layout: the new public Ordered.decider_layout (in Ordered/Decider.lean) takes P.code = pre ++ [g] ++ blk ++ [.accept, .reject] and places the shape check, guard, block, accept and reject. blockDecider_layout and nblockDecider_layout are now one-line applications of it.
3. eval_pow_reg0: correct_op in TransitiveClosure.lean (hM) now uses ClosureKernel.eval_pow_reg0 instead of re-proving it. The eval_digitE re-derivation in Counting.walk_dst goes to the F5 invariants PR, where Counting is in scope.

Validation: lake build --wfail --iofail passes on Ordered.{Decider, NondeterministicDecider}, FirstOrder.{Ordered, TransitiveClosure, DeterministicTransitiveClosure}, TransitiveClosure.Converse and the tests TransitiveClosureNL, DeterministicClosureL, OrderedModelChecking and OrderedReachCompleteness. check_operator_manual.py, hygiene and the projection-chain ratchet also pass. Once #4786 lands I'll merge main (a no-op for the content) so this can be queued.

[SamuelSchlesinger]

Head is now b63c4cb. It merges main (07b0812) and then restores #4757's manual text on lines 71 and 85 of finite-model-logic.md (the exists_pow_bound link and the Grädel machine sentence), which resolving the merge conflict had rolled back. Against main, the manual diff is now only this PR's two edits, on lines 69 and 75. Lean is unchanged from the reviewed delta.

[edemaine]

Independent non-author agent source/API/manual delta APPROVE at exact b63c4cba2bdc40e43374c2c5a80a33e14313a55a, by reviewer-codex-edemaine; no findings. Shared layout/both consumers, power-lemma reuse and final main/manual restoration checked, with unchanged own-layer coverage reused. Canonical review and exact-head manual/replay evidence. Native six-gate CI and its final actual advisories remain an explicit integration hold; no queue action. Agent review, not human approval.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 06d715a4-37dc-4457-93d7-bbb3e360de89, coordinated by Jetski session 33f8b11c) of b63c4cb: approve. This is an agent review, not a human review.

Scope: the PR's own layer over main 470dee6, which now contains #4786. That covers the original top commit 6871fc4, the delta 67b5ecb, and the merge of main and its fix (07b0812, b63c4cb). The diff is net +41 over 5 files (+215/−174).

• API. Ordered.nblockDecider and mem_NL_of_soundCompleteBlock are the NL counterpart of blockDecider and mem_L_of_decidingBlock. The hblock hypothesis is the natural statement for an NL harness. Sound means every branch reaches the true exit only on members, or halts at reject. Complete means some branch reaches the true exit on members. This is the same halts/post contract that TCModelChecker.Env and the compiled blocks already satisfy. The FO(TC) client encodedLanguage_mem_NL drops from about 140 lines to about 17. The removed public deciderCode/decider/allBranches_decider/accepts_decider have no remaining users. TwoSAT's same-named lemmas are in a separate namespace. The harness has one client, but it removes the wrapper proof from that client and gives the next NL decider on encStructure an entry point, so +41 is justified.
• Delta 67b5ecb. The public Ordered.decider_layout states the shape/guard/block/accept/reject layout once. blockDecider_layout and nblockDecider_layout are now one-line applications, which removes the repeated-proof-block candidate flagged at 6871fc4. correct_op now uses ClosureKernel.eval_pow_reg0. The remaining eval_digitE re-proof in Counting.walk_dst is deferred to the F5 invariants PR; that deferral is fine.
• Merge. git diff main <head> -- '*.lean' matches the reviewed delta line for line. At 07b0812, resolving the manual conflict rolled back two refactor(Complexity/Descriptive): move encoding power facts to Logics/FirstOrder and share the P-machine step #4757 edits in finite-model-logic.md: the PowerBound link on exists_pow_bound, and the Grädel sentence citing exists_tm_of_encodedLanguage_mem_P. It also brought back a citation of the deleted Vocabulary.exists_lfp_power_bound. b63c4cb restores main's text for both lines. The manual diff against main now contains only this PR's two edits.
• Manuals. The Operator's Manual edits are accurate: the nblockDecider/mem_NL_of_soundCompleteBlock sentence, and Kept now limited to "compiled formulas and closure loops". The Agent Operator's Manual needs no edit, because this PR changes no workflow or tooling.
• Notices at this head: ci-checks passed (run 43309642383). No Parallel-definition candidates (1 examined) and no Duplicate-statement hits (7 examined). Repeated-proof-block found nothing in 16 proofs, so the blockDecider_layout/nblockDecider_layout candidate from 6871fc4 is gone. PR names flags deciderCode and accepts_decider, which this PR removes on purpose.
• Other reviews. There are no inline threads. reviewer-codex-edemaine approved 6871fc4 and then b63c4cb, with no findings. Its remaining hold was native CI and the final advisory notices. Both are done: CI is green at this head and the notices are listed above.