diff --git a/Complexity.lean b/Complexity.lean
index 8f5f9ddb1..22134781e 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2534,6 +2534,7 @@ public import Complexity.Foundations.Combinatorics.Expander.Mixing
 public import Complexity.Foundations.Combinatorics.Expander.Multigraph
 public import Complexity.Foundations.Combinatorics.Expander.PairShearTranslation
 public import Complexity.Foundations.Combinatorics.Expander.Perm
+public import Complexity.Foundations.Combinatorics.Expander.PiProduct
 public import Complexity.Foundations.Combinatorics.Expander.Power
 public import Complexity.Foundations.Combinatorics.Expander.Random
 public import Complexity.Foundations.Combinatorics.Expander.Reindex
@@ -3142,6 +3143,7 @@ public import Complexity.Probability.PairwiseIndependent
 public import Complexity.Probability.PairwiseIndependentHash
 public import Complexity.Probability.PairwiseIndependentHash.Affine
 public import Complexity.Probability.PairwiseIndependentHash.AtomChannels
+public import Complexity.Probability.PairwiseIndependentHash.ComponentGap
 public import Complexity.Probability.PairwiseIndependentHash.ConditionalAveraging
 public import Complexity.Probability.PairwiseIndependentHash.DetectorChannels
 public import Complexity.Probability.PairwiseIndependentHash.FrameChannel
