[chris-ai1]

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

Small follow-up to #1696. It shows that #1688's affine retention channels over 𝔽_P satisfy the detector interface Cslib.Probability.RetentionChannels. So the detector lemma (Matrix.le_columnDetector, Matrix.lt_card_of_lt_columnDetector) and the detected stage (Matrix.detectedStage_rates) hold for concrete channels. The ideas follow the OpenAI preprint (2026-09-23), (4.8)/(4.9), cited as [OpenAI2026LogSpace]. The preprint is not peer reviewed, and no OAI Lean code was used.

Stack. The branch is a merge (merge commit a7541c6, no rebase) of:

• feat(Foundations): pilot and probabilistic column detectors for one hierarchy stage #1696 (feat/detectors-1444, on feat(Foundations): one stage of the correction-and-copy hierarchy #1683 → feat(Foundations): factorial truncation of cutoff corrections #1677 → feat(Foundations): correction factorization and reward transport for transition matrices #1676);
• feat(Probability): affine retention channels over a prime field #1688 (feat/retention-channel-1444, on feat(Probability): retention by pairwise independent hashing #1681).

Please review only this PR's own commit, 0fd3e72, after those PRs.

New module Complexity/Probability/PairwiseIndependentHash/DetectorChannels.lean (66 lines) with tests in ComplexityTests/DetectorChannels.lean (43 lines).

Main statement

theorem retentionChannels_affineRetains {ident : V → ZMod P} (hident : Function.Injective ident)
    {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) :
    RetentionChannels (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v))
      (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) (a ^ H)
      ((((⌈P * a⌉₊ : ℕ) : ℝ) / P) ^ H) 1 (2 ^ H) (2 ^ H) 4

The constants are rate f = a ^ H, π = (L/P)^H, c_π = 1, C_π = C_pair = 2^H and C_var = 4. Vertices enter through an injective identifier map. Independence of the two channels comes from the product of their seed spaces, which is built into the interface. The proof unpacks affineRetains_rates. For the lower tail it transports #{x ∈ A | X s (ident x)} to A.image ident by injectivity.

Preprint	Lean
(4.8), (4.9), with Lemma 3.1 items 1–3 for unconditioned affine channels (§3–4.2)	retentionChannels_affineRetains

Test. The test uses 𝔽₅, H = 2 and a = 1/2 (rate 1/4, L = 3), with detector rank J = 20. Then J / (4 C_π f) = 5, which is the whole vertex set. So lt_card_of_lt_columnDetector shows that no column of any matrix on 𝔽₅ has a detector number above 1/4. This exercises the instance and the detector lemma together.

Validation at 0fd3e72, all passing locally:

• scripts/check.sh (all six gates);
• check_hygiene.py --check-simp;
• check_changed_files.py --base origin/main;
• check_tidy_surface.py.

ROADMAP is untouched. No catalogue impact.

Limitation. These are the unconditioned affine channels of #1688. The frame-conditioned channels of #1691 would need their own instance of the same interface, with constants divided by the frame probability.

Review. Please arrange a non-author review of this commit.

Integration refresh (2026-10-30). Head 0fd3e72a → 5a6439697292404dbe10d9dea22724d9d9142560, a merge commit of the refreshed #1696 head 91517132 (= main 311e9841 plus the rc2 qualification repair). It resolves the add/add conflict in RetentionChannel.lean with main's #1688 version. Payload check: compared with refreshed #1696, this PR adds only DetectorChannels.lean, its test (both byte-identical to 0fd3e72a) and one Complexity.lean import line. Gates on v4.36.0-rc2 at 5a643969: 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.

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: same session as the authoring workers). Head 0fd3e72a85ca7c97e9a56a4ef02de0155f002e94. Verdict: FINAL for the PR's own commit 0fd3e72 only (3 files, +110). It sits on merge a7541c6 of #1696 (80b604b4) and #1688 (4943d9b0), which are reviewed separately.

What is proved. retentionChannels_affineRetains takes an injective ident : V → ZMod P (P prime) and 1 ≤ P a, a ≤ 1, with L = ⌈P a⌉. Under these hypotheses, retaining v iff the affine seed retains ident v gives RetentionChannels X Y f π c_π C_π C_pair C_var with f = a^H, π = (L/P)^H, c_π = 1, C_π = C_pair = 2^H, C_var = 4. I matched each of the six fields against the RetentionChannels structure in ColumnDetector.lean and against affineRetains_rates/dens_affineRetains:

• dens_X and dens_Y follow from dens_affineRetains after the ℚ≥0 → ℝ cast.
• lower (1·a^H ≤ π) and upper (π ≤ 2^H·a^H) are exactly the rate bounds.
• pair has the same shape as 2^H * a^H * dens{Y y}, and ident's injectivity carries w ≠ y across.
• tail moves A to A.image ident, using filter_image and card_image_of_injective, so #A and the retained counts are preserved.

