Partial proof for weighted_correlated_agreement_over_affine_spaces

[aleph-prover]

⚠️ Your proof request could only be partially completed
Some theorems may only have informal proofs available.
Some hard-to-prove facts may have been replaced with axioms.

---

Proven lemmas: 13/16

The main goal is to prove a “weighted correlated agreement over affine spaces” theorem for Reed–Solomon codes: if a random point u in a certain affine subspace U has probability pr (both > ε and ≥ an explicit bound) of having weighted agreement ≥ α with some RS codeword, then all the generators u i are simultaneously close to some RS codewords v i on a common heavy set ι′ with μ-size ≥ α.

The proof has been decomposed into (i) an affine-line version of the theorem, (ii) a “direction lemma” showing that good average behavior on U forces every direction w′ in the direction submodule to have agree_set ≥ α, and (iii) a final assembly step that combines the direction lemma with a separate theorem that upgrades “all directions are good” into the full correlated-agreement conclusion on the whole affine space.

Progress-wise, most of the line-level and probabilistic plumbing is complete: the affine-line theorem is proved by specializing a known curve theorem, and the direction lemma is proved by finding a good parallel line, converting its parameter distribution to the polynomial-curve distribution, applying the line theorem, and then boosting pointwise equality on a heavy set into an agreement lower bound. In total, 13 of the 16 named sub-results compile; the remaining three are the big affine-space-from-directions theorem, a minimizer/bootstrap lemma for the minimum agreement α★ on U, and a weighted RS list-size bound lemma.

What remains is essentially the “Theorem 1.6 style” global argument: pick u★ ∈ U minimizing agree_set (so α★ is the worst agreement in U), list-decode around u★ to get only L < |F| candidate RS codewords, and use the affine-line theorem on lines through u★ to show U is covered by < |F| proper subspaces—forcing one subspace to be all of U and yielding the common ι′ and correlated v i.

The main current challenge is handling endpoint/parameter issues needed to apply the affine-line theorem at the threshold α★: the existing line lemma assumes α < 1, so one must either split into cases α★ = 1 vs α★ < 1 (using a lemma like agree_set ≤ 1) and/or prove auxiliary facts like errorBound α★ < 1 to discharge the “pr_line > ε★” hypothesis (since on those lines one often gets pr_line = 1). Another missing piece is the weighted RS list-size bound: the current placeholder references a non-existent library lemma, so it likely needs a real proof (e.g. reducing weighted agreement to an unweighted bound via the common denominator M, or locating the correct existing RS list-decoding statement in the library).

[github-actions]

🤖 Gemini PR Summary

Mathematical Formalization

This work advances the formalization of weighted correlated agreement over affine spaces for Reed–Solomon (RS) codes. The proof structure follows a three-part decomposition:

1. Affine-line version: Specializes existing polynomial curve theorems to affine lines.
2. Direction lemma: Demonstrates that favorable average behavior on an affine subspace $U$ implies that every direction in the associated submodule maintains a heavy agreement set.
3. Global assembly: Uses a "Theorem 1.6" style argument, employing list-decoding around an agreement minimizer to show the affine space is covered by a small number of candidate RS codewords.

Progress and Admitted Results

The implementation is partially complete, with 13 of 16 sub-results proven. Significant portions of the probabilistic plumbing and distribution conversions are finalized.

CRITICAL: The following components currently contain sorry placeholders or are unproven:

• weighted_correlated_agreement_over_affine_spaces: The primary theorem for affine spaces remains unfinished.
• Agreement Minimizer: The lemma establishing the existence/properties of the agreement minimizer $\alpha^*$ on $U$ is admitted.
• Weighted RS List-Size Bound: A placeholder exists for this lemma; it currently lacks a formal proof or a valid library reference.
• Endpoint Cases: Handling the $\alpha^* = 1$ boundary condition to satisfy the $\text{pr_line} &gt; \epsilon^*$ hypothesis is incomplete.

Structural Refactoring

The logic in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean has been refactored to decouple low-level probability theory—specifically uniform measures on subspaces—from high-level combinatorial properties of RS codes. This granularity is intended to better handle edge cases where agreement reaches its upper bound and to facilitate the eventual integration of missing list-decoding bounds.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	780
❌ Lines Removed	12

---

Lean Declarations

✏️ **Added:** 15 declaration(s)

