def HexBerlekampZassenhausMathlib.BHKS.representativeColumns (r : ℕ) (sig : ℕ → Array ℚ) : List ℕ

Representative columns for the sig j = sig k equivalence on {0, …, r-1}: the columns whose signature has not been seen at any earlier column. The list is ascending by construction.

Equations

• HexBerlekampZassenhausMathlib.BHKS.representativeColumns r sig = List.filter (fun (j : ℕ) => (List.filter (fun (k : ℕ) => decide (sig k = sig j)) (List.range j)).isEmpty) (List.range r)

def HexBerlekampZassenhausMathlib.BHKS.partitionByMinColumn (r : ℕ) (sig : ℕ → Array ℚ) : List (List ℕ)

Canonical partition of {0, …, r-1} by signature equivalence: one class per representative column, listing exactly the columns with the same signature as that representative. Classes appear in ascending representative order; each class's member list is ascending.

Equations

• One or more equations did not get rendered due to their size.

def HexBerlekampZassenhausMathlib.BHKS.partitionAcc (r : ℕ) (sig : ℕ → Array ℚ) : List (Array ℚ × List ℕ)

The full (signature, members) payload after folding Hex.bhksInsertSignatureClass over List.range r. Each pair pairs a representative column's signature with the ascending list of columns sharing that signature.

Equations

• One or more equations did not get rendered due to their size.

theorem HexBerlekampZassenhausMathlib.BHKS.partitionAcc_map_snd (r : ℕ) (sig : ℕ → Array ℚ) : List.map Prod.snd (partitionAcc r sig) = partitionByMinColumn r sig

Forgetting the signatures in partitionAcc leaves the canonical min-column partition.

theorem HexBerlekampZassenhausMathlib.BHKS.bhksInsertSignatureClass_eq_append (s : Array ℚ) (j : ℕ) (acc : List (Array ℚ × List ℕ)) (hnotin : ∀ p ∈ acc, p.1 ≠ s) : Hex.bhksInsertSignatureClass s j acc = acc ++ [(s, [j])]

If no entry of acc carries signature s, then Hex.bhksInsertSignatureClass s j acc appends (s, [j]) at the end.

theorem HexBerlekampZassenhausMathlib.BHKS.bhksInsertSignatureClass_eq_replace (s : Array ℚ) (j : ℕ) (l r : List (Array ℚ × List ℕ)) (members : List ℕ) (hnotin : ∀ p ∈ l, p.1 ≠ s) : Hex.bhksInsertSignatureClass s j (l ++ (s, members) :: r) = l ++ (s, members ++ [j]) :: r

If acc = l ++ (s, members) :: r and no entry of l carries signature s, then Hex.bhksInsertSignatureClass s j acc replaces the single matching entry's member list with members ++ [j].

theorem HexBerlekampZassenhausMathlib.BHKS.representativeColumns_succ_of_fresh (m : ℕ) (sig : ℕ → Array ℚ) (hfresh : ∀ k < m, sig k ≠ sig m) : representativeColumns (m + 1) sig = representativeColumns m sig ++ [m]

A fresh signature at column m appends m as a new representative.

theorem HexBerlekampZassenhausMathlib.BHKS.representativeColumns_succ_of_match (m : ℕ) (sig : ℕ → Array ℚ) (k₀ : ℕ) (hk₀ : k₀ < m) (hsig : sig k₀ = sig m) : representativeColumns (m + 1) sig = representativeColumns m sig

A column whose signature was already seen adds no new representative.

theorem HexBerlekampZassenhausMathlib.BHKS.mem_representativeColumns_iff (m : ℕ) (sig : ℕ → Array ℚ) (rep : ℕ) : rep ∈ representativeColumns m sig ↔ rep < m ∧ ∀ k < rep, sig k ≠ sig rep

A representative column is the least index with its row-reduced signature.

theorem HexBerlekampZassenhausMathlib.BHKS.representativeColumns_lt (m : ℕ) (sig : ℕ → Array ℚ) (rep : ℕ) (h : rep ∈ representativeColumns m sig) : rep < m

Representative columns lie in {0, …, m-1}.

theorem HexBerlekampZassenhausMathlib.BHKS.representativeColumns_fresh (m : ℕ) (sig : ℕ → Array ℚ) (rep : ℕ) (h : rep ∈ representativeColumns m sig) (k : ℕ) : k < rep → sig k ≠ sig rep

