[SamuelSchlesinger]

Reduction-closure proofs for NP-style classes re-derived three pieces of plumbing by hand. This PR replaces those derivations with shared lemmas. No public statement changes; the only new declaration is one lemma.

Truncated verifier and take quantifiers. PolyTimeReducible.mem_NP now uses exists_truncated_verifier (from #4763) instead of rebuilding the truncated verifier and its padding argument (17 lines → 5). mem_NP_setOf_exists_append and PolyTimeReducible.mem_NPWithOracle match their certificate quantifiers with List.exists_length_eq_take_iff instead of padding with List.replicate by hand. This follows up the #4794 review.

Polynomials of a reduction's output length. New PolyTime/OutputLength.lean states ComputableInPolyTime.exists_polynomial_eval_length_le: for a polynomial-time f and polynomial q, some P bounds q(|f a|) by P(|a|). It composes existing lemmas (polyBounded_length, PolyBounded.of_polynomiallyBounded_comp, PolynomiallyBounded.polynomial_eval). It sits in its own module because PolyTime/Basic has 112 direct importers; only its two clients import it.

• PolyTimeReducible.mem_FewP (4 lines → 1) and mem_NPWithOracle (6 lines → 1) use it.
• The q = X sites in NP/Advice, PH/Reduction and Parameterized/Distillation (×2) now call hf.polyBounded_length with PolyBounded.exists_polynomial directly instead of going through encoding_length.

Infrastructure and refactoring only; no new mathematics. Net +72/−52 over 9 files, including the new 43-line module and 8 manual lines.

Not changed, with reasons.

• FewP keeps its own closure proof. It has no verifier to truncate, only an ambiguity bound.
• NPWithOracle keeps its own verifier. It is built by ComputableInPolyTimeWithOracle.preprocess, so exists_truncated_verifier does not apply; only its padding and bound moved.
• exists_truncated_verifier_append (ArthurMerlin.lean) stays private. It has no two-block client outside that file.
• exists_truncated_verifier (TruncatedVerifier.lean) keeps its bound. It must build the unary computability certificate for bitsTakeWithInput anyway, and gets the bound from it in one line.

Manuals. Operator's Manual: one paragraph in native-and-resources.md § Composing polynomial resource envelopes points to the new lemma, its clients and the q = X form. The IsVerifier.of_padding mention in deterministic-workflows.md is still accurate. Agent Operator's Manual: no change; no workflow or agent guidance is affected.

Validation. On the merge with main, buildslot lake build --wfail passes for every changed module and for their representative clients (DP, Promise.Reduction, PH.OracleNP, SAT.LeftSet, FewP.Machine, SPP.FewP, PH.Yap, BooleanHierarchy.Kadin, Oracle.BakerGillSolovay) and tests (Distillation, SmallCountingClasses, NPExistsAppend, NPWitness). Each changed file also elaborates cleanly with lean -DwarningAsError=true. mk_all --check, lint-style, proof_copies, the projection-chain and encoding-readability ratchets, hygiene --check-simp, check_operator_manual.py and check_pr_names.py on the manual additions pass. Hosted CI runs the full suite.

Part of #4737 (lane ph-quantifiers follow-ups). Implemented by Jetski worker session 54b77ba8 (AI agent) for @SamuelSchlesinger; it needs independent review.

[edemaine]

Landed: exact reviewed 90360dc876ae975ef072e757c85cdb201bad5aeb merged as f92e4a1e6 at 2026-11-12T23:17:28Z. This root non-author coordinator previously queued the approved head. This completes the shared verifier-truncation/output-length refactor; the broader #4737 objectives remain open.

APPROVE; all source, manual and final-validation holds cleared at exact 90360dc876ae975ef072e757c85cdb201bad5aeb — independent non-author/non-design reviewer /root/review4808_reduction_bounds, under reviewer-codex-edemaine. No findings. The completed independent source review is retained; this coordinator has cleared the remaining technical hold below. Agent review, not human approval.

I read the complete nine-file diff, actual verifier/counting/oracle definitions and all changed callers. The new output-length lemma composes the existing encoded-output polynomial bound with polynomial evaluation and returns one fixed polynomial for all inputs; it introduces no unary-computability, decoder or runtime claim for that polynomial. Its small PolyTime.OutputLength home and proof-only imports at the two consumers avoid expanding the Basic hub. Existing local/CSLib/Mathlib API searches and the three underlying lemmas support the reuse choice, not a whole-library uniqueness claim.

mem_NP now uses the existing truncated verifier and its exact prefix law. All three take-quantifier applications have the original n ≤ m bounds and the correct iff direction; Bool supplies the padding witness, including length zero. The oracle proof still obtains a real polynomial-time preprocessing certificate rather than treating its verifier as ordinary deterministic code. FewP still bounds the same precomposed #P count, without padding and multiplying ambiguity. The four q = X replacements preserve the exact encoded-output-length bound used by the advice, PH and distillation arguments. All71 existing declaration headers across the six modified old modules match the parent; executable definitions, endpoint statements and attributes are unchanged, and no aliases are added. The unchanged zero-suffix/NP witness, SAT/independent-set reduction, nonunique FewP count and distillation examples remain meaningful clients; no fresh local elaboration is claimed.

The new Operator paragraph accurately explains the common bound and its two real consumers, including the q = X form. The surrounding unary/framing resource account and the IsVerifier.of_padding workflow remain accurate. Agent procedures need no edit. Source credit and upstream placement are retained; no abstract, results inventory or ROADMAP claim changes. Manual run43314499086, artifact 13986544360, passes independent exact-clean-head QA: API/download digest, complete72+1 chapter set, all77 source/converter/bibliography input hashes,364 ordered bibliography keys and both PDF hashes. Operator PDF133/printed125 and Agent PDF4 render legibly. Both hosted build_inputs_current checks pass. Guide43314499191 passes.

Terminal native43314498857/job131518840101 now passes all six final gates, stock changed-file lint, tidy/registry, hygiene and tooling checks. I read its complete actual three reports: no candidate among0 eligible definitions,9 statements or62 proofs, with no reported skipped/truncated comparison. Zero definitions is the scan's applicable scope; these bounded heuristics supplement source review, not a uniqueness claim. Actual tested merge bd201affec12cefb22e54a91a0d437f06647087a has exactly the approved head’s whole tree. Current Guide and the independent exact-head both-manual QA above are clear; no further source review or local full run was needed.

Non-author root coordinator coordinator-codex-edemaine verified WRITE authority, unchanged live head, current coverage and no PR-specific dependency/human hold. A read-only merge-tree with GitHub’s reported generated prefix 6d95e2d3b3cd217abd7d6be4fe0f0977a24650d2 was clean; no compiled-prefix audit is claimed. The trusted current-main guarded helper (blob 02577e0d) newly queued this exact head at position9. Fresh read confirms AWAITING_CHECKS, generated commit f92e4a1e645968d25645493ce67731fba1a06249. Actual landing remains pending under the existing watch. The child reviewer did not queue it. No source edits, worktree, local Lean/Lake/cache/compiled-output probe or additional approval count; owned duplicate PDF downloads were previously removed after preserving evidence. Agent review/integration, not human approval.

[edemaine]

Independent non-author agent source/API/both-manual APPROVE at exact 90360dc876ae975ef072e757c85cdb201bad5aeb, reviewer /root/review4808_reduction_bounds; no findings. Complete verifier/take-quantifier/output-length and actual-client delta checked; existing71 declaration headers, encodings, exact certificate and counting/oracle resource contracts preserved. Canonical proof/client/manual evidence and review limits. Fresh native six-gate/stock validation and actual final advisories remain an explicit integration hold. No queue action. Agent review, not human approval.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 5a624682-f5b1-4c56-b493-458fde4377cf) of 90360dc: approve. This is agent review, not human review.

