Core Interaction perfect Completeness

theorem coreInteraction_perfectCompleteness :  OracleReduction.perfectCompleteness    (oracleReduction := coreInteractionOracleReduction κ L K P ℓ ℓ' h_l aOStmtIn)    (StmtIn := Statement (L := L) (ℓ := ℓ') (RingSwitchingBaseContext κ L K ℓ P) 0)    (OStmtIn := aOStmtIn.OStmtIn)    (StmtOut := MLPEvalStatement L ℓ')    (OStmtOut := aOStmtIn.OStmtIn)    (WitIn := SumcheckWitness L ℓ' 0)    (WitOut := WitMLP L ℓ')    (relIn := sumcheckRoundRelation κ L K P ℓ ℓ' h_l aOStmtIn 0)    (relOut := aOStmtIn.toRelInput)    (init := init)    (impl := impl) := by  -- Follows from append_perfectCompleteness of interactionPhase and finalSumcheck  apply OracleReduction.append_perfectCompleteness  · apply OracleReduction.seqCompose_perfectCompleteness      (rel := fun i => sumcheckRoundRelation κ L K P ℓ ℓ' h_l aOStmtIn i)      (R := fun i => iteratedSumcheckOracleReduction κ L K P ℓ ℓ' aOStmtIn i)      (h := fun i =>        iteratedSumcheckOracleReduction_perfectCompleteness (κ:=κ) (L:=L) (K:=K)          (P:=P) (ℓ:=ℓ) (ℓ':=ℓ') (h_l:=h_l) (aOStmtIn:=aOStmtIn)          (init:=init) (impl:=impl) i      )  · exact finalSumcheckOracleReduction_perfectCompleteness (κ:=κ) (L:=L) (K:=K)      (P:=P) (ℓ:=ℓ) (ℓ':=ℓ') (h_l:=h_l) (aOStmtIn:=aOStmtIn) (init:=init) (impl:=impl)