def HexBerlekampZassenhausMathlib.BHKS.projFirst (r n : ℕ) : (Fin (r + n) → ℤ) →ₗ[ℤ] Fin r → ℤ

Projection onto the first r coordinates as a ℤ-linear map.

Equations

• HexBerlekampZassenhausMathlib.BHKS.projFirst r n = { toFun := fun (w : Fin (r + n) → ℤ) (i : Fin r) => w (Fin.castAdd n i), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem HexBerlekampZassenhausMathlib.BHKS.projFirst_apply (r n : ℕ) (w : Fin (r + n) → ℤ) (i : Fin r) : (projFirst r n) w i = w (Fin.castAdd n i)

Application rule for the first-block projection.

theorem HexBerlekampZassenhausMathlib.BHKS.projFirst_vectorEquiv_row_mem (L : Hex.BhksLatticeBasis) (hrows : 1 ≤ L.factorCount + L.coeffWidth) (i : Fin (L.factorCount + L.coeffWidth)) (hi : ↑i < Hex.bhksCutPrefixCount L (Hex.bhksProjectedRowsTrace L hrows).reducedMatrix) : (projFirst L.factorCount L.coeffWidth) (HexMatrixMathlib.vectorEquiv ((Hex.bhksProjectedRowsTrace L hrows).reducedMatrix.row i)) ∈ projectedRowSpanInt (Hex.bhksProjectedRows L hrows)

A retained prefix row, projected to its first block, is a generator of the executable projected integer row span.

theorem HexBerlekampZassenhausMathlib.BHKS.projectedRow_exists_retainedSource (L : Hex.BhksLatticeBasis) (hrows : 1 ≤ L.factorCount + L.coeffWidth) (i : Fin (Hex.bhksProjectedRows L hrows).projectedRows.size) : ∃ (j : Fin (L.factorCount + L.coeffWidth)), ↑j < Hex.bhksCutPrefixCount L (Hex.bhksProjectedRowsTrace L hrows).reducedMatrix ∧ ∀ (k : Fin L.factorCount), ((Hex.bhksProjectedRows L hrows).projectedRows.getD ↑i #[]).getD (↑k) 0 = ((Hex.bhksProjectedRowsTrace L hrows).reducedMatrix.row j)[Fin.castAdd L.coeffWidth k]

Every executable projected row comes from a retained row of the traced LLL-reduced basis, and is exactly that row's first-coordinate block.

theorem HexBerlekampZassenhausMathlib.BHKS.projFirst_mem_projectedRowSpanInt_of_mem_prefixSubmodule (L : Hex.BhksLatticeBasis) (hrows : 1 ≤ L.factorCount + L.coeffWidth) (w : Fin (L.factorCount + L.coeffWidth) → ℤ) (hw : w ∈ HexLLLMathlib.prefixSubmodule (Hex.bhksProjectedRowsTrace L hrows).reducedMatrix (Hex.bhksCutPrefixCount L (Hex.bhksProjectedRowsTrace L hrows).reducedMatrix)) : (projFirst L.factorCount L.coeffWidth) w ∈ projectedRowSpanInt (Hex.bhksProjectedRows L hrows)

Projecting a vector of the retained prefix submodule to its first block lands in the executable projected integer row span.

theorem HexBerlekampZassenhausMathlib.BHKS.cutProjectionHypotheses_of_shortVectors (L : Hex.BhksLatticeBasis) (hrows : 1 ≤ L.factorCount + L.coeffWidth) (hbasis : L.basis.independent) (trueSupports : Set (Set (Fin (Hex.bhksProjectedRows L hrows).factorCount))) (data : (S : ↑trueSupports) → SupportShortVectorData L ↑S) : CutProjectionHypotheses (Hex.bhksProjectedRows L hrows) trueSupports

Build CutProjectionHypotheses from any per-support short vector in the BHKS row lattice.

The vector may include nonzero diagonal-period row coefficients. The prefix survivor-span lemma only needs lattice membership plus the tight cut-radius bound, and the final projection only needs the first block to be the support indicator.

@[simp]

theorem HexBerlekampZassenhausMathlib.BHKS.intVectorToRat_zero {r : ℕ} : intVectorToRat 0 = 0

intVectorToRat of the zero vector is the zero rational vector.

@[simp]

theorem HexBerlekampZassenhausMathlib.BHKS.intVectorToRat_add {r : ℕ} (u v : Fin r → ℤ) : intVectorToRat (u + v) = intVectorToRat u + intVectorToRat v

intVectorToRat commutes with pointwise addition.

@[simp]

theorem HexBerlekampZassenhausMathlib.BHKS.intVectorToRat_intSmul {r : ℕ} (n : ℤ) (v : Fin r → ℤ) : intVectorToRat (n • v) = ↑n • intVectorToRat v

intVectorToRat of an integer-scalar multiple is the rational-cast scalar times the rational vector.

theorem HexBerlekampZassenhausMathlib.BHKS.intVectorToRat_mem_span_rat_of_mem_span_int {r : ℕ} {S : Set (Fin r → ℤ)} {v : Fin r → ℤ} (hv : v ∈ Submodule.span ℤ S) : intVectorToRat v ∈ Submodule.span ℚ (intVectorToRat '' S)

Membership in the integer span carries over to membership of the rational-cast vector in the rational span of the rational-cast generators.

theorem HexBerlekampZassenhausMathlib.BHKS.row_projectedRowsRatMatrix_eq_intVectorToRat (L : Hex.BhksProjectedRows) (i : Fin L.projectedRows.size) : (projectedRowsRatMatrix L).row i = intVectorToRat ((projectedRowsIntMatrix L).row i)

The rational projected row is the pointwise rational cast of the integer projected row. Both projectedRowsRatMatrix and projectedRowsIntMatrix read the same underlying L.projectedRows array; the only difference is the codomain.

theorem HexBerlekampZassenhausMathlib.BHKS.range_row_projectedRowsRatMatrix_eq_image (L : Hex.BhksProjectedRows) : (Set.range fun (i : Fin L.projectedRows.size) => (projectedRowsRatMatrix L).row i) = intVectorToRat '' Set.range fun (i : Fin L.projectedRows.size) => (projectedRowsIntMatrix L).row i

The range of the rational projected rows is the image of the range of the integer projected rows under intVectorToRat.