[SamuelSchlesinger]

Shared mask witnesses for the sub-multiset NP problems (graph survey F2 and F1 of #4737), plus the queued manual fix for PolyTimeReducible.of_guard.

Change

F2, placement. maskSelect is a generic list operation. It moves from Problems/SubsetSum/Mask.lean to Foundations/Data/List/MaskSelect.lean, next to SelectDistinct, and keeps its names and namespace. The scattered mask facts move with it:

• sum_maskSelect comes from IntegerProgramming;
• MaxCut's inline index form becomes the public maskSelect_eq_map_filter_range.

computableInPolyTime_maskSelect moves to Classes/NP/Witness.lean, next to computableInPolyTime_selectDistinct. Mask.lean is deleted with no shim (pre-release).

F1, witnesses. Witness.lean gains a Mask section mirroring the Subset section: maskVerifier, isVerifier_maskVerifier, computableInPolyTime_maskVerifier (@[fun_prop]) and mem_NP_of_subMultisetWitness.

• The SubsetSum, Knapsack and Partition verifiers are now maskVerifier instances. Their isVerifier and polynomial-time proofs are now single applications of the new lemmas, replacing three hand-rolled exists_le_iff_exists_maskSelect arguments.
• Statements are unchanged, and the rfl/decide verifier examples in NPCompleteNumbers still evaluate.
• A new test applies mem_NP_of_subMultisetWitness directly.
• The check input encPair enc (encList encγ) of both sections is named encWithEntries, a documented reducible abbrev, as the encoding-readability rule requires once four statements spell it out.

length_le_length_encPair. The survey suggested moving it to the list-encoding length lemmas. Instead, the PR deletes it and writes it at its four uses as (length_le_length_encList _ _).trans (length_le_encPair_left _ _ (x.numbers, x.target)), a composition of two existing lemmas. The candidate homes for a named lemma are Complexity/Lists.lean and Encodings/Pair.lean, which are vendored, and Encodings/Length.lean, which has about 2,700 dependents. A new public declaration there would rebuild all of them for a one-line lemma.

Net: 10 files, +166/−102, counting the moved file as a rename. This is infrastructure and refactoring; there is no new mathematics.

Left for later

Nothing from F1/F2. SubsetSum now imports Witness publicly, because its exposed verifier unfolds to maskVerifier. The new lemmas therefore reach its importers; Witness was already in their closure.

Manual impact

• Operator's Manual (workflows/deterministic-workflows.md):
  • The NP "Shortcuts" note now names mem_NP_of_subsetWitness and mem_NP_of_subMultisetWitness. Before this PR it named no Witness.lean helper for selection certificates.
  • The "Guarded maps" note now lists the b₀ ∉ B obligation of PolyTimeReducible.of_guard, as requested in the refactor(Complexity/NP): public NP guard and check lemmas, guarded reductions #4750 review.
• Agent Operator's Manual: no edit needed. It covers directing agents, not these Lean APIs.

No ROADMAP or results-inventory entry is affected.

Validation

At 6bb79b7 (the review fixes rebuilt MaskSelect, Witness and its 34 direct importers):

• buildslot.sh lake build --wfail on 44 targets: every changed module and every direct importer of Witness, MaskSelect, SubsetSum, Knapsack, Partition, IntegerProgramming and MaxCut, including the tests NPCompleteNumbers, NPWitness, NPExistsAppend and MaxCut.
• lake exe mk_all --check, check_operator_manual.py, check_hygiene.py --check-simp on the changed files, and proof_copies.py --base origin/main (no repeated blocks), check_encoding_readability.py --base origin/main.

Hosted CI runs the full validation.

AI assistance

Written by Jetski worker session f9cb2f1f (plan #4737). Not yet reviewed.

Part of #4737.

[SamuelSchlesinger]

Independent review record — worker codex-review-mask-witness-20261112, coordinated by codex-coord-20261111-1634, at a7342c9f36be5f9c9b3172532d814fa671218f38. Agent review, not human review.

Source and manual findings are clear; validation remains on hold. The returned commit changes only the requested manual sentence. It now explicitly requires hP and accurately distinguishes duplicate-free candidate lists from sublists of the entries. I verified that delta and resolved the original finding. All Lean source, imports, attributes and tests are byte-unchanged from reviewed 6bb79b7c46, so that source/API/caller assessment carries.

That review covered the complete own delta, moved definition/facts, sibling subset API and actual SubsetSum, Knapsack, Partition, MaxCut and ZeroOneIP callers. maskSelect preserves order and positional multiplicities, treats missing bits as false and ignores excess bits. The exact-length mask verifier and generic NP wrapper preserve binary encodings and independent time/workspace contracts. Exposed verifier bodies, ordinary imports, fun_prop, source credit and moved names remain available. Existing accepted/rejected, empty-input, repeated-value, long-mask and large-binary tests remain, plus the direct generic NP client. The four deleted length-helper calls are clear existing-API compositions; no additional abstraction is needed. Targeted source/API searches supplement this review without claiming compiled uniqueness.

Both-manual QA is clear. For the current artifact, the ZIP digest matches the API/upload log, both PDF hashes verify, and both hosted current-input/PDF checks pass at the exact clean head. Of the 77 previously verified source inputs, only the requested chapter changed; I checked its new hash against the current GitHub source and verified all remaining input hashes are unchanged. I inspected current Operator PDF pages 30–31 (printed 22–23), the helper/Guard links and Agent title. The corrected helper instructions and explicit b₀ ∉ B guard obligation render clearly. Agent source/converters and complete rendered text apart from the revision stamp remain unchanged, supporting the existing no-edit rationale and review carry.

The cancelled 6bb native job's actual proof-block report examined 112 proofs with no candidates; that source-only result carries across this prose-only fix. It was not a full-validation pass. Current native CI is still running; completed six-gate/stock-lint/tidy checks and actual definition/statement notices remain holds. The new Guide run is still compiling; the prior full-example compile covers identical Guide/library inputs and skipped HTML. No local Lean/build/current-output queries, approval or queue action.

[SamuelSchlesinger]

Independent agent review by codex-review-mask-witness-20261112 at 6bb79b7c46cbc78643a46e8798a119f7c07913fd: source/API/caller review is clear; changes requested for one manual instruction, detailed inline. This is agent review, not human review.

The moved operation preserves list order, positional multiplicity, missing-false bits and ignored excess bits. The shared verifier's exact polynomial certificate length and sub-multiset semantics match the three migrated number problems; existing binary encodings and independent time/workspace contracts remain intact. The old module/helper copies are removed, exposed verifier bodies and fun_prop use are preserved, and the four length-bound compositions are clear existing-API reuse. No extra abstraction or source redesign requested.

Current native gates and actual final notices are still pending. No local Lean/build/compiled-query checks, approval or queue action.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 9c0f5025-2100-49d1-8e64-6df50d7da920) of a7342c9: approve. This is agent review, not human review.

This is a real consolidation. maskSelect and its facts leave the problem directory for Foundations/Data/List/MaskSelect.lean, which has a one-module public closure; the old Mask.lean publicly pulled in PolyTime.List. MaxCut's inline index form and the sum_maskSelect lemma buried in IntegerProgramming are promoted there. Witness now has a Mask section that exactly mirrors the Subset section. SubsetSum, Knapsack and Partition become maskVerifier instances, so the next sub-multiset problem won't need a fourth copy. Net +58 is within the survey estimate: Witness +70 is mostly docstrings mirroring the Subset section, and the clients net −31.

• length_le_length_encPair deleted: I accept this. Each of its four uses composes two existing, well-named lemmas, and LinearProgramming already writes the same chain inline. The homes for a named lemma are vendored files or a hub with about 2,700 dependents. No open PR uses the name.

• public import of Witness in SubsetSum: this is needed. NPCompleteNumbers evaluates the verifiers by rfl/decide, so their bodies, which name maskVerifier, must stay exposed. SubsetSum's public import closure still shrinks, from 150 to 144 modules.

• mem_NP_of_subMultisetWitness: the statement is natural, a sibling of mem_NP_of_subsetWitness with hP restricted to sublists. Only the test uses it today, because the three problems keep named verifiers. I accept it as the API for the next sub-multiset problem.

• Earlier findings: my interim findings (the encWithEntries abbrev for the encoding ratchet, the manual helper examples, the unused Multiset.AddSub import) are fixed in 6bb79b7. The codex finding r4555754043 (hP missing from the manual Shortcuts sentence) is fixed in a7342c9, and its thread is answered and resolved. No other review findings are open.

• Manuals: the Operator's Manual Shortcuts and Guarded-maps edits are accurate. The Guarded-maps edit matches PolyTimeReducible.of_guard's hb₀ : b₀ ∉ B. I agree the Agent Operator's Manual needs no edit. ROADMAP and the results inventory are unaffected.

• Validation: ci-checks is green at this head. Notices:

  • no repeated proof block in 112 proofs;
  • no parallel definitions among 6 definitions and no duplicate statements among 24 theorems;
  • encoding and projection ratchets clean.

  The PR-names notice flags length_le_length_encPair, which the description names as deleted on purpose. Merge-tree is clean against main 255d5d0.