diff --git a/Complexity/Foundations/Combinatorics/Expander/PiProduct.lean b/Complexity/Foundations/Combinatorics/Expander/PiProduct.lean
new file mode 100644
index 000000000..1fed404c5
--- /dev/null
+++ b/Complexity/Foundations/Combinatorics/Expander/PiProduct.lean
@@ -0,0 +1,123 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.Combinatorics.Expander.BoxProduct
+
+/-!
+# Products of finitely many permutation multigraphs
+
+Given permutation families `σ i : K i → Equiv.Perm (V i)` for the components `i : Fin n`, the
+family `piPerms σ` on the product `∀ i, V i` moves one component at a time: the move `⟨i, k⟩`
+applies `σ i k` to the component `i` and leaves the others alone. Its multigraph is the product
+walk that picks a component with probability proportional to its number of moves and makes one
+move there.
+
+Poincaré inequalities tensorize (`mul_expect_sq_le_piPerms`): if every component satisfies
+`c 𝔼 f² ≤ ∑ k, 𝔼 (f ∘ σ i k - f)²` for functions of mean zero, then so does the product, with the
+same constant. The proof iterates the binary box product (`mul_expect_sq_le_boxProdPerms`) along
+`Fin.consEquiv`. In terms of the second eigenvalue (`secondEigenvalue_ofPerms_piPerms_le`), the
+gap `c / (2 |K|)` of a component with `|K|` moves becomes `c / (2 ∑ i, |K i|)`: for `J` components
+with the same number of moves, the gap is divided by `J`.
+
+This is the product walk over components of the proof of Lemma 6.2 of the OpenAI preprint on
+derandomizing logarithmic space [OpenAI2026LogSpace], with gap `γ / J` for `J` components.
+
+## Main definitions
+
+* `Cslib.RotationMap.piPerms`: the permutations of `∀ i, V i` moving one component.
+
+## Main results
+
+* `Cslib.RotationMap.mul_expect_sq_le_piPerms`: Poincaré inequalities tensorize over `Fin n`.
+* `Cslib.RotationMap.secondEigenvalue_ofPerms_piPerms_le`: the second eigenvalue of the product.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace]
+-/
+
+public section
+
+open Finset Function
+open scoped BigOperators
+
+namespace Cslib.RotationMap
+
+variable {ι : Type*} [DecidableEq ι] {V K : ι → Type*}
+
+/-- The permutations of `∀ i, V i` that move one component: `⟨i, k⟩` applies `σ i k` to the
+component `i`. -/
+@[expose]
+def piPerms (σ : ∀ i, K i → Equiv.Perm (V i)) (k : Σ i, K i) : Equiv.Perm (∀ i, V i) :=
+  Equiv.piCongrRight (update (fun _ ↦ Equiv.refl _) k.1 (σ k.1 k.2))
+
+@[simp]
+theorem piPerms_apply (σ : ∀ i, K i → Equiv.Perm (V i)) (i : ι) (k : K i) (x : ∀ i, V i) :
+    piPerms σ ⟨i, k⟩ x = update x i (σ i k (x i)) := by
+  funext j
+  by_cases h : j = i
+  · subst h
+    simp [piPerms]
+  · simp [piPerms, h]
+
+/-- **Poincaré inequalities tensorize over finitely many components**: if every component family
+satisfies `c 𝔼 f² ≤ ∑ k, 𝔼 v, (f (σ i k v) - f v) ^ 2` for every function `f` of expectation zero,
+then so does `piPerms σ` on the product, with the same constant. -/
+theorem mul_expect_sq_le_piPerms {n : ℕ} {V K : Fin n → Type*} [∀ i, Fintype (V i)]
+    [∀ i, Fintype (K i)] (σ : ∀ i, K i → Equiv.Perm (V i)) {c : ℝ}
+    (hσ : ∀ i (f : V i → ℝ), 𝔼 v, f v = 0 →
+      c * 𝔼 v, f v ^ 2 ≤ ∑ k, 𝔼 v, (f (σ i k v) - f v) ^ 2)
+    (f : (∀ i, V i) → ℝ) (hf : 𝔼 x, f x = 0) :
+    c * 𝔼 x, f x ^ 2 ≤ ∑ k, 𝔼 x, (f (piPerms σ k x) - f x) ^ 2 := by
+  induction n with
+  | zero =>
+    have h0 (x : ∀ i, V i) : f x = 0 := by
+      have : ∀ y : ∀ i, V i, f y = f x := fun y ↦ congrArg f (Subsingleton.elim y x)
+      rw [← hf]
+      simp only [this, Fintype.expect_const]
+    simp only [h0, sub_self]
+    simp
+  | succ n ih =>
+    -- Split off the component `0` and apply the binary box product.
+    let e := Fin.consEquiv V
+    set g : V 0 × (∀ i : Fin n, V i.succ) → ℝ := fun p ↦ f (e p) with hg
+    have hexp (φ : (∀ i, V i) → ℝ) : 𝔼 p, φ (e p) = 𝔼 x, φ x :=
+      Fintype.expect_equiv e _ _ fun _ ↦ rfl
+    have hbox := mul_expect_sq_le_boxProdPerms (σ := σ 0)
+      (τ := piPerms fun i : Fin n ↦ σ i.succ) (hσ 0)
+      (fun g hg ↦ ih (fun i ↦ σ i.succ) (fun i ↦ hσ i.succ) g hg) g
+      (by rw [hexp f]; exact hf)
+    have hL : 𝔼 p, g p ^ 2 = 𝔼 x, f x ^ 2 := hexp fun x ↦ f x ^ 2
+    rw [hL] at hbox
+    refine hbox.trans_eq ?_
+    rw [Fintype.sum_sum_type, Fintype.sum_sigma, Fintype.sum_sigma, Fin.sum_univ_succ]
+    congr 1
+    · refine sum_congr rfl fun k _ ↦ ?_
+      rw [← hexp]
+      refine expect_congr rfl fun p _ ↦ ?_
+      simp only [hg, boxProdPerms_inl, piPerms_apply, e, Fin.consEquiv_apply, Fin.cons_zero,
+        Fin.update_cons_zero]
+    · refine sum_congr rfl fun i _ ↦ sum_congr rfl fun k _ ↦ ?_
+      rw [← hexp]
+      refine expect_congr rfl fun p _ ↦ ?_
+      simp only [hg, boxProdPerms_inr, piPerms_apply, e, Fin.consEquiv_apply, Fin.cons_succ,
+        Fin.cons_update]
+
+/-- **The second eigenvalue of a product of permutation multigraphs**: if every component satisfies
+the Poincaré inequality with constant `c`, then `λ₂ ≤ 1 - c / (2 ∑ i, |K i|)` for the product. For
+`J` components with `m` moves each, the component gap `c / (2 m)` is divided by `J`. -/
+theorem secondEigenvalue_ofPerms_piPerms_le {n : ℕ} {V K : Fin n → Type*} [∀ i, Fintype (V i)]
+    [∀ i, Fintype (K i)] [Nonempty (Σ i, K i)]
+    [Nontrivial (∀ i, V i)] (σ : ∀ i, K i → Equiv.Perm (V i)) {c : ℝ}
+    (hσ : ∀ i (f : V i → ℝ), 𝔼 v, f v = 0 →
+      c * 𝔼 v, f v ^ 2 ≤ ∑ k, 𝔼 v, (f (σ i k v) - f v) ^ 2) :
+    (ofPerms (piPerms σ)).secondEigenvalue ≤ 1 - c / (2 * Fintype.card (Σ i, K i)) :=
+  secondEigenvalue_ofPerms_le _ fun f hf ↦ mul_expect_sq_le_piPerms σ hσ f hf
+
+end Cslib.RotationMap
diff --git a/Complexity/Probability/PairwiseIndependentHash/ComponentGap.lean b/Complexity/Probability/PairwiseIndependentHash/ComponentGap.lean
new file mode 100644
index 000000000..3c0046e9d
--- /dev/null
+++ b/Complexity/Probability/PairwiseIndependentHash/ComponentGap.lean
@@ -0,0 +1,293 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.Combinatorics.Expander.PiProduct
+public import Complexity.Probability.PairwiseIndependentHash.SliceGap
+import Complexity.Foundations.Combinatorics.Expander.PairShearTranslation
+import Complexity.Foundations.Data.Finset.Expect
+
+/-!
+# The spectral gap of the product walk over channels and free bits
+
+The averaging walk of the sampler moves several independent components: `J` conditioned
+channels, with slice coordinates `Frame (P j) H 1 × ZMod (L j) ^ H`, and one block of free bits,
+identified with the torus `ZMod M ^ H` (for `M = 2 ^ q`, the bit strings of length `H q`). On the
+torus, the generators `affineGenerator` act by the affine action alone (`torusMove`). The product
+walk (`componentMove`) picks one component and makes one affine move there.
+
+* **The torus.** For `H ≥ 2`, the coordinate-pair bound
+  `expect_sq_sub_expect_le_pairShearTranslation` with a trivial spectator gives the Poincaré
+  inequality with constant `2048 H`, uniformly in `M` (`expect_sq_le_torusMove`).
+* **The product.** Each channel satisfies the Poincaré inequality with constant `38912 H²`
+  (`expect_sq_le_affineMove`), and so does the torus. Poincaré inequalities tensorize
+  (`mul_expect_sq_le_piPerms`, `mul_expect_sq_le_boxProdPerms`), so the product satisfies it with
+  the same constant (`expect_sq_le_componentMove`). Since the product has `J + 1` times as many
+  moves, its gap is the single-component gap divided by the number `J + 1` of components:
+  `λ₂ ≤ 1 - 1 / (77824 (J + 1) H ^ 4)` and, for the lazy walk, spectral expansion at most
+  `1 - 1 / (155648 (J + 1) H ^ 4)`, uniformly in the primes `P j`, the sides `L j` and `M`.
+* **Conditional averaging.** Transported to the product of the retention slices of identifiers
+  `y j` (`componentEquiv`), the lazy walk contracts the variance by that bound squared per step,
+  uniformly in the identifiers (`expect_walk_pow_componentMove_sub_expect_sq_le`).
+
+This is the product walk of the proof of Lemma 6.2 of the OpenAI preprint on derandomizing
+logarithmic space [OpenAI2026LogSpace]: the free bits as `(ℤ / 2^q ℤ) ^ H` with the affine action
+on that coordinate alone, and "the lazy walk from Lemma 6.1 [applied] to a uniformly selected
+component", with gap `γ_H / J_comp`. The preprint's single-component gap comes from Shalom's
+property (T); the elementary route through coordinate pairs and frames follows OpenAI's Lean
+development, the file
+[`AffineSampling.lean`](https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/lean/OAI/Computability/Logspace/AffineSampling.lean)
+at revision `7ef5c0cc` (`ExactDerandomization.Analysis.Square.square_gap`, `slice_frame`,
+`frame_gap`, `slice_gap`). The statements and the proofs here are independent of that code, which
+was not consulted.
+
+## Main definitions
+
+* `Cslib.Probability.torusMove`: the affine moves of the free-bit torus.
+* `Cslib.Probability.componentMove`: the moves of the product walk over channels and free bits.
+* `Cslib.Probability.componentEquiv`: coordinates on a product of retention slices.
+
+## Main results
+
+* `Cslib.Probability.expect_sq_le_torusMove`: the Poincaré inequality on the torus.
+* `Cslib.Probability.expect_sq_le_componentMove`: the Poincaré inequality for the product walk.
+* `Cslib.Probability.secondEigenvalue_ofPerms_componentMove_le`,
+  `Cslib.Probability.spectralExpansion_lazy_ofPerms_componentMove_le`: the gap `γ / (J + 1)`.
+* `Cslib.Probability.expect_walk_pow_componentMove_sub_expect_sq_le`: conditional averaging over
+  channels and free bits.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace]
+-/
+
+public section
+
+namespace Cslib.Probability
+
+open Finset Function Matrix RotationMap
+open scoped BigOperators
+
+variable {H M : ℕ}
+
+/-! ### The free-bit torus -/
+
+variable (H M) in
+/-- **The affine moves of the free-bit torus** `ZMod M ^ H`: the generators `affineGenerator`
+acting on the torus alone, `w ↦ (1 + E_ab) w` and `w ↦ w + e_i`. -/
+@[expose] def torusMove (k : {p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H) :
+    Equiv.Perm (Fin H → ZMod M) :=
+  affineSL (ZMod M) (affineGenerator H k).1 fun i ↦ ((affineGenerator H k).2 i : ZMod M)
+
+@[simp]
+theorem torusMove_inl (p : {p : Fin H × Fin H // p.1 ≠ p.2}) (w : Fin H → ZMod M) :
+    torusMove H M (.inl p) w = update w p.1.1 (w p.1.1 + w p.1.2) := by
+  simp only [torusMove, affineGenerator, Sum.elim_inl, affineSL_apply,
+    SpecialLinearGroup.map_transvection, SpecialLinearGroup.transvection_mulVec, map_one, one_mul]
+  exact funext fun _ ↦ by simp
+
+@[simp]
+theorem torusMove_inr (i : Fin H) (w : Fin H → ZMod M) :
+    torusMove H M (.inr i) w = update w i (w i + 1) := by
+  ext j
+  simp only [torusMove, affineGenerator, Sum.elim_inr, affineSL_apply, map_one,
+    SpecialLinearGroup.coe_one, one_mulVec, Pi.add_apply, update_apply]
+  split_ifs with h
+  · subst h
+    simp
+  · simp [h]
+
+/-- **The Poincaré inequality for the free-bit torus** `ZMod M ^ H`, for `H ≥ 2`, uniformly in
+`M`: every real function `f` of mean zero has second moment at most `2048 H` times its total squared
+change along the affine moves. -/
+theorem expect_sq_le_torusMove [NeZero M] (hH : 2 ≤ H) (f : (Fin H → ZMod M) → ℝ)
+    (hf : 𝔼 w, f w = 0) :
+    𝔼 w, f w ^ 2 ≤ 2048 * H * ∑ k, 𝔼 w, (f (torusMove H M k w) - f w) ^ 2 := by
+  set D := ∑ k, 𝔼 w, (f (torusMove H M k w) - f w) ^ 2
+  have hterm (k) : 𝔼 w, (f (torusMove H M k w) - f w) ^ 2 ≤ D :=
+    single_le_sum (f := fun k ↦ 𝔼 w, (f (torusMove H M k w) - f w) ^ 2)
+      (fun _ _ ↦ expect_nonneg fun _ _ ↦ sq_nonneg _) (mem_univ k)
+  have hH2 : Nontrivial (Fin H) := Fin.nontrivial_iff_two_le.2 hH
+  choose σ hσ using fun i : Fin H ↦ exists_ne i
+  -- The coordinate-pair bound with a trivial spectator.
+  set F : Unit × (Fin H → ZMod M) → ℝ := fun p ↦ f p.2 with hF
+  have hU (φ : (Fin H → ZMod M) → ℝ) : 𝔼 p : Unit × (Fin H → ZMod M), φ p.2 = 𝔼 w, φ w := by
+    simp [Fintype.expect_prod_type]
+  have h := expect_sq_sub_expect_le_pairShearTranslation (fun _ _ ↦ Equiv.refl Unit) σ hσ F
+  have hL : 𝔼 p, (F p - 𝔼 w, F (p.1, w)) ^ 2 = 𝔼 w, f w ^ 2 := by
+    simp only [hF, hf, sub_zero]
+    exact hU fun w ↦ f w ^ 2
+  have hpair (i : Fin H) (k : Fin 4) :
+      𝔼 p, (F (pairShearTranslationMove (Equiv.refl Unit) (Equiv.refl Unit) i (σ i) k p) -
+        F p) ^ 2 ≤ D := by
+    have hσi : i ≠ σ i := (hσ i).symm
+    fin_cases k
+    · have := hterm (.inl ⟨(i, σ i), hσi⟩)
+      simp only [torusMove_inl] at this
+      refine le_trans (le_of_eq ?_) this
+      rw [← hU]
+      rfl
+    · have := hterm (.inl ⟨(σ i, i), hσi.symm⟩)
+      simp only [torusMove_inl] at this
+      refine le_trans (le_of_eq ?_) this
+      rw [← hU]
+      rfl
+    · have := hterm (.inr i)
+      simp only [torusMove_inr] at this
+      refine le_trans (le_of_eq ?_) this
+      rw [← hU]
+      rfl
+    · have := hterm (.inr (σ i))
+      simp only [torusMove_inr] at this
+      refine le_trans (le_of_eq ?_) this
+      rw [← hU]
+      rfl
+  rw [hL] at h
+  refine h.trans ?_
+  calc 512 * ∑ i, ∑ k, 𝔼 p, (F (pairShearTranslationMove (Equiv.refl Unit) (Equiv.refl Unit)
+        i (σ i) k p) - F p) ^ 2 ≤ 512 * ∑ _i : Fin H, ∑ _k : Fin 4, D := by
+        gcongr with i _ k _
+        exact hpair i k
+    _ = 2048 * H * D := by
+        simp only [sum_const, card_univ, Fintype.card_fin, nsmul_eq_mul]
+        push_cast
+        ring
+
+
+/-! ### Channels and free bits -/
+
+variable {J : ℕ}
+
+variable (H M) in
+/-- **The moves of the product walk** on the coordinates of `J` channels and the free-bit torus:
+`(∀ j, Frame (P j) H 1 × ZMod (L j) ^ H) × ZMod M ^ H`. A move applies an affine move to one
+channel (`affineMove`) or to the torus (`torusMove`). -/
+@[expose] def componentMove (P L : Fin J → ℕ) :
+    (Σ _ : Fin J, {p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H) ⊕
+        ({p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H) →
+      Equiv.Perm ((∀ j, Frame (P j) H 1 × (Fin H → ZMod (L j))) × (Fin H → ZMod M)) :=
+  boxProdPerms (piPerms fun j ↦ affineMove (P j) H (L j) 1) (torusMove H M)
+
+/-- The product walk has `(J + 1) H ^ 2` moves. -/
+theorem card_componentMove_index :
+    Fintype.card ((Σ _ : Fin J, {p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H) ⊕
+      ({p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H)) = (J + 1) * H ^ 2 := by
+  rw [Fintype.card_sum, Fintype.card_sigma, card_affineGenerator_index]
+  simp only [sum_const, card_univ, Fintype.card_fin, smul_eq_mul]
+  ring
+
+variable {P L : Fin J → ℕ} [∀ j, Fact (P j).Prime] [∀ j, NeZero (L j)] [NeZero M]
+
+/-- **The Poincaré inequality for the product walk** over `J` channels and the free-bit torus, for
+`H ≥ 3`, uniformly in the primes `P j`, the sides `L j`, the torus modulus `M` and `J`: every real
+function of mean zero has second moment at most `38912 H²` times its total squared change along the
+moves. -/
+theorem expect_sq_le_componentMove (hH : 3 ≤ H)
+    (f : (∀ j, Frame (P j) H 1 × (Fin H → ZMod (L j))) × (Fin H → ZMod M) → ℝ)
+    (hf : 𝔼 p, f p = 0) :
+    𝔼 p, f p ^ 2 ≤ 38912 * H ^ 2 * ∑ k, 𝔼 p, (f (componentMove H M P L k p) - f p) ^ 2 := by
+  have hH0 : (0 : ℝ) < 38912 * H ^ 2 := by
+    have : (0 : ℝ) < H := by exact_mod_cast (by omega : 0 < H)
+    positivity
+  -- Each component satisfies the Poincaré inequality with constant `1 / (38912 H²)`.
+  have hc {V K : Type} [Fintype V] [Fintype K] (σ : K → Equiv.Perm V)
+      (h : ∀ g : V → ℝ, 𝔼 v, g v = 0 →
+        𝔼 v, g v ^ 2 ≤ 38912 * H ^ 2 * ∑ k, 𝔼 v, (g (σ k v) - g v) ^ 2)
+      (g : V → ℝ) (hg : 𝔼 v, g v = 0) :
+      1 / (38912 * H ^ 2) * 𝔼 v, g v ^ 2 ≤ ∑ k, 𝔼 v, (g (σ k v) - g v) ^ 2 := by
+    rw [one_div_mul_eq_div, div_le_iff₀ hH0]
+    linarith [h g hg]
+  have htorus (g : (Fin H → ZMod M) → ℝ) (hg : 𝔼 w, g w = 0) :
+      𝔼 w, g w ^ 2 ≤ 38912 * H ^ 2 * ∑ k, 𝔼 w, (g (torusMove H M k w) - g w) ^ 2 := by
+    refine (expect_sq_le_torusMove (by omega) g hg).trans ?_
+    have hD : 0 ≤ ∑ k, 𝔼 w, (g (torusMove H M k w) - g w) ^ 2 :=
+      sum_nonneg fun _ _ ↦ expect_nonneg fun _ _ ↦ sq_nonneg _
+    have : (2048 * H : ℝ) ≤ 38912 * H ^ 2 := by
+      have : (1 : ℝ) ≤ H := by exact_mod_cast (by omega : 1 ≤ H)
+      nlinarith
+    exact mul_le_mul_of_nonneg_right this hD
+  have h := mul_expect_sq_le_boxProdPerms
+    (σ := piPerms fun j ↦ affineMove (P j) H (L j) 1) (τ := torusMove H M)
+    (fun g hg ↦ mul_expect_sq_le_piPerms _
+      (fun j ↦ hc _ fun g hg ↦ expect_sq_le_affineMove hH g hg) g hg)
+    (hc _ htorus) f hf
+  rw [one_div_mul_eq_div, div_le_iff₀ hH0, mul_comm] at h
+  exact h
+
+/-- **The second eigenvalue of the product walk** over `J` channels and the free-bit torus is at
+most `1 - 1 / (77824 (J + 1) H ^ 4)`, for `H ≥ 3`, uniformly in the moduli: the single-component
+gap `1 / (77824 H ^ 4)` divided by the number `J + 1` of components. -/
+theorem secondEigenvalue_ofPerms_componentMove_le (hH : 3 ≤ H) :
+    (ofPerms (componentMove H M P L)).secondEigenvalue ≤ 1 - 1 / (77824 * (J + 1) * H ^ 4) := by
+  have hH0 : (0 : ℝ) < H := by exact_mod_cast (by omega : 0 < H)
+  rcases subsingleton_or_nontrivial
+      ((∀ j, Frame (P j) H 1 × (Fin H → ZMod (L j))) × (Fin H → ZMod M)) with hV | hV
+  · rw [secondEigenvalue_eq_zero_of_subsingleton, sub_nonneg]
+    rw [div_le_one (by positivity)]
+    have : (1 : ℝ) ≤ H ^ 4 := one_le_pow₀ (by exact_mod_cast (by omega : 1 ≤ H))
+    have : (0 : ℝ) ≤ J := Nat.cast_nonneg _
+    nlinarith
+  have : Nonempty ((Σ _ : Fin J, {p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H) ⊕
+      ({p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H)) := ⟨.inr (.inr ⟨0, by omega⟩)⟩
+  have h := secondEigenvalue_ofPerms_le (componentMove H M P L) (c := 1 / (38912 * H ^ 2))
+    fun f hf ↦ by
+      have := expect_sq_le_componentMove hH f hf
+      rw [one_div_mul_eq_div, div_le_iff₀ (by positivity)]
+      linarith
+  refine h.trans_eq ?_
+  rw [card_componentMove_index]
+  push_cast
+  field_simp
+  ring
+
+/-- **The spectral gap of the lazy product walk** over `J` channels and the free-bit torus: its
+spectral expansion is at most `1 - 1 / (155648 (J + 1) H ^ 4)`, for `H ≥ 3`, uniformly in the
+primes, the sides and the torus modulus. -/
+theorem spectralExpansion_lazy_ofPerms_componentMove_le (hH : 3 ≤ H) :
+    (ofPerms (componentMove H M P L)).lazy.spectralExpansion ≤
+      1 - 1 / (155648 * (J + 1) * H ^ 4) := by
+  have h₁ :=
+    (ofPerms (componentMove H M P L)).spectralExpansion_lazy_le_one_add_secondEigenvalue_div_two
+  have h₂ := secondEigenvalue_ofPerms_componentMove_le (M := M) (P := P) (L := L) hH
+  have : 1 / (155648 * ((J : ℝ) + 1) * H ^ 4) = (1 / (77824 * (J + 1) * H ^ 4)) / 2 := by
+    rw [div_div]
+    ring
+  rw [this]
+  linarith
+
+variable (M) in
+/-- **Coordinates on a product of retention slices**: a family of channels retaining the
+identifiers `y j`, together with free bits, is a family of slice coordinates together with the
+free bits. -/
+@[expose] def componentEquiv (hL : ∀ j, L j ≤ P j) (y : ∀ j, ZMod (P j)) :
+    (∀ j, RetentionSlice (P j) H 1 (L j) (y j)) × (Fin H → ZMod M) ≃
+      (∀ j, Frame (P j) H 1 × (Fin H → ZMod (L j))) × (Fin H → ZMod M) :=
+  (Equiv.piCongrRight fun j ↦ sliceEquiv (hL j) (y j)).prodCongr (Equiv.refl _)
+
+/-- **Conditional averaging over channels and free bits** (the `L²` case of Lemma 6.2): on the
+product of the retention slices of identifiers `y j` of `J` channels with free bits in
+`ZMod M ^ H`, `t` steps of the lazy product walk contract the variance by
+`(1 - 1 / (155648 (J + 1) H ^ 4)) ^ (2 t)`, for `H ≥ 3`, uniformly in the primes, the sides, the
+identifiers and the torus modulus. -/
+theorem expect_walk_pow_componentMove_sub_expect_sq_le (hH : 3 ≤ H) (hL : ∀ j, L j ≤ P j)
+    (y : ∀ j, ZMod (P j))
+    (f : (∀ j, RetentionSlice (P j) H 1 (L j) (y j)) × (Fin H → ZMod M) → ℝ) (t : ℕ) :
+    𝔼 A, ((((ofPerms (componentMove H M P L)).lazy.reindex
+        (componentEquiv M hL y).symm).walk ^ t) f A - 𝔼 B, f B) ^ 2 ≤
+      (1 - 1 / (155648 * (J + 1) * H ^ 4)) ^ (2 * t) * 𝔼 A, (f A - 𝔼 B, f B) ^ 2 := by
+  have : Nonempty ((Σ _ : Fin J, {p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H) ⊕
+      ({p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H)) := ⟨.inr (.inr ⟨0, by omega⟩)⟩
+  set G := (ofPerms (componentMove H M P L)).lazy.reindex (componentEquiv M hL y).symm
+  refine (G.expect_walk_pow_sub_expect_sq_le t f).trans ?_
+  rw [spectralExpansion_reindex]
+  exact mul_le_mul_of_nonneg_right
+    (pow_le_pow_left₀ (spectralExpansion_nonneg _)
+      (spectralExpansion_lazy_ofPerms_componentMove_le hH) _)
+    (expect_nonneg fun _ _ ↦ sq_nonneg _)
+
+end Cslib.Probability
diff --git a/ComplexityTests/ComponentGap.lean b/ComplexityTests/ComponentGap.lean
new file mode 100644
index 000000000..f3a01b04e
--- /dev/null
+++ b/ComplexityTests/ComponentGap.lean
@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+import ComplexityTests.BoxProductExpander
+import Complexity.Probability.PairwiseIndependentHash.ComponentGap
+
+/-!
+# The product walk over channels and free bits
+
+Concrete moves of a product of permutation families and of the free-bit torus, the Poincaré
+inequality on the cube `(ZMod 2) ^ 3` inherited from the two-point walk, a client of the torus
+inequality for every number of bits, and conditional averaging over two channels over `𝔽₅` and
+`𝔽₇` with eight-valued free bits, with every hypothesis discharged.
+-/
+
+namespace ComplexityTests.ComponentGap
+
+open Cslib Cslib.Probability Cslib.RotationMap Finset
+open ComplexityTests.BoxProductExpander (flip poincare_flip)
+open scoped BigOperators
+
+-- A move of the product changes only its component.
+example : piPerms (fun _ : Fin 3 ↦ flip) ⟨1, ()⟩ ![0, 0, 1] = ![0, 1, 1] := by
+  rw [piPerms_apply]
+  decide
+
+/-- The cube `(ZMod 2) ^ 3`, a product of three edges, inherits the constant `4`. -/
+example (f : (Fin 3 → ZMod 2) → ℝ) (hf : 𝔼 x, f x = 0) :
+    4 * 𝔼 x, f x ^ 2 ≤ ∑ k, 𝔼 x, (f (piPerms (fun _ : Fin 3 ↦ flip) k x) - f x) ^ 2 :=
+  mul_expect_sq_le_piPerms _ (fun _ ↦ poincare_flip) f hf
+
+-- On the torus `(ZMod 8) ^ 3`, `1 + E_01` adds the coordinate `1` to the coordinate `0`, wrapping
+-- around, and a translation adds `1` to one coordinate.
+example : torusMove 3 8 (.inl ⟨(0, 1), by decide⟩) ![7, 1, 0] = ![0, 1, 0] := by
+  rw [torusMove_inl]
+  decide
+example : torusMove 3 8 (.inr 2) ![7, 1, 7] = ![7, 1, 0] := by
+  rw [torusMove_inr]
+  decide
+
+-- Two channels and the torus have `3 · 3 ^ 2 = 27` moves.
+example : Fintype.card ((Σ _ : Fin 2, {p : Fin 3 × Fin 3 // p.1 ≠ p.2} ⊕ Fin 3) ⊕
+    ({p : Fin 3 × Fin 3 // p.1 ≠ p.2} ⊕ Fin 3)) = 27 := card_componentMove_index
+
+/-- **A client of the torus inequality**: for every number `q` of bits per coordinate, a real
+function on `(ZMod (2 ^ q)) ^ 2` invariant under the affine moves is constant. -/
+example (q : ℕ) (f : (Fin 2 → ZMod (2 ^ q)) → ℝ) (hf : ∀ k w, f (torusMove 2 (2 ^ q) k w) = f w)
+    (w w' : Fin 2 → ZMod (2 ^ q)) : f w = f w' := by
+  set f₀ := fun w ↦ f w - 𝔼 v, f v
+  have h := expect_sq_le_torusMove le_rfl f₀ (by simp [f₀, expect_sub_distrib])
+  simp only [f₀, hf, sub_self] at h
+  norm_num at h
+  have h0 := (Fintype.expect_eq_zero_iff_of_nonneg fun w ↦ sq_nonneg (f w - 𝔼 v, f v)).1
+    (le_antisymm h (expect_nonneg fun _ _ ↦ sq_nonneg _))
+  have e (w) : f w = 𝔼 v, f v := sub_eq_zero.1 (pow_eq_zero_iff two_ne_zero |>.1 (congrFun h0 w))
+  rw [e w, e w']
+
+instance (j : Fin 2) : Fact (![5, 7] j).Prime := by
+  fin_cases j
+  exacts [⟨Nat.prime_five⟩, ⟨by decide⟩]
+
+instance (j : Fin 2) : NeZero (![3, 4] j) := by
+  fin_cases j
+  exacts [⟨by norm_num⟩, ⟨by norm_num⟩]
+
+/-- **Conditional averaging over two channels and free bits, with every hypothesis discharged**:
+channels over `𝔽₅` and `𝔽₇` with sides `3` and `4`, conditioned on retaining any identifiers
+`y`, together with free bits in `(ZMod 8) ^ 3`. Each step of the lazy product walk contracts the
+variance by `(1 - 1 / 37822464) ^ 2`. -/
+example (y : ∀ j : Fin 2, ZMod (![5, 7] j))
+    (f : (∀ j, RetentionSlice (![5, 7] j) 3 1 (![3, 4] j) (y j)) × (Fin 3 → ZMod 8) → ℝ)
+    (t : ℕ) :
+    𝔼 A, ((((ofPerms (componentMove 3 8 ![5, 7] ![3, 4])).lazy.reindex
+        (componentEquiv 8 (fun j ↦ by fin_cases j <;> decide) y).symm).walk ^ t) f A -
+          𝔼 B, f B) ^ 2 ≤ (1 - 1 / 37822464) ^ (2 * t) * 𝔼 A, (f A - 𝔼 B, f B) ^ 2 := by
+  have h := expect_walk_pow_componentMove_sub_expect_sq_le le_rfl
+    (fun j ↦ by fin_cases j <;> decide) y f t
+  norm_num at h ⊢
+  exact h
+
+end ComplexityTests.ComponentGap