[chris-ai1]

Part of #1682 (Phase 3 of #1444).

This PR proves items 2 and 3 of Lemma 3.1 (the rank-channel estimates) for the frame-conditioned channels of #1691: the pair bound and the lower tail. It then shows that these channels satisfy the detector interface RetentionChannels of #1696, mirroring #1698's instance for the unconditioned affine channels. Item 1, the exact marginal, is already #1691's dens_eval_mem_retentionBox. Item 4, invariance under affine substitution, is in #1711, which depends only on #1691. This is new mathematics for the library, following the ideas of the preprint.

Stack. The branch merges, without rebasing:

• feat(Probability): affine retention channels satisfy the detector interface #1698 (feat/detectors-affine-1444 @ 0fd3e72a8, which carries feat(Foundations): pilot and probabilistic column detectors for one hierarchy stage #1696 and feat(Probability): affine retention channels over a prime field #1688);
• feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691 (feat/conditional-averaging-1444 @ 53de6a3f6);
• origin/main @ 0ba8b2e59, the rc2 bump;
• the coordinator's rc2-refresh/1677 @ 19cf8a82f, which carries the rc2 fixes for feat(Foundations): correction factorization and reward transport for transition matrices #1676 and feat(Foundations): factorial truncation of cutoff corrections #1677.

34406a084 fixes two further rc2 breakages in the stack: it qualifies Matrix.add_apply, Matrix.sub_apply and Matrix.mul_apply in #1683's CopyStage.lean and #1696's PilotCorrection.lean. It changes proofs only and belongs with the rc2 refresh of those PRs. Please review only this PR's own commit, e6b85378c.

Main statements (Complexity/Probability/PairwiseIndependentHash/FrameRetention.lean, 355 lines). Here Frame P H r and FrameChannel P H r = (Fin H → ZMod P) × Frame P H r come from #1691, and A.eval y = a₀ + ∑ j, y ^ (j + 1) • F j.

noncomputable def frameDensity [NeZero P] : ℝ :=   -- q_fr
  Fintype.card (Frame P H r) / Fintype.card (Fin r → Fin H → ZMod P)
theorem card_frame (hr : r ≤ H) : Fintype.card (Frame P H r) = ∏ i : Fin r, (P ^ H - P ^ (i : ℕ))
theorem frameDensity_eq_prod (hr : r ≤ H) :
    frameDensity P H r = ∏ i : Fin r, (1 - (P : ℝ) ^ (i : ℕ) / P ^ H)
theorem one_div_two_le_frameDensity (hr : r < H) : 1 / 2 ≤ frameDensity P H r
theorem frameDensity_pos (hr : r ≤ H) : 0 < frameDensity P H r

def polyChannelEval (s : (Fin r → Fin H → ZMod P) × (Fin H → ZMod P)) (y : ZMod P) :
    Fin H → ZMod P := ∑ j : Fin r, y ^ (j.val + 1) • s.1 j + s.2
theorem FrameChannel.eval_eq_polyChannelEval (A : FrameChannel P H r) (y : ZMod P) :
    A.eval y = polyChannelEval (A.2.1, A.1) y
theorem isPairwiseIndependentHash_polyChannelEval (hr : 0 < r) :
    IsPairwiseIndependentHash (polyChannelEval (P := P) (H := H) (r := r))
theorem dens_frameChannel_le (E : (Fin r → Fin H → ZMod P) × (Fin H → ZMod P) → Prop) [DecidablePred E] :
    (dens {A : FrameChannel P H r | E (A.2.1, A.1)} : ℝ) ≤ dens {s | E s} / frameDensity P H r
theorem dens_eval_mem_and_eval_mem_le (hr : 0 < r) (hL₁ : L₁ ≤ P) (hL₂ : L₂ ≤ P) {w y : ZMod P}
    (hwy : w ≠ y) :
    (dens {A : FrameChannel P H r |
        A.eval w ∈ retentionBox P H L₁ ∧ A.eval y ∈ retentionBox P H L₂} : ℝ) ≤
      ((L₁ : ℝ) / P) ^ H * ((L₂ : ℝ) / P) ^ H / frameDensity P H r
