theorem HexBerlekampZassenhausMathlib.BHKS.supportPartitionByMinColumn_length_le_partitionByMinColumn_length {r : ℕ} (trueSupports : Set (Set (Fin r))) (sig : ℕ → Array ℚ) (hrefine : ∀ (j k : ℕ) (hj : j < r) (hk : k < r), sig j = sig k → supportEquivalent trueSupports ⟨j, hj⟩ ⟨k, hk⟩) : (supportPartitionByMinColumn trueSupports).length ≤ (partitionByMinColumn r sig).length

Forward refinement of the support partition by the signature partition.

If equal column signatures force support-equivalence; the forward direction, available from the inclusion W ⊆ L' alone (no reverse L' = W separation); then every signature class is contained in one support-equivalence class, so the signature partition refines the support partition and therefore has at least as many classes. The map sending each support representative q to its signature representative sigRep sig q is the witnessing injection.

def HexBerlekampZassenhausMathlib.BHKS.projectedRowsRrefColumnSignature (L : Hex.BhksProjectedRows) (j : ℕ) : Array ℚ

The RREF column signature expression used by Hex.bhksEquivalenceClassIndicators, exposed as a proof-facing definition.

Equations

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

theorem HexBerlekampZassenhausMathlib.BHKS.matrixEquiv_bhksProjectedRowsAsRatMatrix (L : Hex.BhksProjectedRows) : HexMatrixMathlib.matrixEquiv (Hex.bhksProjectedRowsAsRatMatrix L.projectedRows L.projectedRows.size L.factorCount) = projectedRowsRatMatrix L

The executable projected-row matrix transports to the Mathlib-facing rational matrix.

theorem HexBerlekampZassenhausMathlib.BHKS.projectedRowsRrefColumnSignature_eq_iff_coordAgreement (L : Hex.BhksProjectedRows) {j k : ℕ} (hj : j < L.factorCount) (hk : k < L.factorCount) : projectedRowsRrefColumnSignature L j = projectedRowsRrefColumnSignature L k ↔ ∀ v ∈ projectedRowSpaceRat L, v ⟨j, hj⟩ = v ⟨k, hk⟩

Two RREF column signatures agree exactly when every vector of the rational projected row space has equal coordinates at those columns.

theorem HexBerlekampZassenhausMathlib.BHKS.projectedRowsRrefColumnSignature_eq_imp_supportEquivalent_of_cut (L : Hex.BhksProjectedRows) (trueSupports : Set (Set (Fin L.factorCount))) (hcut : CutProjectionHypotheses L trueSupports) {j k : ℕ} (hj : j < L.factorCount) (hk : k < L.factorCount) (hsig : projectedRowsRrefColumnSignature L j = projectedRowsRrefColumnSignature L k) : supportEquivalent trueSupports ⟨j, hj⟩ ⟨k, hk⟩

Forward column-signature implication from the cut inclusion W ⊆ L'.

