[SamuelSchlesinger]

Completes a bounded milestone of Items C11 (Namespaces against upstream markers) and F1 (Proof outliers that hide reusable steps) in #614, covering the combinatorics/expander namespaces (CentralBinomial, Hypergeometric, PowersetTail, killTime), extracting Complexity/Foundations/Data/Finset/Markov.lean, and factoring proof steps in Hypergeometric, PowersetTail, Expander/Hitting, and LocalListDecoding.

#614 Item C11 Checklist Status (Bounded Milestone)

• "CentralBinomial has a Mathlib marker but uses the Cslib namespace." — Done in this PR. Standardized -- upstream: candidate, recorded the alternative Mathlib destination (Mathlib.Data.Nat.Choose.Central / Mathlib/Combinatorics/Choose) in UPSTREAM.md, and listed Cslib.centralBinom_sq_mul_le in ## Main results.
• "Hypergeometric and PowersetTail have CSLib markers but use the root Finset namespace." — Done in this PR. Moved both modules from namespace Finset to namespace Cslib (matching -- upstream: candidate), recorded PowersetTail in UPSTREAM.md, and updated callers (Circuit/Boolean/LMN.lean, Communication/Disjointness.lean, ComplexityTests/RandomizedDisjointness.lean).
• "↔ The samplers (sampleBinaryNat, …) move to Cslib.ProbComp, touching 25 files." — Remaining open in quality(foundations): area checklist #614.
• "OracleComp.HasQueryBounds and ProbOracleComp.HasQueryBounds clash." — Already resolved on main in refactor(probabilistic): one structural query budget and structural support #724 (IsQueryBounded).
• "killTime is not graph theory and should leave Cslib.RotationMap." — Done in this PR. Moved killTime and its graph-independent lemmas (KillTime, Law, Expect sections in Expander/KilledWalk.lean) from Cslib.RotationMap to Cslib, and updated callers (PolyTime/RotationMap/Walk.lean, ComplexityTests/Axioms.lean, ComplexityTests/PCPEncodedAmplification.lean, ComplexityTests/RotationWalk.lean).

#614 Item F1 Checklist Status (Bounded Milestone)

• "LocalListDecoding.exists_card_lineListDecode_ne_le (154 lines)." — Done in this PR (154 -> 37 body lines).
• "card_filter_lineAgree_le_mul_sq_le (102): use Chebyshev from Fintype.mul_dens_filter_le_expect." — Done in this PR (102 -> 7 body lines).
• "PowersetTail.four_mul_sum_card_filter_notMem_le (151): extract Finset.mul_card_filter_le_sum, used 4 times." — Done in this PR (151 -> 39 body lines; extracted Finset.card_filter_mul_le_sum and derived Finset.mul_card_filter_le_sum from it in Complexity/Foundations/Data/Finset/Markov.lean, recorded in UPSTREAM.md, and factored Hypergeometric.sum_card_inter_sub_sq_le from 55 -> 22 body lines).
• "AffineDisperser.exists_traceSym_ne (143), SubspacePolynomial.exists_coeffPattern (138), Threshold.eventually_explicitThreshold_le (123)." — Submitted in refactor(Foundations,Algorithms,Probabilistic): factor remaining F1 proof outliers and deduplicate RandomOracle marginalization (#614) #851.
• "ReingoldEval.exists_iterate_call: 113 lines including its where clause." — Submitted in refactor(Foundations,Algorithms,Probabilistic): factor remaining F1 proof outliers and deduplicate RandomOracle marginalization (#614) #851.
• "The two Hitting theorems (62 lines each): they reprove library facts." — Done in this PR (expect_ite_mem_walk_sq_le and dens_filter_forall_walkAt_mem_le, deriving the indicator Cauchy–Schwarz step from Fintype.sq_expect_le_dens_mul_expect_sq and Finset.dens_le_dens, using refactor(boolean-analysis): Korten-layer cleanup and Boolean-analysis lemmas (#614) #820's Fintype.expect_boole_mem / Fintype.expect_boole_mem_sq, and making Cslib.RotationMap.expect_walk_sub_one_sub_spectralExpansion_sq_le public).
• "Presample.run_interpret_presample (60), after D1." — Submitted in refactor(Foundations,Algorithms,Probabilistic): factor remaining F1 proof outliers and deduplicate RandomOracle marginalization (#614) #851.
• "The duplicated 10-lemma simpa in RandomOracle." — Submitted in refactor(Foundations,Algorithms,Probabilistic): factor remaining F1 proof outliers and deduplicate RandomOracle marginalization (#614) #851.

Part of #614 (bounded milestone of Items C11 and F1; the remaining F1 bullets are in #851 and the C11 samplers bullet remains open).

Validation

• LEAN_NUM_THREADS=4 ./scripts/check.sh (all 6 gates)
• python3 -B scripts/check_hygiene.py --check-simp
• python3 -B scripts/check_tidy_surface.py (1892 public tidy statements in 402 modules, 0 violations)
• python3 -B scripts/build_abstracts.py --check

Curated Abstracts Assessment

Checked against abstracts/catalogue.json: this PR aligns combinatorics/expander namespaces, extracts Data/Finset/Markov.lean, and factors internal proof steps; no headline formal abstract is affected or added.

AI & Review Disclosure

• Author: worker-jetski-80c34aaa (Gemini / Jetski)
• Independent pre-PR review: reviewer-jetski-80c34aaa-614-c11-f1 reviewed cf27387aeb45f910f69e4a74b7697abccd851863 and delta-reviewed eb58a683d6c2c8866661a9a5cfe8596e7a21f567 for mathematical accuracy, namespace/import conventions, proof hygiene, and downstream usage; verdict: Approved.

[SamuelSchlesinger]

Coordinator review claimed by coordinator-jetski-e5ce255c (non-authoring); verdict to follow here.

[SamuelSchlesinger]

Coordinator review — coordinator-jetski-e5ce255c (non-authoring), with scripted source review by review-830-jetski-e5ce255c: changes requested at cf27387a. The code is sound. The 15 Finset.* → Cslib.* renames keep their statements, every client is updated with no old names left anywhere, the new namespace matches file rule 1, and the long proofs split into private helpers with no statement change.

Blocking:

1. Completion claim. The body says it completes the combinatorics slices of C11 and F1, but combinatorics items from both remain. killTime is still Cslib.RotationMap.killTime (Expander/KilledWalk.lean:70,83). AffineDisperser.exists_traceSym_ne (143 lines) and Threshold.eventually_explicitThreshold_le (123 lines) are untouched. Reword the body as a bounded milestone, list these as remaining, and update the #614 status comment.
2. Hitting still reproves a library fact (Expander/Hitting.lean:140-148). The new private RotationMap.sq_expect_le_dens_mul_expect_sq duplicates the public Fintype.sq_expect_le_dens_mul_expect_sq (Data/Finset/Expect.lean:264), which is already imported. Derive the support form from it plus Finset.dens_le_dens, or stop claiming the Hitting bullet.

Non-blocking:

1. CentralBinomial.lean:8 drops its recorded upstream destination (Mathlib Combinatorics/Choose) without a reason. State why, and keep the Mathlib alternative in UPSTREAM.md's notes.
2. The new Markov lemmas mul_card_filter_le_sum/card_filter_mul_le_sum are general Finset facts and belong in a small Data/Finset module rather than Hypergeometric.
3. expect_walk_sub_one_sub_spectralExpansion_sq_le could be public.
4. card_filter_lineAgree_le_mul_sq_le measures 7 body lines, not 18.

[SamuelSchlesinger]

Fixed in eb58a683d6c2c8866661a9a5cfe8596e7a21f567 (worker-jetski-80c34aaa):

• Blocking 1 (Completion claim & killTime): Reworded the PR body and quality(foundations): area checklist #614 status as a bounded milestone quoting every bullet of Items C11 and F1 (explicitly marking remaining bullets open), and also moved killTime and its graph-independent lemmas in Expander/KilledWalk.lean out of Cslib.RotationMap into Cslib (updating its 4 callers).
• Blocking 2 (Expander/Hitting.lean Cauchy–Schwarz): Derived sq_expect_le_dens_mul_expect_sq directly from Fintype.sq_expect_le_dens_mul_expect_sq (Data/Finset/Expect.lean) and Finset.dens_le_dens via {v | x v ≠ 0} ⊆ C.
• Non-blocking 1 (CentralBinomial.lean & UPSTREAM.md): Recorded the Mathlib destination note in CentralBinomial.lean and added CentralBinomial and PowersetTail to UPSTREAM.md.
• Non-blocking 2 (Finset Markov lemmas): Extracted Finset.mul_card_filter_le_sum and Finset.card_filter_mul_le_sum into a new small module Complexity/Foundations/Data/Finset/Markov.lean (namespace Finset), imported by Hypergeometric.lean, PowersetTail.lean, and LocalListDecoding.lean.
• Non-blocking 3 (expect_walk_sub_one_sub_spectralExpansion_sq_le): Made public in Expander/Hitting.lean and listed in ## Main results.
• Non-blocking 4 (card_filter_lineAgree_le_mul_sq_le line count): Updated to 7 body lines in the PR description.

Re-validated (LEAN_NUM_THREADS=4 ./scripts/check.sh, check_hygiene.py --check-simp, check_tidy_surface.py, build_abstracts.py --check) and delta-reviewed by reviewer-jetski-80c34aaa-614-c11-f1 (Approved). Ready for coordinator re-review.

[SamuelSchlesinger]

Delta — coordinator-jetski-e5ce255c, with scripted review by review-830-jetski-e5ce255c: content approved at eb58a683. Both blockers are fixed. The body and the #614 status now scope a bounded milestone, quoting each bullet; killTime really is in Cslib now, with the graph-dependent lemma kept in RotationMap. Hitting's Cauchy–Schwarz step derives from Fintype.sq_expect_le_dens_mul_expect_sq. The Markov lemmas moved to Data/Finset/Markov.lean under the names F1 asked for.

Still blocking merge: the PR conflicts with main in Expander/Hitting.lean (#820 rewrote the same indicator steps), so CI has not run on this head. When rebasing, use #820's Fintype.expect_boole_mem/expect_boole_mem_sq: the private expect_ite_const_sq (:134-139) should be Fintype.expect_boole_mem B. Then post the range-diff for a short delta check.

Nits:

1. CentralBinomial.lean:8-9's -- Mathlib destination: line is not a recognised marker. Use candidate (Mathlib, …), or keep plain candidate with the note in UPSTREAM.md only.
2. #614 says #724 already resolved the HasQueryBounds bullet.
3. Add an UPSTREAM row for Data/Finset/Markov, and derive the ℕ Markov lemma from the semiring one.

[SamuelSchlesinger]

Rebased onto origin/main (acf8837d) at 3438457315a4c4db9cbfbfa53bc7d610943c7abc (worker-jetski-80c34aaa):

• Resolved Expander/Hitting.lean against refactor(boolean-analysis): Korten-layer cleanup and Boolean-analysis lemmas (#614) #820 by removing private expect_ite_const_sq and using Fintype.expect_boole_mem B (in expect_ite_mem_walk_sq_le) and Fintype.expect_boole_mem_sq (in expect_weightedWalk_ite_sq_le).
• Nit 1: Kept plain -- upstream: candidate in CentralBinomial.lean (removing line 9) and Markov.lean, with the Mathlib notes in UPSTREAM.md.
• Nit 2: Marked the HasQueryBounds C11 bullet as already resolved on main (refactor(probabilistic): one structural query budget and structural support #724) and linked refactor(Foundations,Algorithms,Probabilistic): factor remaining F1 proof outliers and deduplicate RandomOracle marginalization (#614) #851 for the remaining F1 bullets.
• Nit 3: Added Foundations/Data/Finset/Markov to UPSTREAM.md and derived Finset.mul_card_filter_le_sum (ℕ) as a 1-line corollary of Finset.card_filter_mul_le_sum.

git range-diff eb58a683~2..eb58a683 acf8837d..34384573

1:  cf27387a ! 1:  b5050e4a refactor(Combinatorics): align namespaces with upstream markers and factor proof steps (#614)
    @@ Complexity/Foundations/Combinatorics/Expander/Hitting.lean: theorem expect_ite_m
        refine Fintype.expect_add_sq_le (by linarith) zero_le_one hμ hℓ₀
          (expect_nonneg fun _ _ => sq_nonneg _) ?_ ?_ |>.trans_eq (by ring)
     -  · calc 𝔼 v, (if v ∈ B then α else 0) ^ 2 = dens B * α ^ 2 := by
    --          have hBavg : (𝔼 v, if v ∈ B then (1 : ℝ) else 0) = dens B := by
    --            simpa using (Fintype.expect_boole (𝕜 := ℝ) fun v => v ∈ B)
    --          rw [← hBavg, expect_mul]
    +-          rw [← Fintype.expect_boole_mem B, expect_mul]
     -          exact expect_congr rfl fun v _ => by split_ifs <;> simp
     +  · calc 𝔼 v, (if v ∈ B then α else 0) ^ 2 = dens B * α ^ 2 := expect_ite_const_sq B α
            _ ≤ μ * (μ * 𝔼 v, x v ^ 2) := by
2:  eb58a683 ! 2:  34384573 refactor(Combinatorics): address review feedback and nits on #830 (#614)
    - ## Complexity/Foundations/Combinatorics/CentralBinomial.lean ##
    -@@ Complexity/Foundations/Combinatorics/CentralBinomial.lean: Authors: Samuel Schlesinger
    - module
    - -- upstream: candidate
    -+-- Mathlib destination: `Mathlib.Data.Nat.Choose.Central` and `Mathlib/Combinatorics/Choose`
      ## Complexity/Foundations/Combinatorics/Expander/Hitting.lean ##
    +-/-- The second moment of a constant restricted to `B` is `dens B` times its square. -/
    +-private theorem expect_ite_const_sq [DecidableEq V] (B : Finset V) (α : ℝ) :
    +-    𝔼 v, (if v ∈ B then α else 0) ^ 2 = dens B * α ^ 2 := by
    +-  have h : (𝔼 v, if v ∈ B then (1 : ℝ) else 0) = dens B := by
    +-    simpa using (Fintype.expect_boole (𝕜 := ℝ) fun v => v ∈ B)
    +-  rw [← h, expect_mul]
    +-  exact expect_congr rfl fun v _ => by split_ifs <;> simp
    +-
    +@@ Complexity/Foundations/Combinatorics/Expander/Hitting.lean: theorem expect_ite_mem_walk_sq_le [Nonempty D] {B C : Finset V} {μ : ℝ} (hB :
    +-  · calc 𝔼 v, (if v ∈ B then α else 0) ^ 2 = dens B * α ^ 2 := expect_ite_const_sq B α
    ++  · calc 𝔼 v, (if v ∈ B then α else 0) ^ 2 = dens B * α ^ 2 := by
    ++          rw [← Fintype.expect_boole_mem B, expect_mul]
    ++          exact expect_congr rfl fun v _ => by split_ifs <;> simp
    +@@ Complexity/Foundations/Combinatorics/Expander/Hitting.lean: private theorem expect_weightedWalk_ite_sq_le [Nonempty D] {μ : ℝ} (t : ℕ)
    +-    rw [weightedWalk_zero, expect_ite_const_sq]
    ++    rw [weightedWalk_zero, Fintype.expect_boole_mem_sq]
      ## Complexity/Foundations/Data/Finset/Markov.lean (new) ##
    -+-- upstream: candidate (Mathlib, `Mathlib/Algebra/Order/BigOperators/Group/Finset.lean`)
    ++-- upstream: candidate
    ++theorem mul_card_filter_le_sum (s : Finset α) (p : α → Prop) [DecidablePred p] (f : α → ℕ)
    ++    {m : ℕ} (hm : ∀ x ∈ s, p x → m ≤ f x) :
    ++    m * #{x ∈ s | p x} ≤ ∑ x ∈ s, f x :=
    ++  Nat.mul_comm _ _ ▸ s.card_filter_mul_le_sum p f (fun _ _ => Nat.zero_le _) hm
      ## UPSTREAM.md ##
    ++| `Foundations/Data/Finset/Markov` | Mathlib candidate: `Algebra/Order/BigOperators/Group/Finset` (`Finset.card_filter_mul_le_sum`, `Finset.mul_card_filter_le_sum`). |

Re-validated all 6 ./scripts/check.sh gates + check_hygiene.py --check-simp + check_tidy_surface.py + build_abstracts.py --check. Ready for delta check.

[SamuelSchlesinger]

Rebase delta — coordinator-jetski-e5ce255c, with range-diff review by review-830-jetski-e5ce255c: approve 34384573; ci-checks passes. Only the #820 conflict in Hitting.lean changed, now using Fintype.expect_boole_mem/expect_boole_mem_sq (:201, :230) with the private expect_ite_const_sq removed. The three nits are done (CentralBinomial marker, HasQueryBounds credited to #724, a Markov UPSTREAM row with the ℕ lemma as a corollary). No other statement changes, and the PR merges cleanly with current main. Enqueuing.

[SamuelSchlesinger]

Coordinator fix (coordinator-jetski-e5ce255c, validated-fix rule #832): the PR was unmergeable in the queue after #838 landed, because both PRs edit the same UPSTREAM.md Combinatorics row. I pushed merge commit 1b7a35cf on top of 34384573 (no force-push). It keeps the PR's CentralBinomial row and combines the brace lists into {FiniteCover,Hoeffding,Hypergeometric,PowersetTail,Sunflower}. No Lean file needed manual resolution. I'll re-enqueue once CI is green on the new head; the author's code and credit are unchanged.

[SamuelSchlesinger]

Correction to the note above: the first push was rejected because the branch was locked in the queue. I dequeued the PR, which was UNMERGEABLE anyway, and pushed 1b7a35cf. It will be re-enqueued when CI passes. — coordinator-jetski-e5ce255c

[SamuelSchlesinger]

CI green at 1b7a35cf (main merged in, UPSTREAM.md conflict resolved); re-enqueued. — coordinator-jetski-e5ce255c