Lemma 4.4 from WHIR

[ElijahVlasov]

Bounds on list decodability of interleaved RS-codes

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Lemma 4.4 from WHIR

Mathematical Formalization

• Core combinatorial bound: card_le_of_pairwise_agree_le in AgreementBound.lean proves a Johnson-type counting bound: for any set of distinct codewords C ⊆ ι → A with pairwise agreements ≤ s²·|ι|, any finite set of codewords within relative distance 1−s−η of a word y has size ≤ 1/(2ηs). This is alphabet-agnostic and serves as the foundational lemma.
• Interleaved Reed–Solomon bound: agree_lt_of_mem_interleavedCodeSet and interleaved_listDecodable in Interleaved.lean apply the core bound to k-fold interleaved RS codes. The second theorem establishes list-decodability with error radius 1 - √ρ - η and list size 1/(2η√ρ) for any η > 0, matching Lemma 4.4 of [ACFY24]. The proof is complete; no sorry or admit are introduced.
• Dependency update: ArkLib.lean adds an import for the new AgreementBound module to keep the graph up-to-date.

Documentation

• A reference to [ACFY24] and an updated authors list are added to the module docstring of Interleaved.lean.

Note: The PR body ("Bounds on list decodability of interleaved RS-codes") is accurate but less specific than the changes; the actual formalization centers on Lemma 4.4 of [ACFY24] and the required combinatorial core.

---

Statistics

Metric	Count
📝 Files Changed	3
✅ Lines Added	167
❌ Lines Removed	1

---

Lean Declarations

✏️ Added: 3 declaration(s)

ArkLib/Data/CodingTheory/ListDecodability/AgreementBound.lean (1)

• theorem card_le_of_pairwise_agree_le {C : Set (ι → A)} {s η : ℝ} (hs : 0 < s) (hη : 0 < η)

ArkLib/Data/CodingTheory/ReedSolomon/Interleaved.lean (2)

• lemma agree_lt_of_mem_interleavedCodeSet {ι : Type*} [Fintype ι] {F : Type*} [Field F]
• theorem interleaved_listDecodable {F : Type*} [Field F]

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

This review identifies one naming convention violation, one documentation gap, and some minor style issues in an otherwise well-structured contribution. The core mathematics appear correct, and the blueprints are consistent. The changes are relevant to the contributing guidelines for ArkLib. The identified issues are flagged below for correction before merging.

---

📄 **Per-File Summaries**

• ArkLib.lean: Added an import for the new ArkLib.Data.CodingTheory.ListDecodability.AgreementBound module, which will provide agreement-bound lemmas relevant to list-decodability theory. This import ensures the file's dependency graph is up-to-date and that downstream code can use the new module's definitions.
• ArkLib/Data/CodingTheory/ListDecodability/AgreementBound.lean: Adds the new file AgreementBound.lean containing the theorem card_le_of_pairwise_agree_le, which proves a Johnson-type counting bound: if distinct codewords in C ⊆ ι → A agree in at most s²·|ι| positions, then any finite set of codewords within relative distance 1−s−η of a word y has size at most 1/(2ηs). This is the alphabet-agnostic core used later to derive the Reed–Solomon list-decoding bound and to transport it to interleaved Reed–Solomon codes. The proof is complete; no sorrys or admits are present.
• ArkLib/Data/CodingTheory/ReedSolomon/Interleaved.lean: The file adds two theorems: agree_lt_of_mem_interleavedCodeSet and interleaved_listDecodable. The first lemma proves that two distinct codewords in the k-fold interleaved Reed–Solomon code agree in fewer than m positions. The second theorem establishes that this interleaved code is list-decodable with error radius 1 - √ρ - η and list size 1/(2η√ρ) for any η > 0, matching the Johnson bound of the base code (lemma 4.4 in [ACFY24]). A reference to [ACFY24] is added to the module docstring, and the authors list is updated. No sorry or admit are introduced.

---

Last updated: 2026-08-17 10:51 UTC.

[github-actions]

Build Timing Report

• Commit: 349d7f2
• Message: Lemma 4.4 from WHIR
• Ref: ElijahVlasov/interleaved-rs
• Comparison baseline: e92dc31 from current base of main.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; validation wrapper ./scripts/validate.sh.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	614.51	1776.31	+1161.80	ok
Warm rebuild	1.93	2.67	+0.74	ok
Validation wrapper	2.40	3.09	+0.69	ok

