theorem Hex.BHKS.abs_cldCoeffs_le_bhksCoeffBound (f g : ZPoly) (p a j : Nat) (y : Int) (hp : 2 ≤ p) (hbound : y.natAbs ≤ bhksCoeffBound f j) (hsep_a : 2 * bhksCoeffBound f j < p ^ a) (hcongr : y % ↑(p ^ a) = DensePoly.coeff (cldQuotientMod f g p a) j % ↑(p ^ a)) : ((cldCoeffs f p a g).getD j 0).natAbs ≤ bhksCoeffBound f j

BHKS Lemma 5.1 column bound for the executable cldCoeffs.

If there exists an exact integer y (morally [x^j] (f * g'.derivative / g') for a true integer factor g' of f that Hensel-lifts to g) congruent to (cldQuotientMod f g p a).coeff j modulo p^a and satisfying |y| ≤ bhksCoeffBound f j, then under the Hensel precision hypothesis 2 * bhksCoeffBound f j < p^a and p ≥ 2, the executable cldCoeffs entry at index j is bounded by bhksCoeffBound f j.

The executable cut must be re-centered at the ambient modulus for this column bound to hold. Hex.psiCut performs that recentering; the bound is then a direct consequence of abs_psiCut_le_of_natAbs_le plus precisionForCoeffBound_spec for the lower cut threshold.

def Hex.bhksProjectedRowsAsRatMatrix (rows : Array (Array Int)) (n r : Nat) : Matrix Rat n r

Lift the projected integer rows of L into a rational row-basis matrix sized n × r, with n := L.projectedRows.size and r := L.factorCount. The matrix is the input to BHKS Lemma 3.3 RREF-based equivalence-class identification.

Equations

• Hex.bhksProjectedRowsAsRatMatrix rows n r = Hex.Matrix.ofFn fun (i : Fin n) (j : Fin r) => ↑((rows.getD ↑i #[]).getD (↑j) 0)

def Hex.bhksColumnSignature (echelonRows : Array (Array Rat)) (j : Nat) : Array Rat

The entries in column j of a row-reduced projected matrix.

Equations

• Hex.bhksColumnSignature echelonRows j = Array.map (fun (x : Array Rat) => x.getD j 0) echelonRows

def Hex.bhksInsertSignatureClass (sig : Array Rat) (j : Nat) : List (Array Rat × List Nat) → List (Array Rat × List Nat)

Add a column index to the class with the same signature, or start a new class.

Equations

• Hex.bhksInsertSignatureClass sig j [] = [(sig, [j])]
• Hex.bhksInsertSignatureClass sig j ((s, members) :: rest) = if s = sig then (s, members ++ [j]) :: rest else (s, members) :: Hex.bhksInsertSignatureClass sig j rest

def Hex.bhksClassIndicator (r : Nat) (members : List Nat) : Array Int

The zero-one indicator vector of a class of column indices.

Equations

• Hex.bhksClassIndicator r members = (List.map (fun (i : Nat) => if i ∈ members then 1 else 0) (List.range r)).toArray

def Hex.bhksEquivalenceClassIndicators (L : BhksProjectedRows) : Array (Array Int)

BHKS equivalence-class indicator vectors over the projected lattice rows of L.

Lifts the projected integer rows into a rational row-basis matrix, runs Matrix.rowReduce over Q, and groups column indices 0, …, r - 1 by their echelon-column signature: indices i and j are equivalent iff every echelon row agrees at positions i and j (BHKS Lemma 3.3 / FLINT Algorithm 8). Each equivalence class produces one compact 0/1 indicator of length r. Classes are emitted in the order they are first observed by ascending column index.

Equations

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

def Hex.liftModulus (d : LiftData) : Nat

The prime-power modulus of a Hensel lift.

Equations

• Hex.liftModulus d = d.p ^ d.k

def Hex.centeredLiftPoly (f : ZPoly) (m : Nat) : ZPoly

Replace every coefficient by its centred representative modulo m.

Equations

• Hex.centeredLiftPoly f m = Hex.DensePoly.ofCoeffs (Array.map (fun (coeff : Int) => Hex.centeredModNat coeff m) (Hex.DensePoly.toArray f))

theorem Hex.coeff_centeredLiftPoly (f : ZPoly) (m i : Nat) : DensePoly.coeff (centeredLiftPoly f m) i = centeredModNat (DensePoly.coeff f i) m

Coefficientwise description of centeredLiftPoly.

theorem Hex.centeredLiftPoly_reduceModPow_eq_of_coeff_natAbs_le (g : ZPoly) (p k B : Nat) (hbound : ∀ (i : Nat), (DensePoly.coeff g i).natAbs ≤ B) (hsep : 2 * B < p ^ k) : centeredLiftPoly (g.reduceModPow p k) (p ^ k) = g

A sufficiently large modulus makes centred coefficient recovery exact.

theorem Hex.centeredLiftPoly_eq_of_reduceModPow_eq (g h : ZPoly) (p k B : Nat) (hbound : ∀ (i : Nat), (DensePoly.coeff g i).natAbs ≤ B) (hsep : 2 * B < p ^ k) (hreduce : h.reduceModPow p k = g.reduceModPow p k) : centeredLiftPoly (h.reduceModPow p k) (p ^ k) = g

Equal sufficiently precise residues recover the same coefficient-bounded polynomial.

def Hex.normalizeCandidateFactor (candidate : ZPoly) : ZPoly

Normalize a candidate integer factor by extracting its primitive part and flipping sign so the leading coefficient is non-negative. Used by bhksIndicatorCandidate? to produce a canonical witness from the centred lift of a scaled lifted-factor product.

Equations

• Hex.normalizeCandidateFactor candidate = if Hex.DensePoly.leadingCoeff candidate.primitivePart < 0 then Hex.DensePoly.scale (-1) candidate.primitivePart else candidate.primitivePart

theorem Hex.normalizeCandidateFactor_eq_of_primitive_nonneg_leading (g : ZPoly) (hprim : g.Primitive) (hsign : 0 ≤ DensePoly.leadingCoeff g) : normalizeCandidateFactor g = g

normalizeCandidateFactor g = g when g is already primitive (content 1) and has non-negative leading coefficient. This is the A2 reconstruction step that asserts the canonical witness produced by bhksIndicatorCandidate? agrees with the expected true factor under those normalization assumptions.

def Hex.bhksIndicatorSelectedFactors (liftedFactors : Array ZPoly) (indicator : Array Int) : Option (Array ZPoly)

Select the lifted factors marked by a nonempty zero-one indicator.

Equations

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

def Hex.bhksIndicatorSelectedFactorsArray (liftedFactors : Array ZPoly) (indicator : Array Int) : Array ZPoly

The array selected by a 0/1 BHKS indicator row.

Equations

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

theorem Hex.bhksIndicatorSelectedFactors_eq_some_selectedArray_of_getD (liftedFactors : Array ZPoly) (indicator : Array Int) (hsize : indicator.size = liftedFactors.size) (hbits : ∀ (i : Nat), i < indicator.size → indicator.getD i 0 = 0 ∨ indicator.getD i 0 = 1) (hnonempty : ∃ (i : Nat), i < indicator.size ∧ indicator.getD i 0 = 1) : bhksIndicatorSelectedFactors liftedFactors indicator = some (bhksIndicatorSelectedFactorsArray liftedFactors indicator)

Successful branch of bhksIndicatorSelectedFactors for well-formed 0/1 indicator rows, returning the canonical selected-factor array.

theorem Hex.bhksIndicatorSelectedFactors_eq_some_of_getD (liftedFactors : Array ZPoly) (indicator : Array Int) (selected : Array ZPoly) (hsize : indicator.size = liftedFactors.size) (hbits : ∀ (i : Nat), i < indicator.size → indicator.getD i 0 = 0 ∨ indicator.getD i 0 = 1) (hnonempty : ∃ (i : Nat), i < indicator.size ∧ indicator.getD i 0 = 1) (hselected : selected = bhksIndicatorSelectedFactorsArray liftedFactors indicator) : bhksIndicatorSelectedFactors liftedFactors indicator = some selected

Successful branch of bhksIndicatorSelectedFactors, stated with an explicit name for the selected-factor array chosen by the caller.

def Hex.bhksIndicatorCandidate? (f : ZPoly) (d : LiftData) (indicator : Array Int) : Option (ZPoly × ZPoly)

Reconstruct and verify one BHKS equivalence-class indicator.

The indicator row is supplied by the later RREF recovery stage. This helper only checks that the row is a nonempty 0/1 vector over the lifted factors, forms the selected lifted-factor product, scales it by f's leading coefficient in the same coordinate, applies the centred integer lift, normalizes content and sign, and accepts the candidate only when exact division of f succeeds.

Equations

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

theorem Hex.bhksIndicatorCandidate?_dvd {f : ZPoly} {d : LiftData} {indicator : Array Int} {candidate quotient : ZPoly} (h : bhksIndicatorCandidate? f d indicator = some (candidate, quotient)) : candidate ∣ f

A successful BHKS indicator candidate divides f. The executable bhksIndicatorCandidate? only returns some (candidate, _) after exactQuotient? f candidate succeeds, so the candidate is a verified integer divisor of f.

theorem Hex.bhksIndicatorCandidate?_primitive {f : ZPoly} {d : LiftData} {indicator : Array Int} {candidate quotient : ZPoly} (h : bhksIndicatorCandidate? f d indicator = some (candidate, quotient)) : candidate.Primitive

A successful BHKS indicator candidate is primitive: the candidate equals normalizeFactorSign (normalizeCandidateFactor _), and shouldRecord = true forces the inner factor to be nonzero, hence primitive.

theorem Hex.bhksIndicatorCandidate?_eq_normalized_directLift {f : ZPoly} {d : LiftData} {indicator : Array Int} {candidate quotient : ZPoly} {selected : Array ZPoly} (h : bhksIndicatorCandidate? f d indicator = some (candidate, quotient)) (hselected : bhksIndicatorSelectedFactors d.liftedFactors indicator = some selected) : candidate = normalizeFactorSign (normalizeCandidateFactor (centeredLiftPoly (DensePoly.scale (DensePoly.leadingCoeff f) selected.polyProduct) (d.p ^ d.k)))

The candidate returned by a successful bhksIndicatorCandidate? call is exactly the canonical normalization of the direct-coordinate scaled centred lift. This is a Mathlib-free surface lemma that avoids exposing the private liftModulus definition.

theorem Hex.bhksIndicatorCandidate?_eq_some_of_directLift (f : ZPoly) (d : LiftData) (indicator : Array Int) (selected : Array ZPoly) (expectedFactor : ZPoly) (hselected : bhksIndicatorSelectedFactors d.liftedFactors indicator = some selected) (hdvd : expectedFactor ∣ f) (hexpected_prim : expectedFactor.Primitive) (hexpected_sign : 0 ≤ DensePoly.leadingCoeff expectedFactor) (hexpected_pos_lc : 0 < DensePoly.leadingCoeff expectedFactor) (hexpected_degree : 0 < DensePoly.natDegree expectedFactor) (hrecovered : centeredLiftPoly (DensePoly.scale (DensePoly.leadingCoeff f) selected.polyProduct) (d.p ^ d.k) = expectedFactor) : ∃ (quotient : ZPoly), bhksIndicatorCandidate? f d indicator = some (expectedFactor, quotient)

A2 reconstruction surface for a single direct-coordinate BHKS indicator.

theorem Hex.bhksIndicatorCandidate?_eq_some_of_scaledCandidate (f : ZPoly) (d : LiftData) (indicator : Array Int) (selected : Array ZPoly) (expectedFactor selectedProduct : ZPoly) (hselected : bhksIndicatorSelectedFactors d.liftedFactors indicator = some selected) (hproduct : selected.polyProduct = selectedProduct) (hdvd : expectedFactor ∣ f) (hexpected_pos_lc : 0 < DensePoly.leadingCoeff expectedFactor) (hexpected_degree : 0 < DensePoly.natDegree expectedFactor) (hrecovered : normalizeFactorSign (centeredLiftPoly (DensePoly.scale (DensePoly.leadingCoeff f) selectedProduct) (d.p ^ d.k)).primitivePart = expectedFactor) : ∃ (quotient : ZPoly), bhksIndicatorCandidate? f d indicator = some (expectedFactor, quotient)

Reconstruct one direct-coordinate BHKS indicator when the canonical scaled recombination candidate is already known exactly.

theorem Hex.bhksIndicatorCandidate?_eq_some_of_directRecovery (f : ZPoly) (d : LiftData) (indicator : Array Int) (selected : Array ZPoly) (expectedFactor : ZPoly) (hselected : bhksIndicatorSelectedFactors d.liftedFactors indicator = some selected) (hdvd : expectedFactor ∣ f) (hexpected_sign : 0 ≤ DensePoly.leadingCoeff expectedFactor) (hexpected_pos_lc : 0 < DensePoly.leadingCoeff expectedFactor) (hexpected_degree : 0 < DensePoly.natDegree expectedFactor) (hrecovered : (centeredLiftPoly (DensePoly.scale (DensePoly.leadingCoeff f) selected.polyProduct) (d.p ^ d.k)).primitivePart = expectedFactor) : ∃ (quotient : ZPoly), bhksIndicatorCandidate? f d indicator = some (expectedFactor, quotient)

Reconstruct one direct-coordinate BHKS indicator from its primitive-part recovery identity.

def Hex.bhksIndicatorOneCount (r : Nat) (indicator : Array Int) : Nat

Count the entries equal to one among the first r indicator entries.

Equations

• Hex.bhksIndicatorOneCount r indicator = List.foldl (fun (count i : Nat) => if (indicator.getD i 0 == 1) = true then count + 1 else count) 0 (List.range r)

def Hex.bhksIndicatorAllOnes (r : Nat) (indicator : Array Int) : Bool

Test whether an indicator has width r and consists entirely of ones.

Equations

• Hex.bhksIndicatorAllOnes r indicator = (indicator.size == r && Hex.bhksIndicatorOneCount r indicator == r)

theorem Hex.bhksIndicatorAllOnes_eq_true_of_getD (r : Nat) (indicator : Array Int) (hsize : indicator.size = r) (hones : ∀ (i : Nat), i < r → indicator.getD i 0 = 1) : bhksIndicatorAllOnes r indicator = true

An indicator of the expected width whose every coordinate is one passes the executable all-ones check.

def Hex.bhksDegenerateIndicatorPartition (L : BhksProjectedRows) (indicators : Array (Array Int)) : Bool

The recovery early-bailout predicate: the projected lattice is empty, the indicator partition is empty, or the indicator partition is the trivial all-ones single class.

Equations

• Hex.bhksDegenerateIndicatorPartition L indicators = (indicators.isEmpty || L.projectedRows.isEmpty || indicators.size == 1 && Hex.bhksIndicatorAllOnes L.factorCount (indicators.getD 0 #[]))

theorem Hex.bhksDegenerateIndicatorPartition_eq_false (L : BhksProjectedRows) (indicators : Array (Array Int)) (hindicators : indicators.isEmpty = false) (hrows : L.projectedRows.isEmpty = false) (hsize : (indicators.size == 1) = false) : bhksDegenerateIndicatorPartition L indicators = false

The proof-facing successful branch of the BHKS degeneracy guard.

def Hex.bhksIndicatorCandidates? (f : ZPoly) (d : LiftData) (indicators : Array (Array Int)) : Option (Array ZPoly)

Reconstruct and verify every BHKS equivalence-class indicator candidate.

Folds bhksIndicatorCandidate? over the list of indicator vectors, pushing the verified candidate factor onto the accumulator on success and short-circuiting to none on the first reconstruction failure.

Equations

• Hex.bhksIndicatorCandidates? f d indicators = Array.foldl (Hex.bhksIndicatorCandidatesStep✝ f d) (some #[]) indicators

theorem Hex.bhksIndicatorCandidates?_dvd {f : ZPoly} {d : LiftData} {indicators : Array (Array Int)} {candidates : Array ZPoly} (h : bhksIndicatorCandidates? f d indicators = some candidates) (factor : ZPoly) : factor ∈ candidates.toList → factor ∣ f

Every candidate emitted by bhksIndicatorCandidates? divides the input polynomial; this is the per-candidate version of the verified exact-division check performed inside bhksIndicatorCandidate?.

theorem Hex.bhksIndicatorCandidates?_primitive {f : ZPoly} {d : LiftData} {indicators : Array (Array Int)} {candidates : Array ZPoly} (h : bhksIndicatorCandidates? f d indicators = some candidates) (factor : ZPoly) : factor ∈ candidates.toList → factor.Primitive

Every candidate emitted by bhksIndicatorCandidates? is primitive. This is the array-level form of the per-candidate primitivity guarantee from normalizeCandidateFactor plus sign normalisation.

theorem Hex.bhksIndicatorCandidates?_leadingCoeff_nonneg {f : ZPoly} {d : LiftData} {indicators : Array (Array Int)} {candidates : Array ZPoly} (h : bhksIndicatorCandidates? f d indicators = some candidates) (factor : ZPoly) : factor ∈ candidates.toList → 0 ≤ DensePoly.leadingCoeff factor

Every candidate emitted by bhksIndicatorCandidates? has nonnegative leading coefficient; this is the array-level form of the per-candidate sign normalisation guarantee.

theorem Hex.bhksIndicatorCandidates?_positive_degree {f : ZPoly} {d : LiftData} {indicators : Array (Array Int)} {candidates : Array ZPoly} (h : bhksIndicatorCandidates? f d indicators = some candidates) (factor : ZPoly) : factor ∈ candidates.toList → 0 < DensePoly.natDegree factor

Every candidate emitted by bhksIndicatorCandidates? has positive degree; this is the array-level form of the per-candidate nonconstant guarantee.

theorem Hex.bhksIndicatorCandidates?_eq_some_of_forall_candidate (f : ZPoly) (d : LiftData) (indicators : Array (Array Int)) (candidates quotients : Array ZPoly) (hsize : candidates.size = indicators.size) (hcandidate : ∀ (i : Nat), i < indicators.size → bhksIndicatorCandidate? f d (indicators.getD i #[]) = some (candidates.getD i 0, quotients.getD i 0)) : bhksIndicatorCandidates? f d indicators = some candidates

If each BHKS equivalence-class indicator reconstructs and verifies to the corresponding candidate factor, the executable candidate fold returns the whole candidate array.

The quotients array records the exact-division witnesses returned by bhksIndicatorCandidate?; only the first component is accumulated by bhksIndicatorCandidates?.

theorem Hex.bhksIndicatorCandidates?_eq_some_of_getD (f : ZPoly) (d : LiftData) (indicators : Array (Array Int)) (candidates : Array ZPoly) (hsize : candidates.size = indicators.size) (hcandidate : ∀ (i : Nat), i < indicators.size → ∃ (quotient : ZPoly), bhksIndicatorCandidate? f d (indicators.getD i #[]) = some (candidates.getD i 0, quotient)) : bhksIndicatorCandidates? f d indicators = some candidates

Assemble the BHKS candidate fold from per-indicator reconstruction facts.

This is the proof-facing surface for callers that know every indicator row reconstructs and exactly divides f: with a size agreement and one quotient witness for each row, the executable fold returns the requested candidate array.

theorem Hex.bhksIndicatorCandidates?_size_eq {f : ZPoly} {d : LiftData} {indicators : Array (Array Int)} {candidates : Array ZPoly} (h : bhksIndicatorCandidates? f d indicators = some candidates) : candidates.size = indicators.size

A successful BHKS indicator-candidate fold produces a candidate array of the same size as the input indicator array. This is the size identity used by ExpectedTrueFactors-shaped consumers that need to align the per-index indicator and factor views.

theorem Hex.ZPoly.ToMonicData.transformedCore_coeff (core : ZPoly) (degree n : Nat) : DensePoly.coeff (transformedCore core degree) n = if n < degree then DensePoly.coeff core n * DensePoly.leadingCoeff core ^ (degree - 1 - n) else if n = degree then 1 else 0

General coefficient law for the monic transform transformedCore. Below the top degree the coefficient is core.coeff n scaled by a power of the leading coefficient; the top coefficient is 1; higher coefficients vanish.

theorem Hex.ZPoly.ToMonicData.dilate_transformedCore (core : ZPoly) (degree : Nat) (hdeg : 1 ≤ degree) (hcore : DensePoly.natDegree core = degree) : dilate (DensePoly.leadingCoeff core) (transformedCore core degree) = DensePoly.C (DensePoly.leadingCoeff core ^ (degree - 1)) * core

Keystone for toMonic inverse recovery. Dilating the monic transform transformedCore core degree by the leading coefficient recovers core scaled by leadingCoeff core ^ (degree - 1). The 1 ≤ degree hypothesis is essential: for a constant core the identity fails unless the leading coefficient is 1. Composed with dilate_mul, this is the inverse-factor correspondence the recombination recovery proof rests on.

theorem Hex.ZPoly.dilate_monic_toMonic (core : ZPoly) (hdeg : 1 ≤ core.toMonic.degree) : dilate (DensePoly.leadingCoeff core) core.toMonic.monic = DensePoly.C (DensePoly.leadingCoeff core ^ (core.toMonic.degree - 1)) * core

Public face of the inverse-recovery keystone, stated on the toMonic monic field rather than the private transformedCore. For a square-free part of degree ≥ 1, dilating (toMonic core).monic by the leading coefficient recovers core scaled by leadingCoeff core ^ (degree - 1). Holds in both the already-monic and the genuine transform branch.

theorem Hex.ZPoly.toMonic_monic_coeff_of_leadingCoeff_ne_one (core : ZPoly) (hmonic : DensePoly.leadingCoeff core ≠ 1) (i : Nat) : DensePoly.coeff core.toMonic.monic i = if i < DensePoly.natDegree core then DensePoly.coeff core i * DensePoly.leadingCoeff core ^ (DensePoly.natDegree core - 1 - i) else if i = DensePoly.natDegree core then 1 else 0

Coefficient law for the monic transform (toMonic core).monic in the genuine-transform branch (leading coefficient ≠ 1). Public face of the private ToMonicData.transformedCore_coeff: below the top degree the coefficient is core.coeff i scaled by a power of the leading coefficient, the top coefficient is 1, and higher coefficients vanish.

theorem Hex.ZPoly.toMonic_monic_degree_getD (core : ZPoly) : DensePoly.natDegree core.toMonic.monic = DensePoly.natDegree core

The monic transform preserves the recorded degree in all cases (sign-free, unconditional companion to toMonic_monic_degree_eq_of_pos_degree).

theorem Hex.ZPoly.toMonic_monic_size_of_pos_degree (core : ZPoly) (hdeg : 0 < DensePoly.natDegree core) : DensePoly.size core.toMonic.monic = DensePoly.natDegree core + 1

Stored size of the monic transform of a positive-degree square-free part: one more than the square-free part degree, in both the already-monic and genuine-transform branches.