feat(binius): adapt rbrKnowledgeSoundness onto completeness-of-binius with new VCVio APIs

[Copilot]

Ports the closed PR #296 (rbrKnowledgeSoundness) on top of PR #383 (completeness-of-binius), adapting to the new VCVio API surface and updated module layout.

New files

• BinaryBasefold/Soundness.lean — RBR knowledge soundness foundational lemmas (Lemmas 4.20–4.25): preTensorCombine, proximity gap bounds, per-block bad-event analysis, QueryPhaseSoundnessStatements
• RingSwitching/BBFSmallFieldIOPCS.lean — Full small-field IOPCS composition (Ring-Switching + BBF) with extractor construction via Extractor.Lens
• ToMathlib/MvPolynomial/Equiv.lean — Polynomial.toMvPolynomial_ne_zero_iff, toMvPolynomial_totalDegree_le

Modified files

• BinaryBasefold/Basic.lean — Added badSumcheckEventProp, extractMLP_eq_some_iff_pair_UDRClose, extractMLP_some_of_isCompliant_at_zero; renamed InitialStatement → MLPEvalStatement (L : Type) (ℓ : ℕ) to make type params explicit
• RingSwitching/Prelude.lean — MLPEvalStatement abbrev updated to parametric form: abbrev MLPEvalStatement (L : Type) (ℓ : ℕ) := BinaryBasefold.MLPEvalStatement L ℓ
• Data/Probability/Instances.lean — Added Pr_or_le (union bound), prob_schwartz_zippel_univariate_deg, prob_poly_agreement_degree_two
• AdditiveNTT/AdditiveNTT.lean — Added iteratedQuotientMap_congr_k
• ArkLib.lean — New imports

Key API adaptations vs PR #296

PR #296	This PR
SelectableType	SampleableType
SimulationInfrastructure.lean	Simulation.lean
import BinaryField.Tower.Prelude	import CodingTheory.ProximityGap.DG25
structure InitialStatement (implicit vars)	structure MLPEvalStatement (L : Type) (ℓ : ℕ)

Warning

Firewall rules blocked me from connecting to one or more addresses (expand for details)

I tried to connect to the following addresses, but was blocked by firewall rules:

• https://api.github.com/graphql
  • Triggering command: /usr/bin/gh gh auth status (http block)
• https://api.github.com/repos/Verified-zkEVM/ArkLib/git/refs/heads/copilot%2Fadapt-rbrknowledge-soundness
  • Triggering command: /usr/bin/curl curl -s -X PATCH -H Authorization: token ****** -H Accept: application/vnd.github.v3+json REDACTED -d {"sha":"ae4849d23679d55d1d720e994ccdd62997ff55e7","force":true} (http block)
  • Triggering command: /usr/bin/gh gh api repos/Verified-zkEVM/ArkLib/git/refs/heads/copilot%2Fadapt-rbrknowledge-soundness (http block)

If you need me to access, download, or install something from one of these locations, you can either:

• Configure Actions setup steps to set up my environment, which run before the firewall is enabled
• Add the appropriate URLs or hosts to the custom allowlist in this repository's Copilot coding agent settings (admins only)

---

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.