theorem HexBerlekampZassenhausMathlib.BHKS.coord_eq_of_mem_trueSupportSpanInt {r : ℕ} (trueSupports : Set (Set (Fin r))) {j k : Fin r} (hjk : supportEquivalent trueSupports j k) {v : Fin r → ℤ} (hv : v ∈ trueSupportSpanInt trueSupports) : v j = v k

Membership in the true-support span forces equal coordinates at columns with the same true-support membership signature.

theorem HexBerlekampZassenhausMathlib.BHKS.mem_trueSupportSpanInt_of_constant_on_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) (hne : ∀ S ∈ trueSupports, S.Nonempty) (v : Fin r → ℤ) (hconstant : ∀ S ∈ trueSupports, ∀ i ∈ S, ∀ j ∈ S, v i = v j) : v ∈ trueSupportSpanInt trueSupports

For a genuine finite partition, a vector belongs to the true-support span whenever it is constant on every part.

Together with coord_eq_of_mem_trueSupportSpanInt, this characterizes W as the integer vectors that are constant on each true support.

theorem HexBerlekampZassenhausMathlib.BHKS.exists_ne_on_support_of_not_mem_trueSupportSpanInt {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) (hne : ∀ S ∈ trueSupports, S.Nonempty) (v : Fin r → ℤ) (hv : v ∉ trueSupportSpanInt trueSupports) : ∃ S ∈ trueSupports, ∃ i ∈ S, ∃ j ∈ S, v i ≠ v j

Any integer vector outside the true-support span varies on at least one part of the genuine partition.

theorem HexBerlekampZassenhausMathlib.BHKS.exists_adjustedVector (L : Hex.BhksLatticeBasis) (hL : BhksBlockForm L) (trueSupports : Set (Set (Fin L.factorCount))) (hcover : ∀ (i : Fin L.factorCount), ∃ S ∈ trueSupports, i ∈ S) (hdisjoint : ∀ S ∈ trueSupports, ∀ T ∈ trueSupports, ∀ i ∈ S, i ∈ T → S = T) (hne : ∀ S ∈ trueSupports, S.Nonempty) (data : (S : ↑trueSupports) → SupportShortVectorData L ↑S) (V U : ℕ) (v : Vector ℤ (L.factorCount + L.coeffWidth)) (hvL : L.basis.memLattice v) (hvBound : ∀ (x : Fin (L.factorCount + L.coeffWidth)), v[x].natAbs ≤ V) (hdataBound : ∀ (S : ↑trueSupports) (x : Fin (L.factorCount + L.coeffWidth)), (data S).vector[x].natAbs ≤ U) (hvW : (fun (i : Fin L.factorCount) => v[Fin.castAdd L.coeffWidth i]) ∉ trueSupportSpanInt trueSupports) : ∃ (w : Vector ℤ (L.factorCount + L.coeffWidth)), L.basis.memLattice w ∧ (∃ (i : Fin L.factorCount), w[Fin.castAdd L.coeffWidth i] = 0) ∧ (∀ S ∈ trueSupports, ∃ i ∈ S, w[Fin.castAdd L.coeffWidth i] ≠ 0) ∧ ∀ (x : Fin (L.factorCount + L.coeffWidth)), w[x].natAbs ≤ V + V * U + trueSupports.ncard * U

Adjust a full BHKS lattice vector outside W by full true-support short vectors. The adjusted vector has a zero exponent at one local factor, but its first block is nonzero on every true support.

The correction is performed on row-combination coefficients, not merely on the projected first block, so the result remains an actual vector of the full BHKS lattice.

theorem HexBerlekampZassenhausMathlib.BHKS.projectedRowSpanInt_le_trueSupportSpanInt_of_no_bad (L : Hex.BhksLatticeBasis) (hL : BhksBlockForm L) (hrows : 1 ≤ L.factorCount + L.coeffWidth) (trueSupports : Set (Set (Fin L.factorCount))) (hcover : ∀ (i : Fin L.factorCount), ∃ S ∈ trueSupports, i ∈ S) (hdisjoint : ∀ S ∈ trueSupports, ∀ T ∈ trueSupports, ∀ i ∈ S, i ∈ T → S = T) (hne : ∀ S ∈ trueSupports, S.Nonempty) (data : (S : ↑trueSupports) → SupportShortVectorData L ↑S) (V U : ℕ) (hretainedBound : ∀ (j : Fin (L.factorCount + L.coeffWidth)), ↑j < Hex.bhksCutPrefixCount L (Hex.bhksProjectedRowsTrace L hrows).reducedMatrix → ∀ (x : Fin (L.factorCount + L.coeffWidth)), ((Hex.bhksProjectedRowsTrace L hrows).reducedMatrix.row j)[x].natAbs ≤ V) (hdataBound : ∀ (S : ↑trueSupports) (x : Fin (L.factorCount + L.coeffWidth)), (data S).vector[x].natAbs ≤ U) (hnoBad : ∀ (w : Vector ℤ (L.factorCount + L.coeffWidth)), L.basis.memLattice w → (∃ (i : Fin L.factorCount), w[Fin.castAdd L.coeffWidth i] = 0) → (∀ S ∈ trueSupports, ∃ i ∈ S, w[Fin.castAdd L.coeffWidth i] ≠ 0) → (∀ (x : Fin (L.factorCount + L.coeffWidth)), w[x].natAbs ≤ V + V * U + trueSupports.ncard * U) → False) : projectedRowSpanInt (Hex.bhksProjectedRows L hrows) ≤ trueSupportSpanInt trueSupports

The geometric half of the BHKS reverse containment. If every bounded adjusted lattice vector with one zero local exponent and a nonzero exponent on every true support is impossible, then every executable retained row belongs to the true-support span.

The theorem isolates all LLL bookkeeping: the caller supplies only coordinate bounds for retained rows and support short vectors, plus the algebraic bad-vector contradiction.

theorem HexBerlekampZassenhausMathlib.BHKS.intVectorToRat_mem_projectedRowSpaceRat (L : Hex.BhksProjectedRows) {v : Fin L.factorCount → ℤ} (hv : v ∈ projectedRowSpanInt L) : intVectorToRat v ∈ projectedRowSpaceRat L

Casting an integer vector in the executable projected span to ℚ places it in the rational row space used by RREF.

theorem HexBerlekampZassenhausMathlib.BHKS.projectedRowSpace_coordAgreement_iff_supportEquivalent (L : Hex.BhksProjectedRows) (trueSupports : Set (Set (Fin L.factorCount))) (hspan : projectedRowSpanInt L = trueSupportSpanInt trueSupports) (j k : Fin L.factorCount) : (∀ v ∈ projectedRowSpaceRat L, v j = v k) ↔ supportEquivalent trueSupports j k

If L' = W, equality of all coordinates in the rational projected row space is exactly equality of true-support membership signatures.