AffineGeneratorsWithMCA

[katyhr]

No description provided.

[github-actions]

🤖 PR Summary

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

The overview must be self-contained, surface any sorry/admit, and evaluate the PR body against the per-file summaries.

---

Statistics

Metric	Count
📝 Files Changed	7
✅ Lines Added	427
❌ Lines Removed	18

---

Lean Declarations

✏️ Added: 15 declaration(s)

ArkLib/Data/CodingTheory/Basic/LinearCode.lean (1)

• def projectedCode_submod

ArkLib/Data/CodingTheory/Prelims.lean (3)

• abbrev affineComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (x : Fin s → F) : ι → F
• abbrev linComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (l : Fin s → F) : ι → F
• lemma affineComb_line {s : ℕ} (U : Fin (s + 1) → (ι → F)) (v lam : Fin s → F) (t : F) :

ArkLib/Data/CodingTheory/ProximityGap/AffineGenerator.lean (8)

• abbrev projectedQuotient [Fintype ι] (LC : LinearCode ι F) (T : Finset ι) : Type
• lemma exists_avg_le [Fintype F] {s : ℕ} (hs : 1 ≤ s) (f : (Fin s → F) → ℕ) (m : ℕ)
• lemma exists_dir_line_ge [Fintype F] [Nonempty F] {s : ℕ}
• lemma exists_line_bound [Fintype F] [Fintype ι] {s : ℕ} (hs : 1 ≤ s)
• lemma exists_succ_not_mem [Fintype ι] {s : ℕ} (LC : LinearCode ι F) (T : Finset ι)
• lemma line_vecMul (W : Fin 2 → (ι → F)) (t : F) :
• lemma proj_lincomb_ker_card_le [Fintype F] [Fintype ι] {s : ℕ}
• theorem AffineLine_MCA_AffineSpaceMCA {ℓ : ℕ} (hℓ : ℓ ≥ 2) (ε_mca : I → ℝ) (LC : LinearCode ι F)

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

• abbrev AffineLineGenerator (F : Type) [Field F] : Generator F (Fin 2) F
• abbrev AffineSpaceGenerator (F : Type) [Field F] (ℓ : ℕ) : Generator (Fin ℓ → F) (Fin (ℓ + 1)) F

ArkLib/Data/Probability/Instances.lean (1)

• theorem prob_uniform_eq_ofReal {F : Type} [Fintype F] [Nonempty F]

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

• lemma generatorSubset [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → ℝ) (LC : LinearCode ι F) in ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean moved from L109 to L109
• lemma pseudoinverseGen [DecidableEq ℓ'] [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → ℝ) in ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean moved from L58 to L58
• def IsMCAGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_mca : I → ℝ) in ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean moved from L98 to L101

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

• Missing docstring for projectedCode_submod.
• projectedCode_submod uses snake_case; should be lowerCamelCase (e.g., projectedCodeSubmod).
• projectedQuotient abbreviation begins with lowercase; should be UpperCamelCase.
• Blank lines inside projectedCode_submod definition violate style guide.
• Removal of notation c|"[T]" and C|"[T]" without deprecation may break downstream code.
• Possible unused imports in AffineGenerator.lean: Mathlib.Algebra.Azumaya.Basic, Mathlib.Algebra.Ring.IsFormallyReal, Mathlib.AlgebraicTopology.SimplexCategory.Basic, Mathlib.Data.Int.Star, Mathlib.FieldTheory.Finiteness, Mathlib.RingTheory.Flat.TorsionFree.
• Reference URL in AffineGenerator.lean has a stray closing brace: }https://eprint.iacr.org/2025/2051}

---

📄 **Per-File Summaries**

• ArkLib.lean: Added an import of ArkLib.Data.CodingTheory.ProximityGap.AffineGenerator to the file's collection of imports. This makes the module and any definitions, theorems, or structures it contains available for use in the current file and the rest of the project, expanding the accessible formalization in the coding theory proximity gap area without introducing any new code or sorry/admit in this file.
• ArkLib/Data/CodingTheory/Basic/LinearCode.lean: Removed the c|["T"] and C|["T"] notation for projectedWord and projectedCode, respectively, requiring explicit function calls. Updated the definition of projectedCode to use projectedWord directly instead of the removed notation. Added a new definition projectedCode_submod that constructs a Submodule F (T → F) from projectedCode, with proofs of zero_mem', add_mem', and smul_mem'.
• ArkLib/Data/CodingTheory/Prelims.lean: Adds the abbreviations affineComb (the affine combination of codewords U at seed x, defined as Matrix.vecMul (Fin.cons 1 x) U) and linComb (the linear combination of direction codewords, ∑ i, l i • U i.succ) for use in affine-space coding theory. Also adds the lemma affineComb_line, which shows that affineComb U (v + t • lam) = affineComb U v + t • (linComb U lam), relating affine combinations along a line to a base affine combination plus a scaled linear combination.
• ArkLib/Data/CodingTheory/ProximityGap/AffineGenerator.lean: This new file adds lemmas and a main theorem establishing that MCA (mutual correlated agreement) for the affine line generator implies MCA for the affine space generator (Lemma 7.1 of [BCGM25]). The AffineMCALemmas section defines supporting results: line_vecMul (explicit affine line combination via vecMul), exists_succ_not_mem (if a projected combination is a codeword but some direction is not, then a successor direction is also not), proj_lincomb_ker_card_le (bound on size of coefficient vectors whose linear combination projects into the code), exists_avg_le (averaging argument for finite fields), exists_dir_line_ge (density of a set along a direction), and exists_line_bound (the key bound comparing densities of bad seeds). The AffineMCAMain section then presents the theorem AffineLine_MCA_AffineSpaceMCA: if AffineLineGenerator has MCA error ε_mca for a linear code LC, then AffineSpaceGenerator has MCA error (1 - 1/|F|)⁻¹ • ε_mca for LC. No sorry or admit appear in the diff.
• ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean: The file changes the type of ε_mca from I → I to I → ℝ in pseudoinverseGen and generatorSubset, aligning the error parameter with the real-valued codomain used elsewhere in the project. A comment typo in the docstring of pseudoinverseGen is also fixed.
• ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean: The module docstring now describes the affine line generator (F -> F² mapping x ↦ (1,x)) and the affine space generator (F^ℓ -> F^(ℓ+1) mapping x ↦ (1,x)). The IsMCAGenerator definition changed the type of its ε_mca parameter from I -> I to I -> ℝ, and IsMCA now uses projectedCode_submod instead of projectedCode. New abbreviations AffineLineGenerator and AffineSpaceGenerator were added, along with a lemma error_in_unit_interval for proving that d/m lies in the unit interval. Docstrings for minSeedCard, minSeedCard_pos, and minSeedCard_le were clarified.
• ArkLib/Data/Probability/Instances.lean: The file adds a new theorem prob_uniform_eq_ofReal that expresses the probability that a property P holds for a uniformly random element of a nonempty finite type F as ENNReal.ofReal of the real-valued ratio |filter P Finset.univ| / |F|. This is a companion to the existing prob_uniform_eq_card_filter_div_card, intended for use when working in ℝ-based goals. Additionally, the open Real declaration is moved from a standalone line to the open block, and Katerina Hristova is added as an author.

---

Last updated: 2026-06-30 22:47 UTC.

[alexanderlhicks]

Can you remove references to this notation accordingly?

[alexanderlhicks]

this works as is with hℓ : ℓ ≥ 1 actually 😄

[alexanderlhicks]

small typo

[alexanderlhicks]

idk if section is needed here

[alexanderlhicks]

I was surprised this was as many lines as it was, claude suggested the following:

 /-- The projected code `C|_T` of a linear code, as a submodule of `T → F`.
  Definition 3.7 [BCGM25]. -/
def projectedCodeSubmod [Field F] [Fintype ι] (LC : LinearCode ι F) (T : Finset ι) :
  Submodule F (T → F) :=
  LC.map (LinearMap.funLeft F F (Subtype.val : T → ι))

which seems like an instance of mathlib being helpful.

[alexanderlhicks]

how about R_{>=0}?