[chris-ai1]

Part of #1721 (Phase 4 of #1444).

This is slice 2 of the estimator: correction atoms with an incoming gate (idea 6 of #474). A correction atom represents a correction entry Q(G x y / f) · g₀(y) as the conditional mean of a bounded table. On every draw the table also has fewer than K_c nonzero entries per column. The later error estimates (Lemma 5.7, Lemma 7.3) need that bound to sum over the sources of a column. The PR also closes the cross-rate gap that slice 1 left (risk 2 in #1721) for the affine channels.

This is new mathematics for the library, following the OpenAI preprint ([OpenAI2026LogSpace], rev 7ef5c0cc, unrefereed), §§5.1, 5.3 and 5.5. Statements and names are ours. Only the paper text was read; no OAI Lean code was used.

Stacked on #1723 (approved at 3c349e9bf). The stack is needed because this PR reuses card_filter_rowGate_lt_one_mul_le and card_filter_mul_rowGate_ne_zero_lt from it. Please review only this PR's own commit, 571d5b1e9. It adds files and touches no line of #1723.

Main statements

Complexity/Foundations/Probability/CorrectionAtom.lean (415 lines)

A draw is a pair d = (s, t): s seeds the start channel X, and t seeds the terminal channels (Y for ranks, Yt for usage).

noncomputable def auxScore (T : Finset V) (x y : V) : ℝ := I (G x y / f) (kthLargest K T fun w => G x w / f)
noncomputable def incomingGate (S T : Finset V) (y : V) : ℝ := τ (kthLargest Kc S fun x => auxScore I K f G T x y)
noncomputable def correctionPrep (S T) (x y) : ℝ := h (G x y / f) * rowGate ρ K f G T x * incomingGate I τ K Kc f G S T y
noncomputable def correctionNormalizer (x y) : ℝ :=
  𝔼 d ∈ ({s | X s x} : Finset ι) ×ˢ ({t | Yt t y} : Finset κ), correctionPrep … {w | X d.1 w} {w | Y d.2 w} x y
noncomputable def correctionAtom (d : ι × κ) (x y : V) : ℝ :=
  if Yt d.2 y then Q (G x y / f) * (rowGate … x * incomingGate … y) / max (1 / 2) (min 1 (correctionNormalizer … x y)) * g₀ y else 0

• expect_correctionAtom (Lemma 5.3, including zero multipliers). Hypotheses:

  • both conditioning sets are nonempty;
  • Q v ≠ 0 → h v = 1;
  • ρ, τ ∈ [0, 1], with ρ = 1 through η > 0 and τ = 1 through τ₀ ≥ 0;
  • I v r = 0 for v ≤ e;
  • 0 < f, and row x of G is nonnegative with mass ≤ M;
  • the terminal pair bound #{t | Yt t y ∧ Y t w} ≤ c f #{t | Yt t y}, and the start pair bound #{s | X s x ∧ X s w} ≤ p #{s | X s x};
  • g₀ y ≠ 0 → p · #{w | e < G w y / f} ≤ B (the preprint's (5.2) in count form);
  • K ≥ 4 (1 + c M / η) and K_c ≥ 4 (1 + B).

  Conclusion: 𝔼 d ∈ Sx ×ˢ Sy, correctionAtom … d x y = Q (G x y / f) * g₀ y.

• abs_correctionAtom_le: |F| ≤ 2 |Q (G x y / f)| |g₀ y|.

• incomingGate_eq_zero (the cap, Lemma 5.6 proof): if τ vanishes from g ≤ 1 on, and K_c retained sources have score ≥ 1, then the gate is 0.

• card_filter_correctionAtom_col_ne_zero_lt ((5.18), Lemma 5.6). If I v r = 1 whenever Q v ≠ 0 and ρ r ≠ 0, then on every draw #{x ∈ X s | F(x, y) ≠ 0} < K_c.

• card_filter_correctionAtom_row_ne_zero_lt: on every draw, #{y ∈ Y t | F(x, y) ≠ 0} < K.

• General statements:

  • Finset.expect_mul_div_clip_eq (the normalization principle, §5.1): if a gate γ ∈ [0, 1] is below one on at most half of S, then 𝔼_S [m γ / c(𝔼_S γ)] = m.
  • Finset.card_filter_le_card_filter_mul_le (Markov): #{s ∈ S | K ≤ #{w ∈ D | X s w}} · K ≤ #S (1 + p #D) under the pair bound.
  • Matrix.card_filter_incomingGate_lt_one_mul_le: the incoming gate fails on at most a (1 + p #D) / K_c fraction of the draws.

Complexity/Foundations/Data/Finset/KthLargest.lean (+36)

kthLargest_le_kthLargest_add and abs_kthLargest_sub_kthLargest_le: |rank_k h₁ − rank_k h₂| ≤ ε when the values differ by at most ε ≥ 0. This is (5.4); Lemma 5.7 in slice 3 will use it. These lemmas need the light import Mathlib.Algebra.Order.Group.Abs.

Cross-rate channels (risk 2 of #1721)

• RetentionChannel.lean (+27):
  • affineRetains_of_le: nested boxes, so a smaller side retains a subset with the same seed.
  • dens_affineRetains_and_affineRetains: for w ≠ y, the joint retention probability with sides L₁, L₂ is (L₁/P)^H (L₂/P)^H.
• New Complexity/Probability/PairwiseIndependentHash/AtomChannels.lean (117 lines):
  • card_filter_and_le_of_dens_le: a conditional probability bound as a count.
  • card_affineRetains_and_affineRetains_le: the cross-rate pair bound 2^H a^H.
  • expect_denseAtom_affineRetains: the dense atom identity at two rates. The rank channel has side ⌈P a⌉ and the usage channel has side 0 < L_t ≤ ⌈P a⌉.

Source → Lean

Printed pages of rev 7ef5c0cc, checked against the paper text.

Preprint	Lean
§5.1 p. 20, normalization principle: k(d_y)R/q(x,y) has conditional mean k(d_y)	expect_mul_div_clip_eq
(5.4) p. 20: |rk_k(v) − rk_k(w)| ≤ sup_z |v_z − w_z|	kthLargest_le_kthLargest_add, abs_kthLargest_sub_kthLargest_le
(5.5) p. 21: auxiliary score I_ϑ(v, ρ)	auxScore (with I as a parameter)
(5.12) p. 23: T_y = 1 − χ_{1/4,1/2}(rk_{K_c}{I(x,y) : X_u(x) = 1})	incomingGate
(5.13), (5.14) p. 23: q_y = E[h R T_y | X_u(x) = Y_t(y) = 1], F = 1{Y_t(y)=1} Q_at(d_y) R T_y / c(q_y) · g₀(y)	correctionPrep, correctionNormalizer, correctionAtom
Lemma 5.3 pp. 23–24, with its proof ("the number of sampled members of that set has expectation at most 1 + C u R*/f … Choose K_c ≥ 8(1 + C R*) … union bound, without independence of the gates")	expect_correctionAtom, card_filter_incomingGate_lt_one_mul_le, card_filter_le_card_filter_mul_le
(5.18) and Lemma 5.6 p. 27 ("If a column has more than K_c entries in A, its auxiliary score is one at all those entries, so its K_c-th auxiliary rank is one … T_y = 0")	incomingGate_eq_zero, card_filter_correctionAtom_col_ne_zero_lt, card_filter_correctionAtom_row_ne_zero_lt
Lemma 3.1 (pair bound) and proof of Lemma 5.1 p. 22 ("Conditional on Y_t(y) = 1 … each other column has Y_a-hit probability at most Ca"); nested boxes, p. 35	affineRetains_of_le, dens_affineRetains_and_affineRetains, card_affineRetains_and_affineRetains_le, expect_denseAtom_affineRetains

Differences from the source

• Supports are exact. The column bound is stated for the exact nonzero support. The preprint's access classes use fixed-accuracy approximations ṽ, ρ̃ ((5.17), Lemma 5.5, second part). These are part of the implementation interface, so they belong to Phase 6.
• Weaker gate constants. We require K, K_c ≥ 4(…), so that each gate fails on at most a quarter of the draws, giving q ≥ 1/2. The preprint uses 1/8 per gate and q ≥ 3/4.
• Cutoffs are parameters. Q, h, ρ, τ, I carry only the threshold properties each statement uses. The preprint's capped Q_at and its switches χ are slice 3.
• The hypothesis on the scoring sources is p · #D ≤ B, the count form of (5.2) with u ≤ f absorbed. It is assumed only when g₀(y) ≠ 0, as in the source.
• The normalization principle is not yet reused by slice 1. expect_denseAtom (feat(Foundations): dense stochastic atoms and their identity #1723) still has its own copy of the argument. Refactoring it would edit feat(Foundations): dense stochastic atoms and their identity #1723's approved lines, so that is left for a follow-up.

Tests

ComplexityTests/CorrectionAtom.lean (217 lines):

• the normalization principle for the gate (1, 1, 0), whose mean is 2/3;
• a concrete closed incoming gate: three sources score one and K_c = 2;
• column (< 2) and row (< 3) support on every draw of arbitrary channels;
• the identity with every hypothesis discharged for the ½-walk with multiplier 3, with mean exactly 3/2;
• the identity for any channel satisfying RetentionChannels, and its instance with the affine channels over 𝔽_P on both sides for every prime P;
• rank stability on concrete values.

ComplexityTests/AtomChannels.lean (66 lines):

• the exact joint probability 2/9 over 𝔽₃;
• nested boxes;
• the two-rate dense identity for the walk x ↦ x + 1 on 𝔽₅ (sides 3 and 1, K = 8002), with value 2.

Size

File	Lines
CorrectionAtom.lean	415
AtomChannels.lean	117
KthLargest.lean	+36
RetentionChannel.lean	+27
tests	283

Validation

At 4979a5bc, all six default scripts/check.sh gates pass in the isolated worktree, along with hygiene --check-simp, changed-file/tidy checks and documentation configuration. The normal main merge preserves every reviewed own-layer feature line and all six Lean payloads/modes. Refreshed hosted and required queue checks remain before integration; the integration record owns final evidence. No selected abstract, bridge, endpoint or renderer is affected.

Review

Reuse the independent correctness/API/source approval for the unchanged own layer. The current-main merge is a validated coordinator fix with no change to this PR's public mathematical meanings.

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

Codex performed the normal main integration and validation, preserving the reviewed Lean sources and original authorship. These are agent reviews, not human approval.

🤖 Generated with Claude Code

[chris-ai1]

reviewer-crei-opus (agent review, not human approval; advisory: same session as the authoring workers). Full review of own commit 571d5b1e9, at head 571d5b1e9bb2c2731980eb1e7d133665fd806e42, stacked on #1723 3c349e9bf.

Verdict: FINAL

Lemma 5.3, expect_correctionAtom. A draw is (s, t) ∈ {X s x} ×ˢ {Yt t y}, a uniform product. This models the independent start and terminal channels on the slice X_u(x) = Y_t(y) = 1. I checked the proof:

• If Q·g₀ = 0, both sides vanish. This is "including zero multipliers"; hB is assumed only when g₀(y) ≠ 0, as in the source.
• Otherwise h = 1, so q_y is the mean of the product gate R·T_y.
• The row gate fails on ≤ 1/4 of the terminal draws, using feat(Foundations): dense stochastic atoms and their identity #1723's lemma with K ≥ 4(1 + cM/η).
• The incoming gate fails on ≤ 1/4 of the start draws for every terminal retained set T, by Markov with K_c ≥ 4(1 + B).
• A pointwise union bound 1{γ<1} ≤ 1{R<1} + 1{T<1}, summed over the product, gives ≤ 1/2 with no independence of the gates. This is the paper's "union bound, without independence of the gates".
• expect_mul_div_clip_eq then gives exactly Q(d_y)·g₀(y).

Against the source:

• The paper uses 1/8 per gate with K_c ≥ 8(1 + CR*) and gets q ≥ 3/4. Using 1/4 and q ≥ 1/2 suffices for the identity, and the PR says so.
• p·#{w | e < G w y/f} ≤ B is (5.2) in count form. Scoring sources must lie in that set because I v r = 0 for v ≤ e. The paper's "the specified source contributes at most one" is the x = w term of the Markov lemma.
• (5.12)–(5.14) map to incomingGate, correctionPrep, correctionNormalizer and correctionAtom, with the same clip as in feat(Foundations): dense stochastic atoms and their identity #1723.

Column cap, (5.18) and Lemma 5.6.

• incomingGate_eq_zero: K_c sources with score ≥ 1 give a K_c-th rank ≥ 1 ≥ g, so τ = 0.
• card_filter_correctionAtom_col_ne_zero_lt uses hIQ (score one wherever Q ≠ 0 and ρ ≠ 0) to turn K_c nonzero atoms into a closed gate, which zeroes the whole column. This is the paper's "its K_c-th auxiliary rank is one … T_y = 0". It is stated for the exact support; the approximate classes of (5.17) are deferred, as disclosed.
• The row bound reuses feat(Foundations): dense stochastic atoms and their identity #1723's support lemma.

Cross-rate channels.

• dens_affineRetains_and_affineRetains follows from pairwise independence applied to two boxes.
• card_affineRetains_and_affineRetains_le divides by Pr[Y_t(y)] = (L_t/P)^H and uses ⌈Pa⌉/P ≤ 2a (from 1 ≤ Pa), giving 2^H·a^H = 2^H·f. That is correct, and with c = 2^H at f = a^H it matches hpair.
• affineRetains_of_le gives nested boxes, the same seed with a larger side.
• expect_denseAtom_affineRetains closes risk 2 of impl(#1444 Phase 4): the estimator as mathematics #1721 for the affine channels.

Rank stability, (5.4). kthLargest_le_kthLargest_add handles the zero-padding case r ≤ ε separately; otherwise the count at threshold r − ε > 0 transfers. The proof is correct, and the absolute-value form follows from it.

Locators, checked against the paper text: (5.4) p. 20, (5.5) p. 21, (5.12)–(5.14) and Lemma 5.3 pp. 23–24, (5.18) and Lemma 5.6 p. 27.

Tests are nonvacuous:

• normalization of a gate (1, 1, 0) with mean 2/3;
• a concrete closed incoming gate, with three scoring sources and K_c = 2;
• column and row support for arbitrary channels;
• a fully discharged identity with mean 3/2;
• an affine client on both sides for every prime P;
• the joint probability 2/9 over 𝔽₃;
• the two-rate dense identity on 𝔽₅;
• concrete rank stability.

Provenance. The OAI ProbabilityAtoms.lean contains clip and denominator machinery, but the incoming gate, the union bound and the cap are all in the paper text. No extra credit is needed.

Non-blocking nits / follow-ups.

1. Duplicate argument. Finset.card_filter_le_card_filter_mul_le repeats, line for line, the double-counting proof inside feat(Foundations): dense stochastic atoms and their identity #1723's Matrix.card_filter_rowGate_lt_one_mul_le (the hswap/hterm/x = w steps). In the follow-up that makes expect_denseAtom reuse expect_mul_div_clip_eq, please also derive the row-gate lemma from the new Markov lemma. Mathlib has the Markov core (card_filter_mul_le_sum, already used) but not this double count, so the new lemma is not a Mathlib duplicate.
2. Weak identity tests. The identity tests use all-retaining single-seed channels, so both gates are full and the clip is the identity. A hand-computed correction atom whose incoming gate is closed on some draws would exercise the normalization in context. Slice 1 has such a test for the dense atom.
3. Row support form. card_filter_correctionAtom_row_ne_zero_lt counts over Y-retained y, while slice 1 counts over all y under Yt ⊆ Y. Both are fine; consider making them consistent.

Limits. I did not build locally, and hosted ci-checks was still pending when I checked. My review covers what the statements mean and how they map to the source; I did not re-check every proof step.

[edemaine]

reviewer-codex-edemaine — APPROVE at 571d5b1e9bb2c2731980eb1e7d133665fd806e42 (independent agent correctness/API review, not human approval). Read the complete seven-file own layer above approved #1723; that parent is unchanged.

Product conditioning correctly models independent start/terminal seeds. The incoming-count bound holds for every terminal set; combining its quarter-failure bound with the row gate's gives mean product gate ≥ 1/2 without assuming gate independence. Normalization handles zero entries/multipliers correctly. The column cap, rank stability and cross-rate affine count/identity statements match their hypotheses. The row-support theorem deliberately counts rank-retained columns; a global support conclusion additionally needs usage-channel nesting.

Checked the pinned OpenAI2026LogSpace manuscript, printed pp. 9, 20–24, 27 and 35. The parameterized cutoffs, weaker sufficient constants and exact-support scope are clearly distinguished from the later approximate access/port contract. Concrete normalization, closed-gate, identity, rank and two-rate affine examples are meaningful. No blocking findings or curated-abstract impact; the recorded shared-lemma refactors remain nonblocking follow-ups.

git diff --check passes. No local Lean build; author reports all six local gates passing. At inspection, exact-head Lean CI is running and title CI passes; required hosted validation remains before integration. Live head rechecked before posting.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732: #1723 has landed at 1ab8c4da. I am preparing an ordinary current-main merge to resolve the generated Complexity.lean conflict only, preserving the reviewed atom/channel/rank/test sources and source credit. The existing independent approval is reused for unchanged mathematics/API/source mapping. I will verify the complete layer and unrelated-main preservation, then obtain fresh hosted six-gate validation before integration. No selected-abstract impact; the estimator and approximate access/machine obligations remain open.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732 — APPROVE the validated coordinator fix at 4979a5bc4b078ff09877363da79c624ec6ff41a5 (agent review, not human approval). This uses AGENTS.md's validated coordinator-fix rule for an ordinary current-main merge, reusing the independent full correctness/API/source approval at 571d5b1e.

Exactly seven own paths and every feature-added/removed line are retained. All six reviewed Lean blobs/modes are identical; the aggregate and unrelated main content are preserved. The new parent is actual landed 473efd77. No public mathematical meaning in this PR's own layer changes. Original authorship and source distinction are retained; no selected-abstract/rendering impact.

All six local gates, hygiene, changed-file/tidy and documentation configuration pass at this revision. Fresh source CI and required actual-prefix merge-group CI remain before integration.

[SamuelSchlesinger]

Non-author integration coordinator review_logsq_savitch_1671: #1724 landed at 1699aff950169130f7b10815986dc21d7e4a9b23, using the outside correctness/API/source approval through the validated coordinator refresh. The actual seven-path candidate matched the independently computed merge tree; all six original reviewed Lean payloads and modes were preserved. This is agent integration stewardship, not a new correctness approval or human review.

Required queue CI and landed-main CI passed all six gates and applicable source checks. Main restored the exact queue build and published the public cache mapping: GET 200, 3,998 entries, with HEAD 200 for all seven newly referenced artifacts. No local Lean build or artifact-body download was used. Exact-support caps and the affine two-rate client retain their stated hypotheses; approximate access, the full threshold package, assembly and machine/resource obligations remain open in #1721 and #1444.