Polynomial Generators have MCA for RSCodes

[katyhr]

Section 9 of [BCGM25].

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Polynomial Generators have MCA for RSCodes

sorry delta: +2 (2 added) — proof obligations increased

Failed to generate AI summary. Please check the per-file summaries and statistics below.

---

Statistics

Metric	Count
📝 Files Changed	8
✅ Lines Added	656
❌ Lines Removed	22

---

Lean Declarations

✏️ Added: 25 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/ProximityGenerator/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/ProximityGenerator/Basic.lean (4)

• abbrev AffineLineGenerator (F : Type) [Field F] : Generator F (Fin 2) F
• abbrev AffineSpaceGenerator (F : Type) [Field F] (ℓ : ℕ) : Generator (Fin ℓ → F) (Fin (ℓ + 1)) F
• def IsPolynomialGeneratorOfFull {s : ℕ} (G : Generator (Fin s → F) ℓ F)
• def UnivariatePowers (d : ℕ) : Generator F (Fin (d + 1)) F

ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean (1)

• lemma tensor_of_MCA_is_MCA [Nonempty S] {S' : Type} [Fintype S'] [Nonempty S'] (LC : LinearCode ι F)

ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean (4)

• lemma PolyGen_MCA_RScode (n d m : ℕ) (hm : 3 ≤ m) {ℓ : Type} [Fintype ℓ] {s : ℕ}
• lemma univarite_powers_MCA (n d m : ℕ) (hm : 3 ≤ m) :
• noncomputable def deg_max {s : ℕ} {ℓ : Type} [Fintype ℓ] (P : ℓ → MvPolynomial (Fin s) F) :
• noncomputable def ε_mca_RS (n d m : ℕ) : I → ℝ

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

• theorem Pr_exists_le {α ι : Type} [Fintype ι] (D : PMF α) (f : ι → α → Prop) :
• theorem Pr_or_le {α : Type} (D : PMF α) (f g : α → Prop) :
• theorem Pr_seq_le_of_forall_le {α β : Type} (Da : PMF α) (Db : PMF β) (Q : α → β → Prop)
• theorem prob_uniform_eq_ofReal {F : Type} [Fintype F] [Nonempty F]

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

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

---

sorry Tracking

❌ Added: 2 `sorry`(s)

ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean (2)

• lemma PolyGen_MCA_RScode (n d m : ℕ) (hm : 3 ≤ m) {ℓ : Type} [Fintype ℓ] {s : ℕ} (L64)
• lemma univarite_powers_MCA (n d m : ℕ) (hm : 3 ≤ m) : (L49)

---

📄 **Per-File Summaries**

• ArkLib.lean: Summary unavailable — error: Error code: 402 - {'error': {'message': 'Insufficient credits. Add more using https://openrouter.ai/settings/credits', 'code': 402}}
• ArkLib/Data/CodingTheory/Basic/LinearCode.lean: Summary unavailable — error: Error code: 402 - {'error': {'message': 'Insufficient credits. Add more using https://openrouter.ai/settings/credits', 'code': 402}}
• ArkLib/Data/CodingTheory/Prelims.lean: Summary unavailable — error: Error code: 402 - {'error': {'message': 'Insufficient credits. Add more using https://openrouter.ai/settings/credits', 'code': 402}}
• ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean: Summary unavailable — error: Error code: 402 - {'error': {'message': 'Insufficient credits. Add more using https://openrouter.ai/settings/credits', 'code': 402}}
• ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean: Summary unavailable — error: Error code: 402 - {'error': {'message': 'Insufficient credits. Add more using https://openrouter.ai/settings/credits', 'code': 402}}
• ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean: Summary unavailable — error: Error code: 402 - {'error': {'message': 'Insufficient credits. Add more using https://openrouter.ai/settings/credits', 'code': 402}}
• ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean: Summary unavailable — error: Error code: 402 - {'error': {'message': 'Insufficient credits. Add more using https://openrouter.ai/settings/credits', 'code': 402}}
• ArkLib/Data/Probability/Instances.lean: Summary unavailable — error: Error code: 402 - {'error': {'message': 'Insufficient credits. Add more using https://openrouter.ai/settings/credits', 'code': 402}}

---

Last updated: 2026-07-06 18:00 UTC.

[github-actions]

🤖 AI Review

Overall Summary:
An error occurred while synthesizing the summary: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

---

Errors during review:

• Agent B failed for ArkLib.lean
• Agent B failed for ArkLib/Data/CodingTheory/Basic/LinearCode.lean
• Agent B failed for ArkLib/Data/CodingTheory/Prelims.lean
• Agent B failed for ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean
• Agent B failed for ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean
• Agent B failed for ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean
• Agent B failed for ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean
• Agent B failed for ArkLib/Data/Probability/Instances.lean

---

🔍 **Mechanical Pre-Check Results**

Escape hatches introduced in this PR (triggers hard verdict rule):

• sorry introduced in ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean: sorry
• sorry introduced in ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean: IsMCAGenerator G ε (ReedSolomon.code D k) := by sorry

Pre-existing escape hatches in touched files (context only, does not affect verdict):

• sorry in ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean line 49: sorry
• sorry in ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean line 64: IsMCAGenerator G ε (ReedSolomon.code D k) := by sorry

🔗 **Cross-File Analysis**

Cross-file analysis failed: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib.lean`**

An error occurred while analyzing ArkLib.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/CodingTheory/Basic/LinearCode.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/Basic/LinearCode.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/CodingTheory/Prelims.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/Prelims.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/Probability/Instances.lean`**

An error occurred while analyzing ArkLib/Data/Probability/Instances.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}