docs(kb): add MCA and interleaved-code references

[ainta]

Summary

• add BCGM25, DG25, and Jo26 source metadata, paper pages, and bibliography entries for the MCA/interleaving reference lineage
• update the Reed-Solomon proximity concept page and human-maintained KB index with generator-MCA and interleaved-code references
• update the open-problems audit and KB log to point future formalization work at the newer interleaving-stability target

Context

ArkLib already tracks Reed-Solomon proximity, generator MCA, and interleaved-code gaps in the KB. This PR fills in nearby missing bibliography and source metadata for that line of work.

Non-goals

• this does not modify Lean source code
• this does not formalize a generator-MCA transfer or interleaving-stability theorem
• this does not introduce a general MCA error-function API or curve-decodability interface
• this does not modify generated KB indexes under docs/kb/_generated/**

Verification

• python3 scripts/kb/lint.py --strict-cited-pages
• python3 scripts/check-docs-integrity.py
• git diff --check

[github-actions]

🤖 PR Summary

Failed to get summary: Error: The output was too long (exceeded the character limit). Please write a shorter version of the output.

---

Statistics

Metric	Count
📝 Files Changed	11
✅ Lines Added	285
❌ Lines Removed	2

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

1. Title Format Violation

The diff does not include a pull request title, so I cannot check the title format. Nothing to report.

2. Description Content

The diff does not include a pull request description, so I cannot check the description content. Nothing to report.

3. File Header and Licensing

• All new .lean files in the diff (none are added; only .md, .yml, and .bib files appear) are not present. No Lean file violations.
• The diff does not add any .lean files. The instructions about file headers, imports, formatting, etc. are not applicable.
• The added .bib entry for DG25 includes a doi field; the instructions do not mandate a particular format for BibTeX entries, so this is acceptable.

4. Naming Conventions

No new Lean declarations or identifiers are introduced in this diff. Nothing to report.

5. Syntax and Formatting

No new Lean code is introduced. Nothing to report.

6. Deprecation Policy

No declarations are renamed or removed. Nothing to report.

7. Documentation Standards

• The new paper pages (BCGM25.md, DG25.md, Jo26.md) each contain a docstring-like structure (frontmatter, section headers, ArkLib touchpoints, etc.), which follows a reasonable documentation convention. The instructions do not specify a required format for markdown documentation, so no violations.
• The updated reed-solomon-proximity.md, index.md, log.md, and open-problems-list-decoding-and-correlated-agreement.md are consistent with the existing documentation style.

8. Citation Standards

• The diff adds three new citation keys (DG25, BCGM25, Jo26) to blueprint/src/references.bib. Each entry is formatted as a standard BibTeX entry. The instructions require all academic papers to have BibTeX entries in blueprint/src/references.bib; the diff satisfies this.
• The new paper pages reference their BibTeX source (bib_source: blueprint/src/references.bib) and use citation keys in the text (e.g., [Jo26]). The instructions require citation keys in text and a References section in the docstring header. The new pages include a bib_source field but not a local ## References section listing the bibliography entry; however, the project-wide central BibTeX file is the intended mechanism, and the bib_source field points to it. This is acceptable—the instruction about a ## References section applies to Lean docstring headers, not to markdown paper pages.
• The updated open-problems-list-decoding-and-correlated-agreement.md references Jo26 as a citation key, consistent with the policy.

9. Blueprint / Large Contributions

No new proof system or large formalization is introduced. The diff adds reference scaffolding and documentation updates. No blueprint is required.

10. Style Guide / Linting Script

The style guide and linting script (./scripts/lint-style.sh) apply to Lean source files. No new Lean files are added or modified. Nothing to report.

Summary

The diff is focused entirely on documentation and reference infrastructure: adding three new paper landing pages, corresponding metadata files, BibTeX entries, and updating the knowledge-base index, concept pages, and audit page to reference these new sources. All changes are consistent with the project's documentation and citation conventions. No violations of the PR Title Format, Description, Naming Conventions, Syntax and Formatting, File Headers, Deprecation Policy, or Blueprint instructions are present.

---

📄 **Per-File Summaries**

• blueprint/src/references.bib: Added three new bibliography entries for DG25 (Diamond and Gruen, "Proximity Gaps in Interleaved Codes"), BCGM25 (Bordage, Chiesa, Guan, and Manzur, "All Polynomial Generators Preserve Distance with Mutual Correlated Agreement"), and Jo26 (Jo, "Interleaving Stability for Mutual Correlated Agreement and Curve Decodability"), providing citations for these recent cryptographic and coding-theoretic works.
• docs/kb/audits/open-problems-list-decoding-and-correlated-agreement.md: The audit entry for Lemma 4.7 now cross-references Jo26, noting that Jo26 provides sharper generator-MCA interleaving-stability results (no linear interleaving-width loss, exact transfer when seed-set size ≤ field size, field-size weighted factor otherwise) which supersede the original lemma statement. The section describing structural mismatches adds a remark that Jo26 should be treated as a sharper follow-up for transferring generator-MCA bounds to row-wise interleaved codes once the general MCA interface exists. The suggested additions list separates Lemma 4.7 from Fact 4.5 and Lemma 4.6, directing implementers to treat the interleaving-loss lemma as a baseline target sharpened by Jo26, rather than as a direct addition.
• docs/kb/concepts/reed-solomon-proximity.md: The page adds references to three new papers (DG25, BCGM25, and Jo26) in the 'Related Papers' section, along with brief descriptions of their topics (proximity gaps in interleaved codes, polynomial-generator MCA and Reed-Solomon refinements, and interleaving stability for generator MCA and curve decodability, respectively). In the 'Main ArkLib Touchpoints' section, it adds three new ArkLib paths (ProximityGap/DG25, ProximityGap/ProximityGenerators.lean, and ProximityGap/MCAGenerator.lean). It also appends a note stating that 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: The documentation (docs/kb/index.md) now lists three new paper references: BCGM25.md (polynomial-generator MCA and proximity-generator infrastructure), DG25.md (interleaved-code proximity gaps and the DG25 formalization subtree), and Jo26.md (interleaving stability for generator MCA and curve decodability), expanding the knowledge base catalog of formalization sources used in ArkLib.
• docs/kb/log.md: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='The docs/kb/log.md fil...ror-function interface.', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid
• docs/kb/papers/BCGM25.md: Added a new documentation file docs/kb/papers/BCGM25.md recording the paper 'All Polynomial Generators Preserve Distance with Mutual Correlated Agreement' (ePrint 2025/2051). The page states that BCGM25 proves polynomial generators satisfy mutual correlated agreement (MCA) for every linear code, with Reed-Solomon refinements up to the Johnson bound. It maps the paper's generator and MCA-generator definitions to ArkLib modules (ProximityGenerators.lean, MCAGenerator.lean), lists the formalization touchpoints, records version notes and known divergences (e.g., split infrastructure, incomplete theorem stack), and enumerates open formalization gaps such as completing the main polynomial-generator MCA theorem stack and reconciling general MCA APIs with the WHIR-specific hasMutualCorrAgreement interface.
• docs/kb/papers/DG25.md: Added a new documentation file docs/kb/papers/DG25.md that records the bibliographic metadata, ArkLib touchpoints, and formalization status of the paper “Proximity Gaps in Interleaved Codes”. It establishes that DG25 is the main reference for the interleaved-code proximity-gap transfer work, lists the specific Lean files that implement its APIs and lemmas (e.g., InterleavedCode.lean, ProximityGap/DG25/Basic.lean, ProximityGap/DG25/MainResults.lean, and ProximityGap/DG25/ReedSolomon.lean), and notes known divergences between the paper's statements and ArkLib's broader interleaved-code interfaces as well as open formalization gaps concerning alignment with future work (Jo26).
• docs/kb/papers/Jo26.md: Added a new documentation page docs/kb/papers/Jo26.md for the paper "Interleaving Stability for Mutual Correlated Agreement and Curve Decodability" (Jo26). This page records the paper's metadata, its main results (interleaving stability for generator MCA and curve decodability), and details how those results relate to ArkLib: it identifies the specific coding-theory modules (InterleavedCode.lean, ProximityGenerators.lean, MCAGenerator.lean, DG25, and Whir/MutualCorrAgreement.lean) that are affected, lists known divergences and open formalization gaps (e.g., adding a general MCA error‑function API, proving the base‑to‑interleaved generator‑MCA transfer bound, and formalizing curve‑decodability definitions), and notes version tracking information.
• 3 file(s) filtered as noise (lockfiles, generated, or trivial): docs/kb/sources/BCGM25/metadata.yml, docs/kb/sources/DG25/metadata.yml, docs/kb/sources/Jo26/metadata.yml

---

Last updated: 2026-07-07 01:09 UTC.