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: 9/10

The main goal is to prove a weighted correlated-agreement theorem over affine spaces: if a random point x in the affine space generated by u has probability pr above an explicit threshold, and α is at least sqrtRate·(1 + 1/(2m)) (with α < 1), then there exist Reed–Solomon codewords v (one for each generator index) such that the set of coordinates i where all u j i match v j i has μ-measure ≥ α. The proof has been decomposed into a “wrapper” theorem that simply instantiates a more direct core lemma, plus several supporting lemmas about (i) monotonicity of μ-measure over sets, (ii) rewriting uniform probabilities as counting ratios, and (iii) basic bounds like agree_set ≤ 1. Most of these supporting pieces are finished: the monotonicity lemma, the probability-as-cardinality lemma, and the agreement ≤ 1 lemmas are all proved, and the wrapper theorem reduces the original statement to the core affine-space lemma.

At this point, all remaining work is concentrated in one missing central lemma: turning the lower bound on the density of “good” points in the affine space (those with agree_set ≥ α) into the existence of the global witness v. The intended strategy is the BCIKS20 §6.3/§7.3 reduction: use a pigeonhole/quotient argument to find a line with many good points, apply the (already planned) line/curve correlated-agreement theorem on that line, then run a minimizer + list-size bound + affine-subspace cover argument and finally a finite-geometry “< |F| proper subspaces can’t cover U” contradiction to force one subspace to equal the whole U. The main challenge is that this “minimizer/list/cover lift” is substantial combinatorial geometry and is not yet available as a packaged lemma in the current library, so the nontrivial-direction case (U.direction ≠ ⊥) is where the proof is stuck. In terms of subproblems, the project is essentially “almost done except for the hard core”: many auxiliary lemmas are complete, the top-level reduction compiles, but 1 key theorem (the combinatorial lift from density to a global v) remains to be proved.

[github-actions]

🤖 Gemini PR Summary

Summary

Formalization of the weighted correlated-agreement (WCA) theorem over affine spaces, a result used in proximity gap analysis for Reed–Solomon codes (BCIKS20 framework). The proof establishes that if a subset of points in an affine space has a measure exceeding a specific threshold, there exist global Reed–Solomon codewords matching the generators across a significant portion of coordinates.

Mathematical Formalization

• WCA over Affine Spaces: Formalizes the statement for weighted_correlated_agreement_over_affine_spaces'. It reduces the top-level theorem to a core affine-space lemma via a "wrapper" pattern.
• Geometric & Combinatorial Lemmas:
  • Monotonicity of $\mu$-measure over sets.
  • Translation of uniform probabilities into counting ratios.
  • Basic bounds for agreement sets (e.g., agree_set ≤ 1).
  • Logic for finite-geometry contradictions, specifically that a finite number of proper subspaces cannot cover a space $U$.
• Data Structures: Updates BCIKS20.lean with definitions for weighted agreements and geometric properties required for Reed–Solomon proximity gaps.

Proof Status & Critical Missing Components

• Current Progress: 9 out of 10 targeted lemmas are complete.
• CRITICAL: The central combinatorial lift theorem, wca_ratio_bound_implies_exists_v, contains a sorry.
• Remaining Work: The proof is incomplete for the non-trivial case where the affine space direction is not bottom (U.direction ≠ ⊥). This requires implementing the "minimizer/list/cover lift" strategy—lifting local density on lines to a global witness $v$—which involves substantial combinatorial geometry not yet fully formalized.

Logic Structure

• Theorem Decomposition: Separates the high-level API from core combinatorial arguments.
• Pigeonhole/Quotient Strategy: The framework is prepared to use a pigeonhole argument on lines to find "good" points, though the final lifting steps remain unfinished.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	536
❌ Lines Removed	20

---

Lean Declarations

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

