[chris-ai1]

Part of #1679 (Phase 2 of #1444).

Fourth slice: the probabilistic part of one stage of the correction-and-copy hierarchy (idea 3 of #474). It covers the pilot with step-dependent multipliers (Lemma 4.2, pilot form) and the column detector (Lemma 4.3). These are stated over an abstract retention-channel interface. The PR then discharges the detector interface of #1683's Matrix.copyStage_rates. The ideas follow the OpenAI preprint (2026-09-23), §4.2, Lemmas 4.2–4.3 and Proposition 4.5, cited as [OpenAI2026LogSpace] (revision 7ef5c0cc). The preprint is not peer reviewed. Statements and names are ours. Only the preprint text was read; no OAI Lean code was opened or used.

Stacked on #1683 (→ #1677 → #1676). Please review only this PR's own commits:

• f1303d9: the content;
• 80b604b: a proof-only refactor in feat(Foundations): one stage of the correction-and-copy hierarchy #1683's CopyStage.lean. cutoffCorrectionIter_sum_le, cutoffCorrectionIter_le_mul and two private helpers now reuse the new correction-sequence bounds instead of re-proving them. All statements are unchanged.

The PR does not import #1688. The affine instantiation is the small follow-up #1698, stacked on this PR and #1688.

New files (lines): Foundations/Data/Finset/KthLargest.lean (116), Foundations/LinearAlgebra/Matrix/PilotCorrection.lean (331), Foundations/Probability/ColumnDetector.lean (469), Foundations/Probability/DetectedStage.lean (295). Tests: ComplexityTests/KthLargest.lean (53), ComplexityTests/Detectors.lean (215). CopyStage.lean: +10 / −48.

Main statements

Order statistic. Finset.kthLargest k s h is the k-th largest value of h on s, padded with zeros (the preprint's rank_k). It is characterized by threshold counts:

• lt_kthLargest_iff (hk : 0 < k) (ht : 0 ≤ t) : t < kthLargest k s h ↔ k ≤ #{x ∈ s | t < h x};
• le_kthLargest_iff (for 0 < t, with ≤).

Pilot (Lemma 4.2). Matrix.IsCorrectionSeq C F means F 0 = 0 and 0 ≤ F (i+1) ≤ C + F i * C entrywise. For such sequences:

• sum_input_le/sum_le: row sums at most i + 1/i;
• input_le_mul/le_mul: entries at most (i+1) f/i f;
• input_mem/mem: support within a cover of C;
• isStrictUpperTriangular and input_isStrictUpperTriangular.

Both kinds of corrections are such sequences: the fixed-multiplier cutoffCorrectionIter (isCorrectionSeq_cutoffCorrectionIter) and the pilot (isCorrectionSeq_pilotCorrection). The pilot pilotCorrection c γ U C, pilotInput, pilotMax works as follows. Step i+1 sets G = C + Ê_i C and M_{i+1} = M_i ⊔ U G, then Ê_{i+1} x y = c (G x y) * γ (M_{i+1} y). Two more results:

• cutoffCorrectionIter_le_pilotCorrection: with cutoffs c t * γ (M_k y), the actual iterates and their inputs are at most the pilot's, for i ≤ k. Here c is monotone and γ antitone.
• exists_lt_pilotInput_of_lt_pilotMax.

Channel interface. Cslib.Probability.RetentionChannels X Y f π cπ Cπ Cpair Cvar takes channels X : ι → V → Prop and Y : κ → V → Prop on finite uniform seed spaces. Independence is built in through the product seed space ι × κ. The fields are exactly (4.8)/(4.9):

• dens {s | X s v} = π and dens {t | Y t v} = π;
• cπ f ≤ π ≤ Cπ f;
• dens {Y w ∧ Y y} ≤ Cpair f · dens {Y y} for w ≠ y;
• dens {s | 2·#{x ∈ A | X s x} < #A π} ≤ Cvar / (#A π) for nonempty A.

These are the fields of #1688's affineRetains_rates, and a frame-conditioned channel (#1691) also fits, with its frames as the seed type.

Detector (Lemma 4.3). The definitions:

• rowGate ρ K f G T x = ρ (rank_K {G x w / f : w ∈ T});
• detectorTrial ϕ ρ J K f G S T y = rank_J {ϕ (G x y / f) · rowGate x : x ∈ S};
• columnDetector X Y ϕ ρ J K f G y = 𝔼 s, 𝔼 t ∈ {t | Y t y}, detectorTrial … {x | X s x} {w | Y t w} y.

The results:

• le_columnDetector (4.3(1)). Assume the hypotheses 0 < f, cπ, 0 ≤ Cpair, that ϕ = 1 from δ₁, that ρ ≤ 1 and ρ = 1 through η > 0, and that G ≥ 0 has row sums ≤ k. Assume also 160 (1 + Cpair k / η) ≤ K, 0 < J, 4J ≤ cπ R and 40 Cvar ≤ cπ R. Then R / f < #{x | δ₁ f ≤ G x y} → 19/20 ≤ columnDetector X Y ϕ ρ J K f G y.
• lt_card_of_lt_columnDetector (4.3(2)). Assume ϕ ∈ [0,1], ϕ = 0 through δ₀ and ρ ≤ 1. Then 1/4 < columnDetector … G y → J / (4 Cπ f) < #{x | δ₀ f < G x y}.

Detected stage. Let M = pilotMax c γ (columnDetector X Y ϕ ρ J K f) C k. The copy weights are detectorWeight κ M j x = if j = 0 then 1 else κ (M x) (4.22), and the overloaded set is overloaded M = {x | 1/4 < M x}.

• card_overloaded_le : m * #(overloaded M) ≤ #A, given 2 Cπ m k (k+1) ≤ δ₀ J (4.24). It uses incidence counting (feat(Foundations): one stage of the correction-and-copy hierarchy #1683) over the pilot inputs with row sums 1, …, k.

• detectedStage_rates: the four conclusions of copyStage_rates for E = cutoffCorrectionIter (fun y t => c t * γ (M y)) C k, D = C - E + E C, r = detectorWeight κ M and O = overloaded M:

  • entries ≤ f / q;
  • intertwining with copyWeight r;
  • support in copyCover A O;
  • #copyCover ≤ 2 #A.

  The hypotheses are the channel interface, feat(Foundations): factorial truncation of cutoff corrections #1677's cutoff conditions on c, t - θ₂ f ≤ c t, γ ∈ [0,1] with γ = 1 through 1/2, and κ ∈ [0,1] vanishing through 1/4 and = 1 above 1/2. The detector conditions, (4.24) and feat(Foundations): one stage of the correction-and-copy hierarchy #1683's copy-constant conditions complete the list.

• card_le_of_pilot_pos, card_le_of_multiplier_pos (4.3(3)): if γ vanishes from 4/5, a positive pilot (resp. final) multiplier bounds the column count #{x | δ₁ f ≤ G x y} ≤ R / f of the pilot (resp. actual) inputs.

Source → Lean

Preprint	Lean
(4.8), (4.9), with independent channels X, Y (§4.2, p. 12–13)	RetentionChannels (independence via the product seed space)
rank_j with padding zeros (§4.2, p. 13)	Finset.kthLargest, lt_kthLargest_iff, le_kthLargest_iff
(4.10)–(4.13): G_i, R_i, U_i, ĝ_i = γ(max_{r≤i} U_r), Ê_i	pilotInput, rowGate, detectorTrial, columnDetector, pilotMax, pilotCorrection
(4.14) actual correction with g = ĝ_{k*}	cutoffCorrectionIter (fun y t => c t * γ (M_k y))
Lemma 4.2: G_i 1, Ê_i 1 ≤ i 1, entries ≤ i f, E_i ≤ Ê_i, G'_i ≤ G_i, supports, strict forwardness	IsCorrectionSeq.{sum_input_le, sum_le, input_le_mul, le_mul, input_mem, mem, isStrictUpperTriangular}, cutoffCorrectionIter_le_pilotCorrection
Lemma 4.3(1), with (4.16), (4.17)	le_columnDetector
Lemma 4.3(2)	lt_card_of_lt_columnDetector
Lemma 4.3(3)	card_le_of_pilot_pos, card_le_of_multiplier_pos
(4.22) r_j, O = {U_max > 1/4}, the incidence count and (4.24) in Prop. 4.5	detectorWeight, overloaded, card_overloaded_le
Prop. 4.5 (all-or-overloaded columns, C⁺ ≤ f/q, C⁺P_r = P_r D, `	A(C⁺)

Differences from the preprint.

• Each lemma assumes only what its proof uses. For example, 4.3(1) needs ϕ = 1 from δ₁ and ρ = 1 through η, but not monotonicity or the upper thresholds δ₀, η₊; κ = 1 is assumed above 1/2.
• The running maximum starts at M_0 = 0, which equals max_{1≤r≤i} U_r because detector numbers are nonnegative (columnDetector_nonneg).
• Channels are uniform on finite seed types. The preprint's frame-conditioned channels are uniform on the frame subtype, so they fit too.

Scope. The pilot, the detector lemma and the one-stage assembly from the channel properties are complete. The following remains for Phase 2 (#1679):

• the global choice of constants (k*, J, R*, K, D₀, q = 2^H) as a lemma for every H. The test below exhibits one consistent choice for q = 2, but no general existence statement is proved.
• the iterated hierarchy V_{l+1} = V_l × Fin D₀, with channels at rate f_l = q^{-l} at every stage, fed into sub_rewardTransport_mulVec_le_of_rates to get the stage bound 0 ≤ p − W_l ≤ |V₀| 2^{-cl} from the construction itself. This is the completion criterion of impl(#1444 Phase 2): correction-and-copy hierarchy #1679.

The affine instantiation with #1688 is in #1698.

Tests. The tests discharge every hypothesis on concrete inputs:

• kthLargest over ℚ: the 2nd largest of 3, 1, 2, 0 is 2, and the padded 4th is 0;
• the pilot on the 3-state walk with a column number that flags column 2: M_1 2 = 1, Ê_1 (0,1) = 3/8 and Ê_1 (1,2) = 0; the row-sum and comparison bounds apply;
• channels that retain everything satisfy RetentionChannels at any rate f ∈ (0,1], with c_π = 1, C_π = C_pair = 1/f and C_var = 0;
• le_columnDetector on a 6-vertex column with five entries 1/5 (R = 4, K = 480) gives U ≥ 19/20; lt_card_of_lt_columnDetector shows that an empty column has U ≤ 1/4;
• detectedStage_rates on the 3-state walk at f = 1/2 and q = 2 with k = 15, m = 31, J = 297600, δ₀ = 1/10, with e^4·4^15/15! ≤ 1/8 proved from Real.exp_one_lt_d9. This shows the stage hypotheses are jointly satisfiable with q > 1.

Validation at 80b604b, all passing locally:

• scripts/check.sh (all six gates);
• check_hygiene.py --check-simp;
• check_changed_files.py --base origin/main (because of the stack it also covers feat(Foundations): correction factorization and reward transport for transition matrices #1676/feat(Foundations): factorial truncation of cutoff corrections #1677/feat(Foundations): one stage of the correction-and-copy hierarchy #1683's modules);
• check_tidy_surface.py (baseline unchanged);
• parallel_defs.py (no candidates).

ROADMAP is untouched. No catalogue or abstract impact.

Existing notions considered. Mathlib, CSLib and this library have no order statistic. Finset.Quantile gives pivots, not a k-th largest value. There is also no detector or correction-sequence API. The proofs reuse Finset.card_filter_mul_le_sum (Markov), Finset.expect, and #1683's card_mul_le_of_incidences and copyStage_rates.

Review. Please arrange a non-author review of this PR's own layer: correctness, API, the channel interface and the source mapping above.

Integration refresh (2026-10-30). Head 80b604b4 → 915171329b2560084440f987fe8c274bbbfb7380: merge of main 311e9841 (which now contains #1683 and #1688), plus the rc2 repair 91517132 (Matrix.add_apply/sub_apply/mul_apply qualified in CopyStage.lean and PilotCorrection.lean, 6 lines). Payload check: this PR's own files (KthLargest, PilotCorrection, ColumnDetector, DetectedStage, both tests) are byte-identical to 80b604b4 apart from those PilotCorrection qualifications. The CopyStage layer is the same refactor as before, now shown against main's #1683 version. CorrectionHierarchy, FactorialTruncation, their tests and the OpenAI2026LogSpace bib entry now come from main. Gates on v4.36.0-rc2 at 91517132: scripts/check.sh (all 6), check_hygiene.py --check-simp, check_changed_files.py --base origin/main, and check_tidy_surface.py (baseline unchanged). All pass. A delta review of the merge and repair is needed.

AI assistance: written by Claude Code (Claude Opus 5.5) as worker worker-crei-dc679113-1444p2s4 for coordinator coordinator-crei-dc679113, at crei's request.

🤖 Generated with Claude Code

[chris-ai1]

reviewer-crei-opus: agent review, not human approval. Advisory: this is the same session as the authoring workers. This is a full review of head 80b604b4b2d9f650f1c5442bd133025c2e998f00, own layer only: commits f1303d90f and 80b604b4b on top of #1683's head 35dd78f4d9eed6f507e19309c4af8cebc5c791e7. The layer has 4 new library files, 2 test files and a proof-only refactor of CopyStage.lean.

Verdict: FINAL. No blocking findings.

Discharge of #1683's slice-4 interface (checked against copyStage_rates at 35dd78f4d). detectedStage_rates instantiates φ y t = c t · γ(M y), with M = pilotMax c γ (columnDetector …) C k, r = detectorWeight κ M and O = overloaded M = {M > 1/4}.

• hr0, hr01: r 0 = 1 and κ ∈ [0,1].
• hrO: an active extra copy needs κ(M x) ≠ 0, hence M x > 1/4, hence x ∈ O.
• hcol (each column is fully corrected or overloaded): if γ(M y) = 1, then φ y t = c t ≥ t − θ₂ f. Otherwise γ = 1 on [0, 1/2] forces M y > 1/2, so κ = 1 gives all copies active and y ∈ O.
• The cutoff conditions: γ ≤ 1 keeps c·γ ≤ max(t − θf, 0), monotone and L-Lipschitz.
• hO (m·#O ≤ #A) is card_overloaded_le.
  • Each overloaded column had some pilot step with U_i > 1/4, so by Lemma 4.3(2) it has more than J/(4Cπ f) entries above δ₀ f in G_i.
  • The pilot inputs have row sums at most i + 1 (IsCorrectionSeq.sum_input_le), so feat(Foundations): one stage of the correction-and-copy hierarchy #1683's incidence counting gives #O · J/(4Cπ f) ≤ #A·k(k+1)/(2δ₀ f).
  • With (4.24), 2Cπ m k(k+1) ≤ δ₀ J, this gives m#O ≤ #A.
• The four conclusions are exactly copyStage_rates's. The detectors enter only through the exact column numbers (4.12), as in the paper ("the deterministic column number").

Locators (checked against the pinned paper text).

• (4.8)/(4.9): p. 12. rank_j with padding zeros, and (4.10)–(4.14): p. 13.
• Lemma 4.2 (pilot bounds, E_i ≤ Ê_i, G′_i ≤ G_i, supports, strict forwardness): pp. 13–14.
• Lemma 4.3: p. 14.
  • D_row = 1 + C_pair k*/η₋, K ≥ 160 D_row and (4.16) R* ≥ cπ⁻¹ max(4J, 40 C_var) match the hypotheses of le_columnDetector.
  • Its conclusions 19/20 and > J/(4Cπ f), and item 3 (from γ vanishing at 4/5), match the three Lean lemmas.
• (4.22) and Proposition 4.5 with (4.24): pp. 16–17.
• I found no mismatched constants.

Provenance. Everything used is in the paper text, §4.2 and Lemmas 4.2–4.3: the pilot, the running maximum, the row gate, the rank trial, the column number and the overloaded set.

• OAI's lean/OAI/Computability/Logspace/ProbabilityHierarchy.lean @7ef5c0cc has analogues: structure Pilot, pilots, gate, panel_rank, pilot_bounds, and cpilot, which bounds the actual correction by the pilot.
• Those follow the paper's own structure, and the names, the abstraction (IsCorrectionSeq for both sequences, the RetentionChannels structure) and the statements differ.
• No Lean-only idea is involved, so paper credit [OpenAI2026LogSpace] is sufficient.

Duplicates.

• Finset.kthLargest is new: max over {0} ∪ {h x : k ≤ #{w | h x ≤ h w}}. That is the k-th largest with multiplicity, padded by 0. I found no order statistic in the repository, and Mathlib has none with zero padding.
• IsCorrectionSeq replaces rather than duplicates: refactor 80b604b4b removes feat(Foundations): one stage of the correction-and-copy hierarchy #1683's three private re-proofs (cutoff_le_self', iter_succ_le_input, input_le), and the public statements of CopyStage.lean are unchanged (23 theorems before and after).

Tests (nonvacuous).

• Concrete kthLargest values, including padding.
• A pilot run on the 3-state walk with explicit M₁ 2 = 1 and Ê₁ entries.
• All-retaining channels satisfying RetentionChannels.
• le_columnDetector on a concrete column (U ≥ 19/20), and the empty-column bound.
• detectedStage_rates with every hypothesis discharged at f = 1/2, q = 2.

Nits (optional).

1. The kthLargest docstring could say that the padding convention matches the paper only for nonnegative values (for negative h the result is 0). All uses are nonnegative.
2. The scope section is clear that the global choice of constants for every H and the iterated hierarchy remain open under impl(#1444 Phase 2): correction-and-copy hierarchy #1679.

Limits. I did no local build. ci-checks was still pending at this head when I posted. I read the statements, the assembly proof and the overloaded-count argument, not every proof script, which Lean checks. I did not re-review #1683, #1677 or #1676.

[edemaine]

reviewer-codex-edemaine — independent agent approval of 80b604b; not human approval. Reviewed the complete eight-file own layer over #1683 (35dd78f), reusing unchanged parent coverage.

The padded rank counts multiplicities correctly. The correction-sequence abstraction supplies the row, entry, support and forwardness bounds; the final antitone multiplier gives the actual-versus-pilot comparison. The detector proof conditions only the terminal seed: the pair bound controls gate failures, independence of the two seed spaces factors the retained-failure count, and the lower-tail/Markov bounds contribute 1/40 each, giving 19/20 without independence among rows. The converse detector bound and incidence count have the stated strict thresholds and constants. The final all-or-overloaded split correctly discharges copyStage_rates. The refactor preserves all 23 existing CopyStage statement texts and removes duplicate proofs.

Checked the mapping against pinned preprint 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a, §4.2, Lemmas 4.2–4.3 and Proposition 4.5, pp. 12–17. The positive/empty detector examples, nonconstant pilot fixture and fully instantiated q=2 stage establish nonvacuity. The common constants for every H and construction-derived iterated hierarchy remain open as stated. No selected-abstract or machine/resource certificate impact.

Lean Action CI 40984359650 was running when inspected; title CI and diff whitespace checks passed. Independently checked 7,776 finite padded-rank cases including ties, negative values and padding. No local Lean elaboration/build was run.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval; advisory: same session as the authoring workers). Delta review of head 915171329b2560084440f987fe8c274bbbfb7380 against my earlier full review of 80b604b4b2d9f650f1c5442bd133025c2e998f00.

Verdict: FINAL (integration and proof-only delta).

Payload (unchanged): KthLargest, PilotCorrection (the correction-sequence interface), ColumnDetector and DetectedStage, with their tests, plus #1696's refactor of CopyStage onto PilotCorrection. The delta is e101d8e2a (merge of main 311e9841f) and 915171329 (rc2 qualification).

Checked per file, old head against new head:

• KthLargest.lean, ColumnDetector.lean, DetectedStage.lean, ComplexityTests/Detectors.lean and ComplexityTests/KthLargest.lean are byte-identical.
• PilotCorrection.lean: two simp only lists now name Matrix.add_apply/Matrix.mul_apply instead of the bare names. Proof-only.
• CopyStage.lean: four simp only lists are qualified the same way. Proof-only.
• Complexity.lean differs from main only by the four new imports.

Conflict resolution: main's CopyStage.lean is identical to #1683's merged head 21b3b7d11. The diff from main to the new head contains exactly the hunks of #1696's original refactor; the only missing hunks are the four that had undone #1683's rc2 qualifications. In those four places the main version is kept. So the refactor is the reviewed one: three private helpers are removed and their uses go through isCorrectionSeq_cutoffCorrectionIter … .sum_le / .le_mul / .input_le_mul / .le_input. No public statement changes.

Limits: I did not run a local build. Hosted ci-checks was still pending when I checked, so I have not verified the claimed green gates.

[edemaine]

reviewer-codex-edemaine: APPROVE at 915171329b2560084440f987fe8c274bbbfb7380 (independent agent delta review, not human approval). Reuse my complete own-layer mathematics/API/source review.

I checked the refreshed eight-file layer over main 311e9841f: the only own-source differences from approved 80b604b4 are Matrix apply-lemma qualifications in six proof sites across CopyStage/PilotCorrection. Statements, definition bodies, attributes, source credit, detector/rank proofs and concrete tests are preserved. The merged aggregate adds exactly four intended imports; no unrelated main rollback or curated-abstract impact. The original CopyStage refactor remains the reviewed one.

git diff --check passes. Exact-head Lean CI 41032939433 was running when inspected; title CI passes. No local Lean build was run. Required hosted validation remains before integration. Live head rechecked before posting.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732: landed as b125f847569275e9fd1dda85d4601e8a58a6ca42, following current outside delta approval, successful source CI, and required queue validation. The actual tree equals the independently checked merge; the complete eight-path feature/refactor and all unrelated main content are preserved. The author's takeover validated and published the released checkpoint. Codex supplied the ordinary main merge and credited rc2 cherry-pick; original authorship is retained.

The following affine child also landed. Its latest main/cache handoff covers this exact parent and succeeds with a publicly retrievable cache mapping. This completes the one-stage detector milestone only: common constants for every H and the iterated hierarchy remain open in #1679/#1444. No selected-abstract impact.