Folding preserves block relative distance balls (Claim 4.22 WHIR)

[ElijahVlasov]

No description provided.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Folding preserves block relative distance balls (Claim 4.22 WHIR)

sorry delta: +1 (1 added) — proof obligations increased

This pull request introduces formal definitions and theorems for block-relative distance on smooth Reed–Solomon codes and establishes the key property that folding preserves block-relative distance balls (Claim 4.22 of [ACFY24]). The main contributions are a new API for coset-FFT-domain blocks, the actual block-relative-distance theory in BlockRelDistance.lean, and the list-decodability lemmas in Folding/ListDecodability.lean. A single sorry is added in Folding.lean for hammDist_foldWord_foldWord. The PR also performs minor refactoring of membership decision procedures and marks one file as obsolete (to be deleted after the STIR/WHIR work).

---

Statistics

Metric	Count
📝 Files Changed	9
✅ Lines Added	784
❌ Lines Removed	158

---

Lean Declarations

✏️ Removed: 5 declaration(s)

ArkLib/Data/CodingTheory/ProximityGap/Folding.lean (4)

• private lemma roots_in_domain_card_eq_if_x_in_domain
• private lemma roots_of_x_in_domain_card
• private lemma roots_of_x_in_domain_eq
• private lemma roots_of_x_in_domain_le_k

ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean (1)

• lemma card_roots {i j : ℕ} (hij : i + j ≤ n) (h : x ∈ subdomain ω (i + j)) :

✏️ Added: 61 declaration(s)

ArkLib/Data/CodingTheory/Basic/BlockRelDistance.lean (31)

• def blockDistance
• def blockRelDistance
• def card_complDisagreementSet [Fintype F] :
• def card_disagreementSet' [Fintype F] :
• def complDisagreementSet [Fintype F]
• def disagreementSet
• lemma blockDistance_eq_hammingDist_k_0 :
• lemma blockRelDistance_eq_one_sub [Fintype F] :
• lemma blockRelDistance_eq_one_sub' [Fintype F] :
• lemma blockRelDistance_eq_relHammingDist_k_0 :
• lemma card_complDisagreementSet_le [Fintype F] :
• lemma card_disagreementSet_k_0 :
• lemma card_disagreementSet_le :
• lemma complDisagreementSet_def' [Fintype F] :
• lemma complDisagreementSet_sub_subdomain [Fintype F] :
• lemma disagreementSet_intersect_subdomain_eq :
• lemma disagreementSet_k_0 :
• lemma disagreementSet_k_0_eq_image :
• lemma disagreementSet_sub_subdomain :
• lemma listBlock_subset_listHamming [Fintype F] [NeZero n]
• lemma relHammingDist_le_blockRelDistance [Fintype F] [NeZero n] (hkn : k ≤ n) :
• noncomputable def blockDistanceFromCode
• noncomputable def blockRelDistanceBall
• noncomputable def blockRelDistanceFromCode
• private def agreementBlockUnion [Fintype F]
• private lemma agreement_sub_agreementBlockUnion [Fintype F] :
• private lemma card_agreementBlockUnion [Fintype F]
• private lemma card_agreementBlockUnion_le [Fintype F] :
• private lemma card_disagreement_le [Fintype F] :
• private lemma relHammingDist_le_sub_agreementBlockUnion [Fintype F] :
• private lemma relHammingDist_le_sub_agreementBlockUnion' [Fintype F] :

ArkLib/Data/CodingTheory/ProximityGap/Folding.lean (2)

• lemma hammDist_foldWord_foldWord [nz : NeZero n] (hn : 2 ∣ n)
• theorem foldWord_k_1' [NeZero n] {α : F} :

ArkLib/Data/CodingTheory/ProximityGap/Folding/ListDecodability.lean (4)

• lemma folding_block_rel_ball [NeZero n]
• lemma folding_contracts_block_distance [NeZero n]
• lemma folding_contracts_block_rel_distance [NeZero n]
• theorem folding_preserves_block_balls [NeZero n]

ArkLib/Data/Domain/CosetFftDomain/Block.lean (19)

• def block (ω : D) (k : ℕ) (x : F) : Finset F
• def blockIdx (ω : D) (k : ℕ) (x : F) : Finset ι
• lemma blockIdx_eq_preimage_block :
• lemma blockIdx_k_1_of_eq {i : ι} (hi : ω i = x) :
• lemma blockIdx_k_1_of_ne_mem (hx : x ∉ ω) :
• lemma blockIdx_x_0 :
• lemma block_eq_nthRootsFinset :
• lemma block_k_1 :
• lemma block_x_0 :
• lemma card_blockIdx :
• lemma card_block_le :
• lemma mem_block :
• lemma mem_blockIdx {i : ι} :
• lemma mem_blockIdx_iff_mem_block {i : ι} :
• lemma mem_blockIdx_self {i : ι} :
• lemma neg_mem_block_iff_mem [NeZero k] (hk : k ≤ n) :
• lemma neg_mem_block_of_mem [NeZero k] (hy : y ∈ block ω k x)
• theorem disjoint_block {x y : F} (hxy : x ≠ y) :
• theorem disjoint_blockIdx {x y : F} (hxy : x ≠ y) :

ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean (5)

• lemma card_block_of_mem_subdomain {i j : ℕ} (hij : i + j ≤ n) (h : x ∈ subdomain ω (i + j)) :
• lemma card_block_of_mem_subdomain' {k : ℕ}
• lemma subdomain_comp
• private lemma subdomain_eval (ω : D) (j : ℕ)
• theorem mem_subdomain_comp_iff_mem

✏️ Affected: 6 declaration(s) (line number changed)

