Proof obligation for `minDist_eq_minDist` in `ArkLib/Data/CodingTheory/InterleavedCode.lean`

[alexanderlhicks]

A proof in ArkLib/Data/CodingTheory/InterleavedCode.lean contains a sorry.

🤖 AI Analysis:

Statement Explanation

This theorem claims that the minimum distance of a LawfulInterleavedCode is equal to the minimum distance of its underlying linear code LC.

The left-hand side, Code.minDist (IC.1.LC : Set (ι → F)), refers to the standard minimum Hamming distance of the linear code LC. This is the smallest number of positions in which any two distinct codewords from LC differ.

The right-hand side, minDist IC.1.MF, is the minimum distance defined for the interleaved code. The InterleavedCode consists of a submodule of matrices, IC.1.MF. The distance between two matrices is defined as the number of columns in which they are not identical (distCodewords). Thus, minDist IC.1.MF is the minimum number of differing columns between any two distinct matrices in the submodule MF.

The hypothesis IC : LawfulInterleavedCode provides the crucial link: IC.isInterleaved guarantees that every row of any matrix in MF is a codeword in LC.

Context

This lemma is a fundamental result connecting the two main components of an InterleavedCode structure: the matrix submodule MF and the linear code LC. It essentially states that, for a lawfully constructed interleaved code, the minimum distance property is preserved from the underlying linear code.

The proof will likely involve unfolding the definitions of minDist for both types of codes and relating them using the properties of submodules and the isInterleaved condition. Note that for linear codes (which are submodules), the minimum distance between distinct codewords is equal to the minimum weight of a non-zero codeword. You will likely find it easier to work with weights instead of distances.

A potential subtlety lies in the generality of the type {IC : LawfulInterleavedCode κ ι F}. The proof for one direction of the equality (≤) holds for any LawfulInterleavedCode. However, the other direction (≥) seems to require that the matrix submodule MF is "rich" enough to contain specific matrices constructed from single codewords of LC. This property is guaranteed if IC is built using the canonical constructor lawfulInterleavedCodeOfLinearCode, but it might not hold for an arbitrary LawfulInterleavedCode. You may also need to handle the edge case where κ is an empty type, perhaps by adding a [Nonempty κ] hypothesis.

Proof Suggestion

A standard way to prove an equality is to show both inequalities. The le_antisymm tactic is useful here. The proof can be structured as follows, reasoning about minimum weights instead of minimum distances.

1. Proof for Code.minDist (IC.1.LC) ≤ minDist (IC.1.MF):

   • Let d_MF be the minimum weight of a non-zero matrix in IC.1.MF. By definition, there is a matrix W ∈ IC.1.MF with W ≠ 0 and distCodewords W 0 = d_MF.
   • Since W is non-zero, it must have at least one non-zero row. Let's call it w, where w = W i for some row index i.
   • Using the isInterleaved property (IC.2), you can deduce that this row w is a non-zero codeword in IC.1.LC.
   • The minimum distance (or weight) of LC must be less than or equal to the weight of any of its non-zero codewords. Thus, Code.minDist (IC.1.LC) ≤ Code.wt w.
   • Relate the weight of the row w to the weight of the matrix W. The set of indices where w is non-zero is a subset of the set of indices of non-zero columns of W. This implies Code.wt w ≤ distCodewords W 0.
   • Combine these inequalities to conclude this direction of the proof.

2. Proof for minDist (IC.1.MF) ≤ Code.minDist (IC.1.LC):

   • This part is more subtle and may require you to assume [Nonempty κ].
   • Let d_LC be the minimum distance of IC.1.LC. Let w be a codeword in LC with Code.wt w = d_LC.
   • The goal is to find a matrix W ∈ IC.1.MF whose weight is d_LC. A good candidate is a matrix that has w as one of its rows and is zero everywhere else.
   • Pick an arbitrary i₀ : κ (which is possible if κ is non-empty). Construct a matrix W such that W i₀ = w and W i = 0 for all i ≠ i₀.
   • You need to show this W is in IC.1.MF. This is where the structure of MF matters. If IC is constructed via codeOfLinearCode, then MF is matrixSubmoduleOfLinearCode κ (IC.1.LC), which is the span of all matrices whose rows are in LC. Your constructed W is one of these generating matrices, so it is in MF.
   • Calculate the weight of W: distCodewords W 0. Show that it is exactly equal to Code.wt w, which is d_LC.
   • Since you've found a matrix in MF with weight d_LC, the minimum weight of MF can be no larger. This establishes minDist (IC.1.MF) ≤ d_LC.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

lemma minDist_eq_minDist [DecidableEq F] {IC : LawfulInterleavedCode κ ι F} :
  Code.minDist (IC.1.LC : Set (ι → F)) = minDist IC.1.MF := by sorry

[adrianmartir]

I can't find the referenced lemma in the linked file, has this already been solved?

[chung-thai-nguyen]

I can't find the referenced lemma in the linked file, has this already been solved?

@adrianmartir The interleaved code APIs have been changed so this is not needed anymore.

[adrianmartir]

Thank you for the quick reply! Does this apply to all the InterleavedCode issues? There are actually no sorries in that file (unless we're supposed to add the lemmas ourselves).

[chung-thai-nguyen]

@adrianmartir Yes. That file is deleted. Fundamental APIs for interleaved codes are already done. The rest of that file was AHIV22 lemmas but it's being handled by another guy already.

[adrianmartir]

Are there any other sorrys that you guys might need help with? I'm eager to try out some new AI-tools on them. The other issues seem to already have people working on them. (I hope it is okay to ask this here)

[lekt9]

This appears resolved on current main. minDist_eq_minDist in ArkLib/Data/CodingTheory/InterleavedCode.lean (around L1073) is now proven with no sorry in its body.

Verification:

• No sorry token in the lemma body (the only "sorry" occurrences in the file are docstring prose such as "proven sorry-free").
• InterleavedCode.lean type-checks via an isolated lake env lean with exit code 0 and no "declaration uses 'sorry'" warning emitted for any declaration in the file.

So the proof obligation flagged by this auto-generated issue looks discharged. Suggest closing as completed after a maintainer confirms it matches intent.