theorem Hex.exactQuotient?_eq_some_of_pos_lc_pos_degree_mul_eq {target candidate quotient : ZPoly} (hpos_lc : 0 < DensePoly.leadingCoeff candidate) (hdegree : 0 < DensePoly.natDegree candidate) (hmul : quotient * candidate = target) : exactQuotient? target candidate = some quotient

Non-monic converse to exactQuotient?_product for divisors with positive leading coefficient. Drops the Monic hypothesis from exactQuotient?_eq_some_of_mul_eq_monic_of_pos_degree in favour of 0 < leadingCoeff candidate, handling the executable division through ZPoly.divMod_eq_mul and packaging the result with exactQuotient?_eq_some_of_divMod_eq_of_shouldRecord. Positive degree alone discharges shouldRecordPolynomialFactor, since 0, C 1, and C (-1) all have natDegree = 0.

def Hex.integerRootCandidates (f : ZPoly) : List Int

Positive and negative divisors of the constant coefficient, hence all possible integer roots.

Equations

• Hex.integerRootCandidates f = List.flatMap (fun (d : Nat) => have r := Int.ofNat d; [r, -r]) (Hex.positiveDivisors✝ (Hex.DensePoly.coeff f 0).natAbs)

def Hex.linearFactorForRoot (r : Int) : ZPoly

The monic polynomial X - r.

Equations

• Hex.linearFactorForRoot r = Hex.DensePoly.ofCoeffs #[-r, 1]

def Hex.splitIntegerRootFactorsAux : ZPoly → List Int → Nat → Array ZPoly × ZPoly

Remove integer-root factors using bounded repeated exact division.

Equations