The constants agree with the docstring and the PR body. Independence between the two channels comes from the interface's product seed space, so using the same channel for X and Y is legitimate.

Nonvacuity and tests. The hypotheses are satisfiable whenever 1/P ≤ a ≤ 1, so the result is not vacuous. The test instantiates the theorem at P = 5, H = 2, a = 1/2, ident = id, then feeds it to lt_card_of_lt_columnDetector with J = 20: the threshold J/(4·C_π·f) = 5 = |𝔽₅| makes the detector bound ≤ 1/4 hold for every matrix. This checks that the instance plugs into the detector lemma with clipped ϕ/ρ. It is not a numerical sanity check of a flagged column; an optional nit would be one example with a larger P where the threshold is below |V|.

Provenance and placement. It cites only the preprint [OpenAI2026LogSpace] (4.8)/(4.9), §4.2, marked "not peer reviewed", and the PR states that no OAI Lean code was used. The module sits next to RetentionChannel.lean in Cslib.Probability, and the umbrella import is sorted. ROADMAP and catalogue are unaffected, which is fine for an interface instance. The limitation (frame-conditioned channels of #1691 need their own instance) is stated.

Limits: I did not build anything with Lean, and I relied on the PR's local check.sh claim plus hosted CI. I did not re-review #1696 or #1688.

[edemaine]

reviewer-codex-edemaine — independent agent approval of 0fd3e72; not human approval. Reviewed the complete three-file own layer over merge a7541c6. The merge has no conflict-resolution delta; the separately reviewed #1696 and #1688/#1681 layers carry forward.

All six RetentionChannels fields follow with the stated constants. Injectivity preserves distinct identifiers, finite-set cardinality and retained counts when transferring the lower tail to A.image ident. Using the same channel predicate for X and Y is sound because the detector samples their seeds independently on the product space. The F₅, H=2, a=1/2 instance is satisfiable and plugs into the detector theorem; its J=20 example deliberately exercises the no-flag regime rather than a positive detector.

The source mapping is to the unrestricted affine sampling ingredients and detector assumptions (4.8)–(4.9), not the frame-conditioned estimates still open for #1691. Placement and reuse are appropriate; no curated-abstract or machine/resource impact.

Lean Action CI 40984641793 was running when inspected; title CI and diff whitespace checks passed. 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 5a6439697292404dbe10d9dea22724d9d9142560 against my earlier review of 0fd3e72a85ca7c97e9a56a4ef02de0155f002e94.

Verdict: FINAL (integration-only delta).

Payload (unchanged): DetectorChannels.lean, the RetentionChannels instance for #1688's unconditioned affine channels, and its test. The delta is merge 5a6439697 of the refreshed #1696 (915171329).

Checked:

• Complexity/Probability/PairwiseIndependentHash/DetectorChannels.lean and ComplexityTests/DetectorChannels.lean are byte-identical to the old head.
• The diff from the new head to main 311e9841f is exactly feat(Foundations): pilot and probabilistic column detectors for one hierarchy stage #1696's eight files plus these two own files plus one Complexity.lean import line: 10 files.
• The add/add conflict in RetentionChannel.lean resolves to main's merged feat(Probability): affine retention channels over a prime field #1688 version byte for byte. That version differs from the stacked copy only in the module docstring, which now cites [OpenAI2026LogSpace] through the bibliography. No declarations differ, so nothing used by DetectorChannels 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. This approval depends on #1696 at 915171329.

[edemaine]

reviewer-codex-edemaine: APPROVE at 5a6439697292404dbe10d9dea22724d9d9142560 (independent agent integration-delta review, not human approval). Reuse my whole-layer review and the refreshed #1696 parent review.

DetectorChannels and its concrete test are byte-identical to approved 0fd3e72a. Relative to parent 915171329b2560084440f987fe8c274bbbfb7380, the entire layer is exactly those two files and one aggregate import; all other parent files are retained. The merged RetentionChannel source is main's already-reviewed version. The unrestricted-channel interpretation, injective identifier transfer and independent product seeds remain unchanged; no new findings or curated-abstract impact.

git diff --check passes. Exact-head Lean CI 41033190052 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 29574df8e9a864aadb14352b82ce546c8ceacb4b, following current outside approval, successful source CI, and required queue validation. The landing tree equals the independently checked actual-parent merge. Both source/test files remain byte-identical to the reviewed version; the three-path layer, parent and preceding main payloads are retained.

The exact main/cache handoff restored that queue producer, passed all six gates and applicable checks, and published a mapping and sampled immutable artifacts verified publicly readable. This instantiates unrestricted affine channels with independent product seeds. Frame-conditioned estimates and the iterated hierarchy remain open in #1679/#1444. No selected-abstract impact; source credit is preserved.