[chris-ai1]

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

This PR proves item 4 of Lemma 3.1 (the rank-channel estimates) for the frame-conditioned channels of #1691. If every identifier y is replaced by αy + β with α ≠ 0, the joint law of all channel evaluations stays the same. This holds for one channel and for any finite family of independent channels. It is new mathematics for the library, following the ideas of the preprint. Items 2–3 and the detector-interface instance are in #1710.

Stack. This PR depends only on #1691; it is independent of #1710 and of #1696/#1698. The branch is #1691 (feat/conditional-averaging-1444 @ 53de6a3f6, on #1688 → #1681), merged with origin/main @ 0ba8b2e59 (the rc2 bump) without rebasing. Please review only this PR's own commit, b70b78ed7.

Construction. Let A = (a₀, F) be a channel, with A.eval y = a₀ + ∑ j, y ^ (j + 1) • F j. Substituting αy + β gives a new channel:

• the constant column is a₀ + ∑ j, β ^ (j + 1) • F j;
• the coefficient columns are F' k = ∑ j, B k j • F j, where B k j = C(j+1, k+1) α^(k+1) β^(j−k).

The matrix B is upper triangular with diagonal α^(k+1), so it is invertible. Hence F' is again a frame (Fintype.linearIndependent_iff with vecMul_injective_iff_isUnit). The map is injective by mulVec_injective_iff_isUnit, so it is a permutation of the finite channel space (Finite.injective_iff_bijective). This means no inverse substitution and no composition law are needed. The value identity is the binomial theorem (add_pow). B and the helpers about it are private.

Main statements (Complexity/Probability/PairwiseIndependentHash/FrameSubstitution.lean, 215 lines; all under [Fact P.Prime]):

def FrameChannel.affineSubst (β : ZMod P) (hα : α ≠ 0) (A : FrameChannel P H r) : FrameChannel P H r
theorem FrameChannel.eval_affineSubst (A : FrameChannel P H r) (y : ZMod P) :
    (A.affineSubst β hα).eval y = A.eval (α * y + β)
theorem FrameChannel.eval_comp_affineSubst (A : FrameChannel P H r) :
    (A.affineSubst β hα).eval = fun y ↦ A.eval (α * y + β)
theorem FrameChannel.affineSubst_injective :
    Function.Injective (affineSubst (P := P) (H := H) (r := r) β hα)
noncomputable def FrameChannel.affineSubstEquiv : FrameChannel P H r ≃ FrameChannel P H r
theorem FrameChannel.affineSubstEquiv_apply (A : FrameChannel P H r) :
    affineSubstEquiv β hα A = A.affineSubst β hα
theorem dens_eval_comp_affine (hα : α ≠ 0) (β : ZMod P)
    (E : (ZMod P → Fin H → ZMod P) → Prop) [DecidablePred E] :
    dens {A : FrameChannel P H r | E fun y ↦ A.eval (α * y + β)} =
      dens {A : FrameChannel P H r | E A.eval}
theorem dens_pi_eval_comp_affine (hα : α ≠ 0) (β : ZMod P) {ι : Type*} [Fintype ι] [DecidableEq ι]
    (E : (ι → ZMod P → Fin H → ZMod P) → Prop) [DecidablePred E] :
    dens {As : ι → FrameChannel P H r | E fun c y ↦ (As c).eval (α * y + β)} =
      dens {As : ι → FrameChannel P H r | E fun c ↦ (As c).eval}

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

Preprint	Lean
Lemma 3.1, item 4, p. 9: replacing every channel argument y by the same injective affine map αy + β leaves the joint law of all evaluations unchanged, provided α ≠ 0 in F_P; in particular, so does a common fixed padding suffix	dens_eval_comp_affine (one channel), dens_pi_eval_comp_affine (independent channels, any event on all evaluations)
Proof, p. 10: the substitution acts on the positive-degree coefficient columns by an invertible triangular matrix with diagonal α, …, α^{h₀−1}, so it preserves the frame condition	FrameChannel.affineSubst (with the private triangular matrix and linearIndependent_substColumns), FrameChannel.eval_affineSubst
Proof, p. 10: an invertible linear change of variables on the coefficient array, so it preserves the uniform measure conditional on the frame condition	FrameChannel.affineSubst_injective, FrameChannel.affineSubstEquiv (a permutation of the conditioned space)

Differences from the source. The statements are ours. Uniform measure is preserved because the map is an injective self-map of a finite set; the paper instead argues through the change of variables. The radix-padding remark (α a power of D₀, with P > D₀) is not formalized separately: it is the special case α = D₀^m with β the suffix.

Tests (ComplexityTests/FrameSubstitution.lean, 63 lines):

• A channel with frame length two over 𝔽₅: eval_affineSubst together with decide gives the value (3, 1) at 3.
• Instances of both invariance theorems: frames of length two in 𝔽₃², and a pair of independent channels.
• Over 𝔽₃, decide counts show that y ↦ 2y + 1 (which swaps 0 and 1) keeps the joint retention count of {0, 1} at 2 of 6. The constant map α = 0 raises it to 4 of 6, so the hypothesis α ≠ 0 is needed.

Validation at b70b78ed7, 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. With #1710, Lemma 3.1 is complete for frame-conditioned channels. The rest of #1682 is unchanged: 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 b70b78ed7: correctness, API (naming, placement) and the source mapping above.

Integration refresh (2026-10-30): merged the refreshed #1691 head ae99b483b (which contains origin/main 311e984) at 04d684ebc, no rebase, no conflicts. Own-layer diff against #1691 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 04d684ebc.

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 b70b78ed7d8920d38318c0e4ffc04c4afc13c3df.

Reviewed the complete three-file own layer and clean merge, reusing #1691's exact-head coverage. No blocking findings. The binomial expansion has the correct coefficient orientation; its triangular matrix has diagonal α^(k+1), so α ≠ 0 preserves linear independence even in small characteristic. Injectivity recovers the frame coefficients and then the constant column. The resulting finite permutation, and its componentwise product, preserve every event on all evaluations.

Checked the mapping against pinned Lemma 3.1(4) and its proof (pp. 9–10). The result assumes prime P and nonzero α, with arbitrary H/r; for nonempty channel spaces use r ≤ H. It is a distributional invariance theorem, with radix-padding specialization left implicit and no machine/resource claim. The rank-two F₅ evaluation and independent-channel tests are nonvacuous; the F₃ counts (2 unchanged, 4 under a constant map) demonstrate why α ≠ 0 matters. API placement/reuse is appropriate; no curated-abstract impact.

Lean CI, title and diff-whitespace checks passed. I ran no local Lean build. Live head rechecked before posting.

[edemaine]

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

The parent merge preserves FrameSubstitution and its concrete tests byte-for-byte. Its entire own layer over ae99b483b6ec4ae26efb95173e1f20c0f1393c50 is exactly those two files and one aggregate import; all other parent files are retained. The nonzero-affine substitution hypotheses, distributional scope and source mapping are unchanged; no curated-abstract impact.

git diff --check passes. Exact-head Lean CI 41034510120 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. Parent #1691 has landed; I merged main at 854a8b799de95378e5465d2e7a5c26ad87c9db84. The only fix was regenerating Complexity.lean with lake exe mk_all, which removed the duplicate #1691 imports that the textual merge produced. Approved 04d684ebcb6b84aaed46fd2b7fb1fe1f7b1cd67b → 854a8b799de95378e5465d2e7a5c26ad87c9db84: payload +/- lines identical to the own layer (ae99b483b..04d684ebc); mk_all --check ok. I will queue once hosted CI passes.