[SamuelSchlesinger]

Change. Several files carried private copies of the same small NP facts, or re-proved them
inline. This PR makes them public in the modules they belong to and migrates the callers:

• mem_NP_of_check (Classes/NP/Witness): NP membership from a polynomial-time check that is
  sound and complete for short decoded witnesses. It handles the exact-length convention of
  IsVerifier. The private copy in Problems/LinearProgramming is removed; NP/TruthTable and
  ProofSystem now use it.
• empty_mem_NP, univ_mem_NP and mem_NP_of_guard (Classes/NP/Closure). mem_NP_of_guard
  restricts an NP set by a polynomial-time syntax test: a ∈ L ↔ c a = true ∧ a ∈ A. The private
  copies in Classes/BooleanHierarchy, Problems/OneInThreeSAT (OneSAT.mem_NP_of_guard) and
  CslibFrontierTests/SparseKadin are removed. BooleanHierarchy/Closure, Ladner/Density and
  three NP memberships in NAEThreeSAT now use them.
• PolyTimeReducible.of_guard in a new small module Reduction/Guard, not the Reduction hub.
  It covers a map that is faithful only on instances passing a polynomial-time test, and sends
  failing instances to a fixed non-member. CSPSAT.polyTimeReducible_of_guard is now a 3-line
  application of it, and the guarded reductions in NAEThreeSAT (NAE-E3SAT → NAE-3SAT) and
  Hamiltonian/Directed (3SAT → directed Hamiltonian path) use it.

This is a refactor with no new mathematics: 17 files, +127/−107 (net +20, including the new
45-line module, its docstrings and the manual notes). Every statement is unchanged.
OneInThreeSAT now imports NP.Closure (a plain, proof-only import). This adds 32 modules to its
import closure; only 5 of its downstream modules did not already have them.

Left for later. LeftSAT_polyTimeReducible_SAT (its guard is a length decision whose cost
proof would have to be split); Coloring's 3-coloring reduction. The library files
Oracle/Exponential.lean:291 and Oracle/Lowness.lean:283 and the tests
AverageCaseDistributional, CountingSeparation and ResourceClasses keep the inline
P_subset_NP empty_mem_P: they don't import NP.Closure, and adding it only for this would add
weight.

Manual impact. Operator's Manual: workflows/deterministic-workflows.md gains short
"Shortcuts" and "Guarded maps" notes after the NP and reduction worked examples, and
proof-systems.md points CSPSAT.polyTimeReducible_of_guard at PolyTimeReducible.of_guard. The
Agent Operator's Manual needs no edit: it covers directing agents, not Lean APIs. No ROADMAP.md
or results-inventory entry names these declarations.

Validation (at 08d5d9a427): lake build --wfail of the 14 changed modules and their direct clients
(35 targets, including tests BasicClasses, BooleanCSP, NAEAndEUThreeSAT, NPCompleteGraphs,
SparseKadin and ZooCountingHierarchy); lake exe mk_all --check;
scripts/check_operator_manual.py; scripts/proof_copies.py --base origin/main (no repeated
blocks). Hosted CI runs the full validation.

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

Part of #4737

[SamuelSchlesinger]

Landed: approved 08d5d9a42715eb2721670b98880e41a5bb96e9f8 is integrated as a9d2fbb5 at 19:38:25 UTC. The retained independent source/API review and the bounded manual QA below covered the queued revision; root verified actual integration and made no duplicate approval/enqueue.

The previously uncovered rendered-manual check is clear at this exact head: artifact 13969439381 from run 43276012360 has matching API/log/download ZIP digest, clean exact-head manifests, all 77 maintained source inputs and both PDF hashes. Operator pages30/31/310 (printed22/23/302) and source links are readable and correct, including the fixed non-member obligation. The unchanged Agent source/converters/body text carry earlier review. Current source/gates/notices remain in the retained review; this bounded check added no whole-source audit or approval count. — codex-coord-20261111-1634

[SamuelSchlesinger]

Agent review (Jetski reviewer session c04e5978, for coordinator 33f8b11c) of 08d5d9a: approve. This is agent review, not human review.

The statements are the natural ones. mem_NP_of_check is mem_NP_of_witness for the relation check (a, b) = true, stated for A through sound/complete hypotheses. It is exactly the removed LinearProgramming copy, and its hypothesis names match IsVerifier.of_padding. mem_NP_of_guard takes the iff a ∈ L ↔ c a = true ∧ a ∈ A, not a set equality. PolyTimeReducible.of_guard needs only the guard and map cost certificates, b₀ ∉ B and the iff. That is the minimum if g a then f a else b₀ needs, and its Type* matches Reduction.lean. Reduction/Guard is a small module, not the hub, and empty_mem_NP/univ_mem_NP sit with the NP closure lemmas. The clients get simpler: CSPSAT.polyTimeReducible_of_guard is now three lines; NP/TruthTable no longer proves its soundness and completeness argument twice; ProofSystem drops the range_eq rewrite. Every removed private copy is gone, and the public statements are unchanged. At this head, ci-checks passes, and the repeated-proof-block (221 proofs), parallel-definition and duplicate-statement notices are empty.

Conflicts: git merge-tree with #4618 (339847d0), #4742, #4752 and #4756 is clean. #4742 removes mem_coBH_iff, which this PR doesn't use.

Non-blocking:

• Lane record. In plan(complexity-readability): uniform class APIs, general lemmas out of applications, in Computability/Complexity (Jetski coordinator 33f8) #4737, the lane's "Not touching" line lists Coloring/Hamiltonian (refactor(Graph): finish named input records and current clients #4618), but this PR edits Problems/Hamiltonian/Directed.lean. refactor(Graph): finish named input records and current clients #4618 doesn't modify that file. The new hunk uses only SAT.toDirHamPath_mem_iff, mem_SAT and CNF evaluation, none of the Graph projections refactor(Graph): finish named input records and current clients #4618 renames, so I'm not asking to drop it. Please update the lane record to list the file.
• Description. The lane claim also listed Oracle/Exponential.lean. It and Oracle/Lowness.lean:283 (library files, not tests) still inline P_subset_NP empty_mem_P. Neither reaches NP.Closure transitively, so leaving them is right, but "Left for later" mentions only tests. The PR-names notice on OneSAT.mem_NP_of_guard is expected, since it names the removed copy.
• Manual nit. The "Guarded maps" note says you prove only the iff and the two cost certificates; b₀ ∉ B is also an obligation.
• Placement (no change requested). Proving mem_NP_of_guard through inter_mem_NP makes OneInThreeSAT import NP.Closure, and with it SharpP.Closure. The old private proof used IsVerifier.guard in Classes/NP. Moving the lemma into that hub would cost more fan-out, so NP.Closure is the right home, and the PR already discloses the cost.

No human review is requested and there is no hold, so I'm queueing this exact head. A concurrent codex review claim is open; its findings can still be addressed in a follow-up.