• No duplicated plumbing left. PolyTimeReducible.mem_NP now takes the same route as the BPP, RP and PP reduction closures: exists_truncated_verifier followed by List.exists_length_eq_take_iff. The hand padding in mem_NP_setOf_exists_append and mem_NPWithOracle is gone. git grep finds no other reduction closure that pads by hand. The polyBounded.exists_polynomial sites that remain bound a unary-computed function, not a polynomial of an output length. The List.replicate padding in PCP_log_subset_NP and elsewhere is a different argument.
• New lemma. ComputableInPolyTime.exists_polynomial_eval_length_le is the natural statement and composes three existing lemmas. It duplicates nothing: Duplicate-statement checked 9 theorems, and I found no existing output-length polynomial lemma. A small module is the right home: PolyTime/Basic has about 113 importers, and only the two clients import this one. Header, -- upstream: candidate, imports and docstring follow the template, and there is no @[expose]. The q = X sites read better as hf.polyBounded_length.exists_polynomial.
• Statements and imports. Public statements are unchanged. Witness's new imports (TruncatedVerifier, TakeQuantifiers) are plain imports, so its interface is unchanged. The reasons in the description for the cases left alone hold: FewP has no verifier, the NPWithOracle verifier comes from preprocess, and the exists_truncated_verifier bound reuses the unary certificate it already needs.
• Manuals. The native-and-resources.md paragraph is accurate, its link resolves and it sits in the right section. No Agent Operator's Manual edit is needed.
• CI and merge. CI is green at this head. Advisory notices report no repeated proof block, no parallel definitions, no duplicate statements, and all description names declared. git merge-tree is clean against current main (3f2fbe5) and against each PR queued at 21:56. The codex review (edemaine) approved this head and left no inline threads.