theorem HexBerlekampZassenhausMathlib.BHKS.traceReducedMatrix_memLattice_iff (L : Hex.BhksLatticeBasis) (hrows : 1 ≤ L.factorCount + L.coeffWidth) (v : Vector ℤ (L.factorCount + L.coeffWidth)) : (Hex.bhksProjectedRowsTrace L hrows).reducedMatrix.memLattice v ↔ L.basis.memLattice v

The reduced matrix stored in the BHKS projected-row trace generates the same integer row lattice as the original BHKS basis. This carries lllNative.shortVectors's .toArray output back to the certified LLL lattice-preservation theorem Hex.lllNative_memLattice_iff.

def HexBerlekampZassenhausMathlib.BHKS.projectedRowsIntMatrix (L : Hex.BhksProjectedRows) : Matrix (Fin L.projectedRows.size) (Fin L.factorCount) ℤ

The projected integer rows of the executable BHKS cut as a Mathlib matrix.

Equations

• HexBerlekampZassenhausMathlib.BHKS.projectedRowsIntMatrix L i j = (L.projectedRows.getD ↑i #[]).getD (↑j) 0

def HexBerlekampZassenhausMathlib.BHKS.projectedRowsRatMatrix (L : Hex.BhksProjectedRows) : Matrix (Fin L.projectedRows.size) (Fin L.factorCount) ℚ

The projected rational rows of the executable BHKS cut as a Mathlib matrix.

Equations

• HexBerlekampZassenhausMathlib.BHKS.projectedRowsRatMatrix L i j = ↑((L.projectedRows.getD ↑i #[]).getD (↑j) 0)

def HexBerlekampZassenhausMathlib.BHKS.projectedRowSpanInt (L : Hex.BhksProjectedRows) : Submodule ℤ (Fin L.factorCount → ℤ)

The integer row span represented by the executable projected BHKS rows. This is the proof-facing L' <= Z^r.

Equations

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

def HexBerlekampZassenhausMathlib.BHKS.projectedRowSpaceRat (L : Hex.BhksProjectedRows) : Submodule ℚ (Fin L.factorCount → ℚ)

The rational row space represented by the same executable projected rows. This is the row-space input used by the RREF equivalence-class stage.

Equations

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

def HexBerlekampZassenhausMathlib.BHKS.intVectorToRat {r : ℕ} (v : Fin r → ℤ) : Fin r → ℚ

Cast an integer vector over the lifted-factor indices to a rational vector.

Equations

• HexBerlekampZassenhausMathlib.BHKS.intVectorToRat v i = ↑(v i)

noncomputable def HexBerlekampZassenhausMathlib.BHKS.indicatorVector {r : ℕ} (S : Set (Fin r)) : Fin r → ℤ

A 0/1 indicator vector for a support of lifted factor indices.

Equations

• HexBerlekampZassenhausMathlib.BHKS.indicatorVector S i = if i ∈ S then 1 else 0

def HexBerlekampZassenhausMathlib.BHKS.trueSupportSpanInt {r : ℕ} (trueSupports : Set (Set (Fin r))) : Submodule ℤ (Fin r → ℤ)

The integer lattice W generated by the indicator vectors of the true factor supports. This is the proof-facing counterpart of the retained projected row lattice projectedRowSpanInt.

Equations

• HexBerlekampZassenhausMathlib.BHKS.trueSupportSpanInt trueSupports = Submodule.span ℤ (Set.range fun (S : ↑trueSupports) => HexBerlekampZassenhausMathlib.BHKS.indicatorVector ↑S)

theorem HexBerlekampZassenhausMathlib.BHKS.indicatorVector_mem_trueSupportSpanInt {r : ℕ} (trueSupports : Set (Set (Fin r))) (S : ↑trueSupports) : indicatorVector ↑S ∈ trueSupportSpanInt trueSupports

Every true-support indicator is one of the generators of W.

@[simp]

theorem HexBerlekampZassenhausMathlib.BHKS.indicatorVector_apply_mem {r : ℕ} (S : Set (Fin r)) {i : Fin r} (hi : i ∈ S) : indicatorVector S i = 1

The indicator is 1 on members.

@[simp]

theorem HexBerlekampZassenhausMathlib.BHKS.indicatorVector_apply_not_mem {r : ℕ} (S : Set (Fin r)) {i : Fin r} (hi : i ∉ S) : indicatorVector S i = 0

The indicator is 0 off members.

theorem HexBerlekampZassenhausMathlib.BHKS.indicatorVector_sq_apply_le_one {r : ℕ} (S : Set (Fin r)) (i : Fin r) : ↑(indicatorVector S i) ^ 2 ≤ 1

Each coordinate of an indicator vector has squared real norm at most one.

theorem HexBerlekampZassenhausMathlib.BHKS.indicatorVector_sq_sum_le_factorCount {r : ℕ} (S : Set (Fin r)) : ∑ i : Fin r, ↑(indicatorVector S i) ^ 2 ≤ ↑r

The squared real norm of a 0/1 indicator vector is at most the ambient dimension.

@[reducible, inline]

abbrev HexBerlekampZassenhausMathlib.BHKS.LiftedFactorSupport (L : Hex.BhksLatticeBasis) : Type

A support of lifted local-factor indices for a BHKS lattice basis.

Equations

• HexBerlekampZassenhausMathlib.BHKS.LiftedFactorSupport L = Set (Fin L.factorCount)

noncomputable def HexBerlekampZassenhausMathlib.BHKS.supportProduct (L : Hex.BhksLatticeBasis) (S : LiftedFactorSupport L) : Hex.ZPoly

Product of the lifted factors selected by a support, using the factor order stored in the BHKS lattice basis. The definition indexes by factorCount rather than the raw array size so it remains well-typed for abstract BhksLatticeBasis values; TrueFactorLift.basis_eq ties these together for the executable basis.

Equations

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

noncomputable def HexBerlekampZassenhausMathlib.BHKS.supportCldSum (L : Hex.BhksLatticeBasis) (S : LiftedFactorSupport L) (f : Hex.ZPoly) (p a : ℕ) : Hex.ZPoly

Sum of the per-selected-factor executable CLD quotients, taken over the same factor order as supportProduct. Its j-th coefficient is the pre-psiCut, pre-indicator column-j entry of the true-factor CLD vector; the centering (psiCut) and indicator weighting are layered on top by the tight-column work described later in this module.

Equations

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

structure HexBerlekampZassenhausMathlib.BHKS.RecoveredLift (L : Hex.BhksLatticeBasis) (S : LiftedFactorSupport L) : Type

Proof-facing package for a true factor in the direct Hensel coordinate.

The selected monic local product represents the integer factor only up to the two constant scales inherent in the direct coordinate:

• leadingCoeff f converts the monic Hensel target back to the input coordinate;

• factorScale is the leading coefficient of the complementary integer factor.

scaledProduct_congr records precisely that proportionality modulo the Hensel modulus. inputScale_coprime says the input leading coefficient is a unit there, which is the exact scalar cancelled after the monic support product is cancelled in logarithmic derivatives. There is no dilation-coordinate recovery equation in this interface.

• f : Hex.ZPoly

  The integer polynomial from which the lattice was constructed.

• p : ℕ

  The prime underlying the Hensel lift.

• a : ℕ

  The exponent in the lift modulus p ^ a.

• liftedFactors : Array Hex.ZPoly

  The local factors used to construct the lattice.

• basis_eq : L = Hex.bhksLatticeBasis self.f self.p self.a self.liftedFactors

  The abstract lattice is the lattice constructed from these data.

• factor : Hex.ZPoly

  The integer factor represented by the support.

• cofactor : Hex.ZPoly

  The complementary integer factor.

• factor_mul : self.factor * self.cofactor = self.f

  The factor and cofactor multiply to the input polynomial.

• factorScale : ℤ

  The scalar relating the support product to the represented factor.

• inputScale_coprime : (Hex.DensePoly.leadingCoeff self.f).gcd (Int.ofNat (self.p ^ self.a)) = 1

  The input leading coefficient is invertible modulo the lift modulus.

• scaledProduct_congr : Hex.ZPoly.congr (Hex.DensePoly.scale (Hex.DensePoly.leadingCoeff self.f) (supportProduct L S)) (Hex.DensePoly.scale self.factorScale self.factor) (self.p ^ self.a)

  The scaled support product agrees with the scaled factor modulo the lift modulus.

theorem HexBerlekampZassenhausMathlib.BHKS.finRange_foldl_add_eq_sum {M : Type u_1} [AddCommMonoid M] {n : ℕ} (g : Fin n → M) : List.foldl (fun (acc : M) (i : Fin n) => acc + g i) 0 (List.finRange n) = ∑ i : Fin n, g i

A fold-sum over List.finRange n equals the finite sum over Fin n.

theorem HexBerlekampZassenhausMathlib.BHKS.vecMul_getElem_eq_sum {n m : ℕ} (M : Hex.Matrix ℤ n m) (c : Vector ℤ n) (k : Fin m) : (Hex.Matrix.vecMul c M)[k] = ∑ i : Fin n, M[i][k] * c[i]

The entry of a row combination at column k is the explicit finite sum, over the row index, of the column-k matrix entries weighted by the coefficients.

theorem HexBerlekampZassenhausMathlib.BHKS.matrixRow_memLattice {n m : ℕ} (M : Hex.Matrix ℤ n m) (i : Fin n) : M.memLattice (M.row i)

Every matrix row belongs to the integer lattice generated by the matrix.

structure HexBerlekampZassenhausMathlib.BHKS.SupportShortVectorData (L : Hex.BhksLatticeBasis) (S : LiftedFactorSupport L) : Type

Certificate for an arbitrary short BHKS lattice vector whose first block is the indicator of a true lifted-factor support.

This is the projection surface needed by period-adjusted BHKS arguments: the short vector need not be the zero-period-row trueFactorCLDVector; it only has to lie in the BHKS row lattice, project to the support indicator, and satisfy the tight cut radius bound.

• vector : Vector ℤ (L.factorCount + L.coeffWidth)

  A short vector in the row lattice.

• memLattice : L.basis.memLattice self.vector

  The vector is an integer combination of the lattice rows.

• project_eq (i : Fin L.factorCount) : self.vector[⟨↑i, ⋯⟩] = indicatorVector S i

  The first coordinates form the indicator vector of S.

• four_mul_sq_norm_le : 4 * ∑ i : Fin (L.factorCount + L.coeffWidth), ↑self.vector[i] ^ 2 ≤ ↑(Hex.bhksCutRadiusSq4 L)

  Four times the squared Euclidean norm is within the cut radius.

theorem HexBerlekampZassenhausMathlib.BHKS.SupportShortVectorData.coord_natAbs_le {L : Hex.BhksLatticeBasis} {S : LiftedFactorSupport L} (D : SupportShortVectorData L S) (x : Fin (L.factorCount + L.coeffWidth)) : D.vector[x].natAbs ≤ Hex.bhksCutRadiusSq4 L

Every coordinate of a support short vector is bounded by the BHKS cut radius. This deliberately uses the radius itself, rather than its square root, so that the later integral coefficient estimate stays elementary.

def HexBerlekampZassenhausMathlib.BHKS.BhksBlockForm (L : Hex.BhksLatticeBasis) : Prop

The BHKS block-form predicate: L.basis is the all-coefficients CLD row basis [ I | A_tilde; 0 | diag ] built by bhksLatticeEntry from L's own data. This holds definitionally for Hex.bhksLatticeBasis (see bhksLatticeBasis_blockForm) and is the only fact the canonical coordinate producers need about the basis.

Equations

• HexBerlekampZassenhausMathlib.BHKS.BhksBlockForm L = (L.basis = Hex.Matrix.ofFn (Hex.bhksLatticeEntry L.factorCount L.coeffWidth L.p L.precision L.cutThresholds L.cldRows))

theorem HexBerlekampZassenhausMathlib.BHKS.bhksLatticeBasis_blockForm (f : Hex.ZPoly) (p a : ℕ) (liftedFactors : Array Hex.ZPoly) : BhksBlockForm (Hex.bhksLatticeBasis f p a liftedFactors)

The executable bhksLatticeBasis has block form by construction.

theorem HexBerlekampZassenhausMathlib.BHKS.vecMul_first_of_blockForm (L : Hex.BhksLatticeBasis) (hL : BhksBlockForm L) (c : Vector ℤ (L.factorCount + L.coeffWidth)) (i : Fin L.factorCount) : (Hex.Matrix.vecMul c L.basis)[Fin.castAdd L.coeffWidth i] = c[Fin.castAdd L.coeffWidth i]

The first block of a row combination of a BHKS block-form basis is exactly the first block of its row-coefficient vector.

theorem HexBerlekampZassenhausMathlib.BHKS.vecMul_tail_of_blockForm (L : Hex.BhksLatticeBasis) (hL : BhksBlockForm L) (c : Vector ℤ (L.factorCount + L.coeffWidth)) (j : Fin L.coeffWidth) : (Hex.Matrix.vecMul c L.basis)[Fin.natAdd L.factorCount j] = ∑ i : Fin L.factorCount, c[Fin.castAdd L.coeffWidth i] * (L.cldRows.getD ↑i #[]).getD (↑j) 0 + Int.ofNat (L.p ^ (L.precision - L.cutThresholds.getD (↑j) 0)) * c[Fin.natAdd L.factorCount j]

The tail block of a row combination of a BHKS block-form basis is its CLD column combination plus the corresponding diagonal-period contribution.

theorem HexBerlekampZassenhausMathlib.BHKS.RecoveredLift.blockForm {L : Hex.BhksLatticeBasis} {S : LiftedFactorSupport L} (D : RecoveredLift L S) : BhksBlockForm L

A recovered lift package supplies the BHKS block form used by coordinate and norm-bound reducers.

theorem HexBerlekampZassenhausMathlib.BHKS.RecoveredLift.liftedFactors_eq {L : Hex.BhksLatticeBasis} {S : LiftedFactorSupport L} (D : RecoveredLift L S) : L.liftedFactors = D.liftedFactors

The packaged basis carries exactly the lifted-factor array used to build the executable BHKS lattice.

theorem HexBerlekampZassenhausMathlib.BHKS.RecoveredLift.cutThresholds_eq {L : Hex.BhksLatticeBasis} {S : LiftedFactorSupport L} (D : RecoveredLift L S) : L.cutThresholds = Hex.bhksCutThresholds D.f D.p

The packaged basis carries exactly the cut thresholds computed from the input polynomial and prime.

theorem HexBerlekampZassenhausMathlib.BHKS.RecoveredLift.cldRows_eq {L : Hex.BhksLatticeBasis} {S : LiftedFactorSupport L} (D : RecoveredLift L S) : L.cldRows = Array.map (fun (g : Hex.ZPoly) => Hex.cldCoeffs D.f D.p D.a g) D.liftedFactors

The packaged basis carries exactly the CLD rows computed from the concrete lifted factors.

theorem HexBerlekampZassenhausMathlib.BHKS.RecoveredLift.factorCount_eq {L : Hex.BhksLatticeBasis} {S : LiftedFactorSupport L} (D : RecoveredLift L S) : L.factorCount = D.liftedFactors.size

The packaged basis factor count is exactly the concrete lifted-factor array size.

theorem HexBerlekampZassenhausMathlib.BHKS.RecoveredLift.coeffWidth_eq {L : Hex.BhksLatticeBasis} {S : LiftedFactorSupport L} (D : RecoveredLift L S) : L.coeffWidth = Hex.DensePoly.natDegree D.f

The packaged basis coefficient width is exactly the input polynomial degree used by the executable CLD rows.

theorem HexBerlekampZassenhausMathlib.BHKS.RecoveredLift.p_eq {L : Hex.BhksLatticeBasis} {S : LiftedFactorSupport L} (D : RecoveredLift L S) : L.p = D.p

The packaged basis modulus base is exactly the recovered lift's prime.

theorem HexBerlekampZassenhausMathlib.BHKS.RecoveredLift.precision_eq {L : Hex.BhksLatticeBasis} {S : LiftedFactorSupport L} (D : RecoveredLift L S) : L.precision = D.a

The packaged basis precision is exactly the recovered lift's Hensel precision.

def HexBerlekampZassenhausMathlib.BHKS.supportEquivalent {r : ℕ} (trueSupports : Set (Set (Fin r))) (j k : Fin r) : Prop

Two supports are equivalent when every projected row is constant across them.

Equations

• HexBerlekampZassenhausMathlib.BHKS.supportEquivalent trueSupports j k = ∀ S ∈ trueSupports, j ∈ S ↔ k ∈ S

def HexBerlekampZassenhausMathlib.BHKS.supportEquivalentAt {r : ℕ} (trueSupports : Set (Set (Fin r))) (j k : ℕ) : Prop

Nat-indexed form of supportEquivalent, convenient for filtering List.range r while retaining proof irrelevance for the bounds.

Equations

• HexBerlekampZassenhausMathlib.BHKS.supportEquivalentAt trueSupports j k = ∃ (hj : j < r) (hk : k < r), HexBerlekampZassenhausMathlib.BHKS.supportEquivalent trueSupports ⟨j, hj⟩ ⟨k, hk⟩

theorem HexBerlekampZassenhausMathlib.BHKS.supportEquivalentAt_iff {r : ℕ} (trueSupports : Set (Set (Fin r))) {j k : ℕ} (hj : j < r) (hk : k < r) : supportEquivalentAt trueSupports j k ↔ supportEquivalent trueSupports ⟨j, hj⟩ ⟨k, hk⟩

The natural-index and finite-index forms of support equivalence agree in range.

theorem HexBerlekampZassenhausMathlib.BHKS.supportEquivalentAt_refl {r : ℕ} (trueSupports : Set (Set (Fin r))) {j : ℕ} (hj : j < r) : supportEquivalentAt trueSupports j j

Support equivalence is reflexive on in-range indices.

theorem HexBerlekampZassenhausMathlib.BHKS.supportEquivalentAt_symm {r : ℕ} (trueSupports : Set (Set (Fin r))) {j k : ℕ} (h : supportEquivalentAt trueSupports j k) : supportEquivalentAt trueSupports k j

Support equivalence is symmetric.

theorem HexBerlekampZassenhausMathlib.BHKS.supportEquivalentAt_trans {r : ℕ} (trueSupports : Set (Set (Fin r))) {i j k : ℕ} (hij : supportEquivalentAt trueSupports i j) (hjk : supportEquivalentAt trueSupports j k) : supportEquivalentAt trueSupports i k

Support equivalence is transitive.

noncomputable def HexBerlekampZassenhausMathlib.BHKS.supportRepresentativeColumns {r : ℕ} (trueSupports : Set (Set (Fin r))) : List ℕ

Minimum representatives of support-equivalence classes, emitted in ascending column order.

Equations

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

noncomputable def HexBerlekampZassenhausMathlib.BHKS.supportClassMembers {r : ℕ} (trueSupports : Set (Set (Fin r))) (rep : ℕ) : List ℕ

The support-equivalence class represented by rep, listed in ascending column order.

Equations

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

noncomputable def HexBerlekampZassenhausMathlib.BHKS.supportPartitionByMinColumn {r : ℕ} (trueSupports : Set (Set (Fin r))) : List (List ℕ)

Canonical partition of columns by true-support membership signatures.

Equations

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

def HexBerlekampZassenhausMathlib.BHKS.classIndicatorArray (r : ℕ) (members : List ℕ) : Array ℤ

The executable indicator-array shape for a finite Nat-indexed class.

Equations

• HexBerlekampZassenhausMathlib.BHKS.classIndicatorArray r members = (List.map (fun (i : ℕ) => if i ∈ members then 1 else 0) (List.range r)).toArray

@[simp]

theorem HexBerlekampZassenhausMathlib.BHKS.classIndicatorArray_size (r : ℕ) (members : List ℕ) : (classIndicatorArray r members).size = r

A class indicator array has one entry per column.

theorem HexBerlekampZassenhausMathlib.BHKS.classIndicatorArray_getD (r : ℕ) (members : List ℕ) (i : ℕ) : (classIndicatorArray r members).getD i 0 = if i < r ∧ i ∈ members then 1 else 0

Entries of a class indicator are one exactly at in-range class members.

theorem HexBerlekampZassenhausMathlib.BHKS.classIndicatorArray_bits (r : ℕ) (members : List ℕ) (i : ℕ) : i < (classIndicatorArray r members).size → (classIndicatorArray r members).getD i 0 = 0 ∨ (classIndicatorArray r members).getD i 0 = 1

Every entry of a class indicator is zero or one.

theorem HexBerlekampZassenhausMathlib.BHKS.classIndicatorArray_has_one_of_mem (r : ℕ) (members : List ℕ) {i : ℕ} (hi : i < r) (hmem : i ∈ members) : (classIndicatorArray r members).getD i 0 = 1

Every in-range class member has indicator entry one.

theorem HexBerlekampZassenhausMathlib.BHKS.mem_supportRepresentativeColumns_iff {r : ℕ} (trueSupports : Set (Set (Fin r))) (rep : ℕ) : rep ∈ supportRepresentativeColumns trueSupports ↔ rep < r ∧ ∀ k < rep, ¬supportEquivalentAt trueSupports k rep

Support-class representatives are precisely the least indices in their classes.

theorem HexBerlekampZassenhausMathlib.BHKS.supportRepresentativeColumns_lt {r : ℕ} (trueSupports : Set (Set (Fin r))) {rep : ℕ} (hrep : rep ∈ supportRepresentativeColumns trueSupports) : rep < r

Every support-class representative is a valid column index.

theorem HexBerlekampZassenhausMathlib.BHKS.supportRepresentativeColumns_min {r : ℕ} (trueSupports : Set (Set (Fin r))) {rep : ℕ} (hrep : rep ∈ supportRepresentativeColumns trueSupports) (k : ℕ) : k < rep → ¬supportEquivalentAt trueSupports k rep

No earlier column is support-equivalent to a representative.

theorem HexBerlekampZassenhausMathlib.BHKS.mem_supportClassMembers_iff {r : ℕ} (trueSupports : Set (Set (Fin r))) (rep j : ℕ) : j ∈ supportClassMembers trueSupports rep ↔ j < r ∧ supportEquivalentAt trueSupports j rep

A column belongs to a representative's class exactly when it is equivalent and in range.

theorem HexBerlekampZassenhausMathlib.BHKS.supportClassMembers_rep_mem {r : ℕ} (trueSupports : Set (Set (Fin r))) {rep : ℕ} (hrep : rep ∈ supportRepresentativeColumns trueSupports) : rep ∈ supportClassMembers trueSupports rep

Every support-class representative belongs to its own class.

theorem HexBerlekampZassenhausMathlib.BHKS.exists_passing_index_of_lt_prefixCount (L : Hex.BhksLatticeBasis) (reduced : Hex.Matrix ℤ (L.factorCount + L.coeffWidth) (L.factorCount + L.coeffWidth)) (j : Fin (L.factorCount + L.coeffWidth)) (hj : ↑j < Hex.bhksCutPrefixCount L reduced) : ∃ (k : Fin (L.factorCount + L.coeffWidth)), ↑j ≤ ↑k ∧ Hex.bhksWithinGramSchmidtCut L (Hex.GramSchmidt.Int.gramDetVec reduced) k = true

Every retained-prefix index is at or before some Gram--Schmidt index that actually passes the executable cut. This is the converse direction needed to control the norms of rows kept only because a later row passes.

theorem HexBerlekampZassenhausMathlib.BHKS.bhksWithinGramSchmidtCut_lt_prefixCount (L : Hex.BhksLatticeBasis) (reduced : Hex.Matrix ℤ (L.factorCount + L.coeffWidth) (L.factorCount + L.coeffWidth)) (k : Fin (L.factorCount + L.coeffWidth)) (hk : Hex.bhksWithinGramSchmidtCut L (Hex.GramSchmidt.Int.gramDetVec reduced) k = true) : ↑k < Hex.bhksCutPrefixCount L reduced

A Gram-Schmidt index that passes the executable cut test lies strictly below the retained prefix length bhksCutPrefixCount, so its row is kept.

theorem HexBerlekampZassenhausMathlib.BHKS.bhksWithinGramSchmidtCut_eq_true_of_le (L : Hex.BhksLatticeBasis) (dets : Vector ℕ (L.factorCount + L.coeffWidth + 1)) (i : Fin (L.factorCount + L.coeffWidth)) (hne : dets.get ⟨↑i, ⋯⟩ ≠ 0) (hle : 4 * (↑(dets.get ⟨↑i + 1, ⋯⟩) / ↑(dets.get ⟨↑i, ⋯⟩)) ≤ ↑(Hex.bhksCutRadiusSq4 L)) : Hex.bhksWithinGramSchmidtCut L dets i = true

The executable cut test passes at index i once the stored leading Gram determinant at i is nonzero and the radius inequality on the consecutive determinant ratio holds.

theorem HexBerlekampZassenhausMathlib.BHKS.bhksWithinGramSchmidtCut_le_of_eq_true (L : Hex.BhksLatticeBasis) (dets : Vector ℕ (L.factorCount + L.coeffWidth + 1)) (i : Fin (L.factorCount + L.coeffWidth)) (hpass : Hex.bhksWithinGramSchmidtCut L dets i = true) : 4 * (↑(dets.get ⟨↑i + 1, ⋯⟩) / ↑(dets.get ⟨↑i, ⋯⟩)) ≤ ↑(Hex.bhksCutRadiusSq4 L)

A successful executable cut test exposes its determinant-ratio inequality.

theorem HexBerlekampZassenhausMathlib.BHKS.retainedRow_normSq_le (L : Hex.BhksLatticeBasis) (reduced : Hex.Matrix ℤ (L.factorCount + L.coeffWidth) (L.factorCount + L.coeffWidth)) (hind : Hex.GramSchmidt.Int.independent reduced) (hred : Hex.isLLLReduced reduced (3 / 4) (1 / 2)) (j : Fin (L.factorCount + L.coeffWidth)) (hj : ↑j < Hex.bhksCutPrefixCount L reduced) : 4 * ↑(reduced.row j).normSq ≤ ↑(L.factorCount + L.coeffWidth) * 2 ^ (L.factorCount + L.coeffWidth - 1) * ↑(Hex.bhksCutRadiusSq4 L)

Every row in the retained prefix has a certified norm bound. A retained row need not itself pass the cut: the witness may be a later passing Gram--Schmidt row. The generic reduced-row estimate accounts for precisely that prefix behavior.

theorem HexBerlekampZassenhausMathlib.BHKS.traceRetainedRow_normSq_le (L : Hex.BhksLatticeBasis) (hrows : 1 ≤ L.factorCount + L.coeffWidth) (hind : Hex.GramSchmidt.Int.independent L.basis) (j : Fin (L.factorCount + L.coeffWidth)) (hj : ↑j < Hex.bhksCutPrefixCount L (Hex.bhksProjectedRowsTrace L hrows).reducedMatrix) : 4 * ↑((Hex.bhksProjectedRowsTrace L hrows).reducedMatrix.row j).normSq ≤ ↑(L.factorCount + L.coeffWidth) * 2 ^ (L.factorCount + L.coeffWidth - 1) * ↑(Hex.bhksCutRadiusSq4 L)

Executable-trace specialization of retainedRow_normSq_le: every source row selected by bhksProjectedRowsTrace satisfies the retained-prefix norm bound.

theorem HexBerlekampZassenhausMathlib.BHKS.traceRetainedRow_coord_natAbs_le (L : Hex.BhksLatticeBasis) (hrows : 1 ≤ L.factorCount + L.coeffWidth) (hind : Hex.GramSchmidt.Int.independent L.basis) (j : Fin (L.factorCount + L.coeffWidth)) (hj : ↑j < Hex.bhksCutPrefixCount L (Hex.bhksProjectedRowsTrace L hrows).reducedMatrix) (x : Fin (L.factorCount + L.coeffWidth)) : ((Hex.bhksProjectedRowsTrace L hrows).reducedMatrix.row j)[x].natAbs ≤ (L.factorCount + L.coeffWidth) * 2 ^ (L.factorCount + L.coeffWidth) * Hex.bhksCutRadiusSq4 L

Every coordinate of a retained LLL row is bounded by a deliberately coarse integral envelope for the retained-row norm estimate.

theorem HexBerlekampZassenhausMathlib.BHKS.mem_prefixSubmodule_of_normSq_le (L : Hex.BhksLatticeBasis) (reduced : Hex.Matrix ℤ (L.factorCount + L.coeffWidth) (L.factorCount + L.coeffWidth)) (hind : Hex.GramSchmidt.Int.independent reduced) (v : Vector ℤ (L.factorCount + L.coeffWidth)) (hv : reduced.memLattice v) (hnorm : 4 * ↑v.normSq ≤ ↑(Hex.bhksCutRadiusSq4 L)) : HexMatrixMathlib.vectorEquiv v ∈ HexLLLMathlib.prefixSubmodule reduced (Hex.bhksCutPrefixCount L reduced)

BHKS prefix survivor-span (Lemma 5.7, forward).

Any lattice vector v of the reduced BHKS basis whose squared length passes the cut test (4·‖v‖² ≤ bhksCutRadiusSq4) lies in the integer span of the retained prefix rows b_0 … b_{t-1}, where t = bhksCutPrefixCount.

The cut keeps a row i iff 4·‖b*_i‖² ≤ bhksCutRadiusSq4, i.e. ‖b*_i‖² ≤ bhksCutRadiusSq4 / 4; the hypothesis is the matching tight bound on v (four times its squared norm within the radius), not the loose ‖v‖² ≤ bhksCutRadiusSq4.

structure HexBerlekampZassenhausMathlib.BHKS.CutProjectionHypotheses (L : Hex.BhksProjectedRows) (trueSupports : Set (Set (Fin L.factorCount))) : Prop

Cut hypotheses needed to connect the executable projected rows to the abstract true-factor supports. Later B4/B5 work discharges indicator_mem_projected from the BHKS norm bound and Gram-Schmidt cut soundness.

• indicator_mem_projected (S : ↑trueSupports) : indicatorVector ↑S ∈ projectedRowSpanInt L

  Every genuine support indicator belongs to the span of the projected rows.

theorem HexBerlekampZassenhausMathlib.BHKS.trueSupportSpanInt_le_projectedRowSpanInt (L : Hex.BhksProjectedRows) (trueSupports : Set (Set (Fin L.factorCount))) (hcut : CutProjectionHypotheses L trueSupports) : trueSupportSpanInt trueSupports ≤ projectedRowSpanInt L

The existing per-support cut theorem is exactly the forward lattice containment W ≤ L'.

theorem HexBerlekampZassenhausMathlib.BHKS.projectedRowSpanInt_le_trueSupportSpanInt_of_rows (L : Hex.BhksProjectedRows) (trueSupports : Set (Set (Fin L.factorCount))) (hrows : ∀ (i : Fin L.projectedRows.size), (projectedRowsIntMatrix L).row i ∈ trueSupportSpanInt trueSupports) : projectedRowSpanInt L ≤ trueSupportSpanInt trueSupports

Reverse containment reduces to checking the retained projected generators. This is the proof-facing endpoint of the bad-vector contradiction: once every retained projected row is in W, its whole integer span is in W.

theorem HexBerlekampZassenhausMathlib.BHKS.projectedRow_mem_projectedRowSpanInt (L : Hex.BhksProjectedRows) (i : Fin L.projectedRows.size) : (projectedRowsIntMatrix L).row i ∈ projectedRowSpanInt L

Every projected matrix row belongs to the integer span of the projected rows.