• theorem mu_set_mono [Fintype ι] [DecidableEq ι] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem weighted_correlated_agreement_over_affine_spaces'_direct [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• def WCA_affineSpace {F ι : Type} [Field F] [DecidableEq F] [Fintype ι] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem wca_exists_eq_of_cover_lt_fieldCard {F V : Type} [Field F] [Fintype F] [DecidableEq F] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem sum_ite_const_eq_card_subtype_mul {α : Type} [Fintype α] (P : α → Prop) [DecidablePred P] (c : ENNReal) : in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem agree_set_le_one {ι F : Type} [Fintype ι] [Nonempty ι] [DecidableEq ι] [Field F] [DecidableEq F] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• def WCA_good {F ι : Type} [Field F] [Fintype F] [DecidableEq F] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem pr_uniformOfFintype_eq_card {α : Type} [Fintype α] [Nonempty α] (P : α → Prop) [DecidablePred P] : in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem wca_exists_base_with_many_good_on_line {F V : Type} [Field F] [Fintype F] [DecidableEq F] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• instance instNonempty_WCA_affineSpace {F ι : Type} [Field F] [DecidableEq F] [Fintype ι] in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem wca_ratio_bound_implies_exists_v [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean
• theorem agree_le_one {ι F : Type} [Fintype ι] [Nonempty ι] [DecidableEq ι] [Field F] [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 L822 to L1333

---

sorry Tracking

✅ **Removed:** 1 `sorry`(s)

• 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 (L842)

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

• theorem wca_ratio_bound_implies_exists_v [DecidableEq ι] [Fintype ι] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean (L1272)

---

🎨 **Style Guide Adherence**

There are more than 20 violations in this diff. Grouped by rule:

• Avoid empty lines inside definitions or proofs (48 violations)

  • Line 830: Empty line inside the proof of agree_le_one.
  • Line 931: Empty line inside the proof of wca_exists_base_with_many_good_on_line.
  • Line 1111: Empty line inside the proof of wca_exists_eq_of_cover_lt_fieldCard.

• Variable Conventions: u, v, w for universes and α, β, γ for generic types (12 violations)

  • Line 819: u is used for a function (term) instead of a universe.
  • Line 933: α is used for a specific subtype instead of a generic type.
  • Line 1133: v is used for a function (term) instead of a universe.

• Naming Conventions: lowerCamelCase for functions/terms, snake_case for theorems, and acronyms as words (7 violations)

  • Line 1 (File path): BCIKS20.lean violates "Acronyms: Treat as words" (should be Bciks20.lean).
  • Line 818: def WCA_affineSpace violates lowerCamelCase and acronym word treatment (should be wcaAffineSpace).
  • Line 915: theorem pr_uniformOfFintype_eq_card violates snake_case.

• Theorem Naming Logic: Avoid ≥ and > in theorem statements (6 violations)

  • Line 926: Hypothesis hGood uses >.
  • Line 1124: Hypothesis uses >.
  • Line 1195: Hypothesis uses >.

• Keep lines under 100 characters (3 violations)

  • Line 926: This line exceeds 100 characters (120 chars).
  • Line 1134: This line exceeds 100 characters (124 chars).
  • Line 1147: This line exceeds 100 characters (117 chars).

• Inequalities with Bottom/Top: In assumptions, use x ≠ ⊥ (3 violations)

  • Line 1121: Hypothesis uses (0 : ℝ≥0) < sr instead of sr ≠ 0.
  • Line 1146: Hypothesis uses (0 : ℝ≥0) < sr instead of sr ≠ 0.
  • Line 1185: Hypothesis uses (0 : ℝ≥0) < sr instead of sr ≠ 0.

• Use the where syntax for defining instances (1 violation)

  • Line 878: instance instNonempty_WCA_affineSpace uses := by instead of the where syntax.

• Manual dot notation for logical connectives (1 violation)

  • Line 988: Uses .2 on an Iff result instead of manual dot notation (e.g., Iff.mpr).

• Avoid parentheses where possible (1 violation)

  • Line 1201: The function call is wrapped in unnecessary parentheses.

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20.lean: This PR introduces several new definitions and auxiliary theorems to formalize weighted correlated agreement (WCA) over affine spaces, including geometric lemmas for affine subspace covers and pigeonhole arguments on lines. It refines the statement of weighted_correlated_agreement_over_affine_spaces' with specific mathematical bounds and adds a core combinatorial lift theorem, wca_ratio_bound_implies_exists_v, which currently contains a sorry placeholder.

---

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

[quangvdao]

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