• One or more equations did not get rendered due to their size.
• Hex.splitIntegerRootFactorsAux x✝¹ x✝ 0 = (#[], x✝¹)
• Hex.splitIntegerRootFactorsAux x✝ [] _fuel.succ = (#[], x✝)

def Hex.quadraticRootCandidates (core : ZPoly) : List Int

For a polynomial of degree two, its at most two integer roots from the quadratic formula. Callers must establish core.natDegree = 2. The integer square root is computed by Newton iteration, so this does not enumerate divisors of the constant coefficient. Exact evaluation rejects nonintegral quotients; exact polynomial division in the caller checks every proposed factor.

Equations

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

def Hex.quadraticIntegerRootFactors? (core : ZPoly) : Option (Array ZPoly)

Factor a quadratic using its integer roots from the quadratic formula. A decline leaves the general modular factorization route available, including quadratics whose rational roots are both nonintegral.

Equations

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

def Hex.exhaustiveIntegerTrialCoreFactorsWithBound (core : ZPoly) (B : Nat) : Array ZPoly

Standalone integer trial-division algorithm for the slow factorization path.

First peels monic linear integer-root factors (x - r) off core via splitIntegerRootFactorsAux, then enumerates non-unit polynomial candidates of degrees 1..deg(afterLinear)/2 with coefficients in [-B, B], dividing each in turn into the running residual. The returned array consists of the linear factors, the bounded-coefficient factors that exactly divided the residual, and the final residual (omitted when it collapses to 1).

The companion theorems exhaustiveIntegerTrialCoreFactorsWithBound_polyProduct, exhaustiveIntegerTrialCoreFactorsWithBound_normalizeFactorSign, and exhaustiveIntegerTrialCoreFactorsWithBound_shouldRecord record the local executable invariants needed by the slow-path factorization reassembly callers.

Equations

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

def Hex.centeredModNat (z : Int) (m : Nat) : Int

The centred representative of z modulo the natural number m.

Equations

• Hex.centeredModNat z m = if m = 0 then z else have r := z % Int.ofNat m; if 2 * r.natAbs ≤ m then r else if r < 0 then r + Int.ofNat m else r - Int.ofNat m

theorem Hex.centeredModNat_zero (m : Nat) : centeredModNat 0 m = 0

Zero is already its centred representative for every modulus.

theorem Hex.centeredModNat_emod_eq_of_natAbs_le (z : Int) (m B : Nat) (hbound : z.natAbs ≤ B) (hsep : 2 * B < m) : centeredModNat (z % ↑m) m = z

Centred reduction recovers an integer whose absolute value is below half the modulus.

structure Hex.LiftModulus : Type

A modulus prepared for repeated centred reduction.

centeredModNat states what the centred representative is: reduce, then subtract the modulus when the residue is past halfway. Evaluating that statement literally derives two values at every call -- the modulus in integer form, and the doubled residue the halfway test 2 * r.natAbs ≤ m compares against. At recovery precision the second is a fresh multi-limb natural, allocated and freed once per leaf. A traversal that reduces against one fixed modulus millions of times wants neither: comparing the residue against a recorded m / 2 decides the same test and builds nothing.

The proof fields pin both derived values to the natural one, so a reduction reading this object is interchangeable with one reading the modulus directly; centered_eq is that statement.

• nat : Nat

  The modulus.

• int : Int

  The modulus as an integer.

• half : Int

  The largest residue that is its own centred representative, nat / 2.

• int_eq : self.int = ↑self.nat

  The recorded integer modulus is the modulus.

• half_eq : self.half = ↑(self.nat / 2)

  The recorded threshold is half the modulus, rounded down.

def Hex.LiftModulus.ofNat (m : Nat) : LiftModulus

Prepare a natural number for repeated centred reduction.

Equations

• Hex.LiftModulus.ofNat m = { nat := m, int := ↑m, half := ↑(m / 2), int_eq := ⋯, half_eq := ⋯ }

@[simp]

theorem Hex.LiftModulus.nat_ofNat (m : Nat) : (ofNat m).nat = m

The prepared modulus records the natural number it was built from.

@[simp]

theorem Hex.LiftModulus.int_ofNat (m : Nat) : (ofNat m).int = ↑m

The prepared integer form is the cast of the underlying modulus.

@[simp]

theorem Hex.LiftModulus.half_ofNat (m : Nat) : (ofNat m).half = ↑(m / 2)

The prepared halfway threshold is half the modulus, rounded down.

theorem Hex.LiftModulus.eq_ofNat (m : LiftModulus) : m = ofNat m.nat

A prepared modulus carries no freedom beyond the modulus it records.

def Hex.LiftModulus.centered (m : LiftModulus) (z : Int) : Int

The centred representative of z against a prepared modulus.

z % modulus is already the least nonnegative residue, so the centred representative is that residue, less the modulus once it is past the recorded halfway threshold. No representation of the modulus is built here: both the reduction and the comparison read values the modulus arrived with.

Equations

• m.centered z = if m.nat = 0 then z else have r := z % m.int; if r ≤ m.half then r else r - m.int

theorem Hex.LiftModulus.centered_eq (m : LiftModulus) (z : Int) : m.centered z = centeredModNat z m.nat

Reducing against a prepared modulus computes the centred representative.

def Hex.centeredResiduePow (p b : Nat) (x : Int) : Int

Centred residue modulo p^b, the mod^± operation in the BHKS cut.

Equations

• Hex.centeredResiduePow p b x = Hex.centeredModNat x (p ^ b)

def Hex.psiCut (p a b : Nat) (x : Int) : Int

BHKS two-sided cut Psi^a_b(x) = (x_amb - (x_amb mod^± p^b)) / p^b, where x_amb := x mod^± p^a is the centered ambient representative.

Centering at the ambient modulus p^a before taking the lower-precision cut is required for the intended semantics: a CLD coefficient passed in as a nonnegative p^a-residue (p^a - c) of a negative exact value -c must be recentered to -c before applying the p^b cut. Without this step the cut produces an oversized output for negative exact coefficients, as shown by the f = x^2 - 5*x + 6, g = x - 2, p = 5, a = 6 counterexample to the old uncentered formulation.

Equations

• Hex.psiCut p a b x = if p ^ b = 0 then 0 else have xCentered := Hex.centeredResiduePow p a x; (xCentered - Hex.centeredResiduePow p b xCentered) / Int.ofNat (p ^ b)

def Hex.cldQuotientModBignum (f g : ZPoly) (p a : Nat) : ZPoly

Bignum reference for cldQuotientMod: reduce f * g' / g modulo p^a using Int polynomial arithmetic. This is the specification the word-sized fast path is proven byte-identical to (cldQuotientMod_eq_spec).

Equations

• Hex.cldQuotientModBignum f g p a = Hex.ZPoly.reduceModPow (Hex.DensePoly.divMod ((f * Hex.DensePoly.derivative g).reduceModPow p a) g).fst p a

def Hex.cldQuotientMod (f g : ZPoly) (p a : Nat) : ZPoly

Mod-p^a representative of f * g.derivative / g, the polynomial whose x^j coefficient is the integer CLD coefficient [x^j] Phi(g) reduced modulo p^a.

Exposed (rather than private) so the BHKS correspondence layer can state the congruence linking the executable quotient to the exact integer CLD coefficient.

Equations

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

def Hex.cldCoeffs (f : ZPoly) (p a : Nat) (g : ZPoly) : Array Int

Centred high-bit CLD coefficients for one lifted local factor.

The returned array has one entry for each coefficient index 0, ..., deg(f)-1; entry j is Psi^a_{ell_j}([x^j] (f * g.derivative / g mod p^a)).

Equations

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

def Hex.cldNumeratorCoeff (f g : ZPoly) (index : Nat) : Int

One coefficient of f * g.derivative, computed without forming the product polynomial.

Equations

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

def Hex.cldLeadingQuotientCoeffs (f g : ZPoly) (p a width : Nat) : Array Int

Leading coefficients of the monic quotient f * g.derivative / g modulo p^a, in descending degree order.

Monic long division determines the quotient from high degree downward. The recurrence therefore stops after width coefficients and avoids constructing the unused low-degree tail.

Equations

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

def Hex.cldLeadingCoeffs (f : ZPoly) (p a : Nat) (g : ZPoly) (width : Nat) : Array Int

Centred high-bit CLD coefficients for the leading width quotient coordinates, in descending degree order.

Equations

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

def Hex.aggregateCldTail (f : ZPoly) (p a j : Nat) (selectedFactors : Array ZPoly) : Int

Aggregate BHKS CLD tail entry for a selected family of lifted local factors.

Unlike cldCoeffs, this cuts once after summing the selected cldQuotientMod coefficients. This is the shape needed by the BHKS true-factor support column: wraparound is controlled on the aggregate residue, not on the sum of separately cut per-factor residues.

Equations

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

theorem Hex.centeredModNat_emod_self (z : Int) (m : Nat) : centeredModNat (z % ↑m) m = centeredModNat z m

centeredModNat depends only on its argument modulo m.

theorem Hex.self_sub_centeredModNat_dvd (z : Int) (m : Nat) : ↑m ∣ z - centeredModNat z m

centeredModNat chooses a representative congruent to the input modulo m.

theorem Hex.centeredResiduePow_add_pow_mul_psiCut (p a b : Nat) (z : Int) (hmod : p ^ b ≠ 0) : centeredResiduePow p a z = centeredResiduePow p b (centeredResiduePow p a z) + ↑(p ^ b) * psiCut p a b z

The BHKS cut decomposes the centered ambient representative into a lower centered residue plus p^b times the high-bit cut coefficient.

theorem Hex.centeredResiduePow_eq_of_natAbs_le (p a : Nat) (y z : Int) (B : Nat) (hbound : y.natAbs ≤ B) (hsep : 2 * B < p ^ a) (hcongr : y % ↑(p ^ a) = z % ↑(p ^ a)) : centeredResiduePow p a z = y

If y is an exact integer with |y| ≤ B, y ≡ z (mod p^a), and the ambient modulus p^a is large enough to separate the centered residue (2*B < p^a), then centeredResiduePow p a z = y.

theorem Hex.psiCut_eq_zero_of_natAbs_le (p a b : Nat) (y z : Int) (B : Nat) (hbound : y.natAbs ≤ B) (hsep_a : 2 * B < p ^ a) (hsep_b : 2 * B < p ^ b) (hcongr : y % ↑(p ^ a) = z % ↑(p ^ a)) : psiCut p a b z = 0

If an exact integer y with |y| ≤ B is congruent to z modulo p^a, and both the ambient modulus p^a and the lower cut modulus p^b separate B (2*B < p^a and 2*B < p^b), then the BHKS two-sided cut psiCut p a b z vanishes.

theorem Hex.abs_psiCut_le_of_natAbs_le (p a b : Nat) (y z : Int) (B : Nat) (hbound : y.natAbs ≤ B) (hsep_a : 2 * B < p ^ a) (hsep_b : 2 * B < p ^ b) (hcongr : y % ↑(p ^ a) = z % ↑(p ^ a)) : (psiCut p a b z).natAbs ≤ B

Absolute-value form of psiCut_eq_zero_of_natAbs_le: under the same hypotheses, |psiCut p a b z| ≤ B. Useful when callers carry the BHKS column bound B = bhksCoeffBound f j and just need an upper bound on the executable cut output.

theorem Hex.cldCoeffs_getD_of_lt (f : ZPoly) (p a : Nat) (g : ZPoly) (j : Nat) (h : j < DensePoly.natDegree f) : (cldCoeffs f p a g).getD j 0 = psiCut p a (bhksCoeffCutThreshold p f j) (DensePoly.coeff (cldQuotientMod f g p a) j)

In-range coordinate of cldCoeffs: for j < deg(f), the executable cldCoeffs array entry is exactly psiCut applied to the corresponding quotient coefficient.

theorem Hex.cldQuotientMod_coeff_decomp_of_lt (f g : ZPoly) (p a j : Nat) (hj : j < DensePoly.natDegree f) (hb : p ^ bhksCoeffCutThreshold p f j ≠ 0) : centeredResiduePow p a (DensePoly.coeff (cldQuotientMod f g p a) j) = centeredResiduePow p (bhksCoeffCutThreshold p f j) (centeredResiduePow p a (DensePoly.coeff (cldQuotientMod f g p a) j)) + ↑(p ^ bhksCoeffCutThreshold p f j) * (cldCoeffs f p a g).getD j 0

In-range CLD coefficients are the high-bit part of cldQuotientMod.

theorem Hex.cldQuotientMod_divMod_reconstruction (f g : ZPoly) (p a : Nat) (hg : DensePoly.Monic g) : have numerator := (f * DensePoly.derivative g).reduceModPow p a; (DensePoly.divMod numerator g).fst * g + (DensePoly.divMod numerator g).snd = numerator

Euclidean reconstruction for the division underlying cldQuotientMod: for a monic divisor g, the raw quotient and remainder of numerator / g recompose numerator, where numerator = (f * g') mod p^a is the dividend cldQuotientMod feeds to DensePoly.divMod before its own mod-p^a reduction of the quotient. The downstream modular-congruence correspondence reduces this exact identity mod p^a.

def Hex.bhksCutThresholds (f : ZPoly) (p : Nat) : Array Nat

Per-coordinate BHKS cut thresholds for the all-coefficients CLD lattice.

Equations

• Hex.bhksCutThresholds f p = (List.map (fun (j : Nat) => Hex.bhksCoeffCutThreshold p f j) (List.range (Hex.DensePoly.natDegree f))).toArray

theorem Hex.bhksCutThresholds_getD_of_lt (f : ZPoly) (p j : Nat) (h : j < DensePoly.natDegree f) : (bhksCutThresholds f p).getD j 0 = bhksCoeffCutThreshold p f j

In-range BHKS cut thresholds are the per-coordinate bhksCoeffCutThreshold.

structure Hex.BhksLatticeBasis : Type

Executable row-basis data for the BHKS all-coefficients CLD lattice.

The basis has row and column dimension factorCount + coeffWidth. Its first factorCount columns are indicator coordinates, and its remaining coeffWidth columns are CLD high-bit coordinates.

• p : Nat

  The prime underlying the lifted factors.

• precision : Nat

  The exponent in the modulus p ^ precision.

• factorCount : Nat

  The number of lifted modular factors.

• coeffWidth : Nat

  The number of coefficient columns used for logarithmic derivatives.

• liftedFactors : Array ZPoly

  The lifted modular factors defining the logarithmic derivatives.

• cutThresholds : Array Nat

  Per-column powers of p discarded from logarithmic-derivative coefficients.

• cldRows : Array (Array Int)

  The scaled logarithmic-derivative coefficient rows.

• basis : Matrix Int (self.factorCount + self.coeffWidth) (self.factorCount + self.coeffWidth)

  The square integer lattice basis containing indicator and coefficient columns.

structure Hex.BhksProjectedRows : Type

Projected BHKS rows after LLL reduction and the Gram-Schmidt cut.

cutRadiusSq4 stores 4 * B'^2 = 4r + n*r^2, avoiding square-root or floating-point arithmetic for the BHKS cut radius.

• factorCount : Nat

  The number of lifted-factor indicator coordinates.

• coeffWidth : Nat

  The number of logarithmic-derivative coefficient coordinates before projection.

• cutRadiusSq4 : Nat

  Four times the squared Gram-Schmidt cut radius.

• reducedRowCount : Nat

  The number of LLL-reduced rows before the Gram-Schmidt cut.

• projectedRows : Array (Array Int)

  The retained rows projected to their factor-indicator coordinates.

def Hex.bhksLatticeEntry (r n p a : Nat) (thresholds : Array Nat) (cldRows : Array (Array Int)) (i j : Fin (r + n)) : Int

One entry of the lattice basis used for logarithmic-derivative recombination.

Equations

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

def Hex.bhksLatticeBasis (f : ZPoly) (p a : Nat) (liftedFactors : Array ZPoly) : BhksLatticeBasis

Build the BHKS all-coefficients CLD row-basis matrix [ I_r | A_tilde; 0 | diag(p^(a-l_j)) ].

The diagonal exponent uses natural subtraction; callers that need the exact BHKS hypotheses should lift to a precision a satisfying every l_j ≤ a.

Equations

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

structure Hex.BhksLeadingLogDerivativeData : Type

Prepared leading logarithmic-derivative rows for a nested column schedule.

• degree : Nat

  Degree of the residual integer polynomial.

• p : Nat

  The prime underlying the lifted factors.

• precision : Nat

  The exponent in the lifting modulus.

• liftedFactors : Array ZPoly

  The lifted factors whose support is to be partitioned.

• coordinates : Array Nat

  Leading coordinates, in descending order.

• cutThresholds : Array Nat

  Cut thresholds corresponding to coordinates.

• cldRows : Array (Array Int)

  Truncated logarithmic-derivative rows corresponding to coordinates.

def Hex.bhksLeadingLogDerivativeData (f : ZPoly) (p a : Nat) (liftedFactors : Array ZPoly) (width : Nat) : BhksLeadingLogDerivativeData

Prepare one maximum-width leading CLD block shared by every smaller prefix in an incremental schedule.

Equations

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

def Hex.BhksLeadingLogDerivativeData.coordinateLattice (data : BhksLeadingLogDerivativeData) (width : Nat) : BhksLatticeBasis

The leading-coordinate lattice on the first width prepared columns.

Equations

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

theorem Hex.bhksLatticeEntry_topLeft (r n p a : Nat) (thresholds : Array Nat) (cldRows : Array (Array Int)) (i j : Fin (r + n)) (hi : ↑i < r) (hj : ↑j < r) : bhksLatticeEntry r n p a thresholds cldRows i j = if ↑i = ↑j then 1 else 0

The upper-left block of the recombination lattice basis is the identity matrix.

theorem Hex.bhksLatticeEntry_bottomLeft (r n p a : Nat) (thresholds : Array Nat) (cldRows : Array (Array Int)) (i j : Fin (r + n)) (hi : r ≤ ↑i) (hj : ↑j < r) : bhksLatticeEntry r n p a thresholds cldRows i j = 0

The lower-left block of the recombination lattice basis is zero.

theorem Hex.bhksLatticeEntry_bottomRight (r n p a : Nat) (thresholds : Array Nat) (cldRows : Array (Array Int)) (i j : Fin (r + n)) (hi : r ≤ ↑i) (hj : r ≤ ↑j) : bhksLatticeEntry r n p a thresholds cldRows i j = have coord := ↑i - r; if ↑j - r = coord then Int.ofNat (p ^ (a - thresholds.getD coord 0)) else 0

The lower-right block of the lattice basis is the diagonal of prime powers p ^ (a - threshold) that scales each CLD coordinate to its precision.

theorem Hex.bhksLatticeEntry_bottomRight_offDiag (r n p a : Nat) (thresholds : Array Nat) (cldRows : Array (Array Int)) (i j : Fin (r + n)) (hi : r ≤ ↑i) (hj : r ≤ ↑j) (hneq : ↑j - r ≠ ↑i - r) : bhksLatticeEntry r n p a thresholds cldRows i j = 0

Off-diagonal entries in the lower-right block of the lattice basis vanish.

theorem Hex.bhksLatticeEntry_bottomRight_diag (r n p a : Nat) (thresholds : Array Nat) (cldRows : Array (Array Int)) (i : Fin (r + n)) (hi : r ≤ ↑i) : bhksLatticeEntry r n p a thresholds cldRows i i = Int.ofNat (p ^ (a - thresholds.getD (↑i - r) 0))

Diagonal entries in the lower-right block are the prescribed prime powers.

theorem Hex.bhksLatticeEntry_bottomRight_diag_pos (r n p a : Nat) (thresholds : Array Nat) (cldRows : Array (Array Int)) (hp : 0 < p) (i : Fin (r + n)) (hi : r ≤ ↑i) (_hthreshold : thresholds.getD (↑i - r) 0 ≤ a) : 0 < bhksLatticeEntry r n p a thresholds cldRows i i

For a positive prime the lower-right diagonal entries are positive, so the lattice basis has full rank on its scaling block.

def Hex.bhksCutRadiusSq4 (L : BhksLatticeBasis) : Nat

Four times the squared BHKS cut radius, 4 * (r + n * (r / 2)^2).

Equations

• Hex.bhksCutRadiusSq4 L = 4 * L.factorCount + L.coeffWidth * L.factorCount * L.factorCount

def Hex.bhksWithinGramSchmidtCut (L : BhksLatticeBasis) (dets : Vector Nat (L.factorCount + L.coeffWidth + 1)) (i : Fin (L.factorCount + L.coeffWidth)) : Bool

Test whether one Gram-Schmidt row lies within the lattice cut radius.

Equations

• Hex.bhksWithinGramSchmidtCut L dets i = if dets.get ⟨↑i, ⋯⟩ = 0 then false else decide (4 * (↑(dets.get ⟨↑i + 1, ⋯⟩) / ↑(dets.get ⟨↑i, ⋯⟩)) ≤ ↑(Hex.bhksCutRadiusSq4 L))

def Hex.bhksProjectIndicator (r n : Nat) (v : Vector Int (r + n)) : Array Int

Retain the factor-indicator coordinates of a full lattice vector.

Equations

• Hex.bhksProjectIndicator r n v = (List.map (fun (j : Nat) => if h : j < r + n then v.get ⟨j, h⟩ else 0) (List.range r)).toArray

def Hex.bhksRowsArrayToMatrix {m : Nat} (n : Nat) (rows : Array (Vector Int m)) : Matrix Int n m

View an array of rows as an n-row matrix, padding absent rows with zeros.

Equations

• Hex.bhksRowsArrayToMatrix n rows = Hex.Matrix.ofFn fun (i : Fin n) (j : Fin m) => (rows.getD (↑i) (Vector.ofFn fun (x : Fin m) => 0))[j]

theorem Hex.bhksRowsArrayToMatrix_row {m n : Nat} (rows : Array (Vector Int m)) (i : Fin n) : (bhksRowsArrayToMatrix n rows).row i = rows.getD (↑i) (Vector.ofFn fun (x : Fin m) => 0)

Each row of the assembled matrix is the corresponding array entry, with absent entries read as the zero vector.

theorem Hex.bhksRowsArrayToMatrix_toArray {m n : Nat} (B : Matrix Int n m) : bhksRowsArrayToMatrix n B.rows.toArray = B

Converting a matrix row array back to a matrix recovers the original matrix.

theorem Hex.lll_delta_lower : 1 / 4 < 3 / 4

The chosen Lovász parameter is strictly above one quarter.

theorem Hex.lll_delta_upper : 3 / 4 ≤ 1

The chosen Lovász parameter is at most one.

def Hex.bhksCutPrefixCount (L : BhksLatticeBasis) (reduced : Matrix Int (L.factorCount + L.coeffWidth) (L.factorCount + L.coeffWidth)) : Nat

Length of the BHKS Lemma 5.7 prefix cut: one past the last Gram-Schmidt index whose squared length is within the radius (0 if none passes). Because the fold runs in increasing index order, the accumulator ends at (max { i : ‖b*_i‖² ≤ radius }) + 1, so retaining indices < t keeps the contiguous prefix b_0 … b_t in original order; including earlier rows whose own Gram-Schmidt norm exceeds the radius.

Equations

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

def Hex.bhksCutProjectReducedRows (L : BhksLatticeBasis) (reduced : Matrix Int (L.factorCount + L.coeffWidth) (L.factorCount + L.coeffWidth)) : Array (Array Int)

Keep the initial reduced rows selected by the cut and project their indicator coordinates.

Equations

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

def Hex.bhksRetainedRowIndices (L : BhksLatticeBasis) (reduced : Matrix Int (L.factorCount + L.coeffWidth) (L.factorCount + L.coeffWidth)) : Array (Fin (L.factorCount + L.coeffWidth))

Indices of the initial reduced rows retained by the Gram-Schmidt cut.

Equations

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

def Hex.bhksProjectRetainedRows (L : BhksLatticeBasis) (reduced : Matrix Int (L.factorCount + L.coeffWidth) (L.factorCount + L.coeffWidth)) (indices : Array (Fin (L.factorCount + L.coeffWidth))) : Array (Array Int)

Project the factor-indicator coordinates of the retained reduced rows.

Equations

• Hex.bhksProjectRetainedRows L reduced indices = Array.map (fun (i : Fin (L.factorCount + L.coeffWidth)) => Hex.bhksProjectIndicator L.factorCount L.coeffWidth (reduced.row i)) indices

structure Hex.BhksProjectedRowsTrace (L : BhksLatticeBasis) : Type

Proof-facing trace for the executable BHKS projected-row construction. It records the unchecked LLL rows, their matrix view, the Gram determinant vector used by the cut, the retained source row indices, and the projected retained rows. bhksProjectedRows below is the old compact projection of this trace.

• reducedRows : Array (Vector Int (L.factorCount + L.coeffWidth))

  The rows returned by exact LLL reduction.

• reducedMatrix : Matrix Int (L.factorCount + L.coeffWidth) (L.factorCount + L.coeffWidth)

  The same reduced rows as a square matrix.

• gramDets : Vector Nat (L.factorCount + L.coeffWidth + 1)

  Determinants of the leading Gram matrices used by the exact cut.

• retainedIndices : Array (Fin (L.factorCount + L.coeffWidth))

  Indices of the reduced rows below the cut radius.

• projectedRetainedRows : Array (Array Int)

  Retained full rows before discarding coefficient coordinates.

• projectedRows : Array (Array Int)

  Retained rows restricted to factor-indicator coordinates.

def Hex.bhksProjectedRowsTrace (L : BhksLatticeBasis) (hrows : 1 ≤ L.factorCount + L.coeffWidth) : BhksProjectedRowsTrace L

Compute the reduced rows, cut data, and projected rows used in lattice recovery.

Equations

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

theorem Hex.bhksProjectedRowsTrace_reducedMatrix_eq (L : BhksLatticeBasis) (hrows : 1 ≤ L.factorCount + L.coeffWidth) : (bhksProjectedRowsTrace L hrows).reducedMatrix = lllNative L.basis (3 / 4) lll_delta_lower lll_delta_upper hrows

The trace's reduced matrix is the matrix returned by exact LLL reduction.

def Hex.bhksProjectedRows (L : BhksLatticeBasis) (hrows : 1 ≤ L.factorCount + L.coeffWidth) : BhksProjectedRows

Run LLL on a BHKS row-basis lattice, discard rows whose Gram-Schmidt squared length exceeds the BHKS radius, and project survivors to the first r indicator coordinates. The squared Gram-Schmidt lengths are computed from the integer leading Gram determinant vector as d_{i+1}/d_i.

The result is the executable L' row data consumed by the later RREF / equivalence-class recovery stage.

Equations

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

theorem Hex.bhksProjectedRows_eq_trace (L : BhksLatticeBasis) (hrows : 1 ≤ L.factorCount + L.coeffWidth) : bhksProjectedRows L hrows = { factorCount := L.factorCount, coeffWidth := L.coeffWidth, cutRadiusSq4 := bhksCutRadiusSq4 L, reducedRowCount := (bhksProjectedRowsTrace L hrows).reducedRows.size, projectedRows := (bhksProjectedRowsTrace L hrows).projectedRows }

The production projection agrees field-by-field with the instrumented bhksProjectedRowsTrace run, so trace-based proofs transfer to the production path.