Ring-Switching Core Interaction Phase

This module implements the core interactive sumcheck phase of the ring-switching protocol.

Iterated Sumcheck Steps

6. P and V execute the following loop: for i ∈ {0, ..., ℓ'-1} do P sends V the polynomial hᵢ(X) := Σ_{w ∈ {0,1}^{ℓ'-i-1}} h(r'₀, ..., r'_{i-1}, X, w₀, ..., w_{ℓ'-i-2}). V requires sᵢ ?= hᵢ(0) + hᵢ(1). V samples r'ᵢ ← L, sets s_{i+1} := hᵢ(r'ᵢ), and sends P r'ᵢ.

Each iteration of the loop constitutes a single round:

• Round i (for i = 1, ..., ℓ'):
  1. Prover sends sumcheck polynomial h_i(X) over large field L
  2. Verifier samples challenge α_i ∈ L
  • Prover & verifier updates state based on challenge

This is the core computational phase with ℓ' rounds, each with 2 messages, and is the main source of RBR knowledge soundness error.

Final Sumcheck Step

7. P computes s' := t'(r'_0, ..., r'_{ℓ'-1}) and sends V s'.
8. V sets e := eq̃(φ₀(r_κ), ..., φ₀(r_{ℓ-1}), φ₁(r'_0), ..., φ₁(r'_{ℓ'-1})) and decomposes e =: Σ_{u ∈ {0,1}^κ} β_u ⊗ e_u.
9. V requires s_{ℓ'} ?= (Σ_{u ∈ {0,1}^κ} eq̃(u_0, ..., u_{κ-1}, r''_0, ..., r''_{κ-1}) ⋅ e_u) ⋅ s'.

Per-round prover / verifier (re-exported from Sumcheck.Structured.SingleRound)

The per-round protocol code was lifted to ArkLib.ProofSystem.Sumcheck.Structured.SingleRound as round{PrvState, OracleProver, OracleVerifier, OracleReduction}, getRoundProverFinalOutput, and roundKnowledgeError, parameterized over a generic Context : Type and OStmtIn : ιₛᵢ → Type.

For backwards compatibility, the wrappers below preserve the original autobound signature (via the surrounding variable block — κ L K ℓ ℓ' aOStmtIn) by specializing Context := RingSwitchingBaseContext κ L K ℓ and OStmtIn := aOStmtIn.OStmtIn. They keep the iteratedSumcheck* names (these are what the sumcheck loop iterates over) and are @[reducible] so that subsequent soundness proofs and the seqCompose loop can still access fields like .KnowledgeStateFunction / .rbrKnowledgeSoundness through them.

@[reducible]

def RingSwitching.SumcheckPhase.iteratedSumcheckPrvState (κ : ℕ) (L : Type) [CommRing L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (aOStmtIn : AbstractOStmtIn L ℓ') (i : Fin ℓ') : Fin (2 + 1) → Type

@[reducible]

noncomputable def RingSwitching.SumcheckPhase.getIteratedSumcheckProverFinalOutput (κ : ℕ) (L : Type) [CommRing L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (aOStmtIn : AbstractOStmtIn L ℓ') (i : Fin ℓ') (finalPrvState : iteratedSumcheckPrvState κ L K P ℓ ℓ' aOStmtIn i 2) : (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) i.succ × ((j : aOStmtIn.ιₛᵢ) → aOStmtIn.OStmtIn j)) × SumcheckWitness L ℓ' i.succ

@[reducible]

noncomputable def RingSwitching.SumcheckPhase.iteratedSumcheckOracleProver (κ : ℕ) (L : Type) [CommRing L] [Nontrivial L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (aOStmtIn : AbstractOStmtIn L ℓ') (i : Fin ℓ') : OracleProver []ₒ (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) i.castSucc) aOStmtIn.OStmtIn (SumcheckWitness L ℓ' i.castSucc) (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) i.succ) aOStmtIn.OStmtIn (SumcheckWitness L ℓ' i.succ) (pSpecSumcheckRound L)

@[reducible]

def RingSwitching.SumcheckPhase.iteratedSumcheckOracleVerifier (κ : ℕ) (L : Type) [CommRing L] [Nontrivial L] [DecidableEq L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (aOStmtIn : AbstractOStmtIn L ℓ') (i : Fin ℓ') : OracleVerifier []ₒ (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) i.castSucc) aOStmtIn.OStmtIn (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) i.succ) aOStmtIn.OStmtIn (pSpecSumcheckRound L)

@[reducible]

noncomputable def RingSwitching.SumcheckPhase.iteratedSumcheckOracleReduction (κ : ℕ) (L : Type) [CommRing L] [Nontrivial L] [DecidableEq L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (aOStmtIn : AbstractOStmtIn L ℓ') (i : Fin ℓ') : OracleReduction []ₒ (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) i.castSucc) aOStmtIn.OStmtIn (SumcheckWitness L ℓ' i.castSucc) (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) i.succ) aOStmtIn.OStmtIn (SumcheckWitness L ℓ' i.succ) (pSpecSumcheckRound L)

theorem RingSwitching.SumcheckPhase.iteratedSumcheckOracleReduction_perfectCompleteness (κ : ℕ) [NeZero κ] (L : Type) [CommRing L] [Nontrivial L] [DecidableEq L] [SampleableType L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) [NeZero ℓ] [NeZero ℓ'] (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') {σ : Type} {init : ProbComp σ} {impl : QueryImpl []ₒ (StateT σ ProbComp)} (i : Fin ℓ') : OracleReduction.perfectCompleteness init impl (sumcheckRoundRelation κ L K P ℓ ℓ' h_l aOStmtIn i.castSucc) (sumcheckRoundRelation κ L K P ℓ ℓ' h_l aOStmtIn i.succ) (iteratedSumcheckOracleReduction κ L K P ℓ ℓ' aOStmtIn i)

@[reducible, inline]

noncomputable abbrev RingSwitching.SumcheckPhase.roundKnowledgeError (L : Type) [Fintype L] (ℓ : ℕ) (i : Fin ℓ) : NNReal

noncomputable def RingSwitching.SumcheckPhase.iteratedSumcheckRbrExtractor (κ : ℕ) (L : Type) [CommRing L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') (i : Fin ℓ') : Extractor.RoundByRound []ₒ (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) i.castSucc × ((j : aOStmtIn.ιₛᵢ) → aOStmtIn.OStmtIn j)) (SumcheckWitness L ℓ' i.castSucc) (SumcheckWitness L ℓ' i.succ) (pSpecSumcheckRound L) fun (_messageIdx : Fin (2 + 1)) => SumcheckWitness L ℓ' i.castSucc

def RingSwitching.SumcheckPhase.iteratedSumcheckKStateProp (κ : ℕ) (L : Type) [CommRing L] [Nontrivial L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') (i : Fin ℓ') (m : Fin (2 + 1)) (tr : ProtocolSpec.Transcript m (pSpecSumcheckRound L)) (stmt : Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) i.castSucc) (witMid : SumcheckWitness L ℓ' i.castSucc) (oStmt : (j : aOStmtIn.ιₛᵢ) → aOStmtIn.OStmtIn j) : Prop

This follows the KState of foldKStateProp

def RingSwitching.SumcheckPhase.iteratedSumcheckKnowledgeStateFunction (κ : ℕ) (L : Type) [CommRing L] [Nontrivial L] [DecidableEq L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') {σ : Type} {init : ProbComp σ} {impl : QueryImpl []ₒ (StateT σ ProbComp)} (i : Fin ℓ') : OracleVerifier.KnowledgeStateFunction init impl (sumcheckRoundRelation κ L K P ℓ ℓ' h_l aOStmtIn i.castSucc) (sumcheckRoundRelation κ L K P ℓ ℓ' h_l aOStmtIn i.succ) (iteratedSumcheckOracleVerifier κ L K P ℓ ℓ' aOStmtIn i) (iteratedSumcheckRbrExtractor κ L K P ℓ ℓ' h_l aOStmtIn i)

Knowledge state function (KState) for single round

theorem RingSwitching.SumcheckPhase.iteratedSumcheckOracleVerifier_rbrKnowledgeSoundness (κ : ℕ) [NeZero κ] (L : Type) [CommRing L] [Nontrivial L] [Fintype L] [DecidableEq L] [SampleableType L] (K : Type) [CommRing K] [Fintype K] [DecidableEq K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) [NeZero ℓ] [NeZero ℓ'] (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') {σ : Type} {init : ProbComp σ} {impl : QueryImpl []ₒ (StateT σ ProbComp)} [IsDomain L] (i : Fin ℓ') : OracleVerifier.rbrKnowledgeSoundness init impl (sumcheckRoundRelation κ L K P ℓ ℓ' h_l aOStmtIn i.castSucc) (sumcheckRoundRelation κ L K P ℓ ℓ' h_l aOStmtIn i.succ) (iteratedSumcheckOracleVerifier κ L K P ℓ ℓ' aOStmtIn i) fun (j : (pSpecSumcheckRound L).ChallengeIdx) => roundKnowledgeError L ℓ' i

RBR knowledge soundness for a single round oracle verifier

Final Sumcheck Step

noncomputable def RingSwitching.SumcheckPhase.finalSumcheckProver (κ : ℕ) (L : Type) [CommRing L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (aOStmtIn : AbstractOStmtIn L ℓ') : OracleProver []ₒ (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) (Fin.last ℓ')) aOStmtIn.OStmtIn (SumcheckWitness L ℓ' (Fin.last ℓ')) (MLPEvalStatement L ℓ') aOStmtIn.OStmtIn (WitMLP L ℓ') (pSpecFinalSumcheck L)

The prover for the final sumcheck step

noncomputable def RingSwitching.SumcheckPhase.finalSumcheckVerifier (κ : ℕ) (L : Type) [CommRing L] [DecidableEq L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') : OracleVerifier []ₒ (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) (Fin.last ℓ')) aOStmtIn.OStmtIn (MLPEvalStatement L ℓ') aOStmtIn.OStmtIn (pSpecFinalSumcheck L)

The verifier for the final sumcheck step

noncomputable def RingSwitching.SumcheckPhase.finalSumcheckOracleReduction (κ : ℕ) (L : Type) [CommRing L] [DecidableEq L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') : OracleReduction []ₒ (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) (Fin.last ℓ')) aOStmtIn.OStmtIn (SumcheckWitness L ℓ' (Fin.last ℓ')) (MLPEvalStatement L ℓ') aOStmtIn.OStmtIn (WitMLP L ℓ') (pSpecFinalSumcheck L)

The oracle reduction for the final sumcheck step

theorem RingSwitching.SumcheckPhase.finalSumcheckOracleReduction_perfectCompleteness (κ : ℕ) [NeZero κ] (L : Type) [CommRing L] [Nontrivial L] [Fintype L] [DecidableEq L] [SampleableType L] (K : Type) [CommRing K] [Fintype K] [DecidableEq K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) [NeZero ℓ] [NeZero ℓ'] (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') {σ : Type} (init : ProbComp σ) (impl : QueryImpl []ₒ (StateT σ ProbComp)) : OracleReduction.perfectCompleteness init impl (sumcheckRoundRelation κ L K P ℓ ℓ' h_l aOStmtIn (Fin.last ℓ')) (AbstractOStmtIn.toRelInput L ℓ' aOStmtIn) (finalSumcheckOracleReduction κ L K P ℓ ℓ' h_l aOStmtIn)

Perfect completeness for the final sumcheck step

noncomputable def RingSwitching.SumcheckPhase.finalSumcheckRbrKnowledgeError (L : Type) [Fintype L] : NNReal

RBR knowledge error for the final sumcheck step

noncomputable def RingSwitching.SumcheckPhase.finalSumcheckRbrExtractor (κ : ℕ) (L : Type) [CommRing L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') : Extractor.RoundByRound []ₒ (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) (Fin.last ℓ') × ((j : aOStmtIn.ιₛᵢ) → aOStmtIn.OStmtIn j)) (SumcheckWitness L ℓ' (Fin.last ℓ')) (WitMLP L ℓ') (pSpecFinalSumcheck L) fun (_m : Fin (1 + 1)) => SumcheckWitness L ℓ' (Fin.last ℓ')

The round-by-round extractor for the final sumcheck step

def RingSwitching.SumcheckPhase.finalSumcheckKStateProp (κ : ℕ) (L : Type) [CommRing L] [Nontrivial L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') {m : Fin (1 + 1)} (tr : ProtocolSpec.Transcript m (pSpecFinalSumcheck L)) (stmt : Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) (Fin.last ℓ')) (witMid : SumcheckWitness L ℓ' (Fin.last ℓ')) (oStmt : (j : aOStmtIn.ιₛᵢ) → aOStmtIn.OStmtIn j) : Prop

noncomputable def RingSwitching.SumcheckPhase.finalSumcheckKnowledgeStateFunction (κ : ℕ) (L : Type) [CommRing L] [Nontrivial L] [DecidableEq L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') {σ : Type} (init : ProbComp σ) (impl : QueryImpl []ₒ (StateT σ ProbComp)) : OracleVerifier.KnowledgeStateFunction init impl (sumcheckRoundRelation κ L K P ℓ ℓ' h_l aOStmtIn (Fin.last ℓ')) (AbstractOStmtIn.toRelInput L ℓ' aOStmtIn) (finalSumcheckVerifier κ L K P ℓ ℓ' h_l aOStmtIn) (finalSumcheckRbrExtractor κ L K P ℓ ℓ' h_l aOStmtIn)

The knowledge state function for the final sumcheck step

theorem RingSwitching.SumcheckPhase.finalSumcheckOracleVerifier_rbrKnowledgeSoundness (κ : ℕ) [NeZero κ] (L : Type) [CommRing L] [Nontrivial L] [Fintype L] [DecidableEq L] [SampleableType L] (K : Type) [CommRing K] [Fintype K] [DecidableEq K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) [NeZero ℓ] [NeZero ℓ'] (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') [Fintype L] [IsDomain L] {σ : Type} (init : ProbComp σ) (impl : QueryImpl []ₒ (StateT σ ProbComp)) : OracleVerifier.rbrKnowledgeSoundness init impl (sumcheckRoundRelation κ L K P ℓ ℓ' h_l aOStmtIn (Fin.last ℓ')) (AbstractOStmtIn.toRelInput L ℓ' aOStmtIn) (finalSumcheckVerifier κ L K P ℓ ℓ' h_l aOStmtIn) fun (x : (pSpecFinalSumcheck L).ChallengeIdx) => finalSumcheckRbrKnowledgeError L

Round-by-round knowledge soundness for the final sumcheck step

@[reducible]

def RingSwitching.SumcheckPhase.sumcheckLoopOracleVerifier (κ : ℕ) (L : Type) [CommRing L] [Nontrivial L] [DecidableEq L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (aOStmtIn : AbstractOStmtIn L ℓ') : OracleVerifier []ₒ (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) 0) aOStmtIn.OStmtIn (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) (Fin.last ℓ')) aOStmtIn.OStmtIn (ProtocolSpec.seqCompose fun (x : Fin ℓ') => pSpecSumcheckRound L)

Composed oracle verifier for the SumcheckStep (seqCompose over ℓ')

@[reducible]

noncomputable def RingSwitching.SumcheckPhase.sumcheckLoopOracleReduction (κ : ℕ) (L : Type) [CommRing L] [Nontrivial L] [DecidableEq L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (aOStmtIn : AbstractOStmtIn L ℓ') : OracleReduction []ₒ (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) 0) aOStmtIn.OStmtIn (SumcheckWitness L ℓ' 0) (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) (Fin.last ℓ')) aOStmtIn.OStmtIn (SumcheckWitness L ℓ' (Fin.last ℓ')) (pSpecSumcheckLoop L ℓ')

Composed oracle reduction for the SumcheckStep (seqCompose over ℓ')

@[reducible]

noncomputable def RingSwitching.SumcheckPhase.coreInteractionOracleVerifier (κ : ℕ) (L : Type) [CommRing L] [Nontrivial L] [DecidableEq L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') : OracleVerifier []ₒ (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) 0) aOStmtIn.OStmtIn (MLPEvalStatement L ℓ') aOStmtIn.OStmtIn (pSpecSumcheckLoop L ℓ' ++ₚ pSpecFinalSumcheck L)

Large-field reduction verifier: Sumcheck seqCompose, then append FinalSum

@[reducible]

noncomputable def RingSwitching.SumcheckPhase.coreInteractionOracleReduction (κ : ℕ) (L : Type) [CommRing L] [Nontrivial L] [DecidableEq L] (K : Type) [CommRing K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') : OracleReduction []ₒ (Sumcheck.Structured.Statement (RingSwitchingBaseContext κ L K ℓ P) 0) aOStmtIn.OStmtIn (SumcheckWitness L ℓ' 0) (MLPEvalStatement L ℓ') aOStmtIn.OStmtIn (WitMLP L ℓ') (pSpecSumcheckLoop L ℓ' ++ₚ pSpecFinalSumcheck L)

Large-field reduction: Sumcheck seqCompose, then append FinalSum

RBR Knowledge Soundness Components for Single Round

theorem RingSwitching.SumcheckPhase.coreInteraction_perfectCompleteness (κ : ℕ) [NeZero κ] (L : Type) [CommRing L] [Nontrivial L] [Fintype L] [DecidableEq L] [SampleableType L] (K : Type) [CommRing K] [Fintype K] [DecidableEq K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) [NeZero ℓ] [NeZero ℓ'] (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') {σ : Type} {init : ProbComp σ} {impl : QueryImpl []ₒ (StateT σ ProbComp)} : OracleReduction.perfectCompleteness init impl (sumcheckRoundRelation κ L K P ℓ ℓ' h_l aOStmtIn 0) (AbstractOStmtIn.toRelInput L ℓ' aOStmtIn) (coreInteractionOracleReduction κ L K P ℓ ℓ' h_l aOStmtIn)

Perfect completeness for large-field reduction (Sumcheck ++ FinalSum)

noncomputable def RingSwitching.SumcheckPhase.sumcheckLoopRbrKnowledgeErrorWithDegree (L : Type) [CommRing L] [Fintype L] (ℓ' d : ℕ) (j : (pSpecSumcheckLoopWithDegree L ℓ' d).ChallengeIdx) : NNReal

RBR knowledge error for a degree-d sumcheck loop, obtained from the seqCompose challenge-index decomposition.

noncomputable def RingSwitching.SumcheckPhase.sumcheckLoopRbrKnowledgeError (L : Type) [CommRing L] [Fintype L] (ℓ' : ℕ) (j : (pSpecSumcheckLoop L ℓ').ChallengeIdx) : NNReal

noncomputable def RingSwitching.SumcheckPhase.coreInteractionRbrKnowledgeErrorWithDegree (L : Type) [CommRing L] [Fintype L] (ℓ' d : ℕ) (j : (pSpecCoreInteractionWithDegree L ℓ' d).ChallengeIdx) : NNReal

RBR knowledge error for the core interaction with a degree-d sumcheck loop. The loop contributes d / |L| per sumcheck challenge; the final sumcheck contributes 1 / |L|.

noncomputable def RingSwitching.SumcheckPhase.coreInteractionRbrKnowledgeError (L : Type) [CommRing L] [Fintype L] (ℓ' : ℕ) (j : (pSpecCoreInteraction L ℓ').ChallengeIdx) : NNReal

Standard Binius ring-switching RBR knowledge error (d = 2) with exact final-step splitting.

theorem RingSwitching.SumcheckPhase.coreInteraction_rbrKnowledgeSoundness (κ : ℕ) [NeZero κ] (L : Type) [CommRing L] [Nontrivial L] [Fintype L] [DecidableEq L] [SampleableType L] (K : Type) [CommRing K] [Fintype K] [DecidableEq K] [Algebra K L] (P : RingSwitchingProfile K L κ) (ℓ ℓ' : ℕ) [NeZero ℓ] [NeZero ℓ'] (h_l : ℓ = ℓ' + κ) (aOStmtIn : AbstractOStmtIn L ℓ') {σ : Type} {init : ProbComp σ} {impl : QueryImpl []ₒ (StateT σ ProbComp)} [IsDomain L] : OracleVerifier.rbrKnowledgeSoundness init impl (sumcheckRoundRelation κ L K P ℓ ℓ' h_l aOStmtIn 0) (AbstractOStmtIn.toRelInput L ℓ' aOStmtIn) (coreInteractionOracleVerifier κ L K P ℓ ℓ' h_l aOStmtIn) (coreInteractionRbrKnowledgeError L ℓ')

RBR knowledge soundness for large-field reduction (Sumcheck ++ FinalSum)