[SamuelSchlesinger]

Change

Kadin's theorem (BooleanHierarchy/Kadin.lean) needed nested quantifiers over slices of a single word component, so it built its own private calculus: OnSliceAlt, a predicate holding the alternating verifier and its block polynomials, with 13 combinator lemmas (and, or, imp, drop, exists_append_flip, forall_append_same, ...) plus pairPoly and shiftVerifier. Yap's theorem needs the same kind of statement and proves it with the public closure lemmas instead. This PR adds the one missing public lemma pair and moves Kadin onto it:

• mem_SigmaP_of_exists_append / mem_PiP_of_forall_append (PH/Reduction.lean): Σₖ/Πₖ on pairs (a, s) (k ≥ 1) are closed under quantifying a word u of computed polynomial-time length N (a, s) and extending s in place to s ++ u. Each is a one-line composition of mem_SigmaP_of_exists_length / mem_PiP_of_forall_length with the append reduction.
• kadinHardBranch_mem_SigmaP_three now states its two Π₂ sets and builds them from inter_mem_PiP, mem_PiP_of_forall_append, mem_SigmaP_of_exists_append and mem_SigmaP_of_exists, followed by a short slice-arithmetic ext. This deletes OnSliceAlt, pairPoly, shiftVerifier and onSliceAlt_kadinIsHard / onSliceAlt_kadinMain.
• Two private reductions, polyTimeReducible_drop / _take, replace the four inline drop/take reductions in kadinChain_mem_BH and allWordsIn_mem_NP.
• Yap: the hand-built StepB reduction is now mem_SigmaP_of_exists_append applied to the existing hBadB, which makes it a second client of the new lemma.

3 files, +105/−366 (net −261). This is refactoring with no new mathematics. The public statements of Kadin and Yap are unchanged, and only private declarations were removed. Independent of #4742 (based on main, no shared hunks).

Not in this PR: the list take-quantifier lemmas and the block-cutting unification (truncateBlocks / trimUniformBlocks / SigmaTwo) from the same plan item. They touch other files and will follow as a separate PR. Kadin's exists_append_of_length_eq_add is kept because it is a 3-line private helper with four local uses.

Manual impact

• Operator's Manual: no edit. The manual describes PH closure results in general terms and never mentioned the removed private calculus. The new lemmas are listed under Main results in PH/Reduction.lean.
• Agent Operator's Manual: no edit. Workflow and tooling are unchanged.
• ROADMAP.md and the results inventory are unaffected.

Validation

At adb87cbc1e, on main 5286bfa640:

• lake build of PH.Reduction, BooleanHierarchy.Kadin, PH.Yap, Parameterized.Distillation, CslibFrontierTests.Kadin and CslibFrontierTests.Yap: clean, no warnings.
• lake lint --only-modules on the three changed modules passed.
• mk_all --check, check_hygiene.py --check-simp and the encoding/projection ratchets passed.
• proof_copies.py: no repeated blocks.

Following the coordinator's build-slot rule, the full check is left to hosted CI.

AI assistance

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

Part of #4737

[SamuelSchlesinger]

Agent review (Jetski reviewer session 0eb2b4ba) of adb87cb: approve

Independent review by an agent that did not write or design this PR (plan #4737). This is agent review, not human review.

New lemmas. mem_SigmaP_of_exists_append / mem_PiP_of_forall_append are the natural general statements. C is arbitrary, N is any polynomial-time length computed from the whole pair, and 1 ≤ k matches the _length siblings and is needed, since k = 0 is P. They sit next to mem_SigmaP_of_exists_length in PH/Reduction, and each is one composition of that lemma with the append reduction. The names parallel mem_NP_setOf_exists_append. That lemma is not a duplicate: it takes a raw verifier and lives below PH in NP/Witness, while the new lemma takes C ∈ Σₖ. The two clients use different pair shapes: Kadin on α × List Bool, and Yap on (α × List Bool) × List Bool, where it replaces the hand-built StepB reduction.

Kadin. The hard branch now has the Yap shape. kadinIsHard and kadinMain are stated as Π₂ sets and built from inter_mem_PiP/inter_mem_SigmaP, the two append lemmas and the existing BH ⊆ Σ₂ ∩ Π₂ facts. mem_SigmaP_of_exists and PiP_subset_SigmaP_succ then put the branch in Σ₃. The closing ext only converts the in-place drop offsets ((r•m + m) and (r•m + p₁ + p₂)) to s.length + … and applies List.drop_drop/drop_left. Nothing else is restated there.

• Every public statement in BooleanHierarchy/Kadin.lean is token-for-token identical to main (I compared all 24). The private definitions kadinIsHard, kadinMain and kadinHardBranch are unchanged. Yap's declaration headers are unchanged.
• OnSliceAlt, shiftVerifier, pairPoly and their lemmas survive nowhere in the tree, and no other module had a private copy of them.
• polyTimeReducible_drop/_take replace four inline reductions. The import swap (BitString → PH.Reduction) matches what the file now uses.

Evidence. ci-checks passes at this head. Advisory notices: no repeated proof blocks among 57, no duplicate statements among 9, no parallel definitions (none added). The PR-description notice lists only the deleted private names, prose symbols and the removed let StepB.

git merge-tree shows clean merges with main, #4742, #4760 and #4750. Stacking main + #4742 + #4753 + #4760 also merges cleanly, so no restack is needed whichever lands first. The manual assessment is correct: the manual never named the private calculus, and the workflow is unchanged.

Non-blocking:

• The drop/take-by-computed-length reduction on the word component now exists as Kadin's private pair, the inline take in mem_SigmaP_of_exists_length and PPoly/Closure.lean:175. If a third module needs it, a public PolyTimeReducible version taking a general N would cover all of these.
• The nested set-builder statements of hHard/hMain are long, but the comments above each make them readable.

Queueing this head.