• theorem weighted_RS_list_size_le_bound [DecidableEq ι] [Fintype ι] [DecidableEq F] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem Pr_uniform_translate_affineSubspace {ι F : Type} [Fintype ι] [Nonempty ι] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem exists_good_parallel_affine_line [DecidableEq ι] [Fintype ι] [DecidableEq F] {l : ℕ} {u : Fin (l + 2) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem agree_ge_mu_set_of_eq_on [DecidableEq ι] [Fintype ι] [DecidableEq F] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem mu_set_filter_pos_subset_of_subset_of_ge [DecidableEq ι] [Fintype ι] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem exists_equiv_polynomialCurveFinite_fin2_of_ne_zero [DecidableEq ι] [Fintype ι] [DecidableEq F] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem average_weighted_agreement_implies_agreement_of_affineSpan [DecidableEq ι] [Fintype ι] [DecidableEq F] {l : ℕ} {u : Fin (l + 2) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem Pr_uniform_bind_comm {α β : Type} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem pr_polynomialCurveFinite_fin2_eq_pr_param [DecidableEq ι] [Fintype ι] [DecidableEq F] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem weighted_affineSpace_min_agree_ge_alpha [DecidableEq ι] [Fintype ι] [DecidableEq F] {l : ℕ} {u : Fin (l + 2) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem mu_set_mono [DecidableEq ι] [Fintype ι] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem weighted_correlated_agreement_over_affine_spaces_of_direction [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem Pr_uniform_congr_equiv {α β : Type} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem weighted_correlated_agreement_affine_line [DecidableEq ι] [Fintype ι] [DecidableEq F] {u : Fin 2 → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem mem_polynomialCurveFinite_fin2_iff [DecidableEq ι] [Fintype ι] [DecidableEq F] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean

✏️ **Affected:** 1 declaration(s) (line number changed)

• theorem weighted_correlated_agreement_over_affine_spaces [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean moved from L786 to L1539

---

sorry Tracking

❌ **Added:** 3 `sorry`(s)

• theorem weighted_correlated_agreement_over_affine_spaces_of_direction [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean (L1537)
• theorem weighted_RS_list_size_le_bound [DecidableEq ι] [Fintype ι] [DecidableEq F] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean (L1318)
• theorem weighted_affineSpace_min_agree_ge_alpha [DecidableEq ι] [Fintype ι] [DecidableEq F] {l : ℕ} {u : Fin (l + 2) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean (L1493)

---

🎨 **Style Guide Adherence**

There are more than 20 style guide violations in this diff. They are grouped below by rule:

• Rule: "Empty Lines: Avoid empty lines inside definitions or proofs."

  • Count: 24 violations.
  • Representative Examples: Line 786, Line 815, Line 1264.

• Rule: "Functions: Prefer fun x ↦ ... over λ x, ...." (Note: The diff uses the => or , syntax instead of the preferred ↦ arrow).

  • Count: 42 violations.
  • Representative Examples: Line 791 (fun a b =>), Line 822 (fun a : α =>), Line 1102 (fun w =>).

• Rule: "Hypotheses: Prefer placing hypotheses to the left of the colon (e.g., (h : P) : Q) rather than using arrows (: P → Q) when the proof introduces them."

  • Count: 37 violations.
  • Representative Examples: Line 852 ((∀ x ∈ ι', u x = v x) → ...), Line 868 ((hα : sqrtRate < α) →), Line 1079 (s ⊆ t → ...).

• Rule: "Operators: Put spaces on both sides of :, :=, and infix operators. Place them before a line break rather than at the start of the next line."

  • Count: 62 violations (primarily missing spaces around : in binders and := in named arguments, as well as operators starting new lines).
  • Representative Examples:
    • Line 801 (Missing spaces in p := ...).
    • Line 822 (Missing space before : in a : α).
    • Line 1215 (Infix operator > placed at the start of the line).

• Rule: "Line Length: Keep lines under 100 characters."

  • Count: 5 violations.
  • Representative Examples: Line 818 (108 chars), Line 1282 (103 chars), Line 1302 (113 chars).

• Rule: "Naming Conventions: Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."

  • Count: 5 violations (due to capitalization or mixed camelCase).
  • Representative Examples: Line 784 (Pr_uniform_bind_comm), Line 838 (Pr_uniform_translate_affineSubspace), Line 1111 (pr_polynomialCurveFinite_fin2_eq_pr_param).

• Rule: "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)."

  • Count: 1 violation.
  • Example: Line 1184 (weighted_RS_list_size_le_bound should use rs or reed_solomon).

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean: This refactor expands the proof of weighted correlated agreement over affine spaces by introducing several probability lemmas for uniform measures and directional agreement on affine subspaces. It decomposes the primary theorem into a more granular sequence of lemmas, including list-decoding bounds and the existence of agreement minimizers, though several core components and the final result still contain sorry placeholders.

---

Last updated: 2026-03-10 06:35 UTC.

[quangvdao]

Closing: partial proof for weighted correlated agreement over affine spaces — large BCIKS20 patch with new sorrys/placeholders. Donor-only.