• lemma foldWordAux_natDegree {k : ℕ} {x : F} : in ArkLib/Data/CodingTheory/ProximityGap/Folding.lean moved from L194 to L166
• private lemma foldWordAux_coeff_eq_foldWordAuxCoeff_fin {i : Fin (2 ^ k)} : in ArkLib/Data/CodingTheory/ProximityGap/Folding.lean moved from L424 to L414
• private lemma foldWordAux_coeff_eq_foldWordAuxCoeff_nat {i : ℕ} : in ArkLib/Data/CodingTheory/ProximityGap/Folding.lean moved from L429 to L418
• private lemma foldWordAux_eq_sum_of_foldWordAuxCoeff : in ArkLib/Data/CodingTheory/ProximityGap/Folding.lean moved from L441 to L428
• private lemma indicated_polynomial_degree_y_lt : in ArkLib/Data/CodingTheory/ProximityGap/Folding.lean moved from L488 to L474
• private lemma indicated_polynomial_eq_foldAux {α : F} (hx : x ∈ s') : in ArkLib/Data/CodingTheory/ProximityGap/Folding.lean moved from L499 to L483

---

sorry Tracking

❌ Added: 1 `sorry`(s)

ArkLib/Data/CodingTheory/ProximityGap/Folding.lean (1)

• lemma hammDist_foldWord_foldWord [nz : NeZero n] (hn : 2 ∣ n) (L247)

---

📋 **Additional Analysis**

The diff introduces new files and modifies existing ones, but contains several violations of the ArkLib style guide, particularly in naming conventions, documentation standards, and line length. Additionally, some proofs are incomplete. Below are the specific findings organized by category.

---

📄 **Per-File Summaries**

• ArkLib.lean: Added three new imports to ArkLib.lean: ArkLib.Data.CodingTheory.Basic.BlockRelDistance, ArkLib.Data.CodingTheory.ProximityGap.Folding.ListDecodability, and ArkLib.Data.Domain.CosetFftDomain.Block. These extend the library's reach into block-relative distance in coding theory, list decodability for the folding proximity gap, and block-specific coset FFT domain definitions.
• ArkLib/Data/CodingTheory/Basic/BlockRelDistance.lean: This file introduces block relative distance for smooth Reed–Solomon codes, mirroring Definition 4.17 of [ACFY24]. It defines disagreementSet, blockDistance, and blockRelDistance (with Δ𞁒/δ𞁒 notation), along with distance-from-code variants blockDistanceFromCode / blockRelDistanceFromCode. Several lemmas relate the k=0 case to standard Hamming distance and relative Hamming distance (e.g., blockDistance_eq_hammingDist_k_0, blockRelDistance_eq_relHammingDist_k_0). The file also provides complDisagreementSet and associated identities, an agreementBlockUnion construction, and the key inequality relHammingDist_le_blockRelDistance (Claim 4.19, Part 1) together with the subset lemma listBlock_subset_listHamming (Claim 4.19, Part 2). No sorry or admit are present.
• ArkLib/Data/CodingTheory/ProximityGap/Folding.lean: The diff refactors foldWordAux and foldValue to use the new blockIdx and block API from ArkLib.Data.Domain.CosetFftDomain.Block instead of building the index set via {i | domain i ^ k = x} and {i | domain i ^ 2 ^ k = x}. foldWordAux now takes a raw k and builds a polynomial of degree < 2^k, and foldValue similarly operates with exponent k rather than 2 ^ k. The lemmas foldWordAux_of_k_2, foldWordAux_natDegree, foldValue_def, foldValue_def', foldValue_pow_x_k, foldWordAuxCoeff, foldWordAux_coeff_eq_foldWordAuxCoeff_fin, foldWordAux_coeff_eq_foldWordAuxCoeff_nat, foldWordAux_eq_sum_of_foldWordAuxCoeff, foldValue_eq_sum_of_foldAuxCoeff_mul_pow_alpha, indicated_polynomial_degree_y_lt, indicated_polynomial_eval_eq_combination_of_correlated, indicated_polynomial_eq_combination_of_correlated, indicated_polynomial_eq_foldAux', foldWordAux_poly_sum, indicated_polynomial_comp_x_k_natDegree, contradictory_hamming_dist_formula, correlated_agreement_implies_contradictory_hamm_dist, dist_from_code_bound_of_correlated_agreement, and folding_preserves_distance are updated accordingly, and the private lemmas roots_of_x_in_domain_eq, roots_of_x_in_domain_card, roots_of_x_in_domain_le_k, and roots_in_domain_card_eq_if_x_in_domain are removed. The theorem foldWord_k_1' and the lemma hammDist_foldWord_foldWord are added, although the latter contains a sorry filling the statement's proof.
• ArkLib/Data/CodingTheory/ProximityGap/Folding/ListDecodability.lean: This new file in the ProximityGap namespace adds three lemmas and a theorem about how the folding operation on codewords contracts block distances and preserves block-relation balls over Reed–Solomon codes. Specifically, folding_contracts_block_distance and folding_contracts_block_rel_distance (with signature δ𞁒(k-1, ω.subdomain 1, foldWord ω u 1 α, foldWord ω f 1 α) ≤ δ𞁒(k, ω, u, f)) show that the block distance and block-relative distance decrease by at least one when folding, assuming 1 ≤ k ≤ n, 2 ∣ n, NeZero n, and a field F of characteristic irrelevant. The lemma folding_block_rel_ball then proves that if a word u lies in the block-relation ball Λ𞁒(code ω n, k, ω, f, δ), then its fold foldWord ω u 1 α belongs to the corresponding ball for the subdomain code of dimension k-1. Finally, folding_preserves_block_balls is a set-inclusion theorem stating that the image of that full block-relation ball under the folding map is contained in the smaller ball. All statements are established under [NeZero n] (ensuring n ≠ 0), and the proofs use omega, aesop, and field arithmetic; no sorry or admit appears.
• ArkLib/Data/Domain/CosetFftDomain/Block.lean: This new file defines a block of a coset FFT domain at a point x, modeled after definition 4.16 of [ACFY24], and uses Finset F to collect y from the domain ω such that y ^ (2 ^ k) = x. A corresponding blockIdx is introduced as the set of indices i where (ω i) ^ (2 ^ k) = x. The file provides lemmas establishing membership criteria (mem_block, mem_blockIdx), cardinality bounds (card_block_le, card_blockIdx), disjointness of blocks and block indices for distinct points (disjoint_block, disjoint_blockIdx), an alternative characterization via nthRootsFinset (block_eq_nthRootsFinset), and special cases for x = 0 and k = 0 (block_x_0, blockIdx_x_0, block_k_1, blockIdx_k_1_of_eq, blockIdx_k_1_of_ne_mem). Under the smoothness condition that the domain is indexed by Fin (2 ^ n) and k ≤ n, it also proves that a block is closed under negation (neg_mem_block_of_mem, neg_mem_block_iff_mem).
• ArkLib/Data/Domain/CosetFftDomain/Mem.lean: Moved the Inhabited instances for ω.toFinset and ω into the CosetFftDomainClass section, removing their explicit ω binder to rely on the section parameter. Added a Decidable (x ∈ ω) instance inside the same section using decidable_of_iff with mem_toFinset_iff_mem, and removed the previous Decidable instance that was defined outside the section after end CosetFftDomain. The end CosetFftDomainClass was relocated to close after these new instances.
• ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean: This diff modifies ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean to rename card_roots to card_block_of_mem_subdomain, updating its statement to use block (subdomain ω i) j x instead of a filtered set, and adjusts root_exists accordingly. It adds a new lemma card_block_of_mem_subdomain' giving the cardinality of block ω k x for k ≤ n. It also adds subdomain_comp, which shows that subdomain (subdomain ω k) j a equals subdomain ω (k + j) i when a and i share the same underlying value, and mem_subdomain_comp_iff_mem, an iff theorem relating membership in the composed subdomain to membership in the (k+j)th subdomain. A new import for ArkLib.Data.Domain.CosetFftDomain.Block is added.
• ArkLib/Data/Domain/FftDomain/Mem.lean: The Decidable instance for x ∈ ω was moved from FftDomain to FftDomainClass and now uses CosetFftDomainClass.mem_toFinset_iff_mem instead of FftDomain.mem_toFinset_iff_mem. The original instance in FftDomain was removed. This makes membership decidable for all FFT domain classes, not just FftDomain.
• ArkLib/ProofSystem/Whir/BlockRelDistance.lean: Added a TODO comment at the top of the file, stating that the file is obsolete and should be deleted once the STIR/WHIR work is finished. No definitions, theorems, or sorry/admit were added or modified.

---

Last updated: 2026-07-09 10:00 UTC.

[alexanderlhicks]

AI-generated review. This review was produced by Codex and has not been written by a human reviewer. Findings were validated at exact head b0e333074acbf895a40d242741378057ff1e7715 using an isolated build, exact-head GitHub CI, Lean axiom audits, direct evaluation of the fold formula, and comparison with the paper.

Conclusion: changes are required; this draft cannot merge in its current form. The deterministic block-distance contraction is useful, and the four advertised Claim-4.22 declarations are axiom-clean when imported narrowly. However, the umbrella build fails, the PR adds a new false sorry-backed theorem, and the final ball statement does not have WHIR Claim 4.22's code parameters.

Validation performed

• lake build ArkLib/./scripts/validate.sh reached 4,050 preceding targets and then failed because the environment already contains BlockRelDistance.disagreementSet. GitHub's exact-head build independently reports the same duplicate declaration.
• Narrow #print axioms checks on folding_contracts_block_distance, folding_contracts_block_rel_distance, folding_block_rel_ball, and folding_preserves_block_balls reported no sorryAx; a separate newly added hammDist_foldWord_foldWord is closed by sorry.
• The Hamming lemma was falsified directly from this PR's own foldWord_k_1: for n = 2, α = 0, zero f, and g differing at one index in one fold pair over any valid odd-characteristic four-point domain (e.g. F_5), source Hamming distance is 1 and folded Hamming distance is 1, so the stated conclusion is 2 ≤ 1. Mathlib defines hammingDist as the cardinality of disagreeing indices, so there is no normalization that could rescue the inequality.
• Compared the ball statement with WHIR Claim 4.22, pp. 29–30: the paper maps RS[F,L,m] to RS[F,L^(2),m-1]; it does not identify m with domain log-size n, map n to n/2, or assume 2 ∣ n.

Required outcome

Rebuild this as a narrow Claim-4.22 change on #603: reuse its canonical block-distance module, remove the false Hamming lemma and spurious evenness condition, and quantify an independent code parameter m with source smoothCode ω m and target smoothCode (ω.subdomain 1) (m-1).

[alexanderlhicks]

AI-generated inline feedback — correctness/trust blocker. This statement is false as well as being closed by a new sorry. Validation: use n = 2, α = 0, f = 0, and let g differ from f at exactly one member of one binary fold pair over an odd-characteristic four-point domain (for example F_5). By foldWord_k_1 immediately above, that pair's folded value changes by 1/2, while every other output remains equal. Hence Δ₀(f,g)=1 and Δ₀(fold f,fold g)=1, making the conclusion 2 ≤ 1; 2 ∣ n is satisfied. WHIR Claim 4.22 needs block-distance contraction, not this raw Hamming claim. Please remove this lemma rather than trying to prove it.

[alexanderlhicks]

AI-generated inline feedback — reproducible build blocker. This duplicates BlockRelDistance.disagreementSet already imported from ProofSystem/Whir/BlockRelDistance.lean. Both isolated lake build ArkLib and the exact GitHub build stop with the same environment-already-contains error. Please rebase on #603 and import its canonical Data-layer declaration instead of introducing a second definition.

[alexanderlhicks]

AI-generated inline feedback — paper fidelity (blocking). Here n is the log-size of the evaluation domain, but it is also used as the RS degree parameter, and line 68 changes the target to n / 2. I checked WHIR Claim 4.22, pp. 29–30: one fold maps RS[F,L,m] (ordinary degree bound 2^m) to RS[F,L^(2),m-1] (bound 2^(m-1)) for an independent m. Please quantify m separately and state this using smoothCode ω m / smoothCode (ω.subdomain 1) (m-1), relying on the corrected Claim-4.15 bridge.

[alexanderlhicks]

AI-generated inline feedback — unnecessary hypothesis. I checked the proof body: hn_dvd : 2 ∣ n is unused, and no such restriction appears in WHIR Claim 4.22. Please remove it from both metric-contraction lemmas. The public [NeZero n] can also be derived locally from 1 ≤ k and k ≤ n, avoiding another redundant caller obligation.