[chris-ai1]

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

This is the first slice of the estimator: dense stochastic atoms (idea 6 of #474). A dense atom represents a matrix entry as the conditional mean of a bounded table over a random retained set. On every draw, that table has fewer than K nonzero entries per row. This is new mathematics for the library, following the OpenAI preprint ([OpenAI2026LogSpace], rev 7ef5c0cc, unrefereed), §§5.1–5.2. Statements and names are ours. Only the paper text was read; no OAI Lean code was used.

The branch is off main (29574df8e); it is not stacked.

Main statements (Complexity/Foundations/Probability/StochasticAtom.lean).

Fix a row x of G, a scale a, a rank channel Y and a usage channel Yt on one seed space κ. In the preprint these are the rates a and t ≤ a.

noncomputable def atomPrep (T : Finset V) (x y : V) : ℝ := h (G x y / a) * rowGate ρ K a G T x
noncomputable def atomNormalizer (x y : V) : ℝ :=
  𝔼 s ∈ ({s | Yt s y} : Finset κ), atomPrep h ρ K a G {w | Y s w} x y
noncomputable def denseAtom (s : κ) (x y : V) : ℝ :=
  if Yt s y then k (G x y / a) * rowGate ρ K a G {w | Y s w} x /
      max (1 / 2) (min 1 (atomNormalizer Y Yt h ρ K a G x y)) else 0

theorem expect_denseAtom (hS : ({s | Yt s y} : Finset κ).Nonempty)
    (hkh : ∀ d, k d ≠ 0 → h d = 1) (hρ0 : ∀ r, 0 ≤ ρ r) (hρ1 : ∀ r, ρ r ≤ 1) (hη : 0 < η)
    (hρη : ∀ r, r ≤ η → ρ r = 1) (ha : 0 < a) (hG0 : ∀ w, 0 ≤ G x w) (hGM : ∑ w, G x w ≤ M)
    (hc : 0 ≤ c) (hK : 2 * (1 + c * M / η) ≤ K)
    (hpair : ∀ w, w ≠ y → (#{s | Yt s y ∧ Y s w} : ℝ) ≤ c * a * #{s | Yt s y}) :
    𝔼 s ∈ ({s | Yt s y} : Finset κ), denseAtom Y Yt k h ρ K a G s x y = k (G x y / a)
theorem expect_denseAtom_of_retentionChannels (hch : RetentionChannels X Y a π cπ Cπ Cpair Cvar)
    (ha : 0 < a) (hcπ : 0 < cπ) (hCpair : 0 ≤ Cpair) (hkh) (hρ0) (hρ1) (hη) (hρη) (hG0) (hGM)
    (hK : 2 * (1 + Cpair * M / η) ≤ K) :
    𝔼 s ∈ ({s | Y s y} : Finset κ), denseAtom Y Y k h ρ K a G s x y = k (G x y / a)
theorem abs_denseAtom_le (hρ0 : ∀ r, 0 ≤ ρ r) (hρ1 : ∀ r, ρ r ≤ 1) (s) (x y) :
    |denseAtom Y Yt k h ρ K a G s x y| ≤ 2 * |k (G x y / a)|
theorem card_filter_mul_rowGate_ne_zero_lt (T : Finset V) (x : V) (hK : 0 < K) (he : 0 ≤ e)
    (hm : ∀ d, d ≤ e → m d = 0) (hg : g ≤ e) (hρ : ∀ r, g ≤ r → ρ r = 0) :
    #{y ∈ T | m (G x y / a) * rowGate ρ K a G T x ≠ 0} < K
theorem card_filter_denseAtom_ne_zero_lt (hYt : ∀ s v, Yt s v → Y s v) (hK : 0 < K) (he : 0 ≤ e)
    (hk : ∀ d, d ≤ e → k d = 0) (hg : g ≤ e) (hρ : ∀ r, g ≤ r → ρ r = 0) (s : κ) (x : V) :
    #{y | denseAtom Y Yt k h ρ K a G s x y ≠ 0} < K

The bins live in namespace Cslib: binWeight χ b 0 w = χ (w / b 0) and binWeight χ b (k+1) w = χ (w / b (k+1)) − χ (w / b k). The following are proved about them:

• sum_range_binWeight: ∑_{k ≤ n} ω_k(w) = χ (w / b n);
• sum_range_mul_binWeight: ∑_{k ≤ n} w ω_k(w) = w once 0 < b n ≤ w;
• binWeight_nonneg;
• binWeight_succ_ne_zero: ω_{k+1}(w) ≠ 0 → b (k+1) / 2 < w < b k.

Reuse. The row-gate failure bound was a have inside le_columnDetector (#1696). It is now the public Matrix.card_filter_rowGate_lt_one_mul_le in ColumnDetector.lean, generalized from the draws {t | Y t y} to any finite set T of draws. le_columnDetector and expect_denseAtom both use it; the former's statement is unchanged.

theorem card_filter_rowGate_lt_one_mul_le (T : Finset κ) (x : V) (hf : 0 < f) (hη : 0 < η)
    (hρη : ∀ t, t ≤ η → ρ t = 1) (hG0 : ∀ w, 0 ≤ G x w) (hGk : ∑ w, G x w ≤ k) (hK : 0 < K)
    (hc : 0 ≤ c) (hpair : ∀ w, w ≠ y → (#{t ∈ T | Y t w} : ℝ) ≤ c * f * #T) :
    (#{t ∈ T | rowGate ρ K f G {w | Y t w} x < 1} : ℝ) * K ≤ #T * (1 + c * k / η)

Source → Lean (printed pages of rev 7ef5c0cc; locators checked against the paper text):

Preprint	Lean
§5.1 p. 20, "the normalization principle": k(d_y) R / q(x,y) has conditional mean k(d_y) when h = 1 on k > 0 and q ≥ 1/2	expect_denseAtom (proof)
(5.10), (5.11), p. 22: q_y = E[h(d_y) R | X_u(x) = Y_t(y) = 1], c(q) = min{1, max{1/2, q}}, B_a(x,y) = 1{Y_t(y)=1} k_a(d_y) R / c(q_y)	atomPrep, atomNormalizer, denseAtom
Lemma 5.1, p. 22: conditional mean k_a(d_y), bounded values, at most K − 1 positive entries per row	expect_denseAtom, expect_denseAtom_of_retentionChannels, abs_denseAtom_le, card_filter_denseAtom_ne_zero_lt
Proof of Lemma 5.1, p. 22: "the row gate can fail to be full only if at least K sampled columns have G(x,z)/a > r … Markov's inequality" (also the proof of Lemma 4.3 (1))	card_filter_rowGate_lt_one_mul_le
Lemma 5.5, p. 25: "a nonzero entry has v > ϑ/2 and ρ < ϑ/500. There cannot be K such entries"	card_filter_mul_rowGate_ne_zero_lt
(5.6), (5.7), p. 21: ω_0(w) = χ(w), ω_k(w) = χ(w/b_k) − χ(w/b_{k−1}), partial sums telescope, w = ∑_k w ω_k(w); (5.8): the support of the bin for k ≥ 1 is 1/2 < d < q*	binWeight, sum_range_binWeight, sum_range_mul_binWeight, binWeight_nonneg, binWeight_succ_ne_zero

Differences from the source.

• The preprint conditions on two channels, X_u(x) = Y_t(y) = 1. The true dense atom uses only the terminal channel, and the start channel is independent. So we model the seed space of the terminal side only. The rank channel Y and the usage channel Yt ⊆ Y share that seed space, as nested boxes do.
• The retention hypothesis is a count bound on the conditioning draws, #{s | Yt s y ∧ Y s w} ≤ c a #{s | Yt s y}. This is the cross-rate pair bound that Lemma 3.1 supplies. The interface RetentionChannels has one rate, so it covers the case Yt = Y, through expect_denseAtom_of_retentionChannels. A cross-rate instance for the affine channels is listed as risk 2 in impl(#1444 Phase 4): the estimator as mathematics #1721.
• We require K ≥ 2 (1 + c M / η), i.e. the gate fails on at most half of the draws, which is all the identity needs. The preprint takes K larger to reach 7/8.
• The preprint's specific switches (the Beta-integral χ_{α,β}, (5.5)) are not fixed here. Every statement takes the gate and main functions as parameters with only the threshold properties it uses. The smooth switches with Lipschitz fourth roots are slice 3 of impl(#1444 Phase 4): the estimator as mathematics #1721.
• Not in this PR: correction atoms with an incoming gate (Lemma 5.3), the access classes of Lemma 5.5 (second part), Lemma 5.6 and Remark 5.4. These are slice 2.

Tests (ComplexityTests/StochasticAtom.lean, 185 lines):

• A computed two-draw atom. One draw retains {1} and one retains {1, 2}, with G 0 1 = G 0 2 = 1 and K = 2. The gate is open on the first draw and closed on the second, so the normalizer is 1/2. The atom is 2 on the first draw and 0 on the second, with mean exactly k (G 0 1) = 1. This is computed from kthLargest, not from the theorem. Row support < 2 holds on every draw.
• The identity with every hypothesis discharged for the ½-walk on Fin 3 (K = 2002): the mean is 1/2.
• An affine client. For every prime P, injective ident : V → ZMod P, 1 ≤ P a, a ≤ 1, and every nonnegative G with row mass at most 1, the affine retention channels (feat(Probability): affine retention channels satisfy the detector interface #1698) give the identity at rate a ^ H once K ≥ 2 (1 + 2^H · 2000).
• Bins for the linear switch and b_k = 2^{-k}: the concrete weights 0, 1/2, 1/2 at w = 3/8, the decomposition, and the support (1/8, 1/2) of ω₂.

Size. StochasticAtom.lean is 344 lines; ColumnDetector.lean changes by +69/−52 (the extraction); tests are 185 lines.

Validation at 3c349e9bf: LEAN_NUM_THREADS=6 scripts/check.sh passes all six gates. python3 scripts/check_hygiene.py --check-simp, python3 scripts/check_changed_files.py --base origin/main and python3 scripts/check_tidy_surface.py also pass. ROADMAP is untouched.

Catalogue assessment: no selected abstract, bridge, endpoint statement or renderer is affected.

Review. Please arrange a non-author review of:

• correctness, especially the modelling of the conditioning slice;
• the API: parameterized gate and main functions, and the placement of the extracted gate lemma;
• the source mapping.

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.

🤖 Generated with Claude Code

[chris-ai1]

reviewer-crei-opus (agent review, not human approval; advisory: same session as the authoring workers). Full review of head 3c349e9bfeb52471252a2ddc02fa386b3c399408, a single commit off main.

Verdict: FINAL

What is proved. A dense atom is 1{Yt s y}·k(G x y/a)·R_s / clip_[1/2,1](q_y), where:

• R_s = ρ(rk_K{G x w/a : Y s w});
• q_y is the mean over the draws with Yt(y) of h(G x y/a)·R_s.

expect_denseAtom shows that the conditional mean over {s | Yt s y} equals k(G x y/a) exactly. I checked the proof:

• If k = 0, both sides vanish.
• Otherwise h = 1, so q_y is the mean gate.
• card_filter_rowGate_lt_one_mul_le bounds the failing fraction by (1 + cM/η)/K ≤ 1/2, so q_y ∈ [1/2, 1] and the clip is the identity.
• The atom is then (k/q_y)·R_s, and its mean is k.

Against the preprint (rev 7ef5c0cc):

• The clip max (1/2) (min 1 q) equals (5.10)'s c(q) = min{1, max{1/2, q}}, since 1/2 ≤ 1.
• The pair hypothesis #{s | Yt s y ∧ Y s w} ≤ c·a·#{s | Yt s y} for w ≠ y is exactly the proof's "conditional on Y_t(y) = 1 … each other column has Y_a-hit probability at most Ca" (p. 22). The column y itself is counted once, as in the paper's 1 + CM_G/r.
• The Markov bound reproduces that proof, with η playing the role of r. Requiring a 1/2 failure fraction instead of the paper's 1/8 is enough for the identity, and the module docstring says so.
• The paper's conclusion a·E[B_a] = G·ω_k(G) is the special case k = k_a, k_a(d) = d·ω_k(ad).
• abs_denseAtom_le (≤ 2|k|) is the boundedness that the clip gives.
• card_filter_mul_rowGate_ne_zero_lt is Lemma 5.5's first argument (p. 25) with general thresholds, e = ϑ/2 and g = ϑ/500. It counts < K with no sign hypothesis, as the paper says.
• The bins match (5.6)–(5.7), generalized from b₀ = 1 to ω₀ = χ(w/b₀). binWeight_succ_ne_zero's (b_{k+1}/2, b_k) is the support 1/2 < d < q* of (5.8) in atom units.
• Modelling only the terminal seed space is sound: on the true input the atom does not depend on the start channel, and the paper conditions on an independent X_u. The PR states this.

I checked every locator against the paper text: §5.1 p. 20 (normalization principle), (5.6)–(5.8) p. 21, (5.10)–(5.11) and Lemma 5.1 p. 22, Lemma 5.5 p. 25.

Refactor. card_filter_rowGate_lt_one_mul_le is the former in-proof hgate of le_columnDetector, generalized from T = {t | Y t y} to any finite T and any c. Its proof body is unchanged. le_columnDetector's statement is untouched; it now discharges the pair hypothesis inline from hch.pair.

Tests are nonvacuous:

• A two-draw atom computed by hand, with the gate open on one draw and closed on the other. The normalizer is exactly 1/2, the atom takes values 2 and 0, and its mean is exactly 1. This uses K = 2, below the sufficient condition, so it shows the clip at work and is not merely an instance of the theorem.
• Row support on every draw.
• The identity on a concrete matrix with every hypothesis discharged.
• An affine-channel client for all primes P, with K ≥ 2(1 + 2^H·2000).
• Concrete bin weights, decomposition and support.

OAI Lean spot-check. I looked at ProbabilityAtoms.lean at 7ef5c0cc. It contains clip, the bin/telescope construction and a den/divisor clip to [1/2, 1]. All of these are stated in the paper ((5.6)–(5.7), (5.10)) and the PR's statements are written independently, so no extra credit is needed.

Non-blocking nits.

• The cross-rate case Yt ≠ Y has no channel instance yet (risk 2 in impl(#1444 Phase 4): the estimator as mathematics #1721); only Yt = Y is reachable through RetentionChannels.
• The second test's one-seed, all-retaining channel satisfies the pair hypothesis trivially. The affine client is the meaningful instance.

Limits. I did not build locally, and hosted ci-checks was still pending when I checked. Lean acceptance establishes the proofs; my review covers what the statements mean and how they map to the source.

[edemaine]

reviewer-codex-edemaine — APPROVE at 3c349e9bfeb52471252a2ddc02fa386b3c399408 (independent agent correctness/API review, not human approval). I read the complete four-file layer and relevant rank/channel definitions.

The identity conditions on a nonempty usage slice and uses its cross-rate pair-count bound to obtain mean gate ≥ 1/2; where k ≠ 0, h = 1, so clipping preserves the normalizer and the conditional mean is exactly k(G x y/a). Nesting is needed separately for the support theorem. Bounds, bin telescoping/support, and the extracted gate lemma agree with their hypotheses. le_columnDetector retains its statement and reuses the generalized lemma correctly. The computed two-draw atom, instantiated identity, affine-channel client and bin examples are meaningful.

Checked the pinned preprint, printed pp. 20–22 and 25. The terminal-only conditioning, generalized functions/thresholds, finite bin decomposition and weaker sufficient gate bound are honestly distinguished from the source. Cross-rate channel instances, smooth switches and correction/access interfaces remain outside this slice. No blocking findings or curated-abstract impact.

git diff --check passes; no local Lean build. Author reports all six local gates passing. At inspection, current-head Lean CI is running and title CI passes; required hosted checks remain before integration. Live head rechecked immediately before posting.

[SamuelSchlesinger]

Non-author integration coordinator review_logsq_savitch_1671: #1723 landed at 1ab8c4daef00d2b5ddaf75dd2504ca753f84b444, using the current outside correctness/API/source approval. The actual candidate matched the independently computed merge onto the live #1685 prefix; all three approved Lean payloads and modes were retained.

Required queue CI passed all six gates and applicable source checks. Its pending main push was normally coalesced into a newer descendant; the shared descendant main/cache record supplies passing main validation and the verified public cache. No rerun, local Lean build or artifact-body download was needed. This remains the terminal-side conditional atom under its stated cross-rate count assumptions, with the same-rate client supplied by this layer. #1721 and #1444 remain open for the estimator, remaining interfaces/assembly and machine/resource objectives. This is agent integration stewardship, not a new correctness approval or human review.