diff --git a/ArkLib.lean b/ArkLib.lean
index e82af39234..0b524a2263 100644
--- a/ArkLib.lean
+++ b/ArkLib.lean
@@ -141,6 +141,7 @@ import ArkLib.Data.Matrix.Basic
 import ArkLib.Data.Matrix.Sparse
 import ArkLib.Data.Matrix.Vandermonde
 import ArkLib.Data.Misc.Basic
+import ArkLib.Data.Module.Basis
 import ArkLib.Data.MvPolynomial.Degrees
 import ArkLib.Data.MvPolynomial.Interpolation
 import ArkLib.Data.MvPolynomial.LinearMvExtension
@@ -158,6 +159,7 @@ import ArkLib.Data.Polynomial.SplitFold
 import ArkLib.Data.Polynomial.Trivariate
 import ArkLib.Data.Probability.Instances
 import ArkLib.Data.Probability.Notation
+import ArkLib.Data.Probability.OracleCompBridge
 import ArkLib.OracleReduction.BCS.Basic
 import ArkLib.OracleReduction.Basic
 import ArkLib.OracleReduction.Cast
@@ -188,6 +190,7 @@ import ArkLib.OracleReduction.ProtocolSpec.Cast
 import ArkLib.OracleReduction.ProtocolSpec.SeqCompose
 import ArkLib.OracleReduction.Salt
 import ArkLib.OracleReduction.Security.Basic
+import ArkLib.OracleReduction.Security.ChallengeRound
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Basic
 import ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Composition
@@ -230,6 +233,12 @@ import ArkLib.ProofSystem.Fri.Spec.SingleRound
 import ArkLib.ProofSystem.Plonk.Basic
 import ArkLib.ProofSystem.RingSwitching.BatchingPhase
 import ArkLib.ProofSystem.RingSwitching.General
+import ArkLib.ProofSystem.RingSwitching.Generic.Batching
+import ArkLib.ProofSystem.RingSwitching.Generic.Carrier
+import ArkLib.ProofSystem.RingSwitching.Generic.Packing
+import ArkLib.ProofSystem.RingSwitching.Generic.Recombine
+import ArkLib.ProofSystem.RingSwitching.Generic.Reduction
+import ArkLib.ProofSystem.RingSwitching.Generic.Relations
 import ArkLib.ProofSystem.RingSwitching.Prelude
 import ArkLib.ProofSystem.RingSwitching.Profile
 import ArkLib.ProofSystem.RingSwitching.Spec
diff --git a/ArkLib/Data/Module/Basis.lean b/ArkLib/Data/Module/Basis.lean
new file mode 100644
index 0000000000..add8c10a00
--- /dev/null
+++ b/ArkLib/Data/Module/Basis.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Hicks
+-/
+
+import Mathlib.LinearAlgebra.Basis.Defs
+
+/-!
+# Basis recombination lemmas
+
+The finite `R`-linear recombination along a basis, `s ↦ ∑ i, s i • b i`, is exactly
+`b.equivFun.symm`, hence a bijection (in particular injective: distinct coordinate tuples
+recombine to distinct module elements). Stated once here so both directions of a free-module
+"pack/unpack" argument (e.g. the ring-switching packing- and opening-basis sides) consume the
+same lemma.
+-/
+
+namespace Module.Basis
+
+variable {ι R M : Type*} [Fintype ι] [Semiring R] [AddCommMonoid M] [Module R M]
+
+/-- Recombination along a basis, `s ↦ ∑ i, s i • b i`, is a bijection: it is
+`b.equivFun.symm` in pointful form. -/
+theorem sum_smul_bijective (b : Basis ι R M) :
+    Function.Bijective (fun s : ι → R => ∑ i, s i • b i) := by
+  have h : (fun s : ι → R => ∑ i, s i • b i) = b.equivFun.symm := by
+    funext s
+    rw [Basis.equivFun_symm_apply]
+  rw [h]
+  exact b.equivFun.symm.bijective
+
+/-- Recombination along a basis is injective: distinct coordinate tuples recombine to
+distinct module elements. -/
+theorem sum_smul_injective (b : Basis ι R M) :
+    Function.Injective (fun s : ι → R => ∑ i, s i • b i) :=
+  b.sum_smul_bijective.injective
+
+end Module.Basis
diff --git a/ArkLib/Data/MvPolynomial/Degrees.lean b/ArkLib/Data/MvPolynomial/Degrees.lean
index 63dbde6a62..dd5896d808 100644
--- a/ArkLib/Data/MvPolynomial/Degrees.lean
+++ b/ArkLib/Data/MvPolynomial/Degrees.lean
@@ -186,6 +186,22 @@ theorem mem_restrictDegree_iff_degreeOf_le (p : MvPolynomial σ R) (n : ℕ) :
   apply Iff.trans (mem_restrictDegree_iff_sup σ p n)
   simp only [degreeOf]
 
+/-- A polynomial with degree at most `1` in each of finitely many variables (e.g. a multilinear
+polynomial) has total degree at most the number of variables. -/
+theorem totalDegree_le_card_of_degreeOf_le_one [Fintype σ] (p : MvPolynomial σ R)
+    (h : ∀ i, p.degreeOf i ≤ 1) : p.totalDegree ≤ Fintype.card σ := by
+  rw [MvPolynomial.totalDegree]
+  refine Finset.sup_le fun m hm => ?_
+  have hsum : (m.sum fun _ e => e) = ∑ i, m i := by
+    rw [Finsupp.sum_fintype]
+    intro i; rfl
+  rw [hsum]
+  calc ∑ i, m i ≤ ∑ _i : σ, 1 :=
+        Finset.sum_le_sum fun i _ =>
+          le_trans (Finset.le_sup (f := fun m => m i) hm)
+            (by rw [← MvPolynomial.degreeOf_eq_sup]; exact h i)
+    _ = Fintype.card σ := by simp
+
 end DegreeOf
 
 section Equiv
diff --git a/ArkLib/Data/MvPolynomial/Multilinear.lean b/ArkLib/Data/MvPolynomial/Multilinear.lean
index 466ce6771e..5f87e1b3cf 100644
--- a/ArkLib/Data/MvPolynomial/Multilinear.lean
+++ b/ArkLib/Data/MvPolynomial/Multilinear.lean
@@ -27,6 +27,15 @@ variable {σ : Type*} {R : Type*}
 instance coeFunctionFin2 [NatCast R] : Coe (σ → Fin 2) (σ → R) where
   coe := fun vec i => vec i
 
+/-- The Boolean-point coercion above agrees with the if-then-else spellings used elsewhere
+(`if · = 1 then 1 else 0` as in `RingSwitchCarrier.boolToE`, or the propositionally identical
+`if · == 1` as in `RingSwitching.compute_s0`); this is the bridge between them. -/
+theorem coe_boolFun_eq_ite [AddMonoidWithOne R] (u : σ → Fin 2) :
+    (u : σ → R) = fun i => if u i = 1 then 1 else 0 := by
+  funext i
+  have h : u i = 0 ∨ u i = 1 := by fin_omega
+  rcases h with h | h <;> simp [h]
+
 variable [CommRing R]
 
 def toEvalsZeroOne (p : MvPolynomial σ R) : (σ → Fin 2) → R :=
@@ -143,6 +152,12 @@ theorem eval_zeroOne_eq_MLE_toEvalsZeroOne (p : MvPolynomial σ R) (x : σ → F
     eval (x : σ → R) p = eval (x : σ → R) (MLE p.toEvalsZeroOne) := by
   simp only [MLE_eval_zeroOne, toEvalsZeroOne]
 
+/-- Evaluating a multilinear extension at an **arbitrary** point expands over the hypercube
+against the eq-indicator: `(MLE g)(r) = ∑_x eq̃(x, r) · g(x)`. -/
+theorem MLE_eval_eq_sum_eqTilde (evals : (σ → Fin 2) → R) (r : σ → R) :
+    MvPolynomial.eval r (MLE evals) = ∑ x : σ → Fin 2, eqTilde (x : σ → R) r * evals x := by
+  simp only [MLE, map_sum, map_mul, eval_C, eqTilde]
+
 section DegreeOf
 
 omit [Fintype σ] in
@@ -210,6 +225,11 @@ theorem MLE_degreeOf (evals : (σ → Fin 2) → R) (i : σ) : degreeOf i (MLE e
   apply (mem_restrictDegree_iff_degreeOf_le _ _).mp
   exact MLE_mem_restrictDegree evals
 
+/-- A multilinear extension over `σ` variables has total degree at most `|σ|`. -/
+theorem MLE_totalDegree_le (evals : (σ → Fin 2) → R) :
+    (MLE evals).totalDegree ≤ Fintype.card σ :=
+  totalDegree_le_card_of_degreeOf_le_one _ (fun i => MLE_degreeOf evals i)
+
 end DegreeOf
 
 -- TODO: add lemmas about the uniqueness of multilinear polynomials up to evaluations on hypercube
@@ -272,6 +292,34 @@ def MLEEquiv : R⦃≤ 1⦄[X σ] ≃ ((σ → Fin 2) → R) where
 def MLEEquivFin {n : ℕ} : R⦃≤ 1⦄[X (Fin n)] ≃ (Fin (2 ^ n) → R) :=
   Equiv.trans MLEEquiv (Equiv.piCongr finFunctionFinEquiv (fun _ => Equiv.refl _))
 
+omit [DecidableEq R] [IsDomain R] in
+/-- **Multilinear `aeval` hypercube expansion**: evaluating a multilinear polynomial over `R` at a
+point `r` of an `R`-algebra `A` expands over the Boolean hypercube against the eq-indicator,
+`aeval r p = ∑ y, eq̃(y, r) · algebraMap R A (p(y))`. The proof self-interpolates the
+coefficient-mapped polynomial over `A` (`is_multilinear_iff_eq_evals_zeroOne`, a root-counting
+argument), whence the `[IsDomain A]` hypothesis; the identity itself holds over any commutative
+ring, and dropping the domain hypothesis is future work. -/
+theorem aeval_multilinear_eq_sum_eqTilde {A : Type*} [CommRing A] [Algebra R A] [IsDomain A]
+    {p : MvPolynomial σ R} (hp : p ∈ R⦃≤ 1⦄[X σ]) (r : σ → A) :
+    aeval r p
+      = ∑ y : σ → Fin 2, eqTilde (y : σ → A) r * algebraMap R A (eval (y : σ → R) p) := by
+  have hq : map (algebraMap R A) p ∈ A⦃≤ 1⦄[X σ] := by
+    rw [mem_restrictDegree] at hp ⊢
+    exact fun s hs i => hp s (support_map_subset _ _ hs) i
+  calc aeval r p = eval r (map (algebraMap R A) p) := by
+        rw [eval_map, aeval_def]
+    _ = ∑ y : σ → Fin 2, eqTilde (y : σ → A) r * (map (algebraMap R A) p).toEvalsZeroOne y := by
+        conv_lhs => rw [← is_multilinear_iff_eq_evals_zeroOne.mp hq]
+        exact MLE_eval_eq_sum_eqTilde _ r
+    _ = ∑ y : σ → Fin 2, eqTilde (y : σ → A) r * algebraMap R A (eval (y : σ → R) p) := by
+        refine Finset.sum_congr rfl fun y _ => ?_
+        congr 1
+        change eval (y : σ → A) (map (algebraMap R A) p) = algebraMap R A (eval (y : σ → R) p)
+        have hpt : (y : σ → A) = fun i => algebraMap R A ((y : σ → R) i) :=
+          funext fun i => (map_natCast (algebraMap R A) _).symm
+        rw [hpt, eval_map]
+        exact (eval₂_comp (algebraMap R A) (y : σ → R) p).symm
+
 end MvPolynomial
 
 end
diff --git a/ArkLib/Data/Probability/Instances.lean b/ArkLib/Data/Probability/Instances.lean
index 3f5ca96fd4..e261d74162 100644
--- a/ArkLib/Data/Probability/Instances.lean
+++ b/ArkLib/Data/Probability/Instances.lean
@@ -452,32 +452,33 @@ lemma Pr_congr {α : Type} {D : PMF α} {P Q : α → Prop}
   congr 1; exact propext (h x)
 
 /-- **Schwartz-Zippel Lemma** (Probability Form):
-For a non-zero multivariate polynomial `P` of total degree at most `d` over a finite field `L`,
-the probability that `P(r)` evaluates to 0 for a uniformly random `r` is at most `d / |L|`. -/
+For a non-zero multivariate polynomial `P` of total degree at most `d` over a finite integral
+domain `R`, the probability that `P(r)` evaluates to 0 for a uniformly random `r` is at most
+`d / |R|`. -/
 lemma prob_schwartz_zippel_mv_polynomial {R : Type} [CommRing R] [IsDomain R] [Fintype R]
     {n : ℕ}
-    (P : MvPolynomial (Fin n) R) (h_nonzero : P ≠ 0) (h_deg : P.totalDegree ≤ n) :
+    (P : MvPolynomial (Fin n) R) (d : ℕ) (h_nonzero : P ≠ 0) (h_deg : P.totalDegree ≤ d) :
     Pr_{ let r ←$ᵖ (Fin n → R) }[ MvPolynomial.eval r P = 0 ] ≤
-      (n : ℝ≥0) / (Fintype.card R : ℝ≥0) := by
+      (d : ℝ≥0) / (Fintype.card R : ℝ≥0) := by
   classical
   rw [prob_uniform_eq_card_filter_div_card]
   push_cast
   have sz_bound := MvPolynomial.schwartz_zippel_totalDegree (R := R) (n := n)
     (p := P) (hp := h_nonzero) (S := Finset.univ)
   simp only [Fintype.piFinset_univ, card_univ] at sz_bound
-  have sz_bound_le_n_div_card_R : ((#{f | (MvPolynomial.eval f) P = 0}) : ℚ≥0)
-    / ((Fintype.card R ^ n)) ≤ (n : ℚ≥0) / ((#(Finset.univ : Finset R)) : ℚ≥0) := by
+  have sz_bound_le_d_div_card_R : ((#{f | (MvPolynomial.eval f) P = 0}) : ℚ≥0)
+    / ((Fintype.card R ^ n)) ≤ (d : ℚ≥0) / ((#(Finset.univ : Finset R)) : ℚ≥0) := by
     calc
       _ ≤ (P.totalDegree : ℚ≥0) / ((#(Finset.univ : Finset R)) : ℚ≥0) := sz_bound
       _ ≤ _ := by
         simp only [card_univ]
         apply div_le_of_le_mul₀ (hb := by simp only [zero_le]) (hc := by simp only [zero_le])
-        -- ⊢ ↑P.totalDegree ≤ ↑n / ↑(Fintype.card R) * ↑(Fintype.card R)
+        -- ⊢ ↑P.totalDegree ≤ ↑d / ↑(Fintype.card R) * ↑(Fintype.card R)
         rw [div_mul_cancel₀ (h := by simp only [ne_eq, Nat.cast_eq_zero, Fintype.card_ne_zero,
           not_false_eq_true])]
         exact Nat.cast_le.mpr h_deg
   have sz_bound_ENNReal : ((#{f | (MvPolynomial.eval f) P = 0}) : ENNReal)
-    / ((Fintype.card R ^ n) : ℕ) ≤ (n : ENNReal) / (Fintype.card R : ENNReal) := by
+    / ((Fintype.card R ^ n) : ℕ) ≤ (d : ENNReal) / (Fintype.card R : ENNReal) := by
     simp_rw [ENNReal.coe_Nat_coe_NNRat]
     conv_lhs => rw [ENNReal.coe_div_of_NNRat (hb := by
       simp only [Nat.cast_pow, ne_eq, pow_eq_zero_iff', Nat.cast_eq_zero, Fintype.card_ne_zero,
@@ -486,11 +487,27 @@ lemma prob_schwartz_zippel_mv_polynomial {R : Type} [CommRing R] [IsDomain R] [F
       Fintype.card_ne_zero, not_false_eq_true])]
     rw [ENNReal.coe_le_of_NNRat]
     simp only [Nat.cast_pow]
-    exact sz_bound_le_n_div_card_R
+    exact sz_bound_le_d_div_card_R
   simp only [Fintype.card_pi, prod_const, card_univ, Fintype.card_fin, Nat.cast_pow, ge_iff_le]
   rw [Nat.cast_pow] at sz_bound_ENNReal
   exact sz_bound_ENNReal
 
+/-- **Schwartz-Zippel**, single-variable sampling form: for a non-zero polynomial in one variable
+(as an `MvPolynomial (Fin 1)`) of total degree at most `d`, the probability that it vanishes at a
+uniformly random point of `R` (sampled directly, not as `Fin 1 → R`) is at most `d / |R|`. -/
+lemma prob_schwartz_zippel_single_variable {R : Type} [CommRing R] [IsDomain R] [Fintype R]
+    (f : MvPolynomial (Fin 1) R) (d : ℕ) (h_nonzero : f ≠ 0) (h_deg : f.totalDegree ≤ d) :
+    Pr_{ let γ ←$ᵖ R }[ MvPolynomial.eval (fun _ : Fin 1 => γ) f = 0 ] ≤
+      (d : ℝ≥0) / (Fintype.card R : ℝ≥0) := by
+  rw [← prob_uniform_singleton_finFun_eq
+    (P := fun γ => MvPolynomial.eval (fun _ : Fin 1 => γ) f = 0)]
+  calc Pr_{ let r ←$ᵖ (Fin 1 → R) }[ MvPolynomial.eval (fun _ : Fin 1 => r 0) f = 0 ]
+      = Pr_{ let r ←$ᵖ (Fin 1 → R) }[ MvPolynomial.eval r f = 0 ] := by
+        refine Pr_congr fun r => ?_
+        have hr : (fun _ : Fin 1 => r 0) = r := funext fun i => congrArg r (Subsingleton.elim 0 i)
+        rw [hr]
+    _ ≤ _ := prob_schwartz_zippel_mv_polynomial f d h_nonzero h_deg
+
 /-- Pushforward of `PMF.uniformOfFintype α` under a map `f : α → β` whose fibers
 over the image all have the same cardinality `k > 0` is the uniform distribution
 on the image of `f`.
diff --git a/ArkLib/Data/Probability/OracleCompBridge.lean b/ArkLib/Data/Probability/OracleCompBridge.lean
new file mode 100644
index 0000000000..0d234096fc
--- /dev/null
+++ b/ArkLib/Data/Probability/OracleCompBridge.lean
@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Hicks
+-/
+
+import VCVio
+import ArkLib.Data.Probability.Instances
+
+/-!
+# Bridge: VCVio `OracleComp` events ↔ `PMF` sampling notation
+
+Round-by-round security games in ArkLib live on the VCVio side (`Pr[E | oa]` over
+`OracleComp`/`ProbComp`), while per-round error analyses are naturally stated against the
+`PMF`-level sampling notation `Pr_{ let c ←$ᵖ C }[ E c ]` (`ArkLib.Data.Probability.Notation`).
+This file provides the bridge:
+
+* `probEvent_uniformSample_eq_pr_uniformOfFintype`: the event probability of a uniform query
+  `$ᵗ C` is exactly that of `PMF.uniformOfFintype C`.
+* `probEvent_bind_uniformSample_le`: a per-prefix `PMF`-level bound transfers to the bind
+  `do let a ← ma; let c ← $ᵗ C; return (a, c)` — the shape of an RBR game whose final
+  round is a uniformly sampled challenge.
+
+Layering: `Data` files may import VCVio (precedent: `ArkLib.Data.Hash.DuplexSponge`).
+-/
+
+open OracleComp ProbabilityTheory NNReal
+
+open scoped ENNReal
+
+section OracleCompBridge
+
+variable {C : Type} [SampleableType C] [Fintype C] [Nonempty C]
+
+/-- The event probability of a uniform query `$ᵗ C` agrees with the `PMF`-level probability
+under `PMF.uniformOfFintype C`: both are `#{c | E c} / #C`. -/
+theorem probEvent_uniformSample_eq_pr_uniformOfFintype (E : C → Prop) :
+    Pr[E | $ᵗ C] = Pr_{ let c ← $ᵖ C}[E c] := by
+  classical
+  rw [probEvent_uniformSample, prob_uniform_eq_card_filter_div_card]
+  simp
+
+/-- A per-prefix `PMF`-level bound on a uniformly sampled challenge transfers to the
+`OracleComp` bind `do let a ← ma; let c ← $ᵗ C; return (a, c)`.
+
+This is the probability core of factoring an RBR game: `ma` is the (already simulated)
+transcript prefix, `c` the fresh challenge, and `E` the bad event. -/
+theorem probEvent_bind_uniformSample_le {A : Type} (ma : ProbComp A)
+    (E : A → C → Prop) {ε : ℝ≥0∞}
+    (h : ∀ a, Pr_{ let c ← $ᵖ C}[E a c] ≤ ε) :
+    Pr[fun x => E x.1 x.2 | do let a ← ma; let c ← $ᵗ C; return (a, c)] ≤ ε := by
+  refine probEvent_bind_le_of_forall_le fun a _ => ?_
+  calc Pr[fun x => E x.1 x.2 | do let c ← $ᵗ C; return (a, c)]
+      = Pr[fun c => E a c | $ᵗ C] := by
+        rw [bind_pure_comp, probEvent_map]
+        rfl
+    _ = Pr_{ let c ← $ᵖ C}[E a c] := probEvent_uniformSample_eq_pr_uniformOfFintype _
+    _ ≤ ε := h a
+
+end OracleCompBridge
diff --git a/ArkLib/OracleReduction/Security/ChallengeRound.lean b/ArkLib/OracleReduction/Security/ChallengeRound.lean
new file mode 100644
index 0000000000..ed0ae3c50c
--- /dev/null
+++ b/ArkLib/OracleReduction/Security/ChallengeRound.lean
@@ -0,0 +1,127 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Hicks
+-/
+
+import ArkLib.OracleReduction.Security.RoundByRound
+import ArkLib.Data.Probability.OracleCompBridge
+
+/-!
+# Factoring the round-by-round game at a challenge round
+
+The round-by-round (knowledge) soundness games (`Verifier.rbrKnowledgeSoundness`,
+`RoundByRound.lean`) all end in the same shape: run a prefix computation (the prover up to
+round `i`), draw the challenge `i` uniformly (`challengeQueryImpl`), and test a bad event on
+the pair. This file factors the probability core out of that shape once and for all:
+`probEvent_challengeRound_le` bounds the game by any `ε` that bounds, for **every** fixed
+prefix outcome, the PMF-level probability of the bad event over a uniform challenge
+(`Pr_{ let c ← $ᵖ (pSpec.Challenge i)}[…]` — the form the per-round error analyses, e.g.
+`BatchingStrategy.separates`, are stated in).
+
+The prefix is an *arbitrary* `OracleComp` over `oSpec + [pSpec.Challenge]ₒ` — no prover
+structure is unfolded here — and the event may post-process the pair through an arbitrary
+`k : A → pSpec.Challenge i → β` (the games return triples that also carry a query log; take
+`β` to be the triple type and `k` the reassembly).
+
+Stated over an arbitrary `oSpec` implementation `impl`, so it applies to the games verbatim.
+-/
+
+noncomputable section
+
+open OracleComp OracleSpec ProtocolSpec ProbabilityTheory
+open scoped NNReal ENNReal
+
+variable {ι : Type} {oSpec : OracleSpec ι} {n : ℕ} {pSpec : ProtocolSpec n}
+  [∀ i, SampleableType (pSpec.Challenge i)]
+  {σ : Type}
+
+namespace Verifier
+
+/-- **Challenge-round factoring for RBR games.** If for every outcome `a` of the prefix the
+bad event `q ∘ k a` has uniform-challenge probability at most `ε`, then the whole game —
+prefix, then uniformly sampled challenge `i`, then `k` — has probability at most `ε`.
+
+This is the bridge from the protocol-level game (`simulateQ` under
+`impl.addLift challengeQueryImpl`, the exact shape of `Verifier.rbrKnowledgeSoundness`) to
+the PMF-level per-round error analyses (`Pr_{ let c ← $ᵖ _}[…]`, e.g.
+`BatchingStrategy.separates`). -/
+theorem probEvent_challengeRound_le
+    (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
+    {A β : Type} (mx : OracleComp (oSpec + [pSpec.Challenge]ₒ) A)
+    (i : pSpec.ChallengeIdx)
+    [Fintype (pSpec.Challenge i)] [Nonempty (pSpec.Challenge i)]
+    (k : A → pSpec.Challenge i → β) (q : β → Prop) {ε : ℝ≥0∞}
+    (h : ∀ a, Pr_{ let c ← $ᵖ (pSpec.Challenge i)}[q (k a c)] ≤ ε) :
+    Pr[q | do
+      (simulateQ (impl.addLift challengeQueryImpl : QueryImpl _ (StateT σ ProbComp))
+        (do
+          let a ← mx
+          let c ← liftComp (pSpec.getChallenge i) _
+          return k a c)).run' (← init)] ≤ ε := by
+  classical
+  -- Peel the state-threaded simulation into its three stages (prefix / challenge / return).
+  simp only [StateT.run'_eq, simulateQ_bind, StateT.run_bind, QueryImpl.addLift_def,
+    QueryImpl.simulateQ_add_liftComp_right, simulateQ_pure, StateT.run_pure]
+  -- Condition on the initial state, then on the prefix outcome.
+  refine probEvent_bind_le_of_forall_le fun s0 _ => ?_
+  rw [probEvent_map]
+  refine probEvent_bind_le_of_forall_le fun p _ => ?_
+  -- The challenge round is a lifted uniform sample (`erw`: the query is under `MonadLift`).
+  simp only [getChallenge]
+  rw [bind_pure_comp, probEvent_map]
+  erw [simulateQ_query]
+  simp only [QueryImpl.liftTarget_apply, OracleQuery.cont, OracleQuery.input_query,
+    StateT.run_map, StateT.run_monadLift, monadLift_self, challengeQueryImpl]
+  rw [bind_pure_comp, probEvent_map]
+  -- Land on the PMF side and close with the per-prefix hypothesis.
+  rw [probEvent_map]
+  -- Re-type the sample at `pSpec.Challenge i` (the oracle-spec `Range` is defeq, not syntactic).
+  change probEvent ($ᵗ (pSpec.Challenge i)) _ ≤ ε
+  exact le_trans (le_of_eq (probEvent_uniformSample_eq_pr_uniformOfFintype _)) (h p.1)
+
+/-- **Game-shaped variant** of `probEvent_challengeRound_le`: specialized to the literal
+prefix-run shape of `Verifier.rbrKnowledgeSoundness` (destructuring `let` over
+`Prover.runWithLogToRound`). Unifying that destructuring bind against the plain-bind shape of
+the general lemma diverges in `whnf` (structure-eta through the prover term), so this variant
+replays the same proof script on the game shape directly — the destructuring matcher is fired
+at the constructor level by one `obtain`. -/
+theorem probEvent_rbrGame_le
+    (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
+    {StmtIn WitIn StmtOut WitOut : Type}
+    (stmtIn : StmtIn) (witIn : WitIn)
+    (prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec)
+    (i : pSpec.ChallengeIdx)
+    [Fintype (pSpec.Challenge i)] [Nonempty (pSpec.Challenge i)]
+    {q : pSpec.Transcript i.1.castSucc × pSpec.Challenge i
+        × QueryLog (oSpec + [pSpec.Challenge]ₒ) → Prop} {ε : ℝ≥0∞}
+    (h : ∀ tr log, Pr_{ let c ← $ᵖ (pSpec.Challenge i)}[q (tr, c, log)] ≤ ε) :
+    Pr[q | do
+      (simulateQ (impl.addLift challengeQueryImpl : QueryImpl _ (StateT σ ProbComp))
+        (do
+          let ⟨⟨transcript, _⟩, proveQueryLog⟩ ←
+            prover.runWithLogToRound i.1.castSucc stmtIn witIn
+          let challenge ← liftComp (pSpec.getChallenge i) _
+          return (transcript, challenge, proveQueryLog))).run' (← init)] ≤ ε := by
+  classical
+  -- Peel the state-threaded simulation (same script as `probEvent_challengeRound_le`).
+  simp only [StateT.run'_eq, simulateQ_bind, StateT.run_bind, QueryImpl.addLift_def,
+    QueryImpl.simulateQ_add_liftComp_right, simulateQ_pure, StateT.run_pure]
+  refine probEvent_bind_le_of_forall_le fun s0 _ => ?_
+  rw [probEvent_map]
+  refine probEvent_bind_le_of_forall_le fun p _ => ?_
+  -- Fire the destructuring matcher at the constructor level.
+  obtain ⟨⟨⟨tr, st⟩, log⟩, s1⟩ := p
+  simp only [getChallenge]
+  rw [bind_pure_comp, probEvent_map]
+  erw [simulateQ_query]
+  simp only [QueryImpl.liftTarget_apply, OracleQuery.cont, OracleQuery.input_query,
+    StateT.run_map, StateT.run_monadLift, monadLift_self, challengeQueryImpl]
+  rw [bind_pure_comp, probEvent_map]
+  rw [probEvent_map]
+  change probEvent ($ᵗ (pSpec.Challenge i)) _ ≤ ε
+  exact le_trans (le_of_eq (probEvent_uniformSample_eq_pr_uniformOfFintype _)) (h tr log)
+
+end Verifier
+
+end
diff --git a/ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean b/ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean
index 66306d3d08..c23c600032 100644
--- a/ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean
+++ b/ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean
@@ -797,10 +797,44 @@ def BBF_SumcheckMultiplierParam : SumcheckMultiplierParam L ℓ (SumcheckBaseCon
     degCombinator := 1
     combinator_natDegree_le := by intro _; exact Polynomial.natDegree_X_le }
 
+/-- The [DP24] coefficient vector of a multilinear witness `t`: its Boolean-hypercube table,
+read in the LSB-first bit order of `Nat.binaryFinMapToNat` (`ω = ∑ⱼ 2^j·wⱼ`, so coefficient `ω`
+is `t` at the point `w j = getBit j ω`). This is the exact inverse of the index mapping the
+novel-coeffs *decoder* uses (`hypercube_evals` above, via `Nat.binaryFinMapToNat`;
+roundtrip: `Nat.getBit_of_binaryFinMapToNat`).
+
+NB: this def replaces the previous inline spelling `fun ω => t.val.eval ω`, whose silent
+coercion `Fin (2^ℓ) → (Fin ℓ → L)` is the *constant* function `fun _ => ↑ω` (pointwise
+`Nat`-cast) — i.e. it read `t`'s diagonal evaluations, making the encoding non-injective
+(`X 0` and `X 1` collapsed) and the consistency predicates below vacuously loose. -/
+def witnessNovelCoeffs (t : L⦃≤ 1⦄[X Fin ℓ]) : Fin (2^ℓ) → L :=
+  fun ω => t.val.eval (fun j => (Nat.getBit j.val ω.val : L))
+
+-- Regression probe for the R7 fix: under the pre-fix diagonal spelling `fun ω => t.val.eval ω`
+-- (whose silent coercion evaluates at the *constant* point `fun _ => ↑ω`), `X 0` and `X 1`
+-- produced identical coefficient vectors, so this inequality was unprovable. The cube-table
+-- encoding pins them apart at `ω = 1`, where bit 0 is `1` but bit 1 is `0`.
+example :
+    witnessNovelCoeffs (L := L) (ℓ := 2)
+      ⟨MvPolynomial.X ⟨0, by omega⟩, by
+        rw [MvPolynomial.mem_restrictDegree_iff_degreeOf_le]
+        intro j; rw [MvPolynomial.degreeOf_X]; split <;> omega⟩
+      ⟨1, by norm_num⟩ ≠
+    witnessNovelCoeffs (L := L) (ℓ := 2)
+      ⟨MvPolynomial.X ⟨1, by omega⟩, by
+        rw [MvPolynomial.mem_restrictDegree_iff_degreeOf_le]
+        intro j; rw [MvPolynomial.degreeOf_X]; split <;> omega⟩
+      ⟨1, by norm_num⟩ := by
+  have h0 : Nat.getBit 0 1 = 1 := rfl
+  have h1 : Nat.getBit 1 1 = 0 := rfl
+  simp only [witnessNovelCoeffs, MvPolynomial.eval_X, h0, h1, Nat.cast_one, Nat.cast_zero]
+  exact one_ne_zero
+
 /-- This condition ensures that the folding witness `f` is properly generated from `t` -/
 def getMidCodewords {i : Fin (ℓ + 1)} (t : L⦃≤ 1⦄[X Fin ℓ]) -- original polynomial t
     (challenges : Fin i → L) : (sDomain 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by omega⟩) → L) :=
-  let P₀ : L⦃< 2^ℓ⦄[X] := polynomialFromNovelCoeffsF₂ 𝔽q β ℓ (by omega) (fun ω => t.val.eval ω)
+  let P₀ : L⦃< 2^ℓ⦄[X] :=
+    polynomialFromNovelCoeffsF₂ 𝔽q β ℓ (by omega) (witnessNovelCoeffs (L := L) t)
   let f₀ : (sDomain 𝔽q β h_ℓ_add_R_rate 0) → L := fun x => P₀.val.eval x.val
   let fᵢ := iterated_fold 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
     (i := 0)
@@ -834,7 +868,8 @@ export Sumcheck.Structured (sumcheckConsistencyProp)
     evaluated on the initial domain S^(0), must be close within unique decoding radius to f^(0) -/
 def firstOracleWitnessConsistencyProp (t : MultilinearPoly L ℓ)
     (f₀ : sDomain 𝔽q β h_ℓ_add_R_rate 0 → L) : Prop :=
-  let P₀ : L⦃< 2 ^ ℓ⦄[X] := polynomialFromNovelCoeffsF₂ 𝔽q β ℓ (by omega) (fun ω => t.val.eval ω)
+  let P₀ : L⦃< 2 ^ ℓ⦄[X] :=
+    polynomialFromNovelCoeffsF₂ 𝔽q β ℓ (by omega) (witnessNovelCoeffs (L := L) t)
   -- The constraint: P_0 evaluated on S^(0) is close within unique decoding radius to f^(0)
   2 * hammingDist (fun x => P₀.val.eval x.val) f₀ < BBF_CodeDistance ℓ 𝓡 ⟨0, by omega⟩
 
diff --git a/ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean b/ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean
index bb2dfaaca1..358927c758 100644
--- a/ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean
+++ b/ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean
@@ -99,7 +99,10 @@ def sumcheckFoldCtxLens : OracleContext.Lens
       let t : L⦃≤ 1⦄[X Fin ℓ'] := outerWitIn.t'
       let H : L⦃≤ 2⦄[X Fin (ℓ' - 0)] := outerWitIn.H
 
-      let P₀ : L⦃< 2^ℓ'⦄[X] := polynomialFromNovelCoeffsF₂ K β ℓ' (by omega) (fun ω => t.val.eval ω)
+      -- NB `BinaryBasefold.witnessNovelCoeffs` = t's cube table (LSB-first); the previous
+      -- inline `fun ω => t.val.eval ω` silently read t's diagonal evaluations (see R7 fix).
+      let P₀ : L⦃< 2^ℓ'⦄[X] := polynomialFromNovelCoeffsF₂ K β ℓ' (by omega)
+        (BinaryBasefold.witnessNovelCoeffs (L := L) t)
       let f₀ : (sDomain K β (h_ℓ_add_R_rate := h_ℓ_add_R_rate))
         ⟨0, by omega⟩ → L := fun x => P₀.val.eval x.val
 
diff --git a/ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean b/ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean
index 5392566e48..2c3e75041e 100644
--- a/ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean
+++ b/ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean
@@ -56,4 +56,33 @@ def BinaryBasefoldAbstractOStmtIn : (RingSwitching.AbstractOStmtIn L ℓ') where
     Binius.BinaryBasefold.firstOracleWitnessConsistencyProp K β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
       t (f₀ := Binius.BinaryBasefold.getFirstOracle K β oStmt)
 
+/-- The Binius codeword-consistency predicate in the generic `commitsTo` orientation
+(oracle statement → committed multilinear → `Prop`, cf.
+`RingSwitching.Generic.PackedCommitment.commitsTo`): the initial oracle commits to `t` iff
+`firstOracleWitnessConsistencyProp t f₀` holds for the first oracle. Same semantics as
+`BinaryBasefoldAbstractOStmtIn.initialCompatibility` (pinned by
+`initialCompatibility_eq_biniusCommitsTo`), re-oriented for the S7 migration onto the generic
+PCS interface.
+
+The underlying predicate reads `t`'s cube table via `witnessNovelCoeffs` (LSB-first bit order;
+see its docstring for the history: the original spelling read `t`'s *diagonal* evaluations
+through a silent coercion, making the encoding non-injective — found at the S5 close-review and
+fixed in this PR). The **functionality proof** (`commitsTo c t → commitsTo c t' → t = t'`) is
+the recorded S7 obligation, provable by unique decoding: two codewords within half the code
+distance of one word coincide; the novel-basis coefficient map is injective; a multilinear is
+determined by its cube table. It bundles into a `PackedCommitment` at S7. -/
+def biniusCommitsTo
+    (oStmt : ∀ j, (BinaryBasefoldAbstractOStmtIn κ L K β ℓ' 𝓡 ϑ h_ℓ_add_R_rate).OStmtIn j)
+    (t : Sumcheck.Structured.MultilinearPoly L ℓ') : Prop :=
+  Binius.BinaryBasefold.firstOracleWitnessConsistencyProp K β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
+    t (f₀ := Binius.BinaryBasefold.getFirstOracle K β oStmt)
+
+omit [NeZero κ] [CharP L 2] [SampleableType L] [DecidableEq K] [NeZero 𝓡] in
+/-- The legacy free hook and the `commitsTo`-oriented predicate are definitionally the same —
+the S5 re-expression is a re-orientation, not a semantic change. -/
+lemma initialCompatibility_eq_biniusCommitsTo :
+    (BinaryBasefoldAbstractOStmtIn κ L K β ℓ' 𝓡 ϑ h_ℓ_add_R_rate).initialCompatibility
+      = fun x => biniusCommitsTo κ L K β ℓ' 𝓡 ϑ h_ℓ_add_R_rate x.2 x.1 :=
+  rfl
+
 end Binius.FRIBinius
diff --git a/ArkLib/ProofSystem/RingSwitching/Generic/Batching.lean b/ArkLib/ProofSystem/RingSwitching/Generic/Batching.lean
new file mode 100644
index 0000000000..c07bf62f0c
--- /dev/null
+++ b/ArkLib/ProofSystem/RingSwitching/Generic/Batching.lean
@@ -0,0 +1,290 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Hicks
+-/
+
+import ArkLib.ProofSystem.RingSwitching.Generic.Carrier
+import ArkLib.Data.Probability.Instances
+import Mathlib.FieldTheory.Finite.GaloisField
+
+/-!
+# Generic Ring-Switching — Batching Separation (S3)
+
+Discharges design step 5 — the *one genuine design axis* of the generic ring switch (see
+`docs/kb/concepts/ring-switching.md`, "The Generic layer", for the spine/pillar vocabulary):
+folding the `|W|` recombined claims into a single claim. The two
+known strategies are not two protocols but two instances of one interface:
+
+* `BatchingStrategy.gammaPowers` — γ-power random linear combination (the "Ring switching,
+  generalized" note [RSG]): sample `γ ←$ P`, weight claim `u` by `γ^u`. Universal (any claim
+  count `e`); error `e/|P|`.
+* `BatchingStrategy.eqFold` — eq-indicator folding (Flock App. B [BRW26]; ArkLib's DP24 batching
+  phase): claims indexed by `{0,1}^κ`, sample `r'' ←$ P^κ`, weight claim `u` by `eq̃(u, r'')`.
+  Power-of-two claim counts only; error `κ/|P|`.
+
+Both `separates` proofs are Schwartz–Zippel over a finite integral domain and reduce to the
+generic `prob_schwartz_zippel_mv_polynomial` (`ArkLib/Data/Probability/Instances.lean`) — the
+strategy supplies only the difference polynomial (`∑ᵤ (s−s')ᵤ Xᵘ` resp. `MLE (s−s')`), its
+nonvanishing, and its degree bound. A downstream instance *picks* a strategy; it never re-proves
+batching (design safety pillar: closed proven menu).
+
+Statement conventions (deliberate, recorded):
+* Challenges are `[Fintype]`/`[Nonempty]` types sampled uniformly via PMF (`Pr_{…}` from
+  `ArkLib/Data/Probability/Notation.lean`), matching the reusable Schwartz–Zippel layer. The
+  bridge to the protocol-level `SampleableType` interface is deferred to S6 (wiring).
+* The structure is `[CommRing P]`-only; `[IsDomain P] [Fintype P]` gate the *proven instances*
+  (and, later, the S6 domain soundness theorem) — the design's fork lives at the theorem, not
+  the vocabulary, keeping the S8 non-domain (Hachi) sibling statable. No `Field` assumption.
+* The base ring `B` does not appear: separation is purely a `P`-fact.
+
+The file also provides `decoupledFieldCarrier` (`P = 𝔽₄ ≠ E = 𝔽₈`), closing the anti-overfit
+gate "R5" (see the KB page): the `[IsDomain P]`-gated layer is exercised on a decoupled
+non-Binius carrier (INV-2).
+
+## References
+
+- [BRW26] Bünz, Rothblum, Wang. "Flock: Fast Proving for Batch Boolean Computations." Cryptology
+  ePrint Archive, Report 2026/1329. Appendix B (eq-fold batching, error `κ/|F|`).
+- [RSG] "Ring switching, generalized." Note, leanEthereum/leanVM-b repository (γ-power batching,
+  error `e/|F|`).
+-/
+
+noncomputable section
+
+namespace RingSwitching.Generic
+
+open Module MvPolynomial ProbabilityTheory
+open scoped NNReal ENNReal
+
+/-- **Batching strategy** (design step 5, the one real design axis): how to fold a `W`-indexed
+family of claims over `P` into a single claim. `weight c u` is the coefficient the challenge `c`
+assigns to claim slot `u`; `separates` is the Schwartz–Zippel guarantee that two *distinct*
+claim-tuples collide after weighting with probability at most `error` — the only fact batching
+soundness (S6) consumes. Instances are a closed, proven menu; a carrier picks one.
+
+The structure itself is gated only on `[CommRing P]`: the domain/finiteness hypotheses live on
+the proven instances (`gammaPowers`/`eqFold`) and on the S6 soundness theorem (`[IsDomain car.P]`,
+the design's honest fork) — NOT on the vocabulary, so a non-domain carrier (Hachi `R_q`, design
+§5's sibling theorem) can still *state* a strategy and supply its own proven `separates`/gap. -/
+structure BatchingStrategy (P : Type) [CommRing P] (W : Type) [Fintype W] where
+  /-- The verifier's batching challenge. -/
+  Challenge : Type
+  [ftC : Fintype Challenge]
+  [neC : Nonempty Challenge]
+  /-- The weight that challenge `c` assigns to claim slot `u`. -/
+  weight : Challenge → W → P
+  /-- The separation error (a probability, compared in `ℝ≥0∞` against a uniform challenge). -/
+  error : ℝ≥0
+  /-- Schwartz–Zippel separation: distinct claim-tuples stay distinct after weighting, except with
+  probability `error` over the challenge. -/
+  separates : ∀ s s' : W → P, s ≠ s' →
+    Pr_{ let c ←$ᵖ Challenge }[ ∑ u, weight c u * s u = ∑ u, weight c u * s' u ]
+      ≤ (error : ℝ≥0∞)
+
+attribute [instance] BatchingStrategy.ftC BatchingStrategy.neC
+
+namespace BatchingStrategy
+
+/-- Transport a batching strategy along an equivalence of claim-index types: same challenge, same
+error, weights composed with the equivalence. This is how S6 lands the proven instances at the
+carrier's opening index (`gammaPowers … |>.reindex (Fintype.equivFin _)` for any finite `ιE`);
+for `eqFold`, supplying `e : W' ≃ (Fin κ → Fin 2)` is exactly the instance's honest obligation to
+choose a bit-indexing of its `2^κ` claims. -/
+def reindex {P : Type} [CommRing P] {W : Type} [Fintype W] (bat : BatchingStrategy P W)
+    {W' : Type} [Fintype W'] (e : W' ≃ W) : BatchingStrategy P W' where
+  Challenge := bat.Challenge
+  weight c u' := bat.weight c (e u')
+  error := bat.error
+  separates s s' hne := by
+    have key : ∀ (c : bat.Challenge) (t : W' → P),
+        ∑ u' : W', bat.weight c (e u') * t u' = ∑ u : W, bat.weight c u * (t ∘ e.symm) u :=
+      fun c t => Fintype.sum_equiv e _ _ (fun u' => by simp)
+    have hne' : s ∘ e.symm ≠ s' ∘ e.symm := fun hcontra =>
+      hne (funext fun u' => by simpa using congrFun hcontra (e u'))
+    refine (Pr_congr fun c => ?_).trans_le (bat.separates (s ∘ e.symm) (s' ∘ e.symm) hne')
+    rw [key c s, key c s']
+
+variable (P : Type) [CommRing P] [IsDomain P] [Fintype P]
+
+/-- **γ-power random linear combination** ([RSG]): sample `γ ←$ P`, weight claim `u ∈ Fin e` by
+`γ^u`. Universal — no structure on the claim count `e`. Error `e/|P|` (the difference polynomial
+`∑ᵤ (s−s')ᵤ Xᵘ` has degree ≤ `e−1`; the stated error rounds up to the paper's `e/|P|`).
+Exponent convention: powers run `γ^0..γ^{e−1}` (the note uses `γ^1..γ^e`) — equivalent for
+separation, and slot `0` carrying the constant weight `1` is the standard RLC normalization. -/
+def gammaPowers (e : ℕ) : BatchingStrategy P (Fin e) where
+  Challenge := P
+  weight γ u := γ ^ (u : ℕ)
+  error := (e : ℝ≥0) / (Fintype.card P : ℝ≥0)
+  separates s s' hne := by
+    classical
+    obtain ⟨u₀, hu₀⟩ := Function.ne_iff.mp hne
+    -- the univariate difference polynomial `∑ᵤ (s u − s' u)·Xᵘ`
+    set f : MvPolynomial (Fin 1) P := ∑ u : Fin e, C (s u - s' u) * X 0 ^ (u : ℕ) with hf
+    -- the collision event is exactly the vanishing of `f` at the challenge
+    have hev : ∀ γ : P,
+        ((∑ u : Fin e, γ ^ (u : ℕ) * s u = ∑ u : Fin e, γ ^ (u : ℕ) * s' u) ↔
+          MvPolynomial.eval (fun _ : Fin 1 => γ) f = 0) := by
+      intro γ
+      have hcalc : MvPolynomial.eval (fun _ : Fin 1 => γ) f
+          = (∑ u : Fin e, γ ^ (u : ℕ) * s u) - ∑ u : Fin e, γ ^ (u : ℕ) * s' u := by
+        rw [hf, map_sum, ← Finset.sum_sub_distrib]
+        exact Finset.sum_congr rfl fun u _ => by
+          simp only [map_mul, eval_C, map_pow, eval_X]; ring
+      rw [hcalc, sub_eq_zero]
+    -- `f ≠ 0`: its `X^{u₀}` coefficient is `s u₀ − s' u₀ ≠ 0`
+    have hcoeff : MvPolynomial.coeff (Finsupp.single 0 (u₀ : ℕ)) f = s u₀ - s' u₀ := by
+      rw [hf, MvPolynomial.coeff_sum]
+      rw [Finset.sum_eq_single u₀]
+      · rw [MvPolynomial.coeff_C_mul, MvPolynomial.coeff_X_pow]
+        simp
+      · intro u _ hu
+        have hne' : Finsupp.single (0 : Fin 1) (u : ℕ) ≠ Finsupp.single 0 (u₀ : ℕ) :=
+          fun h => hu (Fin.val_injective (Finsupp.single_injective _ h))
+        rw [MvPolynomial.coeff_C_mul, MvPolynomial.coeff_X_pow, if_neg hne', mul_zero]
+      · simp
+    have hf_ne : f ≠ 0 := fun h0 => sub_ne_zero_of_ne hu₀ (by rw [← hcoeff, h0]; simp)
+    -- degree bound `e − 1`
+    have hdeg : f.totalDegree ≤ e - 1 := by
+      rw [hf]
+      refine totalDegree_finsetSum_le fun u _ => ?_
+      refine le_trans (totalDegree_mul _ _) ?_
+      have h1 : (C (s u - s' u) : MvPolynomial (Fin 1) P).totalDegree = 0 := totalDegree_C _
+      have h2 : (X (0 : Fin 1) ^ (u : ℕ) : MvPolynomial (Fin 1) P).totalDegree ≤ (u : ℕ) :=
+        le_trans (totalDegree_pow _ _) (by simp [totalDegree_X])
+      have : (u : ℕ) ≤ e - 1 := Nat.le_sub_one_of_lt u.isLt
+      omega
+    refine (Pr_congr hev).trans_le
+      ((prob_schwartz_zippel_single_variable f (e - 1) hf_ne hdeg).trans ?_)
+    rw [ENNReal.coe_div (Nat.cast_ne_zero.mpr Fintype.card_ne_zero)]
+    gcongr
+    exact_mod_cast Nat.sub_le e 1
+
+/-- **eq-fold** ([BRW26] App. B; ArkLib's DP24 batching phase): claims indexed by the Boolean cube
+`{0,1}^κ`; sample `r'' ←$ P^κ`, weight claim `u` by the multilinear eq-indicator `eq̃(u, r'')`
+(the same `eqTilde ↑u r''` fold as `RingSwitching.compute_s0`, boolean point first). Power-of-two
+claim counts only. Error `κ/|P|` (the difference polynomial `MLE (s−s')` is multilinear in `κ`
+variables). -/
+def eqFold (κ : ℕ) : BatchingStrategy P (Fin κ → Fin 2) where
+  Challenge := Fin κ → P
+  weight c u := eqTilde (u : Fin κ → P) c
+  error := (κ : ℝ≥0) / (Fintype.card P : ℝ≥0)
+  separates s s' hne := by
+    classical
+    obtain ⟨u₀, hu₀⟩ := Function.ne_iff.mp hne
+    -- the multilinear difference polynomial `MLE (s − s')`
+    set f : MvPolynomial (Fin κ) P := MLE (fun u => s u - s' u) with hf
+    -- the collision event is exactly the vanishing of `f` at the challenge (MLE eq-expansion)
+    have hev : ∀ c : Fin κ → P,
+        ((∑ u : Fin κ → Fin 2, eqTilde (u : Fin κ → P) c * s u
+            = ∑ u : Fin κ → Fin 2, eqTilde (u : Fin κ → P) c * s' u) ↔
+          MvPolynomial.eval c f = 0) := by
+      intro c
+      have hcalc : MvPolynomial.eval c f
+          = (∑ u : Fin κ → Fin 2, eqTilde (u : Fin κ → P) c * s u)
+            - ∑ u : Fin κ → Fin 2, eqTilde (u : Fin κ → P) c * s' u := by
+        rw [hf, MLE_eval_eq_sum_eqTilde, ← Finset.sum_sub_distrib]
+        exact Finset.sum_congr rfl fun u _ => mul_sub _ _ _
+      rw [hcalc, sub_eq_zero]
+    -- `f ≠ 0`: it interpolates `s − s'`, which is nonzero at `u₀` (INV-3: no vacuous batching)
+    have hf_ne : f ≠ 0 := fun h0 => sub_ne_zero_of_ne hu₀ (by
+      have h := MLE_eval_zeroOne (R := P) u₀ (fun u => s u - s' u)
+      rw [← hf, h0, map_zero] at h
+      exact h.symm)
+    -- degree bound: multilinear in `κ` variables
+    have hdeg : f.totalDegree ≤ κ := by
+      rw [hf]
+      simpa using MLE_totalDegree_le (fun u => s u - s' u)
+    exact (Pr_congr hev).trans_le
+      ((prob_schwartz_zippel_mv_polynomial f κ hf_ne hdeg).trans_eq
+        (ENNReal.coe_div (Nat.cast_ne_zero.mpr Fintype.card_ne_zero)).symm)
+
+end BatchingStrategy
+
+/-! ## Decoupled field carrier (gate "R5") -/
+
+/-- **Decoupled field carrier** (R5 gate): `P = 𝔽₄`, `E = 𝔽₈` — two *fields* with `P ≠ E` and
+distinct ranks (2 ≠ 3) over `B = 𝔽₂`. Unlike `decoupledToyCarrier` (a product ring, not a
+domain), this carrier can exercise every `[IsDomain P]`-gated result (batching here, soundness at
+S6), keeping INV-2 live for the soundness path. `Fact (Nat.Prime 2)` is mathlib's
+`Nat.fact_prime_two`; the bases come from `finrank (ZMod 2) (GaloisField 2 n) = n`. -/
+def decoupledFieldCarrier : RingSwitchCarrier (ZMod 2) where
+  P := GaloisField 2 2
+  E := GaloisField 2 3
+  ιP := Fin 2
+  ιE := Fin 3
+  packBasis := Module.finBasisOfFinrankEq _ _ (GaloisField.finrank (p := 2) (n := 2) (by norm_num))
+  openBasis := Module.finBasisOfFinrankEq _ _ (GaloisField.finrank (p := 2) (n := 3) (by norm_num))
+
+/-! ## Sanity / testable deliverables (S3 §5.3) -/
+
+section Sanity
+
+open BatchingStrategy
+
+-- INV-5 bound pins: the stated errors are *definitionally* the papers' bounds
+-- (γ-RLC `e/|P|`, [RSG]; eq-fold `κ/|P|`, [BRW26]).
+example (P : Type) [CommRing P] [IsDomain P] [Fintype P] (e : ℕ) :
+    (gammaPowers P e).error = (e : ℝ≥0) / (Fintype.card P : ℝ≥0) := rfl
+
+example (P : Type) [CommRing P] [IsDomain P] [Fintype P] (κ : ℕ) :
+    (eqFold P κ).error = (κ : ℝ≥0) / (Fintype.card P : ℝ≥0) := rfl
+
+-- γ-RLC instantiates over a concrete field (𝔽₁₆) with e = 3 claims,
+-- and over a computable-instance field with no `letI` plumbing.
+example :
+    letI : Fintype (GaloisField 2 4) := Fintype.ofFinite _
+    BatchingStrategy (GaloisField 2 4) (Fin 3) :=
+  letI : Fintype (GaloisField 2 4) := Fintype.ofFinite _
+  gammaPowers _ 3
+
+example : BatchingStrategy (ZMod 3) (Fin 3) := gammaPowers _ 3
+
+-- The S8/Hachi fork stays *statable*: a non-domain ring can state a strategy (it must then
+-- supply its own proven `separates`); `[IsDomain]` gates only the proven menu and, later, the
+-- S6 domain soundness theorem — the fork lives at the theorem, not the vocabulary.
+example : Type 1 := BatchingStrategy (ZMod 6) (Fin 2)
+
+-- Reindexing lands a proven instance at an arbitrary (equiv) claim index — the S6 path onto
+-- `car.ιE` (here: eq-fold's `2^2` cube re-indexed as `Fin 4`).
+example : BatchingStrategy (ZMod 3) (Fin (2 ^ 2)) :=
+  (eqFold (ZMod 3) 2).reindex finFunctionFinEquiv.symm
+
+-- R5 closure: batching is exercised at the *decoupled carrier's own* packing algebra — the
+-- `rfl` pin certifies `decoupledFieldCarrier.P` IS `𝔽₄` definitionally (the projection is
+-- opaque to instance search, so the instantiations below are typed at `GaloisField 2 2`), so
+-- the `[IsDomain P]` layer now has a non-Binius witness (INV-2), not merely a nearby lookalike.
+example : decoupledFieldCarrier.P = GaloisField 2 2 := rfl
+
+example :
+    letI : Fintype (GaloisField 2 2) := Fintype.ofFinite _
+    BatchingStrategy (GaloisField 2 2) (Fin 3) :=
+  letI : Fintype (GaloisField 2 2) := Fintype.ofFinite _
+  gammaPowers _ 3
+
+-- eq-fold instantiates at the decoupled carrier's packing algebra too (κ = 2, i.e. 4 claims).
+example :
+    letI : Fintype (GaloisField 2 2) := Fintype.ofFinite _
+    BatchingStrategy (GaloisField 2 2) (Fin 2 → Fin 2) :=
+  letI : Fintype (GaloisField 2 2) := Fintype.ofFinite _
+  eqFold _ 2
+
+-- …and at the projection itself, with the instances landed by definitional transport — the
+-- exact plumbing S6 will need at `car.P`.
+example :
+    letI : IsDomain decoupledFieldCarrier.P := inferInstanceAs (IsDomain (GaloisField 2 2))
+    letI : Fintype decoupledFieldCarrier.P :=
+      letI : Finite decoupledFieldCarrier.P := inferInstanceAs (Finite (GaloisField 2 2))
+      Fintype.ofFinite _
+    BatchingStrategy decoupledFieldCarrier.P (Fin 3) :=
+  letI : IsDomain decoupledFieldCarrier.P := inferInstanceAs (IsDomain (GaloisField 2 2))
+  letI : Fintype decoupledFieldCarrier.P :=
+    letI : Finite decoupledFieldCarrier.P := inferInstanceAs (Finite (GaloisField 2 2))
+    Fintype.ofFinite _
+  gammaPowers _ 3
+
+end Sanity
+
+end RingSwitching.Generic
+
+end
diff --git a/ArkLib/ProofSystem/RingSwitching/Generic/Carrier.lean b/ArkLib/ProofSystem/RingSwitching/Generic/Carrier.lean
new file mode 100644
index 0000000000..54f3d6ad04
--- /dev/null
+++ b/ArkLib/ProofSystem/RingSwitching/Generic/Carrier.lean
@@ -0,0 +1,200 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Hicks
+-/
+
+import ArkLib.ProofSystem.RingSwitching.Prelude
+import Mathlib.Algebra.Algebra.Pi
+import Mathlib.LinearAlgebra.Pi
+
+/-!
+# Generic Ring-Switching — Definitional Layer (S1)
+
+The shrunk carrier for a *generic, field-decoupled* ring switch, plus the derived definitions that
+every ring-switch reduction shares. Design background — the seven-step spine, the safety pillars
+cited below, and the layer's status — is in `docs/kb/concepts/ring-switching.md` ("The Generic
+layer").
+
+Unlike the DP24 `RingSwitchingProfile`, this carrier supplies **only** algebra + `Basis` witnesses:
+the packing algebra `P` and the opening algebra `E` are *unrelated* `B`-algebras (the generalization
+of Diamond–Posen / Flock App. B / the "Ring switching, generalized" note [RSG]). Everything else
+— the eq-decomposition, the bridge `Φ`, the packed polynomial — is *derived* from the two bases, so
+an instance has no lever to supply a law-free coordinate map (design safety pillar 1: `Basis` is the
+safe primitive).
+
+DP24/Binius is the special case `P = E = L`, `B = K` (`towerCarrier`); the decoupled case is
+witnessed by `decoupledToyCarrier` (`P ≠ E`), which keeps the anti-overfit invariant INV-2 live from
+the first session.
+
+This module is **definitional only** — no security proofs. Packing correctness (`packedMLE_eval`,
+and the `packMLE = packedMLE ∘ curry` bridge that keeps the Binius path stable) is S2.
+
+## References
+
+- [DP24] Diamond, Benjamin E., and Jim Posen. "Polylogarithmic Proofs for Multilinears over
+  Binary Towers." Cryptology ePrint Archive (2024).
+- [BRW26] Bünz, Rothblum, Wang. "Flock: Fast Proving for Batch Boolean Computations." Cryptology
+  ePrint Archive, Report 2026/1329. Appendix B (the Φ/matrix-branching-program formulation of
+  the ring switch).
+- [RSG] "Ring switching, generalized." Note, leanEthereum/leanVM-b repository (decoupled
+  packing/opening fields, γ-power batching).
+-/
+
+noncomputable section
+
+namespace RingSwitching.Generic
+
+open Module MvPolynomial Sumcheck.Structured
+
+/-- The packing-layer data a *generic* ring-switch abstracts over. `P` is the packing algebra
+(where the committed dense polynomial lives), `E` the opening algebra (where evaluation claims
+arrive); both are free `B`-modules via `packBasis`/`openBasis`, and — crucially — they are
+**unrelated** to each other. Compare `RingSwitchingProfile`, which bakes in a single tower field and
+supplies coordinate maps + embeddings by hand; here those are all derived from the two bases.
+Carriers live in `Type` 0 (`MultilinearPoly` is `Type`-bound, forcing `P`/`E` : `Type`). -/
+structure RingSwitchCarrier (B : Type) [CommRing B] where
+  /-- Packing algebra (dense-committed polynomial's coefficient ring). -/
+  P : Type
+  /-- Opening algebra (evaluation-claim field/ring). -/
+  E : Type
+  /-- Packing basis index; `|ιP|` = packing rank (arbitrary, need not be a power of two). -/
+  ιP : Type
+  /-- Index set of the opening basis (`|ιE|` = opening rank). -/
+  ιE : Type
+  [commP : CommRing P]
+  [algP : Algebra B P]
+  [commE : CommRing E]
+  [algE : Algebra B E]
+  -- Well-formedness: both algebras are nontrivial. A genuine ring-switch precondition, not a
+  -- convenience — without it a degenerate carrier (e.g. `P = E = PUnit`, empty bases) is a
+  -- *bona-fide* carrier (an empty `Basis` is honest, so "no fake basis" does not exclude it) on
+  -- which the future opening anchor `∀ i, αᵢ = P̂ᵢ(r)` (which lives over `E`) collapses to `univ`.
+  -- The planned `[IsDomain P]` fork guards only `P`; `Nontrivial E` is the symmetric guard needed.
+  [ntP : Nontrivial P]
+  [ntE : Nontrivial E]
+  [ftP : Fintype ιP]
+  [ftE : Fintype ιE]
+  /-- `B`-basis of the packing algebra `P`. -/
+  packBasis : Basis ιP B P
+  /-- `B`-basis of the opening algebra `E`. -/
+  openBasis : Basis ιE B E
+
+attribute [instance] RingSwitchCarrier.commP RingSwitchCarrier.algP RingSwitchCarrier.commE
+  RingSwitchCarrier.algE RingSwitchCarrier.ntP RingSwitchCarrier.ntE RingSwitchCarrier.ftP
+  RingSwitchCarrier.ftE
+
+namespace RingSwitchCarrier
+
+variable {B : Type} [CommRing B] (car : RingSwitchCarrier B)
+
+/-- Boolean hypercube point as a `0`/`1` point over the opening algebra `E`. -/
+def boolToE {m : ℕ} (y : Fin m → Fin 2) : Fin m → car.E :=
+  fun i => if y i = 1 then 1 else 0
+
+/-- **Packing** (design step 1). Pack a family of `B`-valued multilinears into a single
+`P`-valued multilinear: `P_packed(y) = ∑ᵢ (Pᵢ)(y) · packBasisᵢ`. This is the note's "pack across the
+family" primitive — natively rank-agnostic (`ιP` arbitrary). DP24's variable-splitting `packMLE` is
+the special case where the family is the currying of one polynomial's first `κ` variables (bridge
+lemma is S2). -/
+def packedMLE {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) : MultilinearPoly car.P m :=
+  ∑ i, car.packBasis i • componentWise_embed_MLE B m (algebraMap B car.P) (Ps i)
+
+/-- **eq-decomposition** (design step 3). The `u`-th `B`-coordinate of `eq(r, y) ∈ E` in the opening
+basis — the function `A(y,u)` of Flock App. B. This is *not* instance data: it is `openBasis.repr`,
+so the reconstruction law `∑ᵤ A(y,u)·b_u^E = eq(r,y)` is `Basis.sum_repr`, free from mathlib. -/
+def eqCoord {m : ℕ} (r : Fin m → car.E) (y : Fin m → Fin 2) (u : car.ιE) : B :=
+  car.openBasis.repr (eqTilde r (car.boolToE y)) u
+
+/-- **The bridge `Φ : E → P`** (design step 7 / batching). The unique `B`-linear map sending each
+opening basis vector `b_u^E` to `weight u`. Derived via `Basis.constr`, so `B`-linearity and
+`Φ(b_u^E) = weight u` are free — no instance freedom (design safety pillar 1). -/
+def bridge (weight : car.ιE → car.P) : car.E →ₗ[B] car.P :=
+  car.openBasis.constr B weight
+
+/-- **The auxiliary multiplier `B(y) = Φ(eq(r, y))`** (design step 6), as a `P`-multilinear, given
+the batching weights. The verifier evaluates its MLE at the sumcheck output point; efficient
+evaluation (tensor / matrix-branching-program) is a later, off-soundness-path refinement (S9). -/
+def Bmult {m : ℕ} (r : Fin m → car.E) (weight : car.ιE → car.P) : MultilinearPoly car.P m :=
+  ⟨MvPolynomial.MLE (fun y : Fin m → Fin 2 => car.bridge weight (eqTilde r (car.boolToE y))),
+    MLE_mem_restrictDegree _⟩
+
+/-- **The linchpin identity** (design steps 3+5+6+7, unified): the bridge applied to `eq(r,y)`
+expands over the opening basis as `Φ(eq(r,y)) = ∑ᵤ A(y,u)·weight(u)`, i.e. `B(y)` is the
+`weight`-batched recombination of the eq-coordinates. Free from `Basis.constr` — no domain, no
+instance freedom. This is the algebraic heart the batching/sumcheck soundness (S5/S6) pivots on;
+proving it now locks the design's core claim (design safety pillars 1 & 3). -/
+theorem bridge_eqTilde {m : ℕ} (r : Fin m → car.E) (y : Fin m → Fin 2)
+    (weight : car.ιE → car.P) :
+    car.bridge weight (eqTilde r (car.boolToE y)) = ∑ u, car.eqCoord r y u • weight u := by
+  simp only [bridge, eqCoord, Basis.constr_apply_fintype, Basis.equivFun_apply]
+
+end RingSwitchCarrier
+
+/-! ## Instances (INV-2: two structurally distinct carriers) -/
+
+/-- **Tower / Binius carrier**: `P = E = L`, `B = K`, both bases the single field basis `β` — the
+DP24 special case (the shape `binaryTowerProfile` abstracts). -/
+def towerCarrier {K L : Type} [Field K] [Field L] [Algebra K L]
+    {ι : Type} [Fintype ι] (β : Basis ι K L) : RingSwitchCarrier K where
+  P := L
+  E := L
+  ιP := ι
+  ιE := ι
+  packBasis := β
+  openBasis := β
+
+/-- **Decoupled toy carrier**: `P = Fin 2 → ZMod 2` (rank 2), `E = Fin 3 → ZMod 2` (rank 3) over
+`B = ZMod 2`. `P ≠ E` with distinct ranks — a deliberately minimal witness that no definition
+assumes `P = E` (INV-2). Not a domain (a product ring), which is fine here: S1 is definitional.
+A `GaloisField` field pair is a later, more realistic instance (relevant once `[IsDomain]` enters
+at S6). -/
+def decoupledToyCarrier : RingSwitchCarrier (ZMod 2) where
+  P := Fin 2 → ZMod 2
+  E := Fin 3 → ZMod 2
+  ιP := Fin 2
+  ιE := Fin 3
+  packBasis := Pi.basisFun (ZMod 2) (Fin 2)
+  openBasis := Pi.basisFun (ZMod 2) (Fin 3)
+
+/-! ## Sanity / testable deliverables (S1 §5.3) -/
+
+section Sanity
+
+-- Both carriers build (INV-2): tower `P = E` and decoupled `P ≠ E`.
+example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L) :
+    RingSwitchCarrier K := towerCarrier β
+
+example : RingSwitchCarrier (ZMod 2) := decoupledToyCarrier
+
+-- The derived defs apply on the *decoupled* carrier (exercises the `P ≠ E` path).
+-- Note the packing direction the types enforce: a family of `B`-valued (`ZMod 2`) multilinears
+-- packs into a single `P`-valued one.
+example (Ps : decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3) :
+    MultilinearPoly decoupledToyCarrier.P 3 :=
+  decoupledToyCarrier.packedMLE Ps
+
+example (r : Fin 3 → decoupledToyCarrier.E) (y : Fin 3 → Fin 2) (u : decoupledToyCarrier.ιE) :
+    ZMod 2 := decoupledToyCarrier.eqCoord r y u
+
+example (w : decoupledToyCarrier.ιE → decoupledToyCarrier.P) :
+    decoupledToyCarrier.E →ₗ[ZMod 2] decoupledToyCarrier.P :=
+  decoupledToyCarrier.bridge w
+
+example (r : Fin 3 → decoupledToyCarrier.E) (w : decoupledToyCarrier.ιE → decoupledToyCarrier.P) :
+    MultilinearPoly decoupledToyCarrier.P 3 :=
+  decoupledToyCarrier.Bmult r w
+
+-- INV-2 (*semantic*, not just typecheck): the linchpin identity `bridge_eqTilde` holds on the
+-- decoupled `P ≠ E` carrier — a value-level pin of `bridge` and `eqCoord` together.
+example (r : Fin 3 → decoupledToyCarrier.E) (y : Fin 3 → Fin 2)
+    (w : decoupledToyCarrier.ιE → decoupledToyCarrier.P) :
+    decoupledToyCarrier.bridge w (eqTilde r (decoupledToyCarrier.boolToE y))
+      = ∑ u, decoupledToyCarrier.eqCoord r y u • w u :=
+  decoupledToyCarrier.bridge_eqTilde r y w
+
+end Sanity
+
+end RingSwitching.Generic
+
+end
diff --git a/ArkLib/ProofSystem/RingSwitching/Generic/Packing.lean b/ArkLib/ProofSystem/RingSwitching/Generic/Packing.lean
new file mode 100644
index 0000000000..e16706cc46
--- /dev/null
+++ b/ArkLib/ProofSystem/RingSwitching/Generic/Packing.lean
@@ -0,0 +1,259 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Hicks
+-/
+
+import ArkLib.ProofSystem.RingSwitching.Generic.Carrier
+
+/-!
+# Generic Ring-Switching — Packing Correctness (S2)
+
+Discharges the **embedded-point half** of design Hole B / safety pillar 3(i): the generic packing
+correctness identity is proven once, generically, so no downstream instance re-touches it. See
+`docs/kb/concepts/ring-switching.md` ("The Generic layer") for the safety pillars cited below.
+
+Scope, stated honestly: (i) `packedMLE_eval` is the reassembly identity at **base-embedded points**
+`algebraMap ∘ pt` — the only well-typed form, since each `Pᵢ` is a `B`-multilinear (there is no
+`∑ Pᵢ·bᵢ` at a general `P`-point). (ii) full **polynomial** packing correctness (holding at every
+point) is delivered *only for the tower/field case* by `packMLE_eq_packedMLE_curry`, via multilinear
+uniqueness (needs `[IsDomain L]`). (iii) the round-trip for the **generic** `packedMLE` is now
+delivered by the "Generic unpacking" section below (`unpack`, `packedMLE_unpack`,
+`unpack_packedMLE` — coefficient-wise, `CommRing`-only; added at S6 for the extractor per design
+review F2); the DP24-specific `unpackMLE ∘ packMLE = id` round-trip (rank-`2^κ` variable
+merging, design Hole B's second half) remains a follow-up. A future session must still not assume
+non-embedded-point reassembly from this file.
+
+Two results (plus the unpacking section):
+
+* `packedMLE_eval` — the semantic content of packing: evaluating the packed `P`-multilinear at (the
+  image of) a base-ring point `pt` reassembles the base evaluations against the packing basis,
+  `P̂_packed(pt) = ∑ᵢ (algebraMap (P̂ᵢ(pt))) · bᵢ^P`. A pure `Basis`/`MLE` fact — no domain
+  hypothesis, no instance obligation.
+* `packMLE_eq_packedMLE_curry` — the **Binius-stability bridge** (label "R2"): the DP24 rank-`2^κ`
+  variable-splitting `packMLE` is exactly the generic `packedMLE` applied to the curried family of
+  the input polynomial over the tower carrier. This keeps the proven Binius path stable while
+  subsuming it under the generic definition.
+
+## References
+
+- [DP24] Diamond, Benjamin E., and Jim Posen. "Polylogarithmic Proofs for Multilinears over
+  Binary Towers." Cryptology ePrint Archive (2024). Definition 2.2 (prefix variable-splitting).
+- [RSG] "Ring switching, generalized." Note, leanEthereum/leanVM-b repository
+  (arbitrary-rank family packing).
+-/
+
+noncomputable section
+
+namespace RingSwitching.Generic
+
+open Module MvPolynomial Sumcheck.Structured
+
+namespace RingSwitchCarrier
+
+variable {B : Type} [CommRing B] (car : RingSwitchCarrier B)
+
+/-- The underlying `MvPolynomial` of the packed multilinear: the honest
+`∑ᵢ bᵢ^P · map(algebraMap) Pᵢ` (safety pillar 1 — derived from the packing basis, no freedom). -/
+theorem packedMLE_val {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) :
+    (car.packedMLE Ps).val
+      = ∑ i, car.packBasis i • MvPolynomial.map (algebraMap B car.P) (Ps i).val := by
+  rw [packedMLE, Submodule.coe_sum]
+  refine Finset.sum_congr rfl (fun i _ => ?_)
+  rw [Submodule.coe_smul]
+  rfl
+
+/-- **Packing correctness** (design step 1 / safety pillar 3, Hole B). Evaluating the packed
+multilinear at (the image of) a base-ring point `pt` reassembles the base evaluations against the
+packing basis:
+`P̂_packed(algebraMap ∘ pt) = ∑ᵢ (algebraMap (P̂ᵢ(pt))) · bᵢ^P`.
+A pure `Basis`/`MLE` fact — no domain hypothesis, no per-instance obligation. -/
+theorem packedMLE_eval {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) (pt : Fin m → B) :
+    MvPolynomial.eval (fun i => algebraMap B car.P (pt i)) (car.packedMLE Ps).val
+      = ∑ i, algebraMap B car.P ((Ps i).val.eval pt) * car.packBasis i := by
+  have key : ∀ p : MvPolynomial (Fin m) B,
+      MvPolynomial.eval (fun i => algebraMap B car.P (pt i))
+          (MvPolynomial.map (algebraMap B car.P) p)
+        = algebraMap B car.P (MvPolynomial.eval pt p) := by
+    intro p
+    induction p using MvPolynomial.induction_on with
+    | C a => simp
+    | add p q hp hq => simp [map_add, hp, hq]
+    | mul_X p n hp => simp [map_mul, hp]
+  rw [packedMLE_val, MvPolynomial.eval_sum]
+  refine Finset.sum_congr rfl (fun i _ => ?_)
+  rw [MvPolynomial.smul_eval, key]
+  ring
+
+/-! ### Generic unpacking — the `packedMLE` round-trip (S6, design review F2)
+
+The S6 extractor needs a *section* of `packedMLE`. The generic route is coefficient-wise: the
+`i`-th unpacked component takes each packed coefficient to its `i`-th packing-basis
+`B`-coordinate. This stays inside pure `Basis`/coefficient algebra — no evaluation detour, no
+domain hypothesis — so both round-trip directions hold over any `CommRing` (unlike the
+evaluation-interpolation route, which would need `[IsDomain P]`). -/
+
+/-- **Generic unpacking**: the `i`-th component of the unpacked family has coefficients
+`coeff d (unpack t' i) = packBasis.repr (coeff d t') i` (see `unpack_coeff`). This is the generic
+section of `packedMLE` (design review F2); the DP24 rank-`2^κ` variable-*merging* `unpackMLE` is
+a different, Binius-specific map (still a follow-up, see the header). -/
+def unpack {m : ℕ} (t' : MultilinearPoly car.P m) : car.ιP → MultilinearPoly B m :=
+  fun i =>
+    ⟨∑ d ∈ t'.val.support, MvPolynomial.monomial d (car.packBasis.repr (t'.val.coeff d) i), by
+      classical
+      rw [MvPolynomial.mem_restrictDegree]
+      intro s hs j
+      have hsub : (∑ d ∈ t'.val.support,
+            MvPolynomial.monomial d (car.packBasis.repr (t'.val.coeff d) i)).support
+          ⊆ t'.val.support :=
+        MvPolynomial.support_sum.trans (Finset.biUnion_subset.mpr fun d hd =>
+          MvPolynomial.support_monomial_subset.trans (Finset.singleton_subset_iff.mpr hd))
+      exact (MvPolynomial.mem_restrictDegree _ _ _).mp t'.property s (hsub hs) j⟩
+
+/-- The defining coefficient law of `unpack`: coefficients of the `i`-th unpacked component are
+the `i`-th packing-basis `B`-coordinates of the packed coefficients. -/
+theorem unpack_coeff {m : ℕ} (t' : MultilinearPoly car.P m) (i : car.ιP) (d : Fin m →₀ ℕ) :
+    (car.unpack t' i).val.coeff d = car.packBasis.repr (t'.val.coeff d) i := by
+  classical
+  simp only [unpack, MvPolynomial.coeff_sum, MvPolynomial.coeff_monomial]
+  rw [Finset.sum_ite_eq' t'.val.support d]
+  split_ifs with hd
+  · rfl
+  · rw [MvPolynomial.notMem_support_iff.mp hd]
+    simp
+
+/-- **Round-trip, packed side**: packing the unpacked family returns the packed polynomial —
+`unpack` is a section of `packedMLE`. Pure coefficient algebra + `Basis.sum_repr`;
+`CommRing`-only. -/
+theorem packedMLE_unpack {m : ℕ} (t' : MultilinearPoly car.P m) :
+    car.packedMLE (car.unpack t') = t' := by
+  refine Subtype.ext (MvPolynomial.ext _ _ fun d => ?_)
+  rw [packedMLE_val, MvPolynomial.coeff_sum]
+  simp only [MvPolynomial.coeff_smul, MvPolynomial.coeff_map, unpack_coeff, smul_eq_mul]
+  calc ∑ i, car.packBasis i * algebraMap B car.P (car.packBasis.repr (t'.val.coeff d) i)
+      = ∑ i, car.packBasis.repr (t'.val.coeff d) i • car.packBasis i :=
+        Finset.sum_congr rfl fun i _ => by rw [Algebra.smul_def, mul_comm]
+    _ = t'.val.coeff d := car.packBasis.sum_repr _
+
+/-- **Round-trip, family side**: unpacking the packed family returns the family. Together with
+`packedMLE_unpack` this makes `packedMLE` a bijection with explicit inverse `unpack`
+(`CommRing`-only); the S6 completeness direction reads the honest claims through this law. -/
+theorem unpack_packedMLE {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) :
+    car.unpack (car.packedMLE Ps) = Ps := by
+  funext i
+  refine Subtype.ext (MvPolynomial.ext _ _ fun d => ?_)
+  rw [unpack_coeff]
+  have hcoeff : (car.packedMLE Ps).val.coeff d
+      = ∑ j, (Ps j).val.coeff d • car.packBasis j := by
+    rw [packedMLE_val, MvPolynomial.coeff_sum]
+    simp only [MvPolynomial.coeff_smul, MvPolynomial.coeff_map, smul_eq_mul]
+    exact Finset.sum_congr rfl fun j _ => by rw [Algebra.smul_def, mul_comm]
+  rw [hcoeff]
+  exact congrFun (car.packBasis.repr_sum_self fun j => (Ps j).val.coeff d) i
+
+/-- **`packedMLE` is surjective** (design review F2): every packed multilinear is the packing of
+some `B`-family — witnessed constructively by `unpack`, no choice needed. -/
+theorem packedMLE_surjective {m : ℕ} :
+    Function.Surjective (car.packedMLE (m := m)) :=
+  fun t' => ⟨car.unpack t', car.packedMLE_unpack t'⟩
+
+/-- **Boolean read-back of `unpack`**: hypercube evaluations of the `i`-th unpacked component are
+the `i`-th packing-basis coordinates of the packed evaluations. Derived from `packedMLE_eval`
+through the round-trip (`CommRing`-only); this is the evaluation form the S6 Remark-5 read-back
+lemma consumes. -/
+theorem unpack_eval_zeroOne {m : ℕ} (t' : MultilinearPoly car.P m) (i : car.ιP)
+    (y : Fin m → Fin 2) :
+    (car.unpack t' i).val.eval (y : Fin m → B)
+      = car.packBasis.repr (t'.val.eval (y : Fin m → car.P)) i := by
+  have hpt : (y : Fin m → car.P) = fun j => algebraMap B car.P ((y : Fin m → B) j) :=
+    funext fun j => (map_natCast (algebraMap B car.P) _).symm
+  conv_rhs => rw [← car.packedMLE_unpack t', hpt, packedMLE_eval]
+  simp_rw [← Algebra.smul_def]
+  exact (congrFun (car.packBasis.repr_sum_self
+    fun j => (car.unpack t' j).val.eval (y : Fin m → B)) i).symm
+
+end RingSwitchCarrier
+
+/-! ## The Binius-stability bridge (label "R2") -/
+
+/-- The **curried family** of a length-`ℓ` multilinear over the first `κ` (Boolean) coordinates:
+`curryFamily h_l t v` fixes the first `κ` variables to `v` and is the length-`ℓ'` multilinear whose
+Boolean evaluations are `w ↦ t(v, w)` (with `ℓ = ℓ' + κ`). This is the honest currying that DP24's
+`packMLE` packs across; `packMLE_eq_packedMLE_curry` identifies the two. Convention note: this
+follows DP24 Def. 2.2 in packing the **prefix** coordinates; Flock App. B packs the *suffix*
+(`r = (r_hi, r_lo)`) — a pure variable relabeling, and the generic `packedMLE` is
+convention-free, so wiring Flock verbatim later needs only that relabeling, not a different
+packing. -/
+def curryFamily {κ ℓ ℓ' : ℕ} {K : Type} [CommRing K] (h_l : ℓ = ℓ' + κ)
+    (t : MultilinearPoly K ℓ) : (Fin κ → Fin 2) → MultilinearPoly K ℓ' :=
+  fun v => ⟨MvPolynomial.MLE (fun w : Fin ℓ' → Fin 2 =>
+      MvPolynomial.eval (fun i : Fin ℓ =>
+        ((if h : i.val < κ then v ⟨i.val, h⟩ else w ⟨i.val - κ, by omega⟩ : Fin 2) : K)) t.val),
+    MLE_mem_restrictDegree _⟩
+
+/-- **Binius-stability bridge** (label "R2"). The DP24 rank-`2^κ`
+variable-splitting `packMLE` is exactly the generic `packedMLE` applied to the curried family, over
+the tower carrier. So the proven Binius packing path is a *use* of the generic definition, not a
+parallel one.
+
+The `[Field K] [Field L]` hypotheses come from `towerCarrier` and the multilinear-uniqueness step
+(`is_multilinear_eq_iff_eq_evals_zeroOne` needs `[IsDomain L]`); packing itself
+(`packedMLE`/`packedMLE_eval`) needs only `CommRing`. -/
+theorem packMLE_eq_packedMLE_curry {κ : ℕ} [NeZero κ] {K L : Type} [Field K] [Field L] [Algebra K L]
+    {ℓ ℓ' : ℕ} (h_l : ℓ = ℓ' + κ) (β : Basis (Fin κ → Fin 2) K L) (t : MultilinearPoly K ℓ) :
+    packMLE κ L K ℓ ℓ' h_l β t = (towerCarrier β).packedMLE (curryFamily h_l t) := by
+  apply Subtype.ext
+  rw [is_multilinear_eq_iff_eq_evals_zeroOne _ _
+    (packMLE κ L K ℓ ℓ' h_l β t).property
+    ((towerCarrier β).packedMLE (curryFamily h_l t)).property]
+  funext w₀
+  simp only [MvPolynomial.toEvalsZeroOne]
+  rw [packMLE]
+  simp only [MvPolynomial.MLE_eval_zeroOne, Basis.equivFun_symm_apply]
+  -- The packed side, via generic packing correctness `packedMLE_eval` (proven above).
+  -- `(towerCarrier β)` is not reducible, so we land the lemma into `L`/`β` via `exact` (defeq).
+  have hpe : MvPolynomial.eval (fun i : Fin ℓ' => algebraMap K L ((w₀ i : ℕ) : K))
+        ((towerCarrier β).packedMLE (curryFamily h_l t)).val
+      = ∑ v : Fin κ → Fin 2, algebraMap K L ((curryFamily h_l t v).val.eval
+          (fun i => ((w₀ i : ℕ) : K))) * β v :=
+    RingSwitchCarrier.packedMLE_eval (towerCarrier β) (curryFamily h_l t)
+      (fun i => ((w₀ i : ℕ) : K))
+  conv_rhs => rw [show (fun i : Fin ℓ' => ((w₀ i : ℕ) : L))
+      = (fun i => algebraMap K L ((w₀ i : ℕ) : K)) from by
+        funext i; exact (map_natCast (algebraMap K L) _).symm]
+  rw [hpe]
+  simp only [curryFamily, MvPolynomial.MLE_eval_zeroOne, Algebra.smul_def]
+
+/-! ## Sanity / testable deliverables (S2 §5.3) -/
+
+section Sanity
+
+-- INV-2: packing correctness `packedMLE_eval` instantiates on the *decoupled* (`P ≠ E`) carrier
+-- with a genuine 2-element family (`ιP = Fin 2`), not just the tower carrier.
+example (Ps : decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3) (pt : Fin 3 → ZMod 2) :
+    MvPolynomial.eval (fun i => algebraMap (ZMod 2) decoupledToyCarrier.P (pt i))
+        (decoupledToyCarrier.packedMLE Ps).val
+      = ∑ i, algebraMap (ZMod 2) decoupledToyCarrier.P ((Ps i).val.eval pt)
+          * decoupledToyCarrier.packBasis i :=
+  decoupledToyCarrier.packedMLE_eval Ps pt
+
+-- INV-2: the generic round-trip holds on the *decoupled* `P ≠ E` carrier — a non-domain product
+-- ring, pinning that `unpack` and both round-trip directions are `CommRing`-only…
+example (t' : MultilinearPoly decoupledToyCarrier.P 3) :
+    decoupledToyCarrier.packedMLE (decoupledToyCarrier.unpack t') = t' :=
+  decoupledToyCarrier.packedMLE_unpack t'
+
+example (Ps : decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3) :
+    decoupledToyCarrier.unpack (decoupledToyCarrier.packedMLE Ps) = Ps :=
+  decoupledToyCarrier.unpack_packedMLE Ps
+
+-- …and on the *tower* carrier at full generality (arbitrary field extension, arbitrary rank).
+example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L) (m : ℕ) :
+    Function.Surjective ((towerCarrier β).packedMLE (m := m)) :=
+  (towerCarrier β).packedMLE_surjective
+
+end Sanity
+
+end RingSwitching.Generic
+
+end
diff --git a/ArkLib/ProofSystem/RingSwitching/Generic/Recombine.lean b/ArkLib/ProofSystem/RingSwitching/Generic/Recombine.lean
new file mode 100644
index 0000000000..980280cafc
--- /dev/null
+++ b/ArkLib/ProofSystem/RingSwitching/Generic/Recombine.lean
@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Hicks
+-/
+
+import ArkLib.Data.Module.Basis
+import ArkLib.ProofSystem.RingSwitching.Generic.Carrier
+
+/-!
+# Generic Ring-Switching — Recombination Injectivity (S4; opening half @ S5)
+
+Discharges design safe-core (iii), **Flock Remark 5** [BRW26]: naive recombination is complete
+but *not sound* — soundness requires the packing-basis recombination `s ↦ ∑ᵢ sᵢ • bᵢ^P`
+(`B`-coordinates into the packed algebra) to be injective. In the generic design this is not an
+instance obligation: the map *is* `packBasis.equivFun.symm`, so injectivity — indeed bijectivity —
+is inherited from the `Basis` being a bundled linear equivalence (the reusable statement is
+`Module.Basis.sum_smul_bijective`, `ArkLib/Data/Module/Basis.lean`). A fake or lossy recombination
+is unrepresentable (design safety pillar 1; see `docs/kb/concepts/ring-switching.md`, "The Generic
+layer", for the spine-step and pillar vocabulary used here).
+
+Remark 5's soundness argument uses **both bases**: the packing side (this recombination), and the
+uniqueness of `B`-coordinates on the opening side — `openingDecomposition_injective` below — which
+pins the eq-decomposition `A(y,u) = openBasis.repr (eq r y) u` as the *only* `B`-decomposition of
+`eq(r,y)`.
+
+Scope (design §2, pillar-1 clarification): the soundness-relevant injective map is the
+**packing-basis** recombination (step 4). The bridge `Φ = openBasis.constr weight` (step 7) is a
+batching *combiner* and is deliberately not injective for general weights — do not conflate the
+two.
+
+No domain/field hypotheses — pure `CommRing B` + `Basis` module theory — so the result is
+exercised on both S1 carriers (tower and the non-domain decoupled toy) directly (INV-2).
+
+## References
+
+- [BRW26] Bünz, Rothblum, Wang. "Flock: Fast Proving for Batch Boolean Computations." Cryptology
+  ePrint Archive, Report 2026/1329. Appendix B, Remark 5 and Eq. (8)
+  (slice-wise recombination over the packing basis; injectivity in the base-field coefficients).
+-/
+
+noncomputable section
+
+namespace RingSwitching.Generic
+
+open Module
+
+namespace RingSwitchCarrier
+
+variable {B : Type} [CommRing B] (car : RingSwitchCarrier B)
+
+/-- Recombination is a **bijection**: every packed value arises from a *unique* `B`-coordinate
+tuple, because `s ↦ ∑ᵢ sᵢ • bᵢ^P` is exactly `packBasis.equivFun.symm`. The inverse direction is
+how S5's anchor argument reads (packed value determines the coordinates). -/
+theorem recombine_bijective :
+    Function.Bijective (fun s : car.ιP → B => ∑ i, s i • car.packBasis i) :=
+  car.packBasis.sum_smul_bijective
+
+/-- **Recombination injectivity** (design step 4 / safe-core (iii); [BRW26] Remark 5). Distinct
+`B`-coordinate tuples recombine to distinct packed values. This is the property whose *absence*
+makes naive recombination unsound (Flock Remark 5); here it is free from the packing `Basis`. -/
+theorem recombine_injective :
+    Function.Injective (fun s : car.ιP → B => ∑ i, s i • car.packBasis i) :=
+  car.recombine_bijective.injective
+
+/-- **Opening-side uniqueness** ([BRW26] Remark 5, the other half). `B`-coordinates in the
+*opening* basis are unique: `s ↦ ∑ᵤ sᵤ • bᵤ^E` is injective. The load-bearing soundness
+application ([BRW26] p. 38, "by the uniqueness of the 𝔽₂-decomposition") is to the *claim
+values*: a wrong claim over `E` forces a wrong slice `sᵤ` for at least one `u`. It equally pins
+the eq-decomposition `A(y,u) = eqCoord r y u` as the only `B`-reassembly of `eq(r,y)`
+(`Basis.sum_repr` gives existence; this gives uniqueness). The S5/S6 anchor argument reads the
+sumcheck claim back through this map. -/
+theorem openingDecomposition_injective :
+    Function.Injective (fun s : car.ιE → B => ∑ u, s u • car.openBasis u) :=
+  car.openBasis.sum_smul_injective
+
+end RingSwitchCarrier
+
+/-! ## Sanity / testable deliverables (S4 §5.3) -/
+
+section Sanity
+
+-- INV-2: exercised on the *tower* carrier at full generality — arbitrary field extension,
+-- arbitrary finite rank…
+example {K L : Type} [Field K] [Field L] [Algebra K L] {ι : Type} [Fintype ι]
+    (β : Basis ι K L) :
+    Function.Injective
+      (fun s : (towerCarrier β).ιP → K => ∑ i, s i • (towerCarrier β).packBasis i) :=
+  (towerCarrier β).recombine_injective
+
+-- …with a fully concrete pin (no missing instances at a closed type; NB `Pi.basisFun` has the
+-- wrong module structure for `towerCarrier`, `Basis.singleton` works)…
+example : Function.Injective
+    (fun s : (towerCarrier (Basis.singleton (Fin 1) (ZMod 2))).ιP → ZMod 2
+      => ∑ i, s i • (towerCarrier (Basis.singleton (Fin 1) (ZMod 2))).packBasis i) :=
+  (towerCarrier _).recombine_injective
+
+-- …and on the *decoupled* `P ≠ E` carrier — a non-domain product ring, pinning that the result
+-- is CommRing-only (no `[IsDomain]`/`Field` needed anywhere in this file).
+example : Function.Injective
+    (fun s : decoupledToyCarrier.ιP → ZMod 2 => ∑ i, s i • decoupledToyCarrier.packBasis i) :=
+  decoupledToyCarrier.recombine_injective
+
+-- Opening-side uniqueness on the decoupled carrier (`E` of a *different* rank than `P` — the
+-- two halves of Remark 5 genuinely act on different modules here, unlike the tower case).
+example : Function.Injective
+    (fun s : decoupledToyCarrier.ιE → ZMod 2 => ∑ u, s u • decoupledToyCarrier.openBasis u) :=
+  decoupledToyCarrier.openingDecomposition_injective
+
+end Sanity
+
+end RingSwitching.Generic
+
+end
diff --git a/ArkLib/ProofSystem/RingSwitching/Generic/Reduction.lean b/ArkLib/ProofSystem/RingSwitching/Generic/Reduction.lean
new file mode 100644
index 0000000000..9edf7313b6
--- /dev/null
+++ b/ArkLib/ProofSystem/RingSwitching/Generic/Reduction.lean
@@ -0,0 +1,518 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Hicks
+-/
+
+import ArkLib.ProofSystem.RingSwitching.Generic.Relations
+import ArkLib.OracleReduction.Security.ChallengeRound
+
+/-!
+# Generic Ring-Switching — The Phase Reduction (S6-ii)
+
+The hand-written `ProtocolSpec 2` **ring-switch phase**: the prover sends the recombination
+slices, the verifier checks them against the input claims (the [BRW26] Remark-5 read-back —
+DP24's "Check 1" in family form) and replies with a batching challenge; the output is the
+batched sumcheck claim. Written **without** the composition operators, whose upstream
+`OracleVerifier.append.verify` is sorried — so every definition in this file is sorry-free and
+axiom-clean (the composed end-to-end `ringSwitch` is quarantined in `Generic/Assembly.lean`).
+
+## The claim-consistency check is soundness-critical
+
+The S6 design review (roadmap §8) found that omitting the verifier's check of the slices
+against the claims `α` makes the phase's round-by-round knowledge soundness **false**: an
+adversary sends the *honest* slices of a committed `t'₀` against a false claim vector `α`
+(so `phaseRelIn` is empty while `phaseRelOut` holds with probability 1). The check
+(`car.claimConsistent`) closes exactly this: a slice vector passing the check pins the claims
+to the recombination read-back, which `openingDecomposition_injective` makes unique. The
+verifier fails via `OptionT` `failure` — not via a dummy output statement (the legacy
+`failureState` pattern, whose all-zero dummy can itself land in a relation).
+
+## Relations
+
+* `phaseRelIn` — the anchor `openingClaimRel` **and** the binding conjunct
+  `pc.commitsTo (packedMLE wit)`: exactly the oracle-extended input relation promised at S5.
+* `phaseRelOut` — the batched claim `sumcheckClaimRel` at the verifier's challenge weights
+  **and** `commitsTo` carried through (the tail of the chain must land on `pcs.evalRel`).
+
+Chain coherence for the honest prover is `sumcheckClaim_of_slices` (`Relations.lean`); the
+read-back direction (check-passing slices anchor the claims) is the Remark-5 read-back lemma.
+
+## References
+
+- [DP24] Diamond, Benjamin E., and Jim Posen. "Polylogarithmic Proofs for Multilinears over
+  Binary Towers." Cryptology ePrint Archive (2024). Construction 3.1, steps 1–5.
+- [BRW26] Bünz, Rothblum, Wang. "Flock: Fast Proving for Batch Boolean Computations."
+  Cryptology ePrint Archive, Report 2026/1329. Appendix B, Remark 5.
+- [RSG] "Ring switching, generalized." Note, leanEthereum/leanVM-b repository.
+-/
+
+noncomputable section
+
+namespace RingSwitching.Generic
+
+open OracleSpec OracleComp ProtocolSpec Module MvPolynomial Sumcheck.Structured
+  ProbabilityTheory
+open scoped NNReal ENNReal
+
+variable {B : Type} [CommRing B] (car : RingSwitchCarrier B) (m : ℕ)
+  (bat : BatchingStrategy car.P car.ιE) (pc : PackedCommitment car.P m)
+
+-- The commitment's oracle interfaces, as instances (they are structure fields; registering
+-- them is additive and lets the oracle verifier below elaborate against `pc.OStmt`).
+attribute [instance] PackedCommitment.Oᵢ
+
+/-! ## Protocol specification -/
+
+/-- The ring-switch phase protocol: the prover sends the slices `s : ιE → P` (design step 4),
+the verifier replies with a batching challenge (design step 5). -/
+@[reducible]
+def pSpecRingSwitchPhase : ProtocolSpec 2 :=
+  ⟨![.P_to_V, .V_to_P], ![car.ιE → car.P, bat.Challenge]⟩
+
+instance : ∀ j, OracleInterface ((pSpecRingSwitchPhase car bat).Message j)
+  | ⟨0, _⟩ => OracleInterface.instDefault -- the slices, read whole (as DP24 sends ŝ)
+  | ⟨1, _⟩ => OracleInterface.instDefault -- vacuous (V_to_P round)
+
+instance : ∀ j, SampleableType ((pSpecRingSwitchPhase car bat).Challenge j)
+  | ⟨0, h⟩ => by nomatch h -- P_to_V round has no challenge
+  | ⟨1, _⟩ => by
+    simp only [Challenge, Fin.isValue, Matrix.cons_val_one, Matrix.cons_val_fin_one]
+    exact SampleableType.ofFintype _
+
+/-! ## Honest slices -/
+
+namespace RingSwitchCarrier
+
+/-- The honest prover's slices (design step 4): `sᵤ = ∑_y A(y,u) • t'(y)` — the eq-weighted
+hypercube sums of the packed polynomial, i.e. the canonical `sliceRel` witness. -/
+def honestSlices {m : ℕ} (r : Fin m → car.E) (t' : MultilinearPoly car.P m) :
+    car.ιE → car.P :=
+  fun u => ∑ y : Fin m → Fin 2, car.eqCoord r y u • t'.val.eval (y : Fin m → car.P)
+
+/-- The honest slices are (by definition) the `sliceRel` witness for `t'`. -/
+theorem honestSlices_mem_sliceRel {m : ℕ} (r : Fin m → car.E)
+    (t' : MultilinearPoly car.P m) :
+    (car.honestSlices r t', t') ∈ car.sliceRel m r :=
+  fun _ => rfl
+
+end RingSwitchCarrier
+
+/-! ## Prover -/
+
+/-- The phase prover's state: statement + commitment oracles + family throughout; the packed
+polynomial after packing; the challenge once received. -/
+def PhasePrvState : Fin (2 + 1) → Type
+  | ⟨0, _⟩ => (((car.ιP → car.E) × (Fin m → car.E)) × (∀ j, pc.OStmt j))
+      × (car.ιP → MultilinearPoly B m)
+  | ⟨1, _⟩ => (((car.ιP → car.E) × (Fin m → car.E)) × (∀ j, pc.OStmt j))
+      × MultilinearPoly car.P m
+  | _ => ((((car.ιP → car.E) × (Fin m → car.E)) × (∀ j, pc.OStmt j))
+      × MultilinearPoly car.P m) × bat.Challenge
+
+/-- The honest phase prover: packs the family, sends the honest slices, and outputs the
+batched sumcheck claim at the received challenge together with the packed witness. -/
+def ringSwitchPhaseProver :
+    OracleProver (oSpec := []ₒ)
+      (StmtIn := (car.ιP → car.E) × (Fin m → car.E)) (OStmtIn := pc.OStmt)
+      (WitIn := car.ιP → MultilinearPoly B m)
+      (StmtOut := ((Fin m → car.E) × bat.Challenge) × car.P) (OStmtOut := pc.OStmt)
+      (WitOut := MultilinearPoly car.P m)
+      (pSpec := pSpecRingSwitchPhase car bat) where
+  PrvState := PhasePrvState car m bat pc
+
+  input := fun ⟨⟨stmt, oStmt⟩, wit⟩ => ((stmt, oStmt), wit)
+
+  sendMessage
+    | ⟨0, _⟩ => fun ((stmt, oStmt), wit) => do
+      -- Design steps 1+4: pack the family, send the honest slices.
+      let t' := car.packedMLE wit
+      return ⟨car.honestSlices stmt.2 t', ((stmt, oStmt), t')⟩
+    | ⟨1, h⟩ => fun _ => by nomatch h -- V_to_P round
+
+  receiveChallenge
+    | ⟨0, h⟩ => by nomatch h -- P_to_V round
+    | ⟨1, _⟩ => fun st => do
+      return fun c => (st, c)
+
+  output := fun (((stmt, oStmt), t'), c) => do
+    -- Design step 5: the batched sumcheck target at the verifier's challenge.
+    let σ := ∑ u, bat.weight c u * car.honestSlices stmt.2 t' u
+    return (⟨((stmt.2, c), σ), oStmt⟩, t')
+
+/-! ## Verifier -/
+
+open scoped Classical in
+/-- The phase verifier: reads the slices, **checks them against the input claims** (the
+[BRW26] Remark-5 read-back; soundness-critical, see the module docstring), samples the
+batching challenge, and outputs the batched sumcheck target. Fails via `OptionT` on a bad
+slice vector. (`Classical`: the check is a `Prop`; the verifier is already noncomputable.) -/
+def ringSwitchPhaseVerifier :
+    OracleVerifier (oSpec := []ₒ)
+      (StmtIn := (car.ιP → car.E) × (Fin m → car.E)) (OStmtIn := pc.OStmt)
+      (StmtOut := ((Fin m → car.E) × bat.Challenge) × car.P) (OStmtOut := pc.OStmt)
+      (pSpec := pSpecRingSwitchPhase car bat) where
+  verify := fun stmt challenges => do
+    -- Read the slices (whole-message oracle, as DP24's V reads ŝ).
+    let s : car.ιE → car.P ← query
+      (spec := [(pSpecRingSwitchPhase car bat).Message]ₒ) ⟨⟨0, rfl⟩, ()⟩
+    -- The claim-consistency check (design review F1; DP24 Check 1 in family form).
+    if car.claimConsistent stmt.1 s then
+      let c := challenges ⟨1, rfl⟩
+      return ((stmt.2, c), ∑ u, bat.weight c u * s u)
+    else
+      failure
+  embed := ⟨fun j => Sum.inl j, fun a b h => by cases h; rfl⟩
+  hEq := fun _ => rfl
+
+/-- The ring-switch phase, as a hand-written oracle reduction (no composition operators:
+sorry-free, axiom-clean definitions). -/
+def ringSwitchPhase :
+    OracleReduction (oSpec := []ₒ)
+      (StmtIn := (car.ιP → car.E) × (Fin m → car.E)) (OStmtIn := pc.OStmt)
+      (WitIn := car.ιP → MultilinearPoly B m)
+      (StmtOut := ((Fin m → car.E) × bat.Challenge) × car.P) (OStmtOut := pc.OStmt)
+      (WitOut := MultilinearPoly car.P m)
+      (pSpec := pSpecRingSwitchPhase car bat) where
+  prover := ringSwitchPhaseProver car m bat pc
+  verifier := ringSwitchPhaseVerifier car m bat pc
+
+/-! ## Relations -/
+
+/-- **The phase input relation** (the oracle-extended anchor promised at S5): the semantic
+anchor `openingClaimRel` — every claim is the family's evaluation at `r` — **and** the
+binding conjunct: the commitment commits to the *packed* family. -/
+def phaseRelIn :
+    Set ((((car.ιP → car.E) × (Fin m → car.E)) × (∀ j, pc.OStmt j))
+      × (car.ιP → MultilinearPoly B m)) :=
+  { x | ((x.1.1.1, x.1.1.2), x.2) ∈ car.openingClaimRel m
+      ∧ pc.commitsTo x.1.2 (car.packedMLE x.2) }
+
+/-- **The phase output relation**: the batched sumcheck claim at the challenge's weights
+(`sumcheckClaimRel`), with the binding conjunct carried through (the relation chain's tail
+must land on the PCS's `evalRel`). -/
+def phaseRelOut :
+    Set ((((((Fin m → car.E) × bat.Challenge) × car.P)) × (∀ j, pc.OStmt j))
+      × MultilinearPoly car.P m) :=
+  { x | (x.1.1.2, x.2) ∈ car.sumcheckClaimRel m x.1.1.1.1 (bat.weight x.1.1.1.2)
+      ∧ pc.commitsTo x.1.2 x.2 }
+
+/-! ## Round-by-round error -/
+
+/-- The phase's round-by-round knowledge error, as a per-round **vector**: the batching
+strategy's separation error at the (single) challenge round. -/
+def phaseRBRError : (pSpecRingSwitchPhase car bat).ChallengeIdx → ℝ≥0
+  | ⟨1, _⟩ => bat.error
+  | _ => 0
+
+/-! ## Round-by-round knowledge-soundness components -/
+
+/-- Intermediate witness types for the phase's RBR extraction: the family before the slices
+are sent; the packed polynomial once they are (functionality pins it); the packed polynomial
+at the end (= `WitOut`). -/
+def phaseWitMid : Fin (2 + 1) → Type
+  | ⟨0, _⟩ => car.ιP → MultilinearPoly B m
+  | ⟨1, _⟩ => MultilinearPoly car.P m
+  | ⟨2, _⟩ => MultilinearPoly car.P m
+
+/-- The phase's round-by-round extractor: the challenge round is witness-preserving; the
+message round reads the family back through `unpack` (the section of `packedMLE` —
+[BRW26] Remark 5's "uniqueness of the `B`-decomposition" in extractor form). -/
+noncomputable def phaseRbrExtractor :
+    Extractor.RoundByRound []ₒ
+      (StmtIn := ((car.ιP → car.E) × (Fin m → car.E)) × (∀ j, pc.OStmt j))
+      (WitIn := car.ιP → MultilinearPoly B m)
+      (WitOut := MultilinearPoly car.P m)
+      (pSpec := pSpecRingSwitchPhase car bat)
+      (WitMid := phaseWitMid car m) where
+  eqIn := rfl
+  extractMid m' _ _ witSucc :=
+    match m' with
+    | ⟨0, _⟩ => car.unpack witSucc
+    | ⟨1, _⟩ => witSucc
+  extractOut _ _ witOut := witOut
+
+/-- **The phase's RBR knowledge soundness**, as the framework proposition against the fixed
+anchored relations and the per-round error vector (`bat.error` at the single challenge
+round). Recorded as a `Prop`-valued definition (roadmap §8, F3): its proof — the batching
+round via `BatchingStrategy.separates` + `commitsTo_functional` — is the S6 stretch goal,
+and must never be asserted as a bare `theorem … := sorry`. -/
+def ringSwitchPhaseRBRKnowledgeSound {σ : Type} (init : ProbComp σ)
+    (impl : QueryImpl []ₒ (StateT σ ProbComp)) : Prop :=
+  OracleVerifier.rbrKnowledgeSoundness
+    (verifier := ringSwitchPhaseVerifier car m bat pc)
+    (init := init) (impl := impl)
+    (relIn := phaseRelIn car m pc)
+    (relOut := phaseRelOut car m bat pc)
+    (rbrKnowledgeError := phaseRBRError car bat)
+
+/-! ## Round-by-round knowledge soundness (the S6 stretch goal) -/
+
+section RBRKnowledgeSoundness
+
+variable {σ : Type} (init : ProbComp σ) (impl : QueryImpl []ₒ (StateT σ ProbComp))
+
+/-- Auxiliary: an everywhere-false event has probability `0` under any `PMF`. -/
+private lemma pr_eq_zero_of_forall_not {α : Type} (D : PMF α) (P : α → Prop)
+    (h : ∀ x, ¬ P x) : Pr_{ let x ← D }[ P x ] = 0 := by
+  classical
+  rw [prob_tsum_form_singleton]
+  simp [h]
+
+/-- **The phase's knowledge state function.** Round 0 tracks `phaseRelIn` of the extracted
+witness (forced by `toFun_empty`); round 1 (after the slices `s`) tracks the verifier's
+Remark-5 check, the binding conjunct, and the slice relation for the intermediate packed
+witness; round 2 (the full transcript) tracks the check again (the verifier `failure`s
+without it, so no output can land in `phaseRelOut`), binding, and the batched sumcheck claim
+at the challenge's weights.
+
+`[IsDomain car.E]` enters only through `toFun_next` at the message round: the Remark-5
+read-back `openingClaimRel_of_claimConsistent` (the logged S6 deviation, see
+`Relations.lean`). -/
+noncomputable def phaseKnowledgeStateFunction [IsDomain car.E] :
+    (ringSwitchPhaseVerifier car m bat pc).KnowledgeStateFunction init impl
+      (phaseRelIn car m pc) (phaseRelOut car m bat pc)
+      (phaseRbrExtractor car m bat pc) where
+  toFun
+    | ⟨0, _⟩ => fun stmtIn _ witMid => (stmtIn, witMid) ∈ phaseRelIn car m pc
+    | ⟨1, _⟩ => fun stmtIn tr witMid =>
+        car.claimConsistent stmtIn.1.1 (tr 0)
+          ∧ pc.commitsTo stmtIn.2 witMid
+          ∧ ((tr 0 : car.ιE → car.P), witMid) ∈ car.sliceRel m stmtIn.1.2
+    | ⟨2, _⟩ => fun stmtIn tr witMid =>
+        car.claimConsistent stmtIn.1.1 (tr 0)
+          ∧ pc.commitsTo stmtIn.2 witMid
+          ∧ ((∑ u, bat.weight (tr 1) u * (tr 0 : car.ιE → car.P) u), witMid)
+              ∈ car.sumcheckClaimRel m stmtIn.1.2 (bat.weight (tr 1))
+  toFun_empty := fun stmtIn witMid => Iff.rfl
+  toFun_next
+    | ⟨0, _⟩ => fun _ stmtIn tr msg witMid h => by
+        obtain ⟨hc, hcommit, hslice⟩ := h
+        refine ⟨car.openingClaimRel_of_claimConsistent hc hslice, ?_⟩
+        change pc.commitsTo _ (car.packedMLE (car.unpack witMid))
+        rw [car.packedMLE_unpack]
+        exact hcommit
+    | ⟨1, _⟩ => fun hDir => absurd hDir (by simp)
+  toFun_full := fun stmtIn tr witOut h => by
+    classical
+    rw [gt_iff_lt, probEvent_pos_iff] at h
+    obtain ⟨x, hx, hRel⟩ := h
+    rw [OptionT.mem_support_iff] at hx
+    simp only [Verifier.run, OracleVerifier.toVerifier, ringSwitchPhaseVerifier,
+      OptionT.run_mk, support_bind, Set.mem_iUnion] at hx
+    obtain ⟨s0, _, hx⟩ := hx
+    simp only [simulateQ_optionT_bind] at hx
+    -- The verifier's slice read is deterministic: the simulated whole-message query *is*
+    -- (definitionally) the transcript's round-0 message.
+    have hq : (simulateQ
+          (OracleInterface.simOracle2 ([]ₒ : OracleSpec PEmpty.{1}) stmtIn.2
+            (FullTranscript.messages (pSpec := pSpecRingSwitchPhase car bat) tr))
+          (query (spec := [(pSpecRingSwitchPhase car bat).Message]ₒ) ⟨⟨0, rfl⟩, ()⟩
+            : OptionT (OracleComp (([]ₒ : OracleSpec PEmpty.{1})
+                + ([pc.OStmt]ₒ + [(pSpecRingSwitchPhase car bat).Message]ₒ))) _)
+          : OptionT (OracleComp ([]ₒ : OracleSpec PEmpty.{1})) _)
+        = (pure (some (tr (0 : Fin 2)))
+            : OracleComp ([]ₒ : OracleSpec PEmpty.{1}) (Option (car.ιE → car.P))) := rfl
+    rw [hq] at hx
+    -- Collapse the (definitional) pure-binds: the bound slice variable *is* `tr 0`, so the
+    -- verifier's check becomes a concrete `if` we can case on.
+    replace hx : some x ∈ _root_.support (StateT.run'
+        ((simulateQ impl (simulateQ
+            (OracleInterface.simOracle2 ([]ₒ : OracleSpec PEmpty.{1}) stmtIn.2
+              (FullTranscript.messages (pSpec := pSpecRingSwitchPhase car bat) tr))
+            (if car.claimConsistent stmtIn.1.1 (tr (0 : Fin 2))
+              then pure ((stmtIn.1.2, (tr (1 : Fin 2) : bat.Challenge)),
+                ∑ u, bat.weight (tr (1 : Fin 2) : bat.Challenge) u
+                  * (tr (0 : Fin 2) : car.ιE → car.P) u)
+              else failure
+              : OptionT (OracleComp (([]ₒ : OracleSpec PEmpty.{1})
+                  + ([pc.OStmt]ₒ + [(pSpecRingSwitchPhase car bat).Message]ₒ)))
+                  (((Fin m → car.E) × bat.Challenge) × car.P)))
+            : OptionT (StateT σ ProbComp) (((Fin m → car.E) × bat.Challenge) × car.P))
+          >>= (fun a => pure (a, fun i => stmtIn.2 i))
+            : OptionT (StateT σ ProbComp) ((((Fin m → car.E) × bat.Challenge) × car.P)
+                × ((i : pc.ιC) → pc.OStmt i)))
+        s0) := hx
+    by_cases hc : car.claimConsistent stmtIn.1.1 (tr (0 : Fin 2))
+    · -- Check passes: the run is (definitionally) `pure` of the batched output; `x` is pinned.
+      rw [if_pos hc] at hx
+      replace hx : some x ∈ _root_.support
+          ((pure (some (((stmtIn.1.2, (tr (1 : Fin 2) : bat.Challenge)),
+              ∑ u, bat.weight (tr (1 : Fin 2) : bat.Challenge) u
+                * (tr (0 : Fin 2) : car.ιE → car.P) u),
+            fun i => stmtIn.2 i)) : ProbComp _)) := hx
+      simp only [support_pure] at hx
+      obtain rfl := Option.some.inj hx
+      exact ⟨hc, hRel.2, hRel.1⟩
+    · -- Check fails: the run is (definitionally) `failure`, whose support has no `some`.
+      rw [if_neg hc] at hx
+      replace hx : some x ∈ _root_.support
+          ((pure none : ProbComp (Option ((((Fin m → car.E) × bat.Challenge) × car.P)
+              × ((i : pc.ιC) → pc.OStmt i))))) := hx
+      simp at hx
+
+/-- **The per-prefix challenge-round bound**: with the prefix (statement, commitment oracles,
+slices `s`) fixed, the round-1→2 bad event of the RBR game — some intermediate witness fails
+the round-1 state but satisfies the round-2 state after the challenge — has probability at
+most `bat.error` over a uniform batching challenge. `commitsTo_functional` collapses the
+`∃ witMid` to a single committed `t'₀`; the surviving case is exactly
+`BatchingStrategy.separates` on `s` vs the honest slices of `t'₀`
+(via `sumcheckClaim_of_slices`). -/
+private theorem phase_badEvent_le
+    (α : car.ιP → car.E) (r : Fin m → car.E) (oStmt : ∀ j, pc.OStmt j) (s : car.ιE → car.P) :
+    Pr_{ let c ←$ᵖ bat.Challenge }[
+      ∃ t' : MultilinearPoly car.P m,
+        ¬(car.claimConsistent α s ∧ pc.commitsTo oStmt t' ∧ (s, t') ∈ car.sliceRel m r)
+          ∧ (car.claimConsistent α s ∧ pc.commitsTo oStmt t'
+              ∧ ((∑ u, bat.weight c u * s u), t') ∈ car.sumcheckClaimRel m r (bat.weight c)) ]
+      ≤ (bat.error : ℝ≥0∞) := by
+  classical
+  by_cases hlive : ∃ t'₀, pc.commitsTo oStmt t'₀ ∧ car.claimConsistent α s
+      ∧ (s, t'₀) ∉ car.sliceRel m r
+  · -- The live case: a committed `t'₀` whose honest slices differ from `s`.
+    obtain ⟨t'₀, hcm, _, hsl⟩ := hlive
+    have hne : s ≠ car.honestSlices r t'₀ := fun hEq => hsl fun u => congrFun hEq u
+    refine le_trans (Pr_le_Pr_of_implies _ _ _ ?_)
+      (bat.separates s (car.honestSlices r t'₀) hne)
+    rintro c ⟨t', -, -, hcm', hsum⟩
+    obtain rfl : t' = t'₀ := pc.commitsTo_functional hcm' hcm
+    have hsum' : (∑ u, bat.weight c u * s u)
+        = ∑ y : Fin m → Fin 2, car.bridge (bat.weight c) (eqTilde r (car.boolToE y))
+            * t'.val.eval (y : Fin m → car.P) := hsum
+    have h2 : (∑ u, bat.weight c u * car.honestSlices r t' u)
+        = ∑ y : Fin m → Fin 2, car.bridge (bat.weight c) (eqTilde r (car.boolToE y))
+            * t'.val.eval (y : Fin m → car.P) :=
+      car.sumcheckClaim_of_slices (car.honestSlices_mem_sliceRel r t') (bat.weight c)
+    exact hsum'.trans h2.symm
+  · -- The empty case: every committed-and-checked `t'` already satisfies the round-1 state.
+    push Not at hlive
+    refine le_of_eq_of_le (pr_eq_zero_of_forall_not _ _ ?_) zero_le'
+    rintro c ⟨t', hnot1, hc, hcm, -⟩
+    exact hnot1 ⟨hc, hcm, hlive t' hcm hc⟩
+
+/-- **Round-by-round knowledge soundness of the ring-switch phase** (the S6 stretch goal):
+the phase reduction, against the anchored relations `phaseRelIn`/`phaseRelOut`, is
+round-by-round knowledge sound with error `bat.error` at the (single) batching-challenge
+round. Witnesses: `phaseWitMid`, `phaseRbrExtractor`, `phaseKnowledgeStateFunction`; the
+challenge round factors through `Verifier.probEvent_challengeRound_le` and lands on
+`phase_badEvent_le` — `commitsTo_functional` collapses the `∃ witMid`, and the surviving
+event is exactly `BatchingStrategy.separates` on the sent slices vs. the honest slices of
+the committed polynomial (via `sumcheckClaim_of_slices`).
+
+`[IsDomain car.E]` is the accepted S6 hypothesis (Remark-5 read-back, see `Relations.lean`);
+no `[Fintype car.P]`/`[IsDomain car.P]` is needed — the batching error is abstract and
+`bat.separates` is a strategy field. -/
+theorem ringSwitchPhase_rbrKnowledgeSound [IsDomain car.E] {σ : Type} (init : ProbComp σ)
+    (impl : QueryImpl []ₒ (StateT σ ProbComp)) :
+    ringSwitchPhaseRBRKnowledgeSound car m bat pc init impl := by
+  refine ⟨phaseWitMid car m, phaseRbrExtractor car m bat pc,
+    phaseKnowledgeStateFunction car m bat pc init impl, ?_⟩
+  intro stmtIn witIn prover i
+  rcases i with ⟨⟨_ | _ | iv, hlt⟩, hdir⟩
+  · -- Round 0 is P_to_V: not a challenge round.
+    exact nomatch hdir
+  · -- Round 1: the batching challenge. Factor the game through the fixed prefix, then
+    -- the per-prefix PMF bound `phase_badEvent_le` (everything else is definitional:
+    -- the `Fin.snoc` reads of the extended transcript reduce to the prefix reads).
+    letI : Fintype ((pSpecRingSwitchPhase car bat).Challenge ⟨⟨1, hlt⟩, hdir⟩) :=
+      inferInstanceAs (Fintype bat.Challenge)
+    letI : Nonempty ((pSpecRingSwitchPhase car bat).Challenge ⟨⟨1, hlt⟩, hdir⟩) :=
+      inferInstanceAs (Nonempty bat.Challenge)
+    refine Verifier.probEvent_rbrGame_le init impl stmtIn witIn prover _ ?_
+    intro tr log
+    exact phase_badEvent_le car m bat pc stmtIn.1.1 stmtIn.1.2 stmtIn.2 (tr (0 : Fin 1))
+  · -- No round ≥ 2 exists.
+    exact absurd hlt (by omega)
+
+end RBRKnowledgeSoundness
+
+/-! ## Sanity / testable deliverables (S6 §5.3) -/
+
+section Sanity
+
+-- INV-2: the phase reduction is statable on the *tower* carrier (arbitrary field extension,
+-- arbitrary finite rank), with any batching strategy and any commitment…
+example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L)
+    (m : ℕ) (bat : BatchingStrategy (towerCarrier β).P (towerCarrier β).ιE)
+    (pc : PackedCommitment (towerCarrier β).P m) :
+    OracleReduction (oSpec := []ₒ)
+      (StmtIn := ((towerCarrier β).ιP → (towerCarrier β).E) × (Fin m → (towerCarrier β).E))
+      (OStmtIn := pc.OStmt)
+      (WitIn := (towerCarrier β).ιP → MultilinearPoly K m)
+      (StmtOut := ((Fin m → (towerCarrier β).E) × bat.Challenge) × (towerCarrier β).P)
+      (OStmtOut := pc.OStmt)
+      (WitOut := MultilinearPoly (towerCarrier β).P m)
+      (pSpec := pSpecRingSwitchPhase (towerCarrier β) bat) :=
+  ringSwitchPhase (towerCarrier β) m bat pc
+
+-- …and on the *decoupled field* carrier (`P = 𝔽₄ ≠ E = 𝔽₈`), the γ-power strategy landed at
+-- `ιE` by reindexing (the exact S6 plumbing promised at S3), the trivial commitment.
+example :
+    letI : IsDomain decoupledFieldCarrier.P := inferInstanceAs (IsDomain (GaloisField 2 2))
+    letI : Fintype decoupledFieldCarrier.P :=
+      letI : Finite decoupledFieldCarrier.P := inferInstanceAs (Finite (GaloisField 2 2))
+      Fintype.ofFinite _
+    OracleReduction (oSpec := []ₒ)
+      (StmtIn := (decoupledFieldCarrier.ιP → decoupledFieldCarrier.E)
+        × (Fin 3 → decoupledFieldCarrier.E))
+      (OStmtIn := (PackedCommitment.trivial decoupledFieldCarrier.P 3).OStmt)
+      (WitIn := decoupledFieldCarrier.ιP → MultilinearPoly (ZMod 2) 3)
+      (StmtOut := ((Fin 3 → decoupledFieldCarrier.E)
+        × ((BatchingStrategy.gammaPowers decoupledFieldCarrier.P
+            (Fintype.card decoupledFieldCarrier.ιE)).reindex
+            (Fintype.equivFin decoupledFieldCarrier.ιE)).Challenge) × decoupledFieldCarrier.P)
+      (OStmtOut := (PackedCommitment.trivial decoupledFieldCarrier.P 3).OStmt)
+      (WitOut := MultilinearPoly decoupledFieldCarrier.P 3)
+      (pSpec := pSpecRingSwitchPhase decoupledFieldCarrier
+        ((BatchingStrategy.gammaPowers decoupledFieldCarrier.P
+            (Fintype.card decoupledFieldCarrier.ιE)).reindex
+            (Fintype.equivFin decoupledFieldCarrier.ιE))) :=
+  letI : IsDomain decoupledFieldCarrier.P := inferInstanceAs (IsDomain (GaloisField 2 2))
+  letI : Fintype decoupledFieldCarrier.P :=
+    letI : Finite decoupledFieldCarrier.P := inferInstanceAs (Finite (GaloisField 2 2))
+    Fintype.ofFinite _
+  ringSwitchPhase decoupledFieldCarrier 3 _ (PackedCommitment.trivial _ 3)
+
+-- Close-review pins (2026-07-12): `phaseRelIn` is NONEMPTY — true claims + the trivial
+-- commitment on honest data — so the RBR theorem's obligation is not discharged by an empty
+-- input relation…
+example (r : Fin 3 → decoupledToyCarrier.E)
+    (Ps : decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3) :
+    ((((fun i => MvPolynomial.aeval r (Ps i).val), r),
+        fun _ : (PackedCommitment.trivial decoupledToyCarrier.P 3).ιC =>
+          decoupledToyCarrier.packedMLE Ps), Ps)
+      ∈ phaseRelIn decoupledToyCarrier 3 (PackedCommitment.trivial _ 3) :=
+  ⟨fun _ => rfl, rfl⟩
+
+-- …and the RBR theorem itself applies end-to-end at a concrete carrier + PROVEN strategy
+-- (γ-powers on 𝔽₄, separation error 3/4 — a real, nonzero, non-unit error).
+example {σ : Type} (init : ProbComp σ) (impl : QueryImpl []ₒ (StateT σ ProbComp)) :
+    letI : IsDomain decoupledFieldCarrier.P := inferInstanceAs (IsDomain (GaloisField 2 2))
+    letI : Fintype decoupledFieldCarrier.P :=
+      letI : Finite decoupledFieldCarrier.P := inferInstanceAs (Finite (GaloisField 2 2))
+      Fintype.ofFinite _
+    ringSwitchPhaseRBRKnowledgeSound decoupledFieldCarrier 3
+      ((BatchingStrategy.gammaPowers decoupledFieldCarrier.P
+          (Fintype.card decoupledFieldCarrier.ιE)).reindex
+          (Fintype.equivFin decoupledFieldCarrier.ιE))
+      (PackedCommitment.trivial _ 3) init impl :=
+  letI : IsDomain decoupledFieldCarrier.P := inferInstanceAs (IsDomain (GaloisField 2 2))
+  letI : Fintype decoupledFieldCarrier.P :=
+    letI : Finite decoupledFieldCarrier.P := inferInstanceAs (Finite (GaloisField 2 2))
+    Fintype.ofFinite _
+  letI : IsDomain decoupledFieldCarrier.E := inferInstanceAs (IsDomain (GaloisField 2 3))
+  ringSwitchPhase_rbrKnowledgeSound decoupledFieldCarrier 3 _ _ init impl
+
+-- INV-5 pin: the phase error vector is *definitionally* the strategy's separation error at
+-- the challenge round (and 0 elsewhere — there is no other challenge round).
+example (i : (pSpecRingSwitchPhase car bat).ChallengeIdx) (h : i.1 = 1) :
+    phaseRBRError car bat i = bat.error := by
+  rcases i with ⟨i, hi⟩
+  subst h
+  rfl
+
+end Sanity
+
+end RingSwitching.Generic
+
+end
diff --git a/ArkLib/ProofSystem/RingSwitching/Generic/Relations.lean b/ArkLib/ProofSystem/RingSwitching/Generic/Relations.lean
new file mode 100644
index 0000000000..de0b8be2e1
--- /dev/null
+++ b/ArkLib/ProofSystem/RingSwitching/Generic/Relations.lean
@@ -0,0 +1,450 @@
+/-
+Copyright (c) 2026 ArkLib Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Hicks
+-/
+
+import ArkLib.ProofSystem.RingSwitching.Generic.Batching
+import ArkLib.ProofSystem.RingSwitching.Generic.Packing
+import ArkLib.ProofSystem.RingSwitching.Generic.Recombine
+
+/-!
+# Generic Ring-Switching — Anchored Relations + PCS Interface (S5)
+
+Design safety pillars 2 + 4 (see `docs/kb/concepts/ring-switching.md`, "The Generic layer"):
+the **framework-fixed relation chain** and the **PCS binding interface**.
+
+## The relation chain (pillar 4: no free `Prop` anywhere)
+
+Every relation of the generic ring switch is a *framework definition* parameterized only by the
+carrier and the protocol data — an instance has no hook to substitute a weaker predicate:
+
+* `openingClaimRel` — the input anchor (design step 2): `∀ i, αᵢ = P̂ᵢ(r)`, the family's
+  evaluation claims at the common point `r` over the opening algebra `E`. This is the semantic
+  statement the end-to-end soundness theorem (S6) is *about*; fixing it here is what makes
+  "satisfying the interface" mean "getting the right theorem".
+* `sliceRel` — the middle relation after eq-decomposition/recombination (design step 4): the
+  prover-sent slices are the eq-weighted hypercube sums of the packed polynomial,
+  `sᵤ = ∑_y A(y,u) • t'(y)`.
+* `sumcheckClaimRel` — the batched sumcheck input claim (design steps 5–6):
+  `σ = ∑_y Φ_w(eq(r,y)) · t'(y)`, i.e. `∑_y B(y)·t'(y) = σ` with `B = Φ∘eq` the multiplier
+  (`Bmult`'s defining values). `sumcheckClaim_of_slices` proves the chain coheres: batching
+  honest slices with weights `w` *is* the sumcheck claim — via the linchpin `bridge_eqTilde`.
+* `claimConsistent` — the **Remark-5 consistency check** ([BRW26] Remark 5; S6 design review F1):
+  the phase verifier's read-back of the slices against the input claims,
+  `αᵢ = ∑ᵤ (packBasis.repr sᵤ i) • bᵤ^E` — both bases at once. Completeness
+  (`claimConsistent_of_slices`, review F6-4) and the soundness read-back to the anchor
+  (`openingClaimRel_of_claimConsistent`, review F2, via the generic `unpack`) are proven below;
+  both route through `aeval_unpack_of_slices`, whose `[IsDomain car.E]` hypothesis is the one
+  logged S6 deviation (eq-expansion of the anchor by root-counting interpolation over `E`).
+
+## The PCS interface (pillar 2: binding is the PCS's proven semantics, not a free hook)
+
+`PackedCommitment` carries `commitsTo : (∀ j, OStmt j) → MultilinearPoly P m → Prop` **plus the
+functionality law** `commitsTo_functional` (an oracle statement commits to at most one
+polynomial). Functionality is what makes the field *not* a free hook, in two enforced senses:
+
+1. `fun _ _ => True` is *unstatable* as a `commitsTo` (`commitsTo_ne_top`, backed by the `neC`
+   well-formedness guard): functionality would collapse all multilinears into one, contradicting
+   `Nontrivial P`. Compare the legacy `AbstractOStmtIn.initialCompatibility`, which type-admits
+   `True` (design Hole A).
+2. It is exactly what the S6 round-by-round argument needs to collapse the `∃ witMid` event of
+   `rbrKnowledgeSoundness` to the fixed pair fed to `BatchingStrategy.separates` — without it a
+   `|WitMid|` union factor would destroy the batching error bound. (At S5 the law is carried;
+   its in-file consumer is `commitsTo_not_top`/`commitsTo_ne_top`, its main consumer is S6.)
+
+`DenseMLPCS` then mirrors the legacy `MLIOPCS` bundle (protocol + perfect completeness + RBR
+knowledge soundness) with its input relation *fixed* to `PackedCommitment.evalRel` — evaluation
+correctness (`MLPEvalRelation`, reused) **and** `commitsTo` — so the PCS's own security fields
+are stated against the instance's binding predicate: the round-0 knowledge state function must
+track `commitsTo` *bidirectionally* (`KnowledgeStateFunction.toFun_empty` is an iff), and
+completeness must cover every `commitsTo`-satisfying input. Functionality bars the trivial hook;
+a bogus-but-functional predicate survives locally but is caught at S6 composition, where the
+ring switch's completeness needs honest provers to *satisfy* `evalRel`.
+
+**INV-3 audit note.** `commitsTo` is the *sanctioned* hook-shaped `Prop`-valued field of the
+generic layer (well-formedness guards like `neC` are `Prop`-valued too, but are positive
+obligations, not hooks):
+it is law-constrained (`commitsTo_functional`) and consumed by the structure's own security
+fields, unlike the legacy free `initialCompatibility` hook it replaces (retirement of the legacy
+hook is the S7 Binius-migration step; the Binius codeword-consistency predicate is re-expressed
+in `commitsTo` orientation as `Binius.FRIBinius.biniusCommitsTo`, whose functionality proof —
+by unique decoding, over the `witnessNovelCoeffs` cube-table encoding fixed at the S5
+close-review — is the logged S7 obligation).
+
+## References
+
+- [DP24] Diamond, Benjamin E., and Jim Posen. "Polylogarithmic Proofs for Multilinears over
+  Binary Towers." Cryptology ePrint Archive (2024).
+- [BRW26] Bünz, Rothblum, Wang. "Flock: Fast Proving for Batch Boolean Computations." Cryptology
+  ePrint Archive, Report 2026/1329. Appendix B.
+- [RSG] "Ring switching, generalized." Note, leanEthereum/leanVM-b repository.
+-/
+
+noncomputable section
+
+namespace RingSwitching.Generic
+
+open OracleSpec OracleComp ProtocolSpec Module MvPolynomial Sumcheck.Structured
+open scoped NNReal
+
+/-! ## The framework-fixed relation chain (safety pillar 4) -/
+
+namespace RingSwitchCarrier
+
+variable {B : Type} [CommRing B] (car : RingSwitchCarrier B)
+
+/-- **The input anchor** (design step 2, the semantic core of the S6 `relIn`): the batch of
+evaluation claims `∀ i, αᵢ = P̂ᵢ(r)` — each `B`-multilinear of the family evaluates at the
+common point `r` over the opening algebra `E` to its claimed value. Statement =
+(claims, point); witness = the family. The oracle-reduction `relIn` assembled at S6 extends
+this with the input-oracle component and the `commitsTo` binding conjunct; the anchor itself is
+framework-fixed — an instance cannot override or weaken it (safety pillar 4) — and
+`Nontrivial E` (a carrier field) keeps it non-vacuous (see the non-vacuity `example` below). -/
+def openingClaimRel (m : ℕ) :
+    Set (((car.ιP → car.E) × (Fin m → car.E)) × (car.ιP → MultilinearPoly B m)) :=
+  { x | ∀ i, x.1.1 i = MvPolynomial.aeval x.1.2 (x.2 i).val }
+
+/-- **The slice relation** (design step 4, middle): the prover-sent slices `s : ιE → P` are the
+eq-weighted hypercube sums of the packed polynomial, `sᵤ = ∑_y A(y,u) • t'(y)` with
+`A(y,u) = eqCoord r y u` the (unique — `openingDecomposition_injective`) `B`-coordinates of
+`eq(r,y)` in the opening basis. -/
+def sliceRel (m : ℕ) (r : Fin m → car.E) :
+    Set ((car.ιE → car.P) × MultilinearPoly car.P m) :=
+  { x | ∀ u, x.1 u =
+      ∑ y : Fin m → Fin 2, car.eqCoord r y u • x.2.val.eval (y : Fin m → car.P) }
+
+/-- **The batched sumcheck claim** (design steps 5–6, middle): the single claim handed to the
+sumcheck, `σ = ∑_y Φ_w(eq(r,y)) · t'(y)` — the hypercube sum of the multiplier `B(y) = Φ(eq(r,y))`
+(the values defining `Bmult`) against the packed polynomial. -/
+def sumcheckClaimRel (m : ℕ) (r : Fin m → car.E) (w : car.ιE → car.P) :
+    Set (car.P × MultilinearPoly car.P m) :=
+  { x | x.1 = ∑ y : Fin m → Fin 2,
+      car.bridge w (eqTilde r (car.boolToE y)) * x.2.val.eval (y : Fin m → car.P) }
+
+/-- **Chain coherence** (the middle relations compose): batching honest slices with weights `w`
+*is* the sumcheck input claim. This is the `bridge_eqTilde` linchpin doing its designed job —
+`∑_u wᵤ·sᵤ = ∑_y Φ_w(eq(r,y))·t'(y)` by expanding each slice and reassembling the
+eq-coordinates through `Φ`. -/
+theorem sumcheckClaim_of_slices {m : ℕ} {r : Fin m → car.E}
+    {s : car.ιE → car.P} {t' : MultilinearPoly car.P m}
+    (hs : (s, t') ∈ car.sliceRel m r) (w : car.ιE → car.P) :
+    (∑ u, w u * s u, t') ∈ car.sumcheckClaimRel m r w := by
+  change _ = _
+  calc ∑ u, w u * s u
+      = ∑ u, ∑ y : Fin m → Fin 2,
+          car.eqCoord r y u • (w u * t'.val.eval (y : Fin m → car.P)) := by
+        refine Finset.sum_congr rfl fun u _ => ?_
+        have hsu : s u
+            = ∑ y : Fin m → Fin 2, car.eqCoord r y u • t'.val.eval (y : Fin m → car.P) := hs u
+        rw [hsu, Finset.mul_sum]
+        exact Finset.sum_congr rfl fun y _ => mul_smul_comm _ _ _
+    _ = ∑ y : Fin m → Fin 2,
+          (∑ u, car.eqCoord r y u • w u) * t'.val.eval (y : Fin m → car.P) := by
+        rw [Finset.sum_comm]
+        refine Finset.sum_congr rfl fun y _ => ?_
+        rw [Finset.sum_mul]
+        exact Finset.sum_congr rfl fun u _ => (smul_mul_assoc _ _ _).symm
+    _ = ∑ y : Fin m → Fin 2,
+          car.bridge w (eqTilde r (car.boolToE y)) * t'.val.eval (y : Fin m → car.P) := by
+        refine Finset.sum_congr rfl fun y _ => ?_
+        rw [car.bridge_eqTilde]
+
+/-! ### The Remark-5 consistency check (S6 design review F1/F2/F6-4) -/
+
+/-- **The Remark-5 claim-consistency check** ([BRW26] Remark 5; design review F1): the phase
+verifier's check of the prover-sent slices against the input claims — each claim `αᵢ` must be the
+opening-basis recombination of the `i`-th packing-basis coordinates of the slices,
+`αᵢ = ∑ᵤ (packBasis.repr sᵤ i) • bᵤ^E`. This uses **both** bases, which is exactly why it is
+sound: `recombine_injective` (packing side) and `openingDecomposition_injective` (opening side)
+pin both decompositions. `claimConsistent_of_slices` is the completeness direction (honest slices
+pass), `openingClaimRel_of_claimConsistent` the soundness read-back to the anchor. -/
+def claimConsistent (α : car.ιP → car.E) (s : car.ιE → car.P) : Prop :=
+  ∀ i, α i = ∑ u, car.packBasis.repr (s u) i • car.openBasis u
+
+/-- **The slice read-back identity** (the shared core of both directions of the Remark-5 check):
+for honest slices of a packed `t'`, the recombination the check compares `αᵢ` against *is* the
+`i`-th unpacked component's evaluation at `r`:
+`∑ᵤ (packBasis.repr sᵤ i) • bᵤ^E = (unpack t')ᵢ(r)`. The proof expands the anchor evaluation over
+the hypercube (`aeval_multilinear_eq_sum_eqTilde`), reads each hypercube evaluation back through
+`unpack_eval_zeroOne`, and reassembles the eq-coordinates via `Basis.sum_repr` — Flock's "by the
+uniqueness of the 𝔽₂-decomposition" step, in equational form.
+
+**Hypothesis note (the logged S6 deviation):** `[IsDomain car.E]` is an accepted theorem
+hypothesis — the eq-expansion of the anchor interpolates the mapped multilinear over `E` by root
+counting. Both live carriers (`towerCarrier`: `E = L` a field; `decoupledFieldCarrier`:
+`E = 𝔽₈`) satisfy it; generalizing to plain `CommRing E` is future work. -/
+theorem aeval_unpack_of_slices [IsDomain car.E] {m : ℕ} {r : Fin m → car.E}
+    {s : car.ιE → car.P} {t' : MultilinearPoly car.P m}
+    (hs : (s, t') ∈ car.sliceRel m r) (i : car.ιP) :
+    MvPolynomial.aeval r (car.unpack t' i).val
+      = ∑ u, car.packBasis.repr (s u) i • car.openBasis u := by
+  calc MvPolynomial.aeval r (car.unpack t' i).val
+      = ∑ y : Fin m → Fin 2, eqTilde (y : Fin m → car.E) r
+          * algebraMap B car.E ((car.unpack t' i).val.eval (y : Fin m → B)) :=
+        aeval_multilinear_eq_sum_eqTilde (car.unpack t' i).property r
+    _ = ∑ y : Fin m → Fin 2, ∑ u, (car.eqCoord r y u
+          * car.packBasis.repr (t'.val.eval (y : Fin m → car.P)) i) • car.openBasis u := by
+        refine Finset.sum_congr rfl fun y _ => ?_
+        rw [car.unpack_eval_zeroOne]
+        have hb : car.boolToE y = (y : Fin m → car.E) := (coe_boolFun_eq_ite y).symm
+        have h1 : eqTilde (y : Fin m → car.E) r = eqTilde r (car.boolToE y) := by
+          rw [hb]; exact eqPolynomial_symm _ _
+        rw [h1, ← car.openBasis.sum_repr (eqTilde r (car.boolToE y)), Finset.sum_mul]
+        refine Finset.sum_congr rfl fun u _ => ?_
+        rw [smul_mul_assoc, ← Algebra.commutes, ← Algebra.smul_def, smul_smul]
+        rfl
+    _ = ∑ u, car.packBasis.repr (∑ y : Fin m → Fin 2,
+          car.eqCoord r y u • t'.val.eval (y : Fin m → car.P)) i • car.openBasis u := by
+        rw [Finset.sum_comm]
+        refine Finset.sum_congr rfl fun u _ => ?_
+        rw [← Finset.sum_smul]
+        congr 1
+        rw [map_sum, Finsupp.finsetSum_apply]
+        refine Finset.sum_congr rfl fun y _ => ?_
+        rw [map_smul, Finsupp.smul_apply, smul_eq_mul]
+    _ = ∑ u, car.packBasis.repr (s u) i • car.openBasis u := by
+        refine Finset.sum_congr rfl fun u _ => ?_
+        rw [← hs u]
+
+/-- **Remark-5 check completeness** (design review F6-4): honest slices of the packed family pass
+the consistency check against the honest claims — any `α` satisfying the input anchor for the
+family. `[IsDomain car.E]` is inherited from the shared core `aeval_unpack_of_slices` (the logged
+S6 deviation; see there). -/
+theorem claimConsistent_of_slices [IsDomain car.E] {m : ℕ} {r : Fin m → car.E}
+    {α : car.ιP → car.E} {Ps : car.ιP → MultilinearPoly B m} {s : car.ιE → car.P}
+    (hα : ((α, r), Ps) ∈ car.openingClaimRel m)
+    (hs : (s, car.packedMLE Ps) ∈ car.sliceRel m r) :
+    car.claimConsistent α s := fun i => by
+  have h := car.aeval_unpack_of_slices hs i
+  rw [car.unpack_packedMLE] at h
+  exact (hα i).trans h
+
+/-- **Remark-5 read-back, soundness direction** (design review F2): if the claims pass the
+consistency check against slices that are honest for some packed `t'`, then the input anchor
+`openingClaimRel` holds for the claims against the *unpacked* family — the witness the S6
+extractor returns. `[IsDomain car.E]` is inherited from the shared core `aeval_unpack_of_slices`
+(the logged S6 deviation; see there). -/
+theorem openingClaimRel_of_claimConsistent [IsDomain car.E] {m : ℕ} {r : Fin m → car.E}
+    {α : car.ιP → car.E} {s : car.ιE → car.P} {t' : MultilinearPoly car.P m}
+    (hc : car.claimConsistent α s) (hs : (s, t') ∈ car.sliceRel m r) :
+    ((α, r), car.unpack t') ∈ car.openingClaimRel m :=
+  fun i => (hc i).trans (car.aeval_unpack_of_slices hs i).symm
+
+end RingSwitchCarrier
+
+/-! ## The PCS binding interface (safety pillar 2) -/
+
+/-- **The commitment half of a dense multilinear PCS over `P`**: oracle-statement types (the
+commitment as the verifier sees it) together with the binding predicate `commitsTo` and its
+**functionality law** — an oracle statement commits to *at most one* multilinear. Functionality
+is the enforcement making `commitsTo` a genuine binding semantics rather than a free hook
+(`commitsTo_not_top`), and it is exactly what the S6 round-by-round extraction needs to collapse
+the `∃ witMid` event to the fixed claim pair fed to `BatchingStrategy.separates`. -/
+structure PackedCommitment (P : Type) [CommRing P] (m : ℕ) where
+  /-- Index set of the commitment's oracle statements. -/
+  ιC : Type
+  /-- The oracle-statement types (the commitment, as oracles the verifier may query). -/
+  OStmt : ιC → Type
+  /-- Oracle interfaces for the commitment oracles. -/
+  Oᵢ : ∀ i, OracleInterface (OStmt i)
+  -- Well-formedness: a commitment value exists. Same design move as the carrier's `Nontrivial`
+  -- guards: without it, an *empty* oracle-statement type is a bona-fide instance on which
+  -- `commitsTo := fun _ _ => True` is statable (functionality vacuous) and `evalRel = ∅` —
+  -- a vacuous, self-punishing corner, but one that would falsify the "`True` is unstatable"
+  -- guarantee (`commitsTo_ne_top`). Real commitment types are inhabited.
+  [neC : Nonempty (∀ j, OStmt j)]
+  /-- The binding predicate: the oracle statement commits to this multilinear. -/
+  commitsTo : (∀ j, OStmt j) → MultilinearPoly P m → Prop
+  /-- **Functionality**: an oracle statement commits to at most one multilinear. -/
+  commitsTo_functional : ∀ {c : ∀ j, OStmt j} {p p' : MultilinearPoly P m},
+    commitsTo c p → commitsTo c p' → p = p'
+
+namespace PackedCommitment
+
+variable {P : Type} [CommRing P] {m : ℕ}
+
+/-- The trivial (identity) commitment: the oracle *is* the multilinear. The degenerate but
+honest member of the interface — binding holds definitionally. Used as the statability witness;
+real PCSs (FRI-Binius etc.) supply nontrivial oracles at S7. -/
+def trivial (P : Type) [CommRing P] (m : ℕ) : PackedCommitment P m where
+  ιC := Unit
+  OStmt := fun _ => MultilinearPoly P m
+  Oᵢ := fun _ => OracleInterface.instDefault
+  commitsTo := fun c p => c () = p
+  commitsTo_functional := fun h h' => h.symm.trans h'
+
+/-- **`commitsTo` cannot be the free hook `fun _ _ => True`** (design Hole A is closed, not just
+discouraged): functionality forces distinct multilinears — e.g. the constant-`0` and constant-`1`
+MLEs, distinct since `P` is nontrivial — to be uncommitted-to simultaneously. Compare the legacy
+`AbstractOStmtIn.initialCompatibility`, which type-admits `True`. -/
+theorem commitsTo_not_top [Nontrivial P] (pc : PackedCommitment P m) (c : ∀ j, pc.OStmt j) :
+    ¬ ∀ p : MultilinearPoly P m, pc.commitsTo c p := by
+  intro h
+  have h01 : (⟨MLE fun _ => 0, MLE_mem_restrictDegree _⟩ : MultilinearPoly P m)
+      = ⟨MLE fun _ => 1, MLE_mem_restrictDegree _⟩ :=
+    pc.commitsTo_functional (h _) (h _)
+  have hval := congrArg
+    (fun p : MultilinearPoly P m =>
+      p.val.eval (((fun _ => 0) : Fin m → Fin 2) : Fin m → P)) h01
+  simp only [MLE_eval_zeroOne] at hval
+  exact zero_ne_one hval
+
+/-- Function-level form of the enforcement: `commitsTo` **is not** the legacy free hook
+`fun _ _ => True` — for any well-formed `PackedCommitment` (the `neC` guard supplies the
+commitment value the pointwise theorem needs). This is *syntactic* inequality against the
+literal hook; the semantic guarantee (no commitment accepts every polynomial) is
+`commitsTo_not_top`, which `neC` keeps non-vacuous. -/
+theorem commitsTo_ne_top [Nontrivial P] (pc : PackedCommitment P m) :
+    pc.commitsTo ≠ fun _ _ => True := fun h =>
+  pc.commitsTo_not_top (Classical.choice pc.neC) (fun p => by rw [h]; trivial)
+
+/-- **The PCS's own anchored input relation** (what its completeness and knowledge soundness are
+stated against): evaluation correctness — the legacy `MLPEvalRelation`, reused verbatim — *and*
+the binding predicate `commitsTo`. This is the pillar-2 replacement of the legacy
+`AbstractOStmtIn.toRelInput` (whose second conjunct is the free `initialCompatibility`). -/
+def evalRel (pc : PackedCommitment P m) :
+    Set (((MLPEvalStatement P m) × (∀ j, pc.OStmt j)) × (WitMLP P m)) :=
+  { input | MLPEvalRelation P m pc.ιC pc.OStmt input ∧ pc.commitsTo input.1.2 input.2.t }
+
+end PackedCommitment
+
+/-- **A dense multilinear PCS over `P`** (design §6 irreducible obligation 2 — the one honest
+trust boundary): a `PackedCommitment` together with an evaluation oracle reduction and its
+security properties, *stated against the fixed anchored relation* `evalRel` — so `commitsTo`
+is consumed by the structure's own completeness and knowledge-soundness fields (safety
+pillar 2). Mirrors the legacy `MLIOPCS` bundle shape (kept intact for the S7 migration), with
+`evalRel` replacing the free-hook relation `toRelInput`. -/
+structure DenseMLPCS (P : Type) [CommRing P] (m : ℕ) extends PackedCommitment P m where
+  /-- Number of interaction rounds of the evaluation protocol. -/
+  numRounds : ℕ
+  /-- Protocol specification of the evaluation protocol. -/
+  pSpec : ProtocolSpec numRounds
+  /-- Oracle interfaces for the protocol messages. -/
+  Oₘ : ∀ j, OracleInterface (pSpec.Message j)
+  /-- Sampleability of the verifier challenges. -/
+  O_challenges : ∀ i : pSpec.ChallengeIdx, SampleableType (pSpec.Challenge i)
+  /-- The evaluation protocol, as an oracle reduction from the anchored evaluation claim to
+  accept/reject. -/
+  oracleReduction : OracleReduction (oSpec := []ₒ)
+    (StmtIn := MLPEvalStatement P m) (OStmtIn := OStmt)
+    (StmtOut := Bool) (OStmtOut := fun _ : Empty => Unit)
+    (WitIn := WitMLP P m) (WitOut := Unit)
+    (pSpec := pSpec)
+  /-- Perfect completeness w.r.t. the **fixed** anchored relation `evalRel`. -/
+  perfectCompleteness : ∀ {σ : Type} {init : ProbComp σ}
+    {impl : QueryImpl []ₒ (StateT σ ProbComp)},
+    OracleReduction.perfectCompleteness (oSpec := []ₒ)
+      (StmtIn := MLPEvalStatement P m) (OStmtIn := OStmt)
+      (StmtOut := Bool) (OStmtOut := fun _ : Empty => Unit)
+      (WitIn := WitMLP P m) (WitOut := Unit) (pSpec := pSpec) (init := init) (impl := impl)
+      (relIn := toPackedCommitment.evalRel)
+      (relOut := acceptRejectOracleRel)
+      (oracleReduction := oracleReduction)
+  /-- Round-by-round knowledge error of the evaluation protocol. -/
+  rbrKnowledgeError : pSpec.ChallengeIdx → ℝ≥0
+  /-- RBR knowledge soundness w.r.t. the **fixed** anchored relation `evalRel` — the extractor
+  is obligated to produce a witness satisfying `commitsTo` (this is what makes the binding
+  predicate load-bearing rather than decorative). -/
+  rbrKnowledgeSoundness : ∀ {σ : Type} {init : ProbComp σ}
+    {impl : QueryImpl []ₒ (StateT σ ProbComp)},
+    OracleVerifier.rbrKnowledgeSoundness
+      (verifier := oracleReduction.verifier)
+      (init := init) (impl := impl)
+      (relIn := toPackedCommitment.evalRel)
+      (relOut := acceptRejectOracleRel)
+      (rbrKnowledgeError := rbrKnowledgeError)
+
+/-! ## Sanity / testable deliverables (S5 §5.3) -/
+
+section Sanity
+
+-- **Non-vacuity witness** (the `Nontrivial E` guard doing its designed job): the all-`1` claims
+-- on the all-`0` family are NOT in the anchor relation — `openingClaimRel` is not `univ`, so
+-- proving membership carries real semantic content.
+example (r : Fin 3 → decoupledToyCarrier.E) :
+    ((fun _ => 1, r), fun _ => 0) ∉ decoupledToyCarrier.openingClaimRel 3 := by
+  intro h
+  have h0 := h ((0 : Fin 2) : decoupledToyCarrier.ιP)
+  simp only [ZeroMemClass.coe_zero, map_zero] at h0
+  exact one_ne_zero h0
+
+-- INV-2: the whole relation chain typechecks on the *decoupled* `P ≠ E` carrier…
+example (r : Fin 3 → decoupledToyCarrier.E) (w : decoupledToyCarrier.ιE → decoupledToyCarrier.P) :
+    (Set (((decoupledToyCarrier.ιP → decoupledToyCarrier.E) × (Fin 3 → decoupledToyCarrier.E))
+        × (decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3)))
+      × Set ((decoupledToyCarrier.ιE → decoupledToyCarrier.P)
+        × MultilinearPoly decoupledToyCarrier.P 3)
+      × Set (decoupledToyCarrier.P × MultilinearPoly decoupledToyCarrier.P 3) :=
+  ⟨decoupledToyCarrier.openingClaimRel 3,
+   decoupledToyCarrier.sliceRel 3 r,
+   decoupledToyCarrier.sumcheckClaimRel 3 r w⟩
+
+-- …and on the *tower* carrier (arbitrary field extension, arbitrary rank).
+example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L)
+    (m : ℕ) (r : Fin m → (towerCarrier β).E) (w : (towerCarrier β).ιE → (towerCarrier β).P) :
+    (Set ((((towerCarrier β).ιP → (towerCarrier β).E) × (Fin m → (towerCarrier β).E))
+        × ((towerCarrier β).ιP → MultilinearPoly K m)))
+      × Set (((towerCarrier β).ιE → (towerCarrier β).P)
+        × MultilinearPoly (towerCarrier β).P m)
+      × Set ((towerCarrier β).P × MultilinearPoly (towerCarrier β).P m) :=
+  ⟨(towerCarrier β).openingClaimRel m,
+   (towerCarrier β).sliceRel m r,
+   (towerCarrier β).sumcheckClaimRel m r w⟩
+
+-- INV-2: the PCS interface instantiates at both carriers' packing algebras (the trivial
+-- commitment; real PCSs land at S7).
+example : PackedCommitment decoupledToyCarrier.P 3 := .trivial _ 3
+
+example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L) :
+    PackedCommitment (towerCarrier β).P 3 := .trivial _ 3
+
+-- The full PCS bundle is statable at any commutative ring (the S8 Hachi shape included) —
+-- like `BatchingStrategy`, the vocabulary is `CommRing`-only; hypotheses live on theorems.
+example : Type 1 := DenseMLPCS (ZMod 6) 3
+
+-- INV-2: the Remark-5 check (`claimConsistent`) is *statable* with no domain hypothesis, on the
+-- decoupled toy carrier (a non-domain product ring)…
+example (α : decoupledToyCarrier.ιP → decoupledToyCarrier.E)
+    (s : decoupledToyCarrier.ιE → decoupledToyCarrier.P) : Prop :=
+  decoupledToyCarrier.claimConsistent α s
+
+-- …and both of its directions instantiate on the *tower* carrier (`[IsDomain E]` from the field
+-- structure; the projection is opaque to instance search, so it is landed by `letI`)…
+example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L)
+    {m : ℕ} {r : Fin m → (towerCarrier β).E} {α : (towerCarrier β).ιP → (towerCarrier β).E}
+    {s : (towerCarrier β).ιE → (towerCarrier β).P} {t' : MultilinearPoly (towerCarrier β).P m}
+    (hc : (towerCarrier β).claimConsistent α s)
+    (hs : (s, t') ∈ (towerCarrier β).sliceRel m r) :
+    ((α, r), (towerCarrier β).unpack t') ∈ (towerCarrier β).openingClaimRel m :=
+  letI : IsDomain (towerCarrier β).E := inferInstanceAs (IsDomain L)
+  (towerCarrier β).openingClaimRel_of_claimConsistent hc hs
+
+-- …and on the *decoupled field* carrier `P = 𝔽₄ ≠ E = 𝔽₈` (the R5 anti-overfit witness for the
+-- `[IsDomain E]`-gated soundness layer): completeness — honest slices pass the check.
+example {m : ℕ} {r : Fin m → decoupledFieldCarrier.E}
+    {α : decoupledFieldCarrier.ιP → decoupledFieldCarrier.E}
+    {Ps : decoupledFieldCarrier.ιP → MultilinearPoly (ZMod 2) m}
+    {s : decoupledFieldCarrier.ιE → decoupledFieldCarrier.P}
+    (hα : ((α, r), Ps) ∈ decoupledFieldCarrier.openingClaimRel m)
+    (hs : (s, decoupledFieldCarrier.packedMLE Ps) ∈ decoupledFieldCarrier.sliceRel m r) :
+    decoupledFieldCarrier.claimConsistent α s :=
+  letI : IsDomain decoupledFieldCarrier.E := inferInstanceAs (IsDomain (GaloisField 2 3))
+  decoupledFieldCarrier.claimConsistent_of_slices hα hs
+
+-- …and the soundness read-back on the decoupled field carrier too.
+example {m : ℕ} {r : Fin m → decoupledFieldCarrier.E}
+    {α : decoupledFieldCarrier.ιP → decoupledFieldCarrier.E}
+    {s : decoupledFieldCarrier.ιE → decoupledFieldCarrier.P}
+    {t' : MultilinearPoly decoupledFieldCarrier.P m}
+    (hc : decoupledFieldCarrier.claimConsistent α s)
+    (hs : (s, t') ∈ decoupledFieldCarrier.sliceRel m r) :
+    ((α, r), decoupledFieldCarrier.unpack t') ∈ decoupledFieldCarrier.openingClaimRel m :=
+  letI : IsDomain decoupledFieldCarrier.E := inferInstanceAs (IsDomain (GaloisField 2 3))
+  decoupledFieldCarrier.openingClaimRel_of_claimConsistent hc hs
+
+end Sanity
+
+end RingSwitching.Generic
+
+end
diff --git a/blueprint/src/references.bib b/blueprint/src/references.bib
index 0454549ead..b581405b82 100644
--- a/blueprint/src/references.bib
+++ b/blueprint/src/references.bib
@@ -492,3 +492,27 @@ @misc{NOZ26
   year         = {2026},
   url          = {https://eprint.iacr.org/2026/156}
 }
+
+@misc{BRW26,
+      author = {Benedikt Bünz and Ron Rothblum and William Wang},
+      title = {Flock: Fast Proving for Batch Boolean Computations},
+      howpublished = {Cryptology {ePrint} Archive, Paper 2026/1329},
+      year = {2026},
+      url = {https://eprint.iacr.org/2026/1329}
+}
+
+@misc{HJRRR25,
+      author = {Tamir Hemo and Kevin Jue and Eugene Rabinovich and Gyumin Roh and Ron D. Rothblum},
+      title = {Jagged Polynomial Commitments (or: How to Stack Multilinears)},
+      howpublished = {Cryptology {ePrint} Archive, Paper 2025/917},
+      year = {2025},
+      url = {https://eprint.iacr.org/2025/917}
+}
+
+@misc{RSG,
+      title = {Ring switching, generalized},
+      howpublished = {Note, leanEthereum/leanVM-b repository},
+      url = {https://github.com/leanEthereum/leanVM-b/blob/main/misc/ring-switching-generalized.pdf},
+      note = {How to transform a PCS for $\mathbb{F}_{2^f}$ into a PCS for $\mathbb{F}_{2^e}$, for
+              arbitrary $e$ and $f$; decoupled packing/opening fields, $\gamma$-power batching}
+}
diff --git a/docs/kb/concepts/ring-switching.md b/docs/kb/concepts/ring-switching.md
index 62cf587f25..73b7c9fb9f 100644
--- a/docs/kb/concepts/ring-switching.md
+++ b/docs/kb/concepts/ring-switching.md
@@ -53,10 +53,91 @@ and soundness requires `[IsDomain L]` (Schwartz–Zippel).
   `φ₁ = σ₋₁`, `β = ψ` (Theorem 2). `R_q` is not a domain, so the Schwartz–Zippel soundness theorem
   does not apply — Hachi soundness is a separate (CWSS) argument.
 
+## The Generic layer (`ProofSystem/RingSwitching/Generic/`)
+
+A second-generation abstraction, intended to eventually subsume `RingSwitchingProfile` (which it
+leaves untouched during migration). It generalizes from the tower case to **decoupled**
+packing/opening algebras: the committed dense polynomial lives over a packing algebra `P`,
+evaluation claims arrive over an opening algebra `E`, and `P`, `E` are *unrelated* free
+`B`-algebras with chosen bases (`packBasis`, `openBasis`) — following Flock's Appendix B
+(the Φ/matrix-branching-program formulation, [BRW26]) and the "Ring switching, generalized" note
+([RSG]); DP24 tower switching is the special case `P = E = L`.
+
+**The seven-step spine** every ring switch shares (docstrings cite these step numbers):
+(1) pack the family `P_packed = ∑ᵢ Pᵢ·bᵢ^P`; (2) the fixed input claim `∀ i, αᵢ = P̂ᵢ(r)`;
+(3) eq-decompose `A(y,u) = openBasis.repr (eq̃(r,y)) u` over `B`; (4) recombine the slices over
+the packing basis; (5) batch the claims with random weights; (6) sum-check; (7) evaluate `B̂(r')`
+(an efficiency refinement, off the soundness path).
+
+**Safety pillars** (referenced as "pillar 1–4"): (1) every coordinate map / bridge is *derived
+from a bundled `Basis`* (`Basis.repr`, `Basis.constr`) — an instance has no law-free lever;
+(2) commitment binding flows through the PCS's own `commitsTo`, not a free hook; (3) packing
+correctness is proven once, generically; (4) no free `Prop` in the relation chain — the input
+relation is the fixed evaluation anchor of step (2). The carrier also structurally requires
+`Nontrivial P`/`Nontrivial E` (an honest *empty* basis would otherwise admit a degenerate carrier
+that collapses the anchor).
+
+**Status (proven, sorry-free, axiom-clean):**
+
+- [`Carrier.lean`](../../../ArkLib/ProofSystem/RingSwitching/Generic/Carrier.lean) —
+  `RingSwitchCarrier` + derived `packedMLE`/`eqCoord`/`bridge`/`Bmult` and the linchpin
+  `bridge_eqTilde` (`Φ(eq̃(r,y)) = ∑ᵤ A(y,u)·weight u`, Flock Claim 6's expansion); tower and
+  decoupled instances.
+- [`Packing.lean`](../../../ArkLib/ProofSystem/RingSwitching/Generic/Packing.lean) —
+  `packedMLE_eval` (reassembly at base-embedded points — the only well-typed generic form, and
+  sufficient: the papers use the family decomposition only at hypercube points) and
+  `packMLE_eq_packedMLE_curry`, the *Binius-stability bridge* (label "R2"): DP24's rank-`2^κ`
+  `packMLE` is the generic packing of the curried family.
+- [`Batching.lean`](../../../ArkLib/ProofSystem/RingSwitching/Generic/Batching.lean) —
+  `BatchingStrategy P W` (`[CommRing P]`-only vocabulary) with **proven** instances `gammaPowers`
+  (γ-powers, any claim count, error `e/|P|`, [RSG]) and `eqFold` (eq-indicator folding over
+  `{0,1}^κ`, error `κ/|P|`, [BRW26] App. B), both Schwartz–Zippel over `[IsDomain P] [Fintype P]`;
+  `reindex` transports a strategy along `W' ≃ W`. Also the decoupled *field* carrier `𝔽₄ ≠ 𝔽₈`
+  (label "R5": the `[IsDomain]`-gated layer exercised off-Binius).
+- [`Recombine.lean`](../../../ArkLib/ProofSystem/RingSwitching/Generic/Recombine.lean) —
+  `recombine_bijective`/`recombine_injective`: the packing-basis recombination `s ↦ ∑ᵢ sᵢ•bᵢ^P`
+  is `packBasis.equivFun.symm`, hence bijective — Flock Remark 5's fix-side property ("naive
+  recombination is complete but not sound") — plus `openingDecomposition_injective`, Remark 5's
+  opening half (uniqueness of `B`-coordinates in `openBasis`). Both are one-liners over the
+  reusable `Module.Basis.sum_smul_bijective`
+  ([`ArkLib/Data/Module/Basis.lean`](../../../ArkLib/Data/Module/Basis.lean)).
+- [`Relations.lean`](../../../ArkLib/ProofSystem/RingSwitching/Generic/Relations.lean) — the
+  framework-fixed relation chain (pillar 4): the input anchor `openingClaimRel` (step 2, with a
+  non-vacuity witness), the middle `sliceRel` (step 4) and `sumcheckClaimRel` (steps 5–6), and
+  the chain-coherence proof `sumcheckClaim_of_slices` (batching honest slices *is* the sumcheck
+  claim, via `bridge_eqTilde`). Plus the PCS interface (pillar 2): `PackedCommitment` whose
+  `commitsTo` carries the **functionality law** plus a `Nonempty` well-formedness guard
+  (`commitsTo_ne_top`: the `True` hook of the legacy `initialCompatibility` is *unstatable*),
+  and `DenseMLPCS` — the `MLIOPCS`-shaped bundle whose completeness/RBR-knowledge fields are
+  stated against the fixed anchored `evalRel`: the round-0 knowledge state function must track
+  `commitsTo` bidirectionally and completeness must cover every `commitsTo`-satisfying input
+  (a bogus-but-functional predicate survives locally and is caught at S6 composition
+  completeness). The Binius codeword-consistency predicate is re-expressed in `commitsTo`
+  orientation (`Binius.FRIBinius.biniusCommitsTo`, definitionally equal to the legacy hook).
+
+**The honest fork**: field-like instances get the (future) generic Schwartz–Zippel soundness
+theorem under `[IsDomain P]`; non-domain rings (Hachi `R_q`) can still *state* a carrier, a
+`BatchingStrategy`, and a `DenseMLPCS` but are forced into a sibling theorem with their own
+proven gap — the fork lives at the theorem, not the vocabulary.
+
+**Not yet built**: the assembled `ringSwitch` reduction and its soundness statement (gated on
+the upstream composition/sumcheck sorries), the Binius migration (the `biniusCommitsTo`
+functionality proof — by unique decoding over the `witnessNovelCoeffs` cube-table encoding,
+whose original diagonal-reading coercion bug was found at the S5 close-review and fixed in this
+PR — and retirement of the legacy `initialCompatibility` hook), and the MBP-`B̂` efficiency
+layer ([HJRRR25] §4).
+
 ## Core References
 
 - [`../papers/DP24.md`](../papers/DP24.md) — origin of ring switching for binary towers.
 - [`../papers/NOZ26.md`](../papers/NOZ26.md) — Hachi; the extension-field→cyclotomic-ring reduction.
+- [BRW26] Bünz, Rothblum, Wang. "Flock: Fast Proving for Batch Boolean Computations." ePrint
+  2026/1329 — Appendix B: the Φ/MBP formulation the Generic layer follows.
+- [RSG] "Ring switching, generalized." Note, [leanEthereum/leanVM-b](https://github.com/leanEthereum/leanVM-b/blob/main/misc/ring-switching-generalized.pdf) — decoupled packing/opening fields,
+  γ-power batching.
+- [HJRRR25] Hemo, Jue, Rabinovich, Roh, Rothblum. "Jagged Polynomial Commitments (or: How to Stack
+  Multilinears)." ePrint 2025/917 — §4: the MBP-MLE evaluation used by the future efficiency
+  layer.
 
 ## Main ArkLib Touchpoints
 
diff --git a/docs/wiki/repo-map.md b/docs/wiki/repo-map.md
index 2286f1f669..59515e9b66 100644
--- a/docs/wiki/repo-map.md
+++ b/docs/wiki/repo-map.md
@@ -116,6 +116,17 @@ home_page/            site assets and assembled website root
   reconstruction laws), `Prelude.lean` the shared defs + the Binius instance `binaryTowerProfile`,
   and `General.lean` the full reduction and generic security theorems. Binius instantiates it in
   `ProofSystem/Binius/FRIBinius/` (`biniusProfile`); Hachi (`NOZ26`) is the intended next instance.
+  A second-generation layer lives under `ProofSystem/RingSwitching/Generic/`: a shrunk,
+  `Basis`-derived carrier (`Carrier.lean`: `RingSwitchCarrier`, decoupled packing/opening
+  algebras `P ≠ E` allowed), proven packing correctness + the DP24-compat bridge
+  (`Packing.lean`), the proven batching-strategy menu (`Batching.lean`: `BatchingStrategy`,
+  `gammaPowers`, `eqFold`, Schwartz–Zippel under `[IsDomain]`), recombination injectivity on
+  both bases (`Recombine.lean`, Flock Remark 5, over the reusable
+  `Data/Module/Basis.lean:sum_smul_bijective`), and the framework-fixed relation chain + PCS
+  binding interface (`Relations.lean`: `openingClaimRel` anchor, middle relations,
+  `PackedCommitment`/`DenseMLPCS` with a functionality-constrained `commitsTo`); it is intended
+  to eventually subsume the `Profile.lean` path, which it deliberately leaves untouched during
+  migration.
   Background: KB concept page `docs/kb/concepts/ring-switching.md`; blueprint section
   `proof_systems/ring_switching.tex`. Structured sum-check support lives in
   `ProofSystem/Sumcheck/Structured*` and `ProofSystem/Sumcheck/Domain.lean`.