Block Relative distance refactor + proofs

[ElijahVlasov]

Improvements to Block Relative distance stuff + proof of the lemma 4.19 from the WHIR paper.

[ElijahVlasov]

To be reviewed after #599

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Block Relative distance refactor + proofs

This PR refactors the block relative distance module, moves deprecated code to an Obsolete namespace, and proves Claim 4.19 from the WHIR paper [ACFY24]. The core new definitions and lemmas are in BlockRelDistance.lean; other files are updated to support the refactor or expose the Obsolete namespace. No sorry or admit placeholders are introduced.

---

Statistics

Metric	Count
📝 Files Changed	6
✅ Lines Added	321
❌ Lines Removed	18

---

Lean Declarations

✏️ Removed: 5 declaration(s)

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

• lemma blockIdx_k_1_of_eq {i : ι} (hi : ω i = x) :
• lemma blockIdx_k_1_of_ne_mem (hx : x ∉ ω) :
• lemma block_k_1 :
• lemma block_x_0 :
• lemma card_block_le :

✏️ Added: 34 declaration(s)

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

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

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

• lemma blockIdx_k_0_of_eq {i : ι} (hi : ω i = x) :
• lemma blockIdx_k_0_of_ne_mem (hx : x ∉ ω) :
• lemma block_card_le :
• lemma block_k_0 :
• theorem disjoint_block {x y : F} (hxy : x ≠ y) :
• theorem disjoint_blockIdx {x y : F} (hxy : x ≠ y) :

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff introduces a new file BlockRelDistance.lean and modifies several other files to integrate it. The instructions provided for review (the

---

📄 **Per-File Summaries**

• ArkLib.lean: Added import of ArkLib.Data.CodingTheory.Basic.BlockRelDistance, which introduces definitions and theorems related to block relative distance in coding theory, expanding the framework's coverage of distance metrics.
• ArkLib/Data/CodingTheory/Basic/BlockRelDistance.lean: Creates ArkLib/Data/CodingTheory/Basic/BlockRelDistance.lean to define the core quantities and lemmas for block relative distance, following Definition 4.17 and Claim 4.19 of [ACFY24]. The file introduces disagreementSet (the set of subdomain elements whose block contains a pointwise disagreement between two functions), blockDistance (its cardinality), and blockRelDistance (the ratio to the size of the subdomain), along with scoped notations Δ𞁒 and δ𞁒. It also defines blockDistanceFromCode / blockRelDistanceFromCode (distances to a code) and blockRelDistanceBall (the list of codewords within a given δ, with notation Λ𞁒). Supporting lemmas are provided: card_disagreementSet_le (bound by subdomain size), disagreementSet_k_0 and disagreementSet_k_0_eq_image (specialization at k=0), and blockDistance_eq_hammingDist_k_0 / blockRelDistance_eq_relHammingDist_k_0 (simplification to standard Hamming distance/relative distance when k=0). The key result relHammingDist_le_blockRelDistance (Claim 4.19, Part 1) establishes that the standard relative Hamming distance δᵣ(f,g) lower-bounds the k-wise block relative distance, and listBlock_subset_listHamming (Claim 4.19, Part 2) deduces the corresponding inclusion of proximity balls. A private section defines complDisagreementSet, agreementBlockUnion, and proves auxiliary properties card_agreementBlockUnion, relHammingDist_le_sub_agreementBlockUnion, and blockRelDistance_eq_one_sub used in the main proof.
• ArkLib/Data/Domain/CosetFftDomain/Block.lean: The diff modifies ArkLib/Data/Domain/CosetFftDomain/Block.lean with several changes. The docstring for block is corrected to say 2^kth roots instead of kth roots. The lemma block_x_0 (stating block ω k 0 = ∅) is removed. The lemma block_k_1 is renamed to block_k_0 and its statement is unchanged. The lemma card_block_le is renamed to block_card_le. The aesop proof of block_eq_nthRootsFinset is simplified by removing the (add unsafe cases Nat) clause. Two new theorems are added: disjoint_block, which states that blocks for different points x ≠ y are disjoint, and disjoint_blockIdx, which states that the corresponding index sets are also disjoint. The lemmas blockIdx_k_1_of_eq and blockIdx_k_1_of_ne_mem are renamed to blockIdx_k_0_of_eq and blockIdx_k_0_of_ne_mem, respectively, with no change in their statements.
• ArkLib/ProofSystem/Whir/BlockRelDistance.lean: The file now wraps its entire existing content (from the open statements through the listBlock_subset_listHamming lemma) inside a new inner namespace Obsolete within BlockRelDistance. This deprecates those definitions and lemmas, changing their fully qualified names (e.g., BlockRelDistance.Obsolete.listBlock_subset_listHamming) and breaking any code that imports them directly. No other changes were made.
• ArkLib/ProofSystem/Whir/Folding.lean: Added Obsolete to the open block, making an Obsolete namespace available in the Fold namespace. No definitions, theorems, or other declarations were added, removed, or modified; the file contains no sorry or admit.
• ArkLib/ProofSystem/Whir/RBRSoundness.lean: Opened the Obsolete namespace in WhirIOP.

The diff adds Obsolete to the open clause of the WhirIOP namespace to bring that module's definitions into scope. This is the only change — no theorems, definitions, or structures were added, modified, or removed, and no sorry or admit was introduced.

---

Last updated: 2026-07-17 16:21 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 b28cb192bb62f6a674489296dae282524ecca4ef against the source paper, Lean's axiom output, repository builds, current consumers, and exact-head CI logs.

Conclusion: the mathematics is strong, but integration changes are needed before landing. The new Data-layer definitions faithfully capture WHIR Definitions 4.16–4.18 and Claim 4.19, pp. 27–28. Both Claim 4.19 conclusions are fully proved and axiom-clean. This is the strongest complete paper result in this four-PR series.

Validation performed

• lake build ArkLib completed all 4,110 jobs at this exact SHA. ./scripts/validate.sh exited only for the inherited missing NOZ26 BibTeX key, not a Lean failure.
• #print axioms BlockRelDistance.relHammingDist_le_blockRelDistance and #print axioms BlockRelDistance.listBlock_subset_listHamming reported no sorryAx.
• Statement-by-statement comparison checked block fibers, normalization by |L^(2^k)|, the block ball, Hamming lower bound, and list inclusion against WHIR 4.16–4.19.
• GitHub's exact website job was inspected: this PR causes missing links for BlockRelDistance.block, BlockRelDistance.minBlockRelDistance, and BlockRelDistance.listBlockRelDistance; SendClaim.completeness in the same job is inherited.
• Current WHIR consumers were searched: ProofSystem/Whir/Folding.lean and RBRSoundness.lean still explicitly use the quarantined Obsolete API. A synthetic current-main + #603 + #657 stack builds (4,128 jobs), so #657 is compatible with the proposed canonical layer.

Required outcome

1. Preserve compatibility aliases (or provide a documented migration) for renamed domain declarations.
2. Migrate/bridge the old WHIR consumers instead of leaving the proved API as a parallel island.
3. Repair the three stale blueprint declaration links and run ./scripts/validate.sh --site.
4. Describe the smooth-code-free metric as an intentional generalization of the paper's constrained-RS presentation.

[alexanderlhicks]

AI-generated inline feedback — compatibility. The corrected k = 0 names are mathematically better, but diff/API inspection confirms that this PR removes block_k_1, card_block_le, blockIdx_k_1_of_eq, blockIdx_k_1_of_ne_mem, and block_x_0. Please keep deprecated aliases for the renamed declarations and retain the useful zero-block theorem for a migration window. This is particularly important because the related #616 head and existing WHIR work use the prior surface.

[alexanderlhicks]

AI-generated inline feedback — canonical ownership. I validated usages with a repository-wide search: ProofSystem/Whir/Folding.lean explicitly opens this Obsolete namespace, and RBRSoundness.lean continues to depend on its indexPowT/ball semantics and gap-backed results. Please add a concrete bridge or migrate those consumers in this PR (or link a scoped, blocking follow-up with the exact declarations to replace). Otherwise the faithful, proved WHIR 4.16–4.19 API is not yet advancing the proof-system formalization that consumes it.

[alexanderlhicks]

AI-generated inline feedback — source attribution. I checked WHIR Definitions 4.17–4.18, p. 27: the paper presents these notions for a constrained Reed–Solomon code, whereas this Lean definition validly generalizes away from the unused code parameter to any smooth domain/words. Please describe that as an intentional generalization, not as what the paper itself does. A short note explaining how the paper instance is recovered would make the fidelity boundary explicit.