This is the one-directional half of projectedRowsRrefColumnSignature_eq_iff_supportEquivalent_of_projectedRowSpan_eq that needs only the forward inclusion supplied by CutProjectionHypotheses (each true-support indicator lies in L'), not the reverse L' = W separation. Equal RREF column signatures mean every vector of the rational row space agrees on those two columns; since each support indicator lies in L' (hence in the rational row space), the two columns lie in exactly the same true supports.

theorem HexBerlekampZassenhausMathlib.BHKS.projectedRowsRrefColumnSignature_eq_iff_supportEquivalent_of_span_eq (L : Hex.BhksProjectedRows) (trueSupports : Set (Set (Fin L.factorCount))) (hspan : projectedRowSpanInt L = trueSupportSpanInt trueSupports) {j k : ℕ} (hj : j < L.factorCount) (hk : k < L.factorCount) : projectedRowsRrefColumnSignature L j = projectedRowsRrefColumnSignature L k ↔ supportEquivalent trueSupports ⟨j, hj⟩ ⟨k, hk⟩

Exact RREF signature semantics once the retained projected lattice is the true-support lattice.

theorem HexBerlekampZassenhausMathlib.BHKS.partitionByMinColumn_eq_supportPartition_of_span_eq (L : Hex.BhksProjectedRows) (trueSupports : Set (Set (Fin L.factorCount))) (hspan : projectedRowSpanInt L = trueSupportSpanInt trueSupports) : partitionByMinColumn L.factorCount (projectedRowsRrefColumnSignature L) = supportPartitionByMinColumn trueSupports

Equality L' = W identifies the canonical RREF signature partition with the canonical true-support partition, including class order and member order.

theorem HexBerlekampZassenhausMathlib.BHKS.bhksEquivalenceClassIndicators_eq_supportPartition (L : Hex.BhksProjectedRows) (trueSupports : Set (Set (Fin L.factorCount))) (hspan : projectedRowSpanInt L = trueSupportSpanInt trueSupports) : Hex.bhksEquivalenceClassIndicators L = (List.map (classIndicatorArray L.factorCount) (supportPartitionByMinColumn trueSupports)).toArray

At L' = W, the executable indicator array is exactly the ordered array of indicator vectors for the true-support equivalence classes.

theorem HexBerlekampZassenhausMathlib.BHKS.supportClassMembers_eq_support_of_partition {r : ℕ} (trueSupports : Set (Set (Fin r))) (hcover : ∀ (i : Fin r), ∃ S ∈ trueSupports, i ∈ S) (hdisjoint : ∀ S ∈ trueSupports, ∀ T ∈ trueSupports, ∀ i ∈ S, i ∈ T → S = T) {rep : ℕ} (hrep : rep ∈ supportRepresentativeColumns trueSupports) : ∃ S ∈ trueSupports, ∀ (j : ℕ), j ∈ supportClassMembers trueSupports rep ↔ ∃ (hj : j < r), ⟨j, hj⟩ ∈ S

For a genuine partition, the support-equivalence class represented by rep is the unique true support containing rep.

This is the set-level half of the executable recovery correspondence: after L' = W, an RREF class is not merely support-equivalent to a true support; its ascending member list enumerates that support exactly.

theorem HexBerlekampZassenhausMathlib.BHKS.bhksIndicatorSelectedFactorsArray_classIndicatorArray_toList (liftedFactors : Array Hex.ZPoly) (members : List ℕ) : (Hex.bhksIndicatorSelectedFactorsArray liftedFactors (classIndicatorArray liftedFactors.size members)).toList = List.map (fun (i : ℕ) => liftedFactors.getD i 0) (List.filter (fun (i : ℕ) => decide (i ∈ members)) (List.range liftedFactors.size))

Selecting lifted factors with a canonical class indicator is the same order-preserving filter of the lifted-factor array by class membership.

theorem HexBerlekampZassenhausMathlib.BHKS.bhksEquivalenceClassIndicators_size_eq (L : Hex.BhksProjectedRows) : (Hex.bhksEquivalenceClassIndicators L).size = (partitionByMinColumn L.factorCount (projectedRowsRrefColumnSignature L)).length

The number of executable equivalence-class indicators equals the length of the signature partition partitionByMinColumn over the RREF column signatures. This is a pure restatement of the executable fold semantics, independent of any lattice hypothesis.

theorem HexBerlekampZassenhausMathlib.BHKS.supportPartitionByMinColumn_length_le_bhksEquivalenceClassIndicators_size (L : Hex.BhksProjectedRows) (trueSupports : Set (Set (Fin L.factorCount))) (hcut : CutProjectionHypotheses L trueSupports) : (supportPartitionByMinColumn trueSupports).length ≤ (Hex.bhksEquivalenceClassIndicators L).size

Forward count bound: the executable equivalence-class partition emits at least one class per true-support-equivalence class.

This is the forward-only count_ge argument: from the cut inclusion W ⊆ L' (CutProjectionHypotheses, certified by the closed cut-survival argument) the emitted partition refines the true-support partition, so the emitted class count is at least the support-partition length. It needs no reverse L' = W separation; and hence no bad-vector resultant valuation; establishing the lower count bound from the forward inclusion alone.