Smol changes

[ElijahVlasov]

I took the liberty to address @alexanderlhicks's comment regarding the definition of projectedCode_submod and added a few useful lemmas for membership to projectedCode.

[github-actions]

🤖 PR Summary

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

The PR titled 'Smol changes' primarily refactors coding-theory code to use a vector-space-style • (scalar multiplication) instead of pointwise *, cleans up proofs via aesop, and introduces a new lemma and API for matrix multiplication of codewords. No new sorry or admit placeholders are added.

Mathematical Formalization

• linComb (ArkLib/Data/CodingTheory/Prelims.lean): The linear-combination definition is refactored from a pointwise lambda fun k => ∑ i, l i * U i.succ k to the direct sum-of-scalar-multiplication form ∑ i, l i • U i.succ. This makes the expression more idiomatic in a vector-space context.

• matrixMulCodewords (ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean): The definition is refactored from an explicit sum to Matrix.row (A * Matrix.of U). A new simp lemma matrixMulCodewords_apply recovers the original pointwise expansion.

• proj_lincomb_ker_card_le (ArkLib/Data/CodingTheory/ProximityGap/AffineGenerator.lean): The filter condition is changed from projectedWord (fun k => ∑ i, l i * w i k) T to projectedWord (∑ i, l i • w i) T. The cardinality argument is restructured with aesop.

Proof Completion (no sorry/admit introduced)

• No new sorry or admit placeholders are added in any file.

Refactoring

• proj_lincomb_ker_card_le (see above) and exists_line_bound (ArkLib/Data/CodingTheory/ProximityGap/AffineGenerator.lean): The nlinarith step is replaced with aesop (add safe (by nlinarith)).
• line_vecMul (ArkLib/Data/CodingTheory/ProximityGap/AffineGenerator.lean): The proof is replaced with a single aesop call.
• isMCA_generatorByRightMul_of_isMCA (ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean): The hT_proj equality is closed by aesop (replacing manual convert–ext–simp). The hj contradiction block is restructured to use mem_projectedCode_submod, convert, a short have that invokes simp_all, and a final aesop block over mulVec.

Documentation

• No explicit documentation changes beyond the lemma matrixMulCodewords_apply being marked simp.

The core change is in the refactored linComb, matrixMulCodewords, and the proof rewrites in AffineGenerator.lean and MCAGenerator.lean; the remaining adjustments are mechanical replacements of * with • and nlinarith with aesop.

---

Statistics

Metric	Count
📝 Files Changed	4
✅ Lines Added	61
❌ Lines Removed	79

---

Lean Declarations

✏️ Added: 7 declaration(s)

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

• lemma mem_projectedCode {C : Set (ι → F)} {T : Finset ι} {w : ↥T → F} :
• lemma mem_projectedCode_submod [Field F] {LC : LinearCode ι F} {T : Finset ι} {w : ↥T → F} :
• lemma projectedWord_apply {c : ι → F} {T : Finset ι} {i : T} :
• lemma projectedWord_eq_funLeft [Field F] {T : Finset ι} {c : ι → F} :
• lemma restrict_mem_projectedCode_iff {C : Set (ι → F)} {T : Finset ι} {w : ι → F} :
• lemma restrict_mem_projectedCode_of_codeword_eq {C : Set (ι → F)} {T : Finset ι} {w : ι → F}

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

• lemma matrixMulCodewords_apply {A : Matrix ℓ ℓ' F} {U : ℓ' → ι → F} {i : ℓ} {k : ι} :

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

• def projectedCode (C : Set (ι → F)) (T : Finset ι) : Set (T → F) in ArkLib/Data/CodingTheory/Basic/LinearCode.lean moved from L265 to L269
• def projectedCode_submod [Field F] (LC : LinearCode ι F) (T : Finset ι) : Submodule F (T → F) in ArkLib/Data/CodingTheory/Basic/LinearCode.lean moved from L270 to L287
• def matrixMulCodewords (A : Matrix ℓ ℓ' F) (U : ℓ' → ι → F) : ℓ → ι → F in ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean moved from L51 to L51

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Style and documentation violations in the diff, primarily around theorem naming and missing docstrings.

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/Basic/LinearCode.lean: Summary unavailable — AI generation failed.
• ArkLib/Data/CodingTheory/Prelims.lean: The definition of linComb was refactored: the body replaced a pointwise lambda expression fun k => ∑ i, l i * U i.succ k with the direct sum-of-scalar-multiplication form ∑ i, l i • U i.succ. This eliminates an explicit function abstraction by using • (scalar multiplication on function vectors) instead of * (field multiplication applied pointwise), making the linear combination more idiomatic in the vector-space style. No new theorems, declarations, or sorry/admit are introduced.
• ArkLib/Data/CodingTheory/ProximityGap/AffineGenerator.lean: The lemma line_vecMul proof is replaced with a single aesop call. In exists_succ_not_mem, the proof uses projectedCode_submod LC T and mem_projectedCode_submod, and expresses the linear combination via scalar multiplication (∑ i, x i • U i.succ) instead of pointwise multiplication. proj_lincomb_ker_card_le changes its filter condition from projectedWord (fun k => ∑ i, l i * w i k) T to projectedWord (∑ i, l i • w i) T and restructures the cardinality argument with aesop. exists_line_bound replaces a nlinarith step with aesop (add safe (by nlinarith)). No sorry or admit are introduced.
• ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean: The definition of matrixMulCodewords is refactored from an explicit sum to Matrix.row (A * Matrix.of U), and the lemma matrixMulCodewords_apply (with simp attribute) is added to recover the original pointwise expansion. The proof of the helper isMCA_generatorByRightMul_of_isMCA is rewritten: the hT_proj equality is now closed by aesop (replacing manual convert–ext–simp), and the hj contradiction block is restructured to use mem_projectedCode_submod, convert, a short have that invokes simp_all, and a final aesop block over mulVec. No sorry or admit are introduced.

---

Last updated: 2026-07-29 14:28 UTC.