Folding Context PoC

[ElijahVlasov]

Folding context reduces the input complexity for the various folding lemmas.

A folding context is a triple of natural numbers k, d, n with the property 1 ≤ k ≤ d ≤ n. We're introducing grind/simp lemmas to simplify working with folding contexts.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Folding Context PoC

This PR introduces a new typeclass FoldingContext (and its variants) to package the constraints 1 ≤ k ≤ d ≤ n and provides a collection of simp/grind-tagged lemmas that automatically discharge the arithmetic inequalities required by the folding lemmas in the proximity‑gap hierarchy. The existing proofs in Folding.lean and ListDecodability.lean are refactored to use the new typeclass, simplifying their hypotheses and reducing manual case‑analysis. Two minor additions in the CosetFftDomain files (a cardinality lemma and a warning suppression) are also included.

Mathematical Formalization

• New file ArkLib/Data/CodingTheory/ProximityGap/Folding/FoldingContext.lean defines four typeclasses:
  • FoldingContextLeft k d – requires 1 ≤ k ≤ d
  • FoldingContextRight d n – requires 1 ≤ d ≤ n
  • FoldingContextMiddle k n – requires 1 ≤ k ≤ n
  • FoldingContext k d n – requires 1 ≤ k ≤ d ≤ n; derives FoldingContextMiddle.
    Utility constructors (mk', ofMiddle, oneStep) and a large set of simp/grind lemmas (e.g., k_sub_one_le_n_sub_one, two_pow_k_le_two_pow_n, n_sub_k_add_k, pow_2_d_sub_k_mul_pow_2_k, pow_2_k_mul_le_pow_2_d_iff, n_sub_1_sub_k_sub_1_eq_n_sub_k) are provided. These lemmas automate the arithmetic identities and inequalities needed by downstream folding proofs.

Refactoring

• ArkLib/Data/CodingTheory/ProximityGap/Folding.lean – The following theorems now use FoldingContext (or FoldingContextMiddle, FoldingContextLeft) in place of separate explicit hypotheses hk : k ≤ n, hkd : 2 ^ k ∣ d, hd0 : 0 < d, h_d_n : d ≤ 2 ^ n:

  • interpolate_eq_folding_poly_eval
  • foldWord_codeword
  • foldWord_evalOnPoints
  • foldWord_mem_code_of_mem_code (the proof no longer contains a case split on hd : d = 0)
  • contradictory_hamming_dist_formula
  • correlated_agreement_implies_contradictory_hamm_dist
  • dist_from_code_bound_of_correlated_agreement
  • folded_rate_eq
  • folded_sqrtRate_eq
  • folding_preserves_distance
    All code‑dimension parameters are converted from d (or d / (2 ^ k)) to 2 ^ d (or 2 ^ (d - k)). Proofs are simplified by using the typeclass to derive needed inequalities.

• ArkLib/Data/CodingTheory/ProximityGap/Folding/ListDecodability.lean – The four lemmas folding_contracts_block_distance, folding_contracts_block_rel_distance, folding_block_rel_ball, and folding_preserves_block_balls (claim 4.22 of [ACFY24]) are refactored to use FoldingContext / FoldingContextMiddle hypotheses, replacing explicit hk : 1 ≤ k, hkn : k ≤ n, hd : k ≤ d. Internal arithmetic reasoning is updated to use the typeclass‑provided lemmas (e.g., FoldingContext.n_sub_1_sub_k_sub_1_eq_n_sub_k, FoldingContext.oneStep), and some omega/aesop tactics are replaced with grind/simp. The statements of the theorems are unchanged.

• ArkLib.lean – Adds an import of ArkLib.Data.CodingTheory.ProximityGap.Folding.FoldingContext to make the new module available via the top‑level ArkLib import.

Supporting Infrastructure

• ArkLib/Data/Domain/CosetFftDomain/Mem.lean – Adds lemma card_toFinset_le_fintype_card (marked @[simp high]) stating Finset.card (toFinset ω) ≤ Fintype.card F for any ω with Fintype ι and DecidableEq F. This supports reasoning about finiteness of coset FFT domains.

• ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean – Adds set_option warning.simp.varHead false immediately before the @[simp] theorem mem_subdomain_comp_iff_mem to suppress a simp variable‑head warning.

No sorry or admit placeholders are introduced anywhere in this PR.

---

Statistics

Metric	Count
📝 Files Changed	6
✅ Lines Added	405
❌ Lines Removed	185

---

Lean Declarations

✏️ Removed: 1 declaration(s)

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

• private lemma folded_rate_div_eq_helper {d : ℕ}

✏️ Added: 23 declaration(s)

ArkLib/Data/CodingTheory/ProximityGap/Folding/FoldingContext.lean (22)

• def mk' {k d n : ℕ} (h_k_ge_1 : 1 ≤ k) (h_k_le_d : k ≤ d)
• def ofMiddle {k n : ℕ} [FoldingContextMiddle k n] : FoldingContext k n n where
• def oneStep {k d n : ℕ} [FoldingContext k d n] : FoldingContext 1 d n where
• lemma d_sub_k_add_k {k d : ℕ} [FoldingContextLeft k d] :
• lemma d_sub_k_add_n {k d n : ℕ} [FoldingContext k d n] :
• lemma k_sub_one_le_n_sub_one {k d n : ℕ} [FoldingContext k d n] :
• lemma min_pow_2_d_pow_2_n {d n : ℕ} [FoldingContextRight d n] :
• lemma n_sub_1_sub_k_sub_1_eq_n_sub_k {k n : ℕ} [FoldingContextMiddle k n] :
• lemma n_sub_k_add_d {k d n : ℕ} [FoldingContext k d n] :
• lemma n_sub_k_add_k {k n : ℕ} [FoldingContextMiddle k n] :
• lemma one_add_sub_one {k d : ℕ} [FoldingContextLeft k d] :
• lemma one_add_sub_one' {k n : ℕ} [FoldingContextMiddle k n] :
• lemma pow_2_d_sub_k_mul_pow_2_k {A : Type*} [Monoid A] [OfNat A 2]
• lemma pow_2_k_mul_le_pow_2_d_iff {A : Type*} [Monoid A] [LinearOrder A] [MulLeftMono A]
• lemma pow_2_k_mul_le_pow_2_d_of {A : Type*} [Monoid A] [LinearOrder A] [MulLeftMono A] [OfNat A 2]
• lemma pow_2_k_mul_pow_2_d_sub_k {A : Type*} [Monoid A] [OfNat A 2]
• lemma pow_2_n_sub_1_sub_k_sub_1_eq_n_sub_k
• lemma pow_2_n_sub_k_eq_n_sub_k
• lemma two_pow_d_le_two_pow_n
• lemma two_pow_d_sub_k_le_two_pow_n_sub_k
• lemma two_pow_k_le_two_pow_d
• lemma two_pow_k_le_two_pow_n

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

• lemma card_toFinset_le_fintype_card [Fintype F] [Fintype ι] [DecidableEq F] :

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

• lemma folded_rate_eq {d : ℕ} [FoldingContext k d n] : in ArkLib/Data/CodingTheory/ProximityGap/Folding.lean moved from L766 to L726
• lemma folded_sqrtRate_eq {d : ℕ} [FoldingContext k d n] : in ArkLib/Data/CodingTheory/ProximityGap/Folding.lean moved from L797 to L740
• theorem foldWord_codeword {d : ℕ} [FoldingContext k d n] in ArkLib/Data/CodingTheory/ProximityGap/Folding.lean moved from L345 to L346
• theorem foldWord_evalOnPoints [FoldingContextMiddle k n] in ArkLib/Data/CodingTheory/ProximityGap/Folding.lean moved from L359 to L359
• theorem foldWord_mem_code_of_mem_code {d : ℕ} [FoldingContext k d n] in ArkLib/Data/CodingTheory/ProximityGap/Folding.lean moved from L372 to L374
• lemma folding_block_rel_ball {d : ℕ} [FoldingContext k d n] in ArkLib/Data/CodingTheory/ProximityGap/Folding/ListDecodability.lean moved from L84 to L81
• lemma folding_contracts_block_distance [FoldingContextMiddle k n] in ArkLib/Data/CodingTheory/ProximityGap/Folding/ListDecodability.lean moved from L38 to L39
• lemma folding_contracts_block_rel_distance [FoldingContextMiddle k n] in ArkLib/Data/CodingTheory/ProximityGap/Folding/ListDecodability.lean moved from L68 to L67
• theorem folding_preserves_block_balls {d : ℕ} [FoldingContext k d n] {α : F} {δ : ℝ≥0} : in ArkLib/Data/CodingTheory/ProximityGap/Folding/ListDecodability.lean moved from L107 to L101

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The diff introduces a FoldingContext typeclass hierarchy to carry the constraints 1 ≤ k ≤ d ≤ n and refactors several theorems to use it, simplifying signatures and proofs. The changes are largely in line with the project's style, but several violations of the style guide and potential issues are noted below.

---

📄 **Per-File Summaries**

• ArkLib.lean: Added an import of ArkLib.Data.CodingTheory.ProximityGap.Folding.FoldingContext to ArkLib.lean. This makes the FoldingContext module available as part of the ArkLib top‑level import, presumably because it defines types or structures (such as a folding context) that are used elsewhere in the proximity‑gap or folding hierarchy.
• ArkLib/Data/CodingTheory/ProximityGap/Folding.lean: The file replaces explicit hypotheses hk : k ≤ n, hkd : 2 ^ k ∣ d, hd0 : 0 < d, h_d_n : d ≤ 2 ^ n with the typeclass FoldingContext k d n (or FoldingContextMiddle k n, FoldingContextLeft k d) in interpolate_eq_folding_poly_eval, foldWord_codeword, foldWord_evalOnPoints, foldWord_mem_code_of_mem_code, contradictory_hamming_dist_formula, correlated_agreement_implies_contradictory_hamm_dist, dist_from_code_bound_of_correlated_agreement, folded_rate_eq, folded_sqrtRate_eq, and folding_preserves_distance. All code‑dimension parameters are converted from d (or d / (2 ^ k)) to 2 ^ d (or 2 ^ (d - k)), and the proofs are simplified by using the typeclass to derive the needed inequalities. The proof of foldWord_mem_code_of_mem_code no longer contains a case split on hd : d = 0. No sorry or admit are added.
• ArkLib/Data/CodingTheory/ProximityGap/Folding/FoldingContext.lean: This file introduces four new type classes—FoldingContextLeft k d, FoldingContextRight d n, FoldingContextMiddle k n, and FoldingContext k d n—that package the inequalities 1 ≤ k ≤ d ≤ n (or subsets thereof) and derive FoldingContextMiddle from FoldingContext. It provides several utility constructions (mk', ofMiddle, oneStep) and a large collection of simp/grind-tagged lemmas (e.g., k_sub_one_le_n_sub_one, two_pow_k_le_two_pow_n, n_sub_k_add_k, pow_2_d_sub_k_mul_pow_2_k, pow_2_k_mul_le_pow_2_d_iff, and n_sub_1_sub_k_sub_1_eq_n_sub_k) that automatically discharge arithmetic identities and inequalities needed by downstream folding proofs. No sorry or admit is present.
• ArkLib/Data/CodingTheory/ProximityGap/Folding/ListDecodability.lean: This diff refactors the four folding/decodability lemmas in ListDecodability.lean (claim 4.22 of [ACFY24]) to use the newly-introduced FoldingContext / FoldingContextMiddle typeclass hypotheses, replacing the previous explicit hypotheses like hk : 1 ≤ k, hkn : k ≤ n, and hd : k ≤ d; correspondingly, the setup arithmetic inside the proofs is simplified by invoking typeclass-provided lemmas (e.g. FoldingContext.n_sub_1_sub_k_sub_1_eq_n_sub_k, FoldingContext.oneStep), and some omega/aesop tactics are replaced with grind/simp calls. The declarations affected are folding_contracts_block_distance, folding_contracts_block_rel_distance, folding_block_rel_ball, and folding_preserves_block_balls; the statements (the block-distance and block-relative-distance contraction inequalities and the preservation of block-relative balls under foldWord) are otherwise unchanged. The diff also adds an import of ProximityGap/Folding/FoldingContext. No sorry or admit appears in the diff.
• ArkLib/Data/Domain/CosetFftDomain/Mem.lean: Added lemma card_toFinset_le_fintype_card (decorated @[simp high]), which states that Finset.card (toFinset ω) ≤ Fintype.card F for any ω with Fintype ι and DecidableEq F. The proof is Finset.card_le_card (by simp). This provides a useful bound on the size of the image set relative to the field, supporting reasoning about coset FFT domain finiteness. No other changes, sorries, or renames.
• ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean: Added set_option warning.simp.varHead false immediately before the @[simp] theorem mem_subdomain_comp_iff_mem, suppressing a simp variable-head warning for that declaration. No other theorems, definitions, or signatures were changed; no sorry or admit were introduced.

---

Last updated: 2026-08-06 15:07 UTC.

[github-actions]

Build Timing Report

• Commit: 135bfc5
• Message: Folding Context PoC
• Ref: ElijahVlasov/folding-context
• Comparison baseline: 3aad40c from the previous successful PR update.
• 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	862.44	895.04	+32.60	ok
Warm rebuild	2.42	2.44	+0.02	ok
Validation wrapper	2.58	2.51	-0.07	ok

Incremental Rebuild Signal

• Warm rebuild saved 892.60s vs clean (366.82x 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
122.00	127.00	-5.00	ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Weight.lean
76.00	72.00	+4.00	ArkLib/ProofSystem/Stir/Combine.lean
74.00	58.00	+16.00	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
66.00	55.00	+11.00	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
64.00	59.00	+5.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean
56.00	49.00	+7.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
49.00	53.00	-4.00	ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean
48.00	45.00	+3.00	ArkLib/Data/CodingTheory/ProximityGap/Folding.lean
42.00	41.00	+1.00	ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean
41.00	43.00	-2.00	ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean
40.00	38.00	+2.00	ArkLib/OracleReduction/LiftContext/Reduction.lean
38.00	27.00	+11.00	ArkLib/Data/CodingTheory/PolishchukSpielman/Existence.lean
38.00	36.00	+2.00	ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean
37.00	35.00	+2.00	ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
36.00	31.00	+5.00	ArkLib/OracleReduction/Security/RoundByRound.lean
36.00	24.00	+12.00	ArkLib/Data/CodingTheory/DivergenceOfSets.lean
36.00	24.00	+12.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/JointAgreement.lean
35.00	33.00	+2.00	ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Hensel.lean
33.00	33.00	+0.00	ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
32.00	28.00	+4.00	ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean