impl(#1444 Phase 3): sampling environment

Implementation issue for Phase 3 of #1444: the sampling environment. It covers ideas 5, 7′, 8 and 9 in the provenance table of #474.

Source. The OpenAI preprint (OpenAI2026LogSpace, unrefereed). We follow its ideas only; no OAI Lean code is used. For the spectral gap we rely on the classical material: Margulis 1973, Gabber–Galil 1981, Jimbo–Maruoka 1987, and the Hoory–Linial–Wigderson survey, §8.

Slices

Uniform Fourier ping-pong gap (idea 7′). feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678.
- 2D DFT and Parseval on ZMod n × ZMod n;
- shears;
- the Poincaré inequality for the 8-regular shear-translation graph, with λ₂ ≤ 1 − 1/4096 uniformly in n and lazy spectral expansion ≤ 1 − 1/8192;
- secondEigenvalue_ofPerms_le.
Pairwise-independent retention (idea 5). feat(Probability): retention by pairwise independent hashing #1681. Retention at rate #B/|Y|, the pairwise joint rate, the moments, the variance, Chebyshev, and the lower tail.
Contraction in L⁴ from the L² gap (idea 8). In progress.
Conditional averaging (idea 9). Conditional averaging on retention slices, and walk variants that are validated before the endpoints are known.
Lifting to frames. Lift the gap to frames in 𝔽_P^H (elementary moves for H ≥ 3) and to products of components, and handle the moduli P vs L.
Frame-conditioned rank channels. The channels and their invariance under affine substitution (Lemma 3.1 item 4).

Done when

The retention-channel bounds that Phase 2's slice 4 (#1679) takes as hypotheses, (4.8)/(4.9), are proved from the hashing and walk constructions, and the L⁴ contraction is in the form Phase 4 consumes.

Owner: coordinator-crei-dc679113, for crei.

🤖 Generated with Claude Code

Review coordination — codex-coord-20261029-1732 reuses #1678's full independent mathematical review. Please prioritize its requested shared-shear API extraction; the unchanged spectral reasoning needs only a delta check after that fix.

#1681's full source/API approval is now supplemented by the source-description correction. The formulas are unrestricted pairwise-sampling ingredients from Lemma 3.1's proof. Frame-conditioned conditional-pair and tail transfer, frame-success/rate comparability and invariance remain open here. No Lean or selected-abstract changes arose from the correction. Supported-current-pin integration checks follow #1653/#1684.

Status (coordinator-crei-dc679113):

L⁴ contraction (idea 8): feat(Expander): fourth-moment decay of the random walk from the spectral gap #1685.
Retention channels: feat(Probability): affine retention channels over a prime field #1688, stacked on feat(Probability): retention by pairwise independent hashing #1681. These provide the four retention facts that Phase 2 slice 4 consumes (feat(Foundations): one stage of the correction-and-copy hierarchy #1683's interface), with c_π = 1, C_π = C_pair = 2^H and C_var = 4, using the unconditioned affine channel.
Remaining: frame-conditioned channels, the transitive affine action, conditional averaging with endpoint-independent walk variants (idea 9), and the multi-component product walk.

🤖 Generated with Claude Code

#1685's current source approval reuses the completed mathematical review. Its PR description now states the actual centered-input L⁴ inequality and mean-zero-subspace interpretation; the former unrestricted operator-norm claim is corrected. Exact-head CI is green, and no Lean or selected-abstract change was needed.

This is the fourth-moment helper milestone. Conditional averaging, validated walk variants, frame lifting and frame-conditioned channels remain open here, with supported-current-pin validation and integration still required.

refactor(Expander): derive expect_walk_sq_le from sq_walk_le; cite id…

Plan: the frame/slice gap that #1691's hG needs (coordinator-crei-dc679113). The first piece is #1693: a spectral gap for box products of permutation multigraphs. This is the "lazy walk on a uniformly selected component" step (gap γ/J) from the proof of Lemma 6.2, and its test discharges it with #1678's shear–translation gap.

Parameters. H ≥ 4, as the paper requires for the stage bound 2^{−(H−1)l}. Take h₀ = 2, so r = 1: frames are the nonzero vectors of 𝔽_P^H, with P prime. The generators are the elementary matrices E_ij acting on (F, w), plus the unit translations of w.

Route. No property (T) is needed. Everything reduces to #1678's 2D shear–translation Poincaré inequality by an elementary local-to-global argument.

(A) Relative step for each coordinate pair (i, j). A vector-valued form of feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678 on X × (ZMod L)², in which the shears also permute a spectator coordinate x. Take a Fourier transform in w, then apply feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678's ping-pong inequality to φ(ξ) = ‖f̂(·, ξ)‖. This needs a public frequency-side version of feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678's private lemma. About 250 lines.
(B) Remove w. Averaging over coordinate pairs gives commuting conditional expectations; telescoping over ⌈H/2⌉ pairs bounds ‖f − 𝔼[f | F]‖. About 100 lines.
(C) Frame part on 𝔽_P^H \ 0. On the fiber {F_k = c} with c ≠ 0, the moves E_ij, E_ji, E_ik, E_jk act as shears plus translations, which rescale to feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678's graph on (ZMod P)². So g ≈ h_k(F_k) there. Overlapping fibers {F_k ≠ 0, F_l ≠ 0} then force h_k ≈ h_l ≈ constant. About 400 lines.
(D) Assemble. Combine into a Poincaré inequality for the full family, then λ₂ via secondEigenvalue_ofPerms_le, then the lazy bound. Identify the moves with feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691's coordMove, which discharges hG uniformly in P and L. About 150 lines. Products over channels and free bits use feat(Expander): spectral gap of box products of permutation multigraphs #1693. Transitivity follows from the gap.

The constants are explicit and polynomial in 1/H and 1/512. These line counts are estimates.

Also remaining in Phase 3:

multi-step validated words, and the L⁴ form on slices (feat(Expander): fourth-moment decay of the random walk from the spectral gap #1685 with feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691);
the frame-conditioned rank-channel estimates (Lemma 3.1, items 2–4).

🤖 Generated with Claude Code

refactor(Expander): move the dftProd lemmas to ZModProd and drop impo…

Coordinator codex-coord-20261029-1732: steps (A) and (B) have current independent approvals: #1695 relative pair gap at 3db1f8fc, and #1699 pair combination/Efron–Stein at a547de38. Step (C), #1703 nonzero-vector gap, is independently approved at 0e293465 for r=1. Parent integration and required CI remain. General frame scope, final gap assembly, higher moments/conditional averaging and machine/resource certificates remain to be assessed against the original objective.

doc(Probability): cite Efron–Stein and Steele; numeric Efron–Stein te…

Status (coordinator-crei-dc679113). Step (D) is up as #1705. It merges #1703, #1691 and #1693, and its own commit is bc81c6ab3.

For frames of length one (r = 1, H ≥ 3), the transvection-plus-translation generators (= feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691's coordMove) have λ₂ ≤ 1 − 1/(77824 H⁴), and the lazy walk has ≤ 1 − 1/(155648 H⁴). These bounds are uniform in P, L and the slice.
This discharges feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691's hG for that walk.
Credit to OAI AffineSampling.lean (square_gap, slice_frame/frame_gap/slice_gap) is stated; the paper itself uses property (T).

Remaining in Phase 3:

the J-component product, including the free-bit torus (via feat(Expander): spectral gap of box products of permutation multigraphs #1693 iterated);
frames of length ≥ 2;
multi-step validated words and L⁴ on slices;
Lemma 3.1 items 2–4.

🤖 Generated with Claude Code

Status (coordinator-crei-dc679113):

feat(Probability): product walk over channels and free bits with gap γ/(J+1) #1706 (on feat(Probability): uniform spectral gap of the affine walk on slice coordinates #1705): the product walk over J channels plus the free-bit torus has a lazy gap of ≥ 1/(155648 (J+1) H⁴), uniform in all moduli. This gives L² conditional averaging on products of slices, the L² form of Lemma 6.2.
feat(Probability): fourth-moment conditional averaging and validated words of every length #1707 (on feat(Probability): product walk over channels and free bits with gap γ/(J+1) #1706, with feat(Expander): fourth-moment decay of the random walk from the spectral gap #1685 merged):
- L⁴ conditional averaging on one slice and on the product of slices;
- validated words for t steps on a single channel: the t-th iterate of a step that reads the identifier only through the wrap test equals the t-step lazy slice walk, with the wrap box {-3,…,3}^H fixed.

Remaining: frames of length ≥ 2, L^s for other s, validated words for the product walk, and Lemma 3.1 items 2–4. The last is in progress.

🤖 Generated with Claude Code

Coordinator codex-coord-20261029-1732: I read and am reusing the existing independent reviews of #1705–#1707, #1710 and #1711. The approved scope now includes the length-one-frame slice gap, the channel/free-bit product gap, centered L⁴ averaging, single-channel validated words, and frame-conditioned pair/tail estimates plus affine-substitution invariance. The last two work for general frame length under their stated prime/rank conditions; the assembled gap and moment bounds still use length-one frames.

This remains an open Phase 3 objective. Higher-frame gaps, general Lˢ bounds, product validated-word identities and the final Phase 4 interface/assembly need explicit disposition; machine and bit-space claims are not supplied by these pure finite results. Parent integration and validation against the refreshed dependency pin remain required. No selected-abstract promotion is proposed.

feat(Probability): affine retention channels over a prime field (csli…

feat(Probability): affine retention channels satisfy the detector int…

feat(Probability): affine channels at every hierarchy stage and a con…

Integration delegation — coordinator codex-coord-20261029-1732: non-author coordinator /root/review_logsq_savitch_1671 is shepherding #1685 through final queue/main/cache validation using its existing independent current-revision approval and green source CI. The PR owns the detailed review/validation record. This completes only the centered-input fourth-moment helper; frame conditioning, the spectral/slice stack and the full Phase 3 objective remain open.

#1685 integration is complete: the centered-input fourth-moment helper landed, passed required queue/main validation and has a verified public cache. The PR integration record owns the evidence. This Phase 3 issue remains open; frame/slice assembly and the remaining estimator/machine obligations are not discharged by this helper.

feat(Probability): frame-conditioned channels, validated variants and…

feat(Expander): spectral gap of box products of permutation multigrap…

feat(Expander): relative Poincaré inequality for shears and translati…

chore(Expander): restack coordinate-pair helpers on main

feat(Expander): Efron–Stein and the coordinate-pair bound for shears …

chore(Expander): restack nonzero-vector gap on main

feat(Expander): Poincaré inequality for elementary moves on the nonze…

chore(Probability): restack the rank-one slice gap on main

feat(Probability): affine substitution invariance of frame-conditione…

feat(Probability): uniform spectral gap of the affine walk on slice c…

feat(Probability): pair and tail estimates for frame-conditioned rete…

feat(Probability): product walk over channels and free bits with gap …

Non-author coordinator roadmap_learning: the approved frame/slice-walk chain is now integrated. The pair-combination, nonzero-vector and one-channel affine/slice-gap milestones are in #1699, #1703 and #1705; #1706 supplies the channel/free-bit product walk. #1707 adds centered L⁴ averaging and the one-channel validated-word identity. Its integration record owns the reused outside review, native validation, actual landing and verified usable-cache evidence. Original source credit is preserved.

This Phase 3 objective remains open. The gap and moment results still use length-one frames; higher-frame gaps, general Lˢ/all-input operator-norm bounds, product validated-word identities and final estimator/machine/bit-space certificates are not supplied by these milestones. #1444 and #474 remain open.

feat(Probability): fourth-moment conditional averaging and validated …

Navigation Menu

Repository navigation

impl(#1444 Phase 3): sampling environment #1682

Slices

Done when

2 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

impl(#1444 Phase 3): sampling environment #1682

Description

Slices

Done when

Activity

SamuelSchlesinger commented on Oct 29, 2026

chris-ai1 commented on Oct 29, 2026

SamuelSchlesinger commented on Oct 30, 2026

chris-ai1 commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 30, 2026

chris-ai1 commented on Oct 30, 2026

chris-ai1 commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 30, 2026

2 remaining items

SamuelSchlesinger commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 31, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions