Tensor product of MCA generators

[katyhr]

Lemma 4.4 of [BCGM25]. Weaker version (checking with authors)

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Tensor product of MCA generators

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

---

Statistics

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

---

Lean Declarations

✏️ Added: 19 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/MCAGenerator.lean (1)

• lemma tensor_of_MCA_is_MCA [Nonempty S] {S' : Type} [Fintype S'] [Nonempty S'] (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 (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)

• 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.

---

📄 **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/ProximityGap/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/ProximityGap/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/ProximityGap/ProximityGenerators.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:01 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/ProximityGap/AffineGenerator.lean
• Agent B failed for ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean
• Agent B failed for ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean
• Agent B failed for ArkLib/Data/Probability/Instances.lean

---

🔗 **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/ProximityGap/AffineGenerator.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/ProximityGap/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/ProximityGap/MCAGenerator.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/ProximityGap/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/ProximityGap/ProximityGenerators.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.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.'}]}}