A representative column's signature does not occur at any earlier column.

theorem HexBerlekampZassenhausMathlib.BHKS.filter_range_succ (m : ℕ) (p : ℕ → Bool) : List.filter p (List.range (m + 1)) = List.filter p (List.range m) ++ if p m = true then [m] else []

Filtering List.range (m + 1) splits as filtering range m plus the trailing element.

theorem HexBerlekampZassenhausMathlib.BHKS.filter_range_succ_sig_eq (m : ℕ) (sig : ℕ → Array ℚ) (rep : ℕ) : List.filter (fun (j : ℕ) => decide (sig j = sig rep)) (List.range (m + 1)) = List.filter (fun (j : ℕ) => decide (sig j = sig rep)) (List.range m) ++ if sig m = sig rep then [m] else []

The members list of the entry for rep in partitionAcc (m + 1) sig factors as the members at step m plus m itself if sig m = sig rep.

theorem HexBerlekampZassenhausMathlib.BHKS.partitionAcc_entry_eq_of_ne (m : ℕ) (sig : ℕ → Array ℚ) (rep : ℕ) (hne : sig m ≠ sig rep) : (sig rep, List.filter (fun (j : ℕ) => decide (sig j = sig rep)) (List.range (m + 1))) = (sig rep, List.filter (fun (j : ℕ) => decide (sig j = sig rep)) (List.range m))

If signatures are decidably distinct at rep and m, the partitionAcc m sig entry for rep extends trivially to step m + 1.

theorem HexBerlekampZassenhausMathlib.BHKS.representativeColumns_decompose_at (m : ℕ) (sig : ℕ → Array ℚ) (k₀ : ℕ) (hk₀ : k₀ ∈ representativeColumns m sig) : ∃ (suffix : List ℕ), representativeColumns m sig = representativeColumns k₀ sig ++ k₀ :: suffix ∧ ∀ rep ∈ suffix, k₀ < rep ∧ rep ∈ representativeColumns m sig

Decompose representativeColumns m sig around a known representative k₀ ∈ representativeColumns m sig. The list splits as the representativeColumns k₀ sig prefix, then k₀, then a suffix of reps in (k₀, m).

theorem HexBerlekampZassenhausMathlib.BHKS.partitionAcc_succ (m : ℕ) (sig : ℕ → Array ℚ) : partitionAcc (m + 1) sig = Hex.bhksInsertSignatureClass (sig m) m (partitionAcc m sig)

The inductive step: partitionAcc (m + 1) sig is one bhksInsertSignatureClass application above partitionAcc m sig.

theorem HexBerlekampZassenhausMathlib.BHKS.foldl_bhksInsertSignatureClass_eq_partitionAcc (r : ℕ) (sig : ℕ → Array ℚ) : List.foldl (fun (acc : List (Array ℚ × List ℕ)) (j : ℕ) => Hex.bhksInsertSignatureClass (sig j) j acc) [] (List.range r) = partitionAcc r sig

The fold over List.range r of Hex.bhksInsertSignatureClass produces exactly the canonical partition accumulator.

theorem HexBerlekampZassenhausMathlib.BHKS.bhksInsertSignatureClass_fold_eq_partitionByMinColumn (r : ℕ) (sig : ℕ → Array ℚ) : List.map Prod.snd (List.foldl (fun (acc : List (Array ℚ × List ℕ)) (j : ℕ) => Hex.bhksInsertSignatureClass (sig j) j acc) [] (List.range r)) = partitionByMinColumn r sig

Partition semantics of Hex.bhksInsertSignatureClass.

The classes emitted by folding Hex.bhksInsertSignatureClass over List.range r form the canonical min-column partition of {0, …, r-1} by signature equality.

theorem HexBerlekampZassenhausMathlib.BHKS.rowReduce_columnAgreement_iff_forall_mem_span_coord_eq {n r : ℕ} (M : Hex.Matrix ℚ n r) (j k : Fin r) : (∀ (i : Fin n), M.rowReduce.echelon[i][j] = M.rowReduce.echelon[i][k]) ↔ ∀ v ∈ Submodule.span ℚ (Set.range (HexMatrixMathlib.matrixEquiv M).row), v j = v k

Two columns of the RREF echelon matrix agree iff every vector in the original row span has equal entries at those columns.

This is the abstract row-span version of the executable bhksColumnSignature comparison: equality of column slices of the echelon rows is represented here by pointwise equality over the Fin n row index.