Incremental Rebuild Signal

• Warm rebuild saved 1773.64s vs clean (665.28x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
132.00	62.00	+70.00	ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Weight.lean
104.00	48.00	+56.00	ArkLib/Data/CodingTheory/ListDecodability/Bounds/KKH26Asymptotic.lean
88.00	37.00	+51.00	ArkLib/ProofSystem/Stir/Combine.lean
74.00	41.00	+33.00	ArkLib/Data/CodingTheory/SubspaceDesign.lean
71.00	27.00	+44.00	ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean
69.00	32.00	+37.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean
67.00	35.00	+32.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
65.00	38.00	+27.00	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
64.00	35.00	+29.00	ArkLib/Data/CodingTheory/JohnsonBound/Family.lean
61.00	31.00	+30.00	ArkLib/Data/CodingTheory/ListDecodability/Bounds/LargeAlphabet/Pigeonhole.lean
59.00	36.00	+23.00	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
56.00	29.00	+27.00	ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean
53.00	27.00	+26.00	ArkLib/Data/CodingTheory/ProximityGap/Folding.lean
50.00	23.00	+27.00	ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
46.00	19.00	+27.00	ArkLib/Data/CodingTheory/ListDecodability/Bounds/LargeAlphabet/Centers.lean
45.00	22.00	+23.00	ArkLib/Data/MvPolynomial/EvenAndOdd.lean
43.00	15.00	+28.00	ArkLib/Data/CodingTheory/DivergenceOfSets.lean
42.00	21.00	+21.00	ArkLib/OracleReduction/LiftContext/Reduction.lean
41.00	27.00	+14.00	ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean
39.00	21.00	+18.00	ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean

[quangvdao]

Thanks, Ilia (and Aristotle) — this is a clean and useful formalization.

I reviewed exact head 349d7f2815f73717894287aa747a3ba0e1aacaae against the recorded PR base e92dc315f453db88dd7351c88e889caf0e6bf269, and checked integration against current upstream main at 5a9626d331d713c7e74efa7e3d93b7d0ec9c4dc2.

Verdict

Approved. I found no mathematical-correctness, source-correspondence, abstraction, or trust-boundary blocker.

Statement and source review

• Code.card_le_of_pairwise_agree_le correctly isolates the alphabet-agnostic Johnson-type counting argument: pairwise agreement bounded by (s²|ι|) yields list size at most (1/(2ηs)) inside radius (1-s-η).
• agree_lt_of_mem_interleavedCodeSet correctly reduces equality of interleaved symbols to equality in a differing row and applies the Reed–Solomon agreement bound.
• interleaved_listDecodable then instantiates the generic theorem with sqrtRate, whose square is min m |ι| / |ι|. This matches WHIR Lemma 4.4 in the intended nonsaturated regime.
• The Lean statement is safely a little stronger than the paper: it does not require a nonempty interleaving index or the paper's upper bound on (η). At the boundary cases, distinct codewords are impossible or the decoding radius becomes negative, so this does not create an unsound claim.

The abstraction split is good: the generic combinatorial result lives in ListDecodability/AgreementBound, while the Reed–Solomon module supplies only the code-specific pairwise-agreement fact. No new sorry, admit, unsafe declaration, or axiom is introduced.

Validation

• All hosted checks are green on the exact reviewed head, including the clean build, validation wrapper, blueprint/docs, imports, docs integrity, and whitespace.
• A synthetic merge-tree check against current upstream main is clean.
• I did not rerun the full validation suite on that synthetic current-main merge; updating the branch should trigger that final integration run.

Nonblocking polish before merge

• Please retitle this in the repository's conventional format, for example feat(coding-theory): prove interleaved RS list-decodability.
• The PR body would be more reviewer-friendly if it named WHIR Lemma 4.4, the new generic agreement theorem, and the safe strengthening described above.

Thank you for pushing this through — the resulting theorem boundary is reusable and well chosen.

[alexanderlhicks]

see

ArkLib/ArkLib/Data/CodingTheory/ReedSolomon/ListDecodability.lean

Line 34 in 5b263f4

lemma card_le_of_subset_closeCodewords [Nonempty ι] (domain : ι ↪ F) {m : ℕ} (hm : 0 < m)

[alexanderlhicks]

when rebasing, this should work:
refine Code.isListDecodable_of_forall_finset_card_le fun y T hT => ?_