[SamuelSchlesinger]

Change

A single combinator for "pad a verifier to a longer string" and "add two #P counts taken at different lengths", so closure proofs no longer assemble andVerifier … allFalseVerifier with Nat.exists_eq_add_of_le plumbing by hand. Refactoring and API only, with no new mathematics.

• Classes/SharpP/Combinators.lean adds:

  • padVerifier k V := andVerifier k V allFalseVerifier, with acceptCount_padVerifier_of_le (on any length n ≥ k a the count equals the count of V at k a).
  • sumVerifier k₁ k₂ V₁ V₂ := selectVerifier (padVerifier k₁ V₁) (padVerifier k₂ V₂), with acceptCount_sumVerifier (at length k₁ a + k₂ a + 1 the counts add).
  • @[fun_prop] polynomial-time rules for both.

  acceptCount_andVerifier_allFalseVerifier, which needed the length written as k a + n, is replaced by the _of_le lemma; no client is left using it.

• Classes/SharpP/Oracle.lean: oracle rules computableInPolyTimeWithOracle_padVerifier / _sumVerifier.

• Migrated clients:

  • SharpP.add_mem and SharpPWithOracle.add_mem now use sumVerifier.
  • These use padVerifier with acceptCount_padVerifier_of_le: the reverse direction of mem_PPWithOracle_iff_exists_GapPWithOracle (PP/Oracle), GapP.pow_mem_polyTime (SharpP/Aggregation), mem_SharpP_of_polyTime_length (SharpP/Closure), and the padded product witness in SharpP/Products.
  • The private acceptCount_padWitness re-proof in Toda/Hierarchy.lean is deleted. The ⊕P witness there is now a padVerifier.

• CslibFrontierTests/BasicClasses.lean: the padding example uses padVerifier. A new checked example evaluates sumVerifier.

Net +23 lines (+127/−104). The new API, with docstrings, outweighs the removed code: Toda's 20-line private lemma, the allFalseVerifier oracle side conditions copied into SharpPWithOracle.add_mem and PP/Oracle, and the length arithmetic (Nat.exists_eq_add_of_le, Nat.add_comm realignments) at the other sites. The gain is one padding lemma and one sum combinator in place of seven hand-built copies, not fewer lines. The survey's estimated savings were optimistic.

SharpP/Lowness.lean has no padding client to migrate. PP/Characterization.lean uses andVerifier … allFalseVerifier through acceptCount_andVerifier_true with free suffix bits that multiply the count; it is not a padding application.

Usage note: when k is left as _, rewriting with acceptCount_padVerifier_of_le _ _ h needs (a := x) if h does not determine a, because the pattern ?k ?a is higher-order. Passing k and V explicitly also works.

Manual impact

Operator's Manual: no edit. No chapter names andVerifier, allFalseVerifier or the removed lemmas (git grep), and the counting conventions in manual/machines-and-classes/verifiers-counting-interaction.md are unchanged. Agent Operator's Manual: no edit, since no workflow or tooling changed. ROADMAP.md, results/README.md and CslibFrontierResults/ do not name the changed declarations. The fun_prop note in PolyTime/Plain.lean lists selectVerifier, andVerifier and orVerifier as having plain rules. It is still accurate and is not edited here, to avoid rebuilding that module's clients.

Validation

At 3b38ac5 (main a9b7d36 merged in):

• lake build --wfail --iofail on the eight changed modules and all their direct importers, including the tests BasicClasses, ClassClosure, PolyTimeMixes, CountingAggregation, CountingProducts and RelativizedCounting.
• lake exe mk_all --check; python3 -B scripts/check_operator_manual.py.
• python3 scripts/proof_copies.py --base origin/main: no repeated proof block.
• python3 scripts/parallel_defs.py --theorems --no-build-check (before the merge): no existing statement among the 13 added or changed theorems. Coverage is partial: unrelated modules new on main had no local build outputs.

Full validation is left to CI.

AI assistance

Jetski worker session c0af227b, plan #4737. Agent-written; not yet reviewed by a human.

Part of #4737

[SamuelSchlesinger]

Independent reviewer worker codex-review-SharpP-padding-20261112: APPROVE 3b38ac554dff227a9d656169ae5b7334ad68ab3b. I did not author or design this patch. This is independent agent review, not human/platform approval.

I read the complete eight-file own delta (relative to merged base a9b7d36e98), the old/new combinators and count arguments, ordinary/oracle resource rules and migrated callers/tests. padVerifier preserves the count only under the stated k a ≤ n; its unique false suffix includes empty padding. sumVerifier uses a disjoint selector bit and retains the exact old k₁ a + k₂ a + 1 witness length. Unary length computation, framed instance/witness encodings, native polynomial-time/space conventions and oracle bounds for arbitrary replies are preserved through the existing composition rules. SharpP/SharpPWithOracle addition, PP/Oracle sign counting, common-width aggregation/products and Toda's prefixed witness use the intended API. Existing product tests retain unequal row widths, zero factors and empty products; the padding test includes zero padding, and the concrete unequal-length sum is five accepting witnesses. No count or resource weakening found.

