Merge remote-tracking branch 'origin/main' into completeness-of-binius

Author: chung-thai-nguyen

blueprint/src/references.bib

@@ -169,14 +169,6 @@ @misc{NOZ26
   url = {https://eprint.iacr.org/2026/156}
 }
 
-@misc{NOZ26,
-  author = {Ngoc Khanh Nguyen and George O'Rourke and Jiapeng Zhang},
-  title = {Hachi: Efficient Lattice-Based Multilinear Polynomial Commitments over Extension Fields},
-  howpublished = {Cryptology {ePrint} Archive, Paper 2026/156},
-  year = {2026},
-  url = {https://eprint.iacr.org/2026/156}
-}
-
 @inproceedings{DP25,
   author = {Diamond, Benjamin E. and Posen, Jim},
   title = {Succinct Arguments over Towers of Binary Fields},
@@ -239,6 +231,33 @@ @inproceedings{ACFY25
   organization={Springer}
 }
 
+@article{DG25,
+  title        = {Proximity Gaps in Interleaved Codes},
+  author       = {Diamond, Benjamin E. and Gruen, Angus},
+  journal      = {IACR Communications in Cryptology},
+  volume       = {1},
+  number       = {4},
+  year         = {2025},
+  doi          = {10.62056/a0ljbkrz},
+  url          = {https://cic.iacr.org/p/1/4/8}
+}
+
+@misc{BCGM25,
+  title        = {All Polynomial Generators Preserve Distance with Mutual Correlated Agreement},
+  author       = {Bordage, Sarah and Chiesa, Alessandro and Guan, Ziyi and Manzur, Ignacio},
+  howpublished = {Cryptology {ePrint} Archive, Paper 2025/2051},
+  year         = {2025},
+  url          = {https://eprint.iacr.org/2025/2051}
+}
+
+@misc{Jo26,
+  title        = {Interleaving Stability for Mutual Correlated Agreement and Curve Decodability},
+  author       = {Jo, Sunghyeon},
+  howpublished = {Cryptology {ePrint} Archive, Paper 2026/891},
+  year         = {2026},
+  url          = {https://eprint.iacr.org/2026/891}
+}
+
 @article{listdecoding,
   title={Algorithmic results in list decoding},
   author={Guruswami, Venkatesan and others},

docs/kb/_generated/lean-citations.json

@@ -219,7 +219,7 @@
     "ArkLib/ProofSystem/Binius/FRIBinius/General.lean": [
       "DP24"
     ],
-    "ArkLib/ProofSystem/RingSwitching/General.lean": [
+    "ArkLib/ProofSystem/Binius/RingSwitching/General.lean": [
       "DP24"
     ],
     "ArkLib/ProofSystem/Fri/Spec/SingleRound.lean": [
@@ -339,7 +339,7 @@
     "DP24": [
       "ArkLib/ProofSystem/Binius/BinaryBasefold/General.lean",
       "ArkLib/ProofSystem/Binius/FRIBinius/General.lean",
-      "ArkLib/ProofSystem/RingSwitching/General.lean"
+      "ArkLib/ProofSystem/Binius/RingSwitching/General.lean"
     ],
     "FRI1216": [
       "ArkLib/ProofSystem/Fri/Spec/SingleRound.lean"

docs/kb/audits/open-problems-list-decoding-and-correlated-agreement.md

@@ -79,7 +79,7 @@ ArkLib, missing, or present in a materially different form.
 | Remark 4.4 MCA with proximity loss | missing | none | No matching notion was found. |
 | Fact 4.5 `εpg ≤ εca ≤ εmca` | missing | related CA/proximity-gap predicates in [ArkLib/Data/CodingTheory/ProximityGap/Basic.lean](../../../ArkLib/Data/CodingTheory/ProximityGap/Basic.lean) | Not expressible in current ArkLib interfaces because `εca` and `εmca` are not defined as numeric errors. |
 | Lemma 4.6 MCA equals CA below unique decoding radius | missing | none | No general theorem of this form was found. |
-| Lemma 4.7 interleaving degrades MCA by at most `t` | missing | none | No general interleaving-vs-MCA theorem was found. |
+| Lemma 4.7 interleaving degrades MCA by at most `t` | missing | none; see [`Jo26`](../papers/Jo26.md) | No general interleaving-vs-MCA theorem was found. Jo26 gives a sharper interleaving-stability target for generator MCA: no linear interleaving-width loss, exact transfer when the seed-set size is at most the field size, and a field-size weighted factor otherwise. |
 | Theorem 4.8 AHIV17 general-code unique-decoding bound | missing | related but different [ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean](../../../ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean) | AHIV22 is present, but not this general `εmca/εca` statement. |
 | Theorem 4.9 RS unique-decoding results | present-but-different | `RS_correlatedAgreement_affineLines_uniqueDecodingRegime` and `RS_correlatedAgreement_affineLines` in [ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/UniqueDecoding.lean](../../../ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/UniqueDecoding.lean) and [ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/Main.lean](../../../ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/Main.lean) | Item 1 is represented via predicate-style CA for RS. Item 2, the BCHKS25 proximity-loss refinement, is missing. The main file still has a `sorry` in the non-unique-decoding branch. |
 | Remark 4.10 small proximity-loss simplification | missing | none | Depends on missing `εca` error-function interface. |
@@ -153,6 +153,8 @@ The largest mismatches between the paper and ArkLib are structural rather than m
    still lists mutual correlated agreement as missing. The existing
    [ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean](../../../ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean)
    file is WHIR/proximity-generator specific and is not a drop-in formalization of Section 4.
+   Jo26 should be treated as the sharper follow-up reference for transferring generator-MCA bounds
+   to row-wise interleaved codes once the general MCA interface exists.
 
 3. Some core BCIKS20 interfaces are present, but the list-decoding regime branch is incomplete.
    In particular,
@@ -235,7 +237,9 @@ The largest mismatches between the paper and ArkLib are structural rather than m
    missing Johnson corollaries.
 
 2. Add the general CA/MCA theorems in the unique-decoding regime first.
-   This includes the paper's Fact 4.5, Lemma 4.6, Lemma 4.7, and the AHIV17/BCHKS25 style results.
+   This includes the paper's Fact 4.5 and Lemma 4.6, and the AHIV17/BCHKS25 style results.
+   Treat Lemma 4.7's interleaving-loss statement as a baseline target sharpened by the newer
+   generator-MCA interleaving-stability results in [`Jo26`](../papers/Jo26.md).
 
 3. Add line-decoding and its implication to MCA before attempting the most recent capacity-level
    theorems.

docs/kb/concepts/reed-solomon-proximity.md

@@ -9,11 +9,19 @@ coding-theory machinery as formalized in ArkLib.
 - [`../papers/ACFY24.md`](../papers/ACFY24.md) - WHIR context built on Reed-Solomon proximity.
 - [`../papers/ACFY24stir.md`](../papers/ACFY24stir.md) - STIR protocol context built on the same
   surrounding coding-theory ecosystem.
+- [`../papers/DG25.md`](../papers/DG25.md) - proximity gaps in interleaved codes.
+- [`../papers/BCGM25.md`](../papers/BCGM25.md) - polynomial-generator MCA and Reed-Solomon
+  refinements.
+- [`../papers/Jo26.md`](../papers/Jo26.md) - interleaving stability for generator MCA and curve
+  decodability.
 
 ## Main ArkLib Touchpoints
 
 - [`../../../ArkLib/Data/CodingTheory/ProximityGap/Basic.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/Basic.lean)
 - [`../../../ArkLib/Data/CodingTheory/ProximityGap/BCIKS20`](../../../ArkLib/Data/CodingTheory/ProximityGap/BCIKS20)
+- [`../../../ArkLib/Data/CodingTheory/ProximityGap/DG25`](../../../ArkLib/Data/CodingTheory/ProximityGap/DG25)
+- [`../../../ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean)
+- [`../../../ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean)
 - [`../../../ArkLib/Data/CodingTheory/ReedSolomon.lean`](../../../ArkLib/Data/CodingTheory/ReedSolomon.lean)
 - [`../../../ArkLib/ProofSystem/Whir`](../../../ArkLib/ProofSystem/Whir)
 - [`../../../ArkLib/ProofSystem/Stir/ProximityGap.lean`](../../../ArkLib/ProofSystem/Stir/ProximityGap.lean)
@@ -22,3 +30,5 @@ coding-theory machinery as formalized in ArkLib.
 
 - This is the right starting point for many paper-driven PRs in coding theory and WHIR/STIR.
 - Deep theorem-by-theorem comparisons should live in audit pages rather than in this overview.
+- `Jo26` should be treated as follow-up infrastructure for existing MCA/interleaving formalization
+  rather than as a top-level protocol reference.

docs/kb/index.md

@@ -17,11 +17,17 @@ This is the main catalog for ArkLib's knowledge base.
   `ProofSystem/Stir` development.
 - [`papers/BCIKS20.md`](papers/BCIKS20.md) - proximity gaps for Reed-Solomon codes and the main
   coding-theory formalization it drives in ArkLib.
+- [`papers/BCGM25.md`](papers/BCGM25.md) - polynomial-generator MCA and related ArkLib
+  proximity-generator infrastructure.
 - [`papers/BCS16.md`](papers/BCS16.md) - original IOP reference used by the core oracle-reduction
   layer.
 - [`papers/BBS24.md`](papers/BBS24.md) - formal verification reference for sum-check.
+- [`papers/DG25.md`](papers/DG25.md) - interleaved-code proximity gaps and the DG25 formalization
+  subtree.
 - [`papers/DP24.md`](papers/DP24.md) - binary-tower multilinear proof reference for the Binius
   development.
+- [`papers/Jo26.md`](papers/Jo26.md) - interleaving stability for generator MCA and curve
+  decodability.
 
 The paper index now also includes scaffolded landing pages for all other citation keys currently
 used in `ArkLib/**/*.lean`, including:

docs/kb/log.md

@@ -129,3 +129,20 @@ Updated `ArkLib/Data/Polynomial/RationalFunctions.lean` with an explicit functio
 variable, regular-element closure lemmas, and a concrete low-degree `ξ` regularity helper.
 The Appendix A rational-functions audit now records this as the next denominator-clearing layer
 toward `ClaimA2.ξ_regular`.
+
+## [2026-06-16] seed | MCA and interleaving references
+
+Seeded paper pages and source metadata for:
+
+- `BCGM25`
+- `DG25`
+- `Jo26`
+
+and updated the Reed-Solomon proximity concept page to include the current MCA-generator and
+interleaved-code reference lineage.
+
+## [2026-06-16] refine | interleaving MCA audit target
+
+Updated the list-decoding and correlated-agreement audit to record `Jo26` as the sharper follow-up
+target for the missing interleaving-vs-MCA theorem once ArkLib has a general MCA error-function
+interface.

docs/kb/papers/BCGM25.md

@@ -0,0 +1,64 @@
+---
+kind: paper
+bibkey: BCGM25
+title: "All Polynomial Generators Preserve Distance with Mutual Correlated Agreement"
+year: 2025
+bib_source: blueprint/src/references.bib
+canonical_url: https://eprint.iacr.org/2025/2051
+source_metadata: ../sources/BCGM25/metadata.yml
+status: seeded
+related_concepts:
+  - reed-solomon-proximity
+related_modules:
+  - ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
+  - ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean
+---
+
+# BCGM25
+
+## At A Glance
+
+`BCGM25` is the ePrint reference for ArkLib's current general proximity-generator and
+MCA-generator definitions.
+It proves that polynomial generators satisfy mutual correlated agreement for every linear code,
+with Reed-Solomon refinements up to the Johnson bound.
+
+## What ArkLib Uses From This Paper
+
+- Generator definitions and zero-evading/MDS/polynomial-generator interfaces in
+  [`ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean).
+- MCA generator definitions and linear-transformation closure statements in
+  [`ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean).
+- The broader formalization target that polynomial-generator MCA bounds should become reusable
+  coding-theory infrastructure rather than WHIR-only assumptions.
+
+## Main ArkLib Touchpoints
+
+- [`ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean)
+- [`ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean)
+- [`ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean`](../../../ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean)
+
+## Version Notes
+
+- `BCGM25` is currently tracked as ePrint 2025/2051.
+- Keep theorem numbering tied to the ePrint version unless a later published version is added
+  under a separate key.
+
+## Known Divergences From ArkLib
+
+- ArkLib currently splits proximity-generator infrastructure between a general coding-theory layer
+  and WHIR-specific protocol files.
+- Some paper statements are represented as reusable definitions before the corresponding complete
+  theorem stack is present.
+
+## Open Formalization Gaps
+
+- Complete the main polynomial-generator MCA theorem stack.
+- Reconcile general MCA-generator APIs with the WHIR-specific `hasMutualCorrAgreement` interface.
+- Track interleaving stability results from `Jo26` as follow-up infrastructure for using BCGM25
+  bounds on interleaved codes.
+
+## Source Access
+
+- Source metadata: [`../sources/BCGM25/metadata.yml`](../sources/BCGM25/metadata.yml)
+- Public reference: [`blueprint/src/references.bib`](../../../blueprint/src/references.bib)

docs/kb/papers/DG25.md

@@ -0,0 +1,61 @@
+---
+kind: paper
+bibkey: DG25
+title: "Proximity Gaps in Interleaved Codes"
+year: 2025
+bib_source: blueprint/src/references.bib
+canonical_url: https://cic.iacr.org/p/1/4/8
+source_metadata: ../sources/DG25/metadata.yml
+status: seeded
+related_concepts:
+  - reed-solomon-proximity
+related_modules:
+  - ArkLib/Data/CodingTheory/InterleavedCode.lean
+  - ArkLib/Data/CodingTheory/ProximityGap/DG25
+---
+
+# DG25
+
+## At A Glance
+
+`DG25` is the IACR Communications in Cryptology reference for proximity gaps in interleaved codes.
+It is the main citation behind ArkLib's current DG25 subtree and the interleaved-code proximity
+gap transfer work.
+
+## What ArkLib Uses From This Paper
+
+- Row-wise and interleaved-code APIs in
+  [`ArkLib/Data/CodingTheory/InterleavedCode.lean`](../../../ArkLib/Data/CodingTheory/InterleavedCode.lean).
+- Interleaved affine-line proximity-gap transfer lemmas in
+  [`ArkLib/Data/CodingTheory/ProximityGap/DG25`](../../../ArkLib/Data/CodingTheory/ProximityGap/DG25).
+- Reed-Solomon specializations of the interleaved-code proximity-gap framework.
+
+## Main ArkLib Touchpoints
+
+- [`ArkLib/Data/CodingTheory/InterleavedCode.lean`](../../../ArkLib/Data/CodingTheory/InterleavedCode.lean)
+- [`ArkLib/Data/CodingTheory/ProximityGap/DG25/Basic.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/DG25/Basic.lean)
+- [`ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean)
+- [`ArkLib/Data/CodingTheory/ProximityGap/DG25/ReedSolomon.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/DG25/ReedSolomon.lean)
+
+## Version Notes
+
+- `DG25` refers to the IACR Communications in Cryptology article with DOI
+  `10.62056/a0ljbkrz`.
+
+## Known Divergences From ArkLib
+
+- ArkLib exposes generic interleaved-code and word-stack APIs that are broader than the paper's
+  immediate proximity-gap transfer statements.
+- Some formalization details are arranged by reusable code-theory interfaces rather than by paper
+  section.
+
+## Open Formalization Gaps
+
+- Keep DG25 transfer results aligned with later MCA-oriented interleaving stability work in `Jo26`.
+- Clarify which interleaving results should live under DG25-specific files and which should move
+  into a general interleaved-code/proximity-generator layer.
+
+## Source Access
+
+- Source metadata: [`../sources/DG25/metadata.yml`](../sources/DG25/metadata.yml)
+- Public reference: [`blueprint/src/references.bib`](../../../blueprint/src/references.bib)

docs/kb/papers/Jo26.md

@@ -0,0 +1,78 @@
+---
+kind: paper
+bibkey: Jo26
+title: "Interleaving Stability for Mutual Correlated Agreement and Curve Decodability"
+year: 2026
+bib_source: blueprint/src/references.bib
+canonical_url: https://eprint.iacr.org/2026/891
+source_metadata: ../sources/Jo26/metadata.yml
+status: seeded
+related_concepts:
+  - reed-solomon-proximity
+related_modules:
+  - ArkLib/Data/CodingTheory/InterleavedCode.lean
+  - ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
+  - ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean
+  - ArkLib/Data/CodingTheory/ProximityGap/DG25
+  - ArkLib/ProofSystem/Whir
+---
+
+# Jo26
+
+## At A Glance
+
+`Jo26` proves interleaving stability for two coding-theoretic soundness properties used in modern
+IOP/SNARK analyses: generator mutual correlated agreement and curve decodability.
+The main ArkLib relevance is that row-wise interleaving does not introduce the previously tracked
+linear interleaving-width loss for generator MCA.
+
+## What ArkLib Uses From This Paper
+
+- The generator-MCA transfer bound from a base code `C` to the row-wise interleaved code
+  `C^{≡s}`.
+- The exact-transfer case for `|Ω| ≤ q`, which makes affine-line MCA invariant under row-wise
+  interleaving.
+- The observation that polynomial-generator MCA bounds can be transferred to interleaved codes
+  without an additional interleaving-width factor.
+- The marked curve-decodability formulation and its equivalence to the standard definition for
+  additive codes, as future infrastructure for curve-decodability formalization.
+
+## Main ArkLib Touchpoints
+
+- [`ArkLib/Data/CodingTheory/InterleavedCode.lean`](../../../ArkLib/Data/CodingTheory/InterleavedCode.lean)
+  provides row-wise/interleaved-code representations.
+- [`ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean)
+  and
+  [`ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean)
+  provide the general generator and MCA-generator layer.
+- [`ArkLib/Data/CodingTheory/ProximityGap/DG25`](../../../ArkLib/Data/CodingTheory/ProximityGap/DG25)
+  contains adjacent interleaved-code proximity-gap transfer results.
+- [`ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean`](../../../ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean)
+  contains the current WHIR-specific MCA layer that should eventually reuse the general
+  coding-theory interface.
+
+## Version Notes
+
+- `Jo26` is currently tracked as ePrint 2026/891.
+- The ePrint metadata date is May 6, 2026.
+
+## Known Divergences From ArkLib
+
+- ArkLib does not yet expose a complete general code-level MCA error-function API matching the
+  paper's `ε_G(C, δ)` formulation.
+- Curve decodability is not yet a first-class ArkLib coding-theory abstraction.
+- Existing interleaved-code formalization is already present, but the exact statement shape needed
+  for `Jo26` will likely require a small interface layer around generator-MCA error functions.
+
+## Open Formalization Gaps
+
+- Add general code-level MCA error-function wrappers for the existing generator-MCA predicates.
+- Formalize the base-to-interleaved generator-MCA transfer bound.
+- Add the exact-transfer corollary for `|Ω| ≤ q`.
+- Introduce curve-decodability and marked curve-decodability definitions.
+- Prove the equivalence and interleaving-transfer results for curve decodability.
+
+## Source Access
+
+- Source metadata: [`../sources/Jo26/metadata.yml`](../sources/Jo26/metadata.yml)
+- Public reference: [`blueprint/src/references.bib`](../../../blueprint/src/references.bib)

docs/kb/sources/BCGM25/metadata.yml

@@ -0,0 +1,5 @@
+bibkey: BCGM25
+source_kind: eprint
+canonical_url: https://eprint.iacr.org/2025/2051
+committed_artifacts: []
+notes: "General polynomial-generator mutual-correlated-agreement reference cited by ArkLib's proximity-generator files."