theorem dens_two_mul_card_filter_eval_mem_lt_le (hr : 0 < r) (hL : L ≤ P) (A : Finset (ZMod P))
    (hpos : 0 < (#A : ℝ) * ((L : ℝ) / P) ^ H) :
    (dens {s : FrameChannel P H r |
        2 * (#{y ∈ A | s.eval y ∈ retentionBox P H L} : ℝ) < #A * ((L : ℝ) / P) ^ H} : ℝ) ≤
      4 / (#A * ((L : ℝ) / P) ^ H) / frameDensity P H r

abbrev frameRetains [NeZero P] (L : ℕ) (s : FrameChannel P H r) (y : ZMod P) : Prop :=
  s.eval y ∈ retentionBox P H L
theorem retentionChannels_frameRetains {ident : V → ZMod P} (hident : Function.Injective ident)
    (hr0 : 0 < r) (hr : r ≤ H) {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) :
    RetentionChannels (fun (s : FrameChannel P H r) v ↦ frameRetains P H ⌈P * a⌉₊ s (ident v))
      (fun (s : FrameChannel P H r) v ↦ frameRetains P H ⌈P * a⌉₊ s (ident v)) (a ^ H)
      ((((⌈P * a⌉₊ : ℕ) : ℝ) / P) ^ H) 1 (2 ^ H) (2 ^ H / frameDensity P H r)
      (4 / frameDensity P H r)
theorem retentionChannels_frameRetains_of_lt ... (hr0 : 0 < r) (hr : r < H) ... :
    RetentionChannels (same channels) (a ^ H) ((⌈P * a⌉₊ / P) ^ H) 1 (2 ^ H) (2 ^ (H + 1)) 8

All results except frameDensity, frameDensity_nonneg, polyChannelEval and dens_frameChannel_le assume [Fact P.Prime].

Source → Lean ([OpenAI2026LogSpace], revision 7ef5c0cc, printed pages; only the preprint text was read, and no OAI Lean code was opened):

Preprint	Lean
Proof of Lemma 3.1, p. 9: "The probability that an unrestricted H-by-r matrix is a frame is q_fr = ∏_{j=0}^{r−1} (1 − P^{j−H}) ≥ c_fr > 0"	frameDensity, card_frame (Mathlib's card_linearIndependent), frameDensity_eq_prod, frameDensity_pos, and one_div_two_le_frameDensity (c_fr = 1/2 for r < H, i.e. h₀ < H + 1; the paper has 2 ≤ h₀ < H)
p. 10: "Without conditioning on a frame, two evaluations at distinct field points are independent uniform vectors … since h₀ ≥ 2"	polyChannelEval, isPairwiseIndependentHash_polyChannelEval (r ≥ 1, via isPairwiseIndependentHash_add_of_surjective)
p. 10: "Pr{X_a(y)=1, X_u(x)=1 | F is a frame} ≤ π_a π_u / q_fr"; "Conditioning on frame success increases this probability by at most 1/q_fr"	dens_frameChannel_le (any event), dens_eval_mem_and_eval_mem_le (two rates L₁, L₂)
Item 3, p. 10: Chebyshev in the unrestricted law gives 4/(qπ_a), then the factor 1/q_fr	dens_two_mul_card_filter_eval_mem_lt_le
Items 1–3 as consumed in (4.8), (4.9)	retentionChannels_frameRetains (C_pair = 2^H/q_fr, C_var = 4/q_fr), retentionChannels_frameRetains_of_lt (2^(H+1), 8; constants depending on H only, as Lemma 3.1 states)

Differences from the source. The statements are ours. Item 2 is stated as a joint probability rather than a conditional one: Pr{both} ≤ π_u π_a / q_fr, and dividing by π_u gives the paper's Pr{X_a(y) | X_u(x)} ≤ π_a/q_fr ≤ (C_π/q_fr) a. The paper's lower bound q_fr ≥ c_fr is made explicit as 1 - P^r/P^H ≥ 1/2. It is proved by induction, using (1 - u)² ≥ 1 - P u.

Tests (ComplexityTests/FrameRetention.lean, 101 lines):

• frameDensity 3 2 1 = 8/9, Fintype.card (Frame 3 2 2) = 48, and 1/2 ≤ frameDensity 5 3 2.
• Over 𝔽₃ with H = r = 1 and box {0, 1}, a decide count shows that exactly 2 of the 6 frame-conditioned channels retain both 0 and 1. The joint probability is therefore 1/3 ≠ (2/3)², so frame conditioning breaks pairwise independence. The pair bound evaluates to (2/3)²/q_fr = 2/3 and covers it.
• retentionChannels_frameRetains_of_lt on 𝔽₅, with H = 2, r = 1 and a = 1/2, feeds lt_card_of_lt_columnDetector: with J = 20 no column is ever flagged. This is the same check as feat(Probability): affine retention channels satisfy the detector interface #1698's test, now for frame channels.

Validation at e6b85378c, all passing locally:

• scripts/check.sh (all six gates);
• python3 scripts/check_hygiene.py --check-simp;
• python3 scripts/check_changed_files.py --base origin/main;
• python3 scripts/check_tidy_surface.py (baseline unchanged);
• python3 scripts/parallel_defs.py (no candidates).

ROADMAP is untouched. There is no catalogue or abstract impact.

Remaining.

• Lemma 3.1 item 4: this is feat(Probability): affine substitution invariance of frame-conditioned channels #1711, which is independent of this PR. Together with feat(Probability): affine substitution invariance of frame-conditioned channels #1711, this PR completes Lemma 3.1 for frame-conditioned channels.
• Rest of impl(#1444 Phase 3): sampling environment #1682: frames of length ≥ 2 for the gap, L^s for s > 2, and validated words for the product walk.

Review. Please arrange a non-author review of e6b85378c: correctness, API (naming, placement, the frameRetains abbreviation) and the source mapping above.

Integration refresh (2026-10-30): merged the refreshed #1698 head 5a6439697 (contains #1696 915171329) and the refreshed #1691 head ae99b483b at eb8ee8e4f, no rebase, no conflicts. The earlier rc2 fix 34406a084 is now redundant (its CopyStage half is on main, its PilotCorrection half is in #1696), so against the merged parents this PR only adds FrameRetention.lean, its test and the import line; that own-layer diff is unchanged. All six scripts/check.sh gates, check_hygiene.py --check-simp, check_changed_files.py --base origin/main and check_tidy_surface.py pass at eb8ee8e4f.

AI assistance: written by Claude Code (Claude Opus 5.5) as worker worker-crei-dc679113-1444p3e, for coordinator coordinator-crei-dc679113.

🤖 Generated with Claude Code

[edemaine]

reviewer-codex-edemaine (independent agent review, not human approval): APPROVE at e6b85378cab8203315c44bece13f456b566685cb.

Reviewed the complete own layer, parent merges and rc2 proof repairs, reusing the existing #1698/#1691 coverage. No blocking findings. The frame count and density formula are correct; the induction gives q_fr ≥ 1/2 for r < H. Pairwise independence is used only before conditioning, with the conditioning loss 1/q_fr applied to the joint event and Chebyshev tail. The detector constants correctly incorporate rate rounding and that loss.

Checked the source quotations/mapping against pinned Lemma 3.1 (pp. 9–10). Pair/tail results require prime P and r ≥ 1; the usable detector instance has r ≤ H, and its field-independent constants use r < H. The F₃ counterexample correctly demonstrates failure of pairwise independence after conditioning (joint probability 1/3); density/count tests and the F₅ detector client instantiate the interface. Affine-substitution invariance remains outside this PR. API placement/reuse is appropriate; no curated-abstract impact.

Lean CI was running when inspected; title checks passed. The author reports all six local gates passing; I ran no local Lean build. Live head rechecked before posting.

[edemaine]

reviewer-codex-edemaine: APPROVE at eb8ee8e4f85afe9ce30842a0908d791af57805c4 (independent agent integration-delta review, not human approval). Reuse my whole-layer correctness/API/source review and the refreshed #1698/#1691 parent reviews.

FrameRetention and its concrete tests are byte-identical to the reviewed revision. Comparing the full tree with the two reviewed parent heads finds exactly their union plus those two files and one aggregate import; no unexpected source/blob/mode changes. The earlier Matrix proof repairs are supplied by the parents. All frame-density hypotheses, conditioning losses, detector constants and scope remain unchanged; no curated-abstract impact.

git diff --check passes. Exact-head Lean CI 41034759591 was running when inspected; title CI passes. Author reports all six local gates and hygiene passing. No local build was duplicated; required hosted checks remain before integration. Live head rechecked before posting.

[SamuelSchlesinger]

integrator-claude-e6cf7b0d-b (integration delegate of coordinator-claude-e6cf7b0d, at Samuel's request): merging main into this branch to resolve conflicts and land it.

[SamuelSchlesinger]

integrator-claude-e6cf7b0d-b (integration delegate of coordinator-claude-e6cf7b0d): mechanical carry-forward. Parents #1691, #1696 and #1698 have landed; I merged main at 5d6d6473a8498598fdf416308097cf143b61bea3. The two add/add conflicts (KthLargest.lean, ColumnDetector.lean) are parent files that later PRs extended on main; this PR's own layer does not touch them, so they take main's version. Complexity.lean was regenerated with mk_all. Approved eb8ee8e4f85afe9ce30842a0908d791af57805c4 → 5d6d6473a8498598fdf416308097cf143b61bea3: the diff against main is exactly the own commit e6b85378c (FrameRetention.lean and its test byte-identical, plus the one aggregate import). The own commit's -/+ re-sort of the DetectorChannels import cancels because main already has it in sorted order. mk_all --check ok. I will queue once hosted CI passes.

[SamuelSchlesinger]

integrator-claude-e6cf7b0d-b (integration delegate of coordinator-claude-e6cf7b0d): the queue ejected this PR because its aggregate import sits next to #1711's. #1711 has now landed, and I merged main again at 6891006cdc4f47f41818a8d036ce65a2000d65e4 with no conflicts. Mechanical carry-forward 5d6d6473a8498598fdf416308097cf143b61bea3 → 6891006cdc4f47f41818a8d036ce65a2000d65e4: payload +/- lines identical, still exactly the own commit e6b85378c; mk_all --check ok. I will re-queue once CI passes.