The corrected exclusion record is accurate: there is no padding client in current SharpP/Lowness; #4150's Lowness edit is an unrelated identity certificate. PP/Characterization's free suffix bits multiply counts and are not a padVerifier application, independently of #4763 ownership. Toda/Counting's pure predicate count already directly uses lower-level WordCount factorization; forcing a dummy-instance verifier conversion offers no clear improvement there. No deferred migration is being accepted merely for scheduling.

Both manuals need no edit: actual fixed-polynomial witness/count and oracle conventions remain unchanged, and no role/procedure changes. All maintained manual inputs, converters, checker and workflow are byte-identical to the landed base a9b7d36e98; the PDF workflow's path filter therefore does not run. No affected page or new PDF artifact/render QA is required, and no older whole-book artifact is claimed as current. Results/retired abstracts and ROADMAP scope are unchanged. Source whitespace check passed. No author-branch edits or local Lean/Lake/cache/build/current-output/compiled-query probes.

Current native CI passed all six gates, the axiom test, stock lints, hygiene, tidy/encoding/projection ratchets, compiled result-registry references and manual-link/excerpt checks. I read the actual untruncated notices: no parallel candidates among 2 definitions, no matching theorem statement among 13, and no repeated block among 83 proofs. These supplement the source/API searches above; they do not establish uniqueness. The two PR-name advisories accurately name declarations explicitly removed by this PR. CI checked merge af45b7fc8f30; all eight owned files are byte-identical to the reviewed head. Guide CI compiled the examples and passed documentation pins; rendered HTML was correctly skipped.

Fresh PR/task/review reads showed the same open, ready head and no unresolved review or integration hold. The trusted exact-head helper newly queued #4784 at this revision (position 6); this is not a landing claim. Root retains actual landing watch. Parent scope remains #4737.

[SamuelSchlesinger]

Agent review (Jetski reviewer session aa3000d8-52c2-410f-8f18-9f617338b54e) of 3b38ac5: approve. This is agent review, not human review.

The case for the change holds. It doesn't save lines, but it names one fact that was rebuilt by hand in seven places, with three different spellings of the length arithmetic. One of those copies was a 20-line private re-proof.

Do the clients read better? At most sites, yes. None got worse.

• SharpP.add_mem and SharpPWithOracle.add_mem are clearly better: one witness and one rewrite. The e₁/e₂ instantiations, the Nat.add_comm realignment and the oracle hfalse side condition are gone.
• mem_SharpP_of_polyTime_length and SharpP.prod_range_mem lose their Nat.exists_eq_add_of_le destructuring; hle a feeds the lemma directly.
• Toda's PH_subset_BPOp_ParityP witness is now a padVerifier, closed by one rewrite and rfl. The private acceptCount_padWitness, which re-derived acceptCount_andVerifier with allFalseVerifier through card_filter_not_any, is deleted.
• GapP.pow_mem_polyTime stays the same length but loses the Nat.add_comm step. In PP/Oracle, the two simpa only [..., Nat.add_comm] steps become a plain rw chain plus one hn. That site can't use sumVerifier, because the second verifier is negated after padding.

Names and statements. padVerifier/sumVerifier sit with andVerifier/orVerifier/selectVerifier. acceptCount_padVerifier_of_le follows Mathlib's _of_le convention. Its hypothesis k a ≤ n is the natural one, and empty padding is included. acceptCount_sumVerifier at length k₁ a + k₂ a + 1 is exactly what both add_mem clients use. An _of_le generalization would have no client. Each combinator has plain and oracle polynomial-time rules.

Should acceptCount_andVerifier_allFalseVerifier have stayed? No. Its left side is spelled andVerifier k V allFalseVerifier and only matches padVerifier k V after unfolding. Keeping it would leave two spellings of padding. The _of_le lemma covers its k a + n case through Nat.le_add_right. No remaining library site, and no open PR (I scanned the diffs of all 74), uses it or padWitness. The remaining andVerifier … allFalseVerifier use in PP/Characterization multiplies by free suffix bits; it isn't padding.

Other checks:

• No existing equivalent definition (parallel-definition notice: none among the 2 new definitions).
• Toda's new SharpP.Combinators import is needed, and WordCount is still used there.
• No open PR touches these eight files.
• Both manuals: I agree no edit is needed. No chapter names these combinators, and the counting conventions are unchanged.
• CI at this head: ci-checks and guide pass. No repeated proof block (83 proofs), no parallel definition, no duplicate statement (13 theorems). The names notice lists only the two declarations this PR removes on purpose.
• Other reviewers: the one existing review comment, from codex-review-SharpP-padding-20261112, is a clear source/API verdict that was waiting only on hosted gates, which now pass. It has no open findings, and there are no inline threads. The corrected "Not done" note (no padding client in SharpP/Lowness) matches what I found on main and in perf(PolyTime): make ComputableInPolyTime irreducible #4150.

Non-blocking:

1. The fun_prop note in PolyTime/Plain.lean still names only selectVerifier, andVerifier and orVerifier. It's not wrong, but it's incomplete. Add padVerifier and sumVerifier the next time that file changes.
2. If k is left as _ and a is not determined, the call needs (a := x). Leaving h out (rw [acceptCount_padVerifier_of_le]) and closing the side goal should avoid that (I haven't tested it), because the rewrite then matches padVerifier ?k ?V and ?a against the goal first. The usage note in the body already covers this, so this is a style option only.

Queueing this head.