theorem Hex.ZPoly.QuadraticMultifactorLiftInvariant_of_choosePrimeData (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) (hp_prime : Nat.Prime primeData.p) (hp : 1 < primeData.p) (hB : 1 ≤ B) (hcore_monic : DensePoly.Monic core) (hfactors_monic : ∀ (g : FpPoly primeData.p), g ∈ primeData.factorsModP → DensePoly.Monic g) (hproduct_mod_p : (Array.map FpPoly.liftToZ primeData.factorsModP).polyProduct.congr core primeData.p) (hcoprime : QuadraticMultifactorCoprimeSplits primeData.p primeData.factorsModP.toList) (hnonempty : primeData.factorsModP.toList ≠ []) : QuadraticMultifactorLiftInvariant primeData.p B core (Array.map FpPoly.liftToZ primeData.factorsModP).toList

PrimeChoiceData-shaped wrapper around Hex.ZPoly.quadraticMultifactorLiftInvariant_of_factorsModP.

Given monic core, an admissible 1 ≤ B, and the minimal modular boundary facts about primeData.factorsModP -- per-factor monicness, product congruence modulo primeData.p, sequential split coprimality, and a nonempty witness -- this produces the recursive quadratic multifactor lift invariant on the lifted modular factors that henselLiftData consumes.

The Mathlib-free downstream theorem HexBerlekampZassenhausMathlib.henselLiftData_liftedFactor_monic already feeds this invariant into Hex.ZPoly.multifactorLiftQuadratic_each_monic.

def Hex.bhksCoeffBound (f : ZPoly) (j : Nat) : Nat

Integer coefficient bound B_j used by the BHKS all-coefficients CLD lattice.

Equations

• Hex.bhksCoeffBound f j = Hex.Nat.choose (Hex.DensePoly.natDegree f - 1) j * Hex.DensePoly.natDegree f * f.coeffL2NormBound

def Hex.bhksColumnFloor (f : ZPoly) : Nat

Twice the largest per-column CLD coefficient bound of f.

Equations

• Hex.bhksColumnFloor f = 2 * List.foldl (fun (acc j : Nat) => max acc (Hex.bhksCoeffBound f j)) 0 (List.range (Hex.DensePoly.natDegree f + 1))

def Hex.bhksBound (f : ZPoly) : Nat

Integer upper bound for the production BHKS resultant contradiction.

Writing n = degree f, the components are deliberately coarse:

• R = 4n + n³ bounds the cut radius;

• V = 2n · 2^(2n) · R bounds a retained LLL row coordinate;

• E = V + V·R + 2^n·R bounds every coordinate after the full-lattice true-support adjustment;

• C = 500 · (bhksColumnFloor f + 1) bounds every cut power and low residue, using the production selector's p ≤ 500;

• M = (n+1)·E·C bounds every coefficient of the reconstructed auxiliary;

• the final power term bounds the Leibniz expansion of a Sylvester matrix of size at most 2n (using (2n)! ≤ (2n)^(2n)).

The leading 1 makes the bound strictly larger than the absolute resultant. Unlike the former paper-shaped placeholder, every component here is tied directly to the executable lattice, selector, and resultant proof.

Equations

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

def Hex.ceilLogPAux (p target : Nat) : Nat → Nat → Nat → Nat

Bounded iteration finding the least exponent whose p-power reaches target.

Equations

• Hex.ceilLogPAux p target 0 x✝¹ x✝ = x✝¹
• Hex.ceilLogPAux p target fuel.succ x✝¹ x✝ = if target ≤ x✝ then x✝¹ else Hex.ceilLogPAux p target fuel (x✝¹ + 1) (x✝ * p)

def Hex.ceilLogP (p target : Nat) : Nat

Small executable ceil_log_p helper.

For 1 < p, ceilLogP p target searches for the least visible exponent whose p-power is at least target. The degenerate p ≤ 1 case returns zero because the BHKS fast path is only used with admissible primes.

Equations

• Hex.ceilLogP p target = if p ≤ 1 then 0 else Hex.ceilLogPAux p target (target + 1) 0 1

def Hex.bhksCoeffCutThreshold (p : Nat) (f : ZPoly) (j : Nat) : Nat

Per-coordinate BHKS precision threshold ell_j := ceil_log_p (2 * B_j + 1).

Equations

• Hex.bhksCoeffCutThreshold p f j = Hex.ceilLogP p (2 * Hex.bhksCoeffBound f j + 1)

def Hex.defaultSubsetBudget : Nat

Global cap on direct classical recombination candidates.

Shared between the engine that spends it and the prime planner that prices it: Hex.scoutPays bounds a plan's remaining recombination by this, because beyond it the direct search declines rather than continuing.

Equations

• Hex.defaultSubsetBudget = 262144

def Hex.precisionForCoeffBound (B p : Nat) : Nat

Hensel precision exponent for a Mignotte coefficient bound.

For the Mignotte criterion p^a > 2·B, returns the smallest exponent a with p^a ≥ 2·B + 1 (equivalently p^a > 2·B). The two quantities are different; B is a magnitude on integer coefficients, a is the small exponent on the Hensel modulus p^a; and must not be conflated.

Equations

• Hex.precisionForCoeffBound B p = Hex.ceilLogP p (2 * B + 1)

theorem Hex.le_pow_ceilLogP {p : Nat} (hp : 2 ≤ p) (target : Nat) : target ≤ p ^ ceilLogP p target

Correctness of ceilLogP: when 2 ≤ p, the returned exponent satisfies target ≤ p ^ ceilLogP p target.

This bound is consumed by precisionForCoeffBound_spec below; the strict-inequality Mignotte side condition 2 * B < p ^ precisionForCoeffBound B p follows by chaining this with the target target = 2 * B + 1.

theorem Hex.ceilLogP_le_of_le_pow {p : Nat} (hp : 2 ≤ p) (target a : Nat) (h : target ≤ p ^ a) : ceilLogP p target ≤ a

Minimality of ceilLogP: when 2 ≤ p and target ≤ p ^ a, the least exponent returned by ceilLogP is at most a.

This is the upper-bound companion to le_pow_ceilLogP. Together they pin ceilLogP p target between the least admissible exponent and any witness a, which the BHKS period rows need to know the cut threshold ℓ_j does not exceed the ambient Hensel precision a (ℓ_j ≤ a, so the diagonal exponent a − ℓ_j is a genuine subtraction).

theorem Hex.pow_ceilLogP_le_mul {p target : Nat} (hp : 2 ≤ p) (htarget : 0 < target) : p ^ ceilLogP p target ≤ p * target

The power selected by ceilLogP overshoots a positive target by at most one factor of the base. This is the upper-bound companion needed when a BHKS proof reconstructs ordinary coefficients from the high-bit lattice columns.

theorem Hex.two_mul_bhksCoeffBound_le_bhksColumnFloor (f : ZPoly) {j : Nat} (hj : j ≤ DensePoly.natDegree f) : 2 * bhksCoeffBound f j ≤ bhksColumnFloor f

Every in-range CLD column bound is dominated by bhksColumnFloor.

theorem Hex.pow_bhksCoeffCutThreshold_le (f : ZPoly) {p j : Nat} (hp2 : 2 ≤ p) (hp500 : p ≤ 500) (hj : j ≤ DensePoly.natDegree f) : p ^ bhksCoeffCutThreshold p f j ≤ 500 * (bhksColumnFloor f + 1)

For the production selector range p ≤ 500, every in-range cut power is bounded by the explicit C component of bhksBound.

theorem Hex.precisionForCoeffBound_spec {p : Nat} (hp : 2 ≤ p) (B : Nat) : 2 * B < p ^ precisionForCoeffBound B p

The executable Mignotte precision exponent satisfies the Mignotte side condition 2 * B < p ^ precisionForCoeffBound B p whenever the modulus is at least 2.

This is the reusable bound consumed by ForwardRecoveryInputs constructors that need to discharge the mignotte_precision field at the actual executable precision returned by henselLiftData f (precisionForCoeffBound B p).

def Hex.subsetSplits : List ZPoly → List (List ZPoly × List ZPoly)

Enumerate every way to partition a list of polynomials into a (selected, unselected) pair while preserving the original order in each component. Used by the exhaustive recombination search to drive the slow path.

Equations

• One or more equations did not get rendered due to their size.
• Hex.subsetSplits [] = [([], [])]

def Hex.subsetSplitsWithFirst : List ZPoly → List (List ZPoly × List ZPoly)

Variant of subsetSplits that forces the first element of the input list into the selected component. This is what the recombination search actually iterates over, since the head of the remaining local factors must end up in some recovered factor and tracking that explicitly avoids enumerating the same subset twice through different traversal orders.

Equations

• Hex.subsetSplitsWithFirst [] = []
• Hex.subsetSplitsWithFirst (factor :: factors) = List.map (fun (split : List Hex.ZPoly × List Hex.ZPoly) => (factor :: split.fst, split.snd)) (Hex.subsetSplits factors)

def Hex.firstSome {α β : Type} : List α → (α → Option β) → Option β

Return the first some produced by applying f to elements of xs in order, or none if every application is none.

Equations

• Hex.firstSome [] x✝ = none
• Hex.firstSome (x_2 :: xs) x✝ = match x✝ x_2 with | some y => some y | none => Hex.firstSome xs x✝

theorem Hex.reassemblePolynomialFactors_mem_normalization_or_core (d : FactorNormalizationData) (coreFactors : Array ZPoly) (factor : ZPoly) (hmem : factor ∈ (reassemblePolynomialFactors d coreFactors).toList) : factor ∈ (polynomialNormalizationPrefixFactors d).toList ∨ factor ∈ coreFactors.toList

Public wrapper for the reassembly membership split used by downstream factor-output classifiers.

def Hex.reassemblyExpansionComplete (d : FactorNormalizationData) (coreFactors : Array ZPoly) : Prop

The repeated-part expansion fully consumed the normalization residual, so reassemblePolynomialFactors uses its expanded branch rather than the non-decomposed repeated-part fallback.

Equations

• Hex.reassemblyExpansionComplete d coreFactors = ((Hex.expandRepeatedPartFactorArray d.repeatedPart coreFactors).snd = 1)

theorem Hex.reassemblePolynomialFactors_mem_xPower_or_core_of_expansionComplete (d : FactorNormalizationData) (coreFactors : Array ZPoly) (factor : ZPoly) (hcomplete : reassemblyExpansionComplete d coreFactors) (hmem : factor ∈ (reassemblePolynomialFactors d coreFactors).toList) : factor ∈ (xPowerFactorArray d.xPower).toList ∨ factor ∈ coreFactors.toList

Sharp membership split for the complete-expansion branch of reassembly.

When the repeated part has been completely expanded by the supplied square-free part factors, a reassembled raw factor is either an extracted X-power factor or one of the supplied factors of the square-free part. In particular, it cannot be the non-decomposed repeatedPartFactorArray fallback.

theorem Hex.normalizeFactorSign_ne_zero_of_ne_zero (f : ZPoly) (hf : f ≠ 0) : normalizeFactorSign f ≠ 0

Sign normalization preserves nonzeroness.

theorem Hex.collectFactorMultiplicities_entry_mem_normalized_raw (factors : Array ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ (collectFactorMultiplicities factors).toList) : ∃ (raw : ZPoly), raw ∈ factors.toList ∧ entry.fst = normalizeFactorSign raw

Every collected (factor, multiplicity) entry comes from some raw factor after sign normalization. This is the theorem-level wrapper for the collectFactorMultiplicities step.

theorem Hex.collectFactorMultiplicities_entry_multiplicity_pos (factors : Array ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ (collectFactorMultiplicities factors).toList) : 0 < entry.snd

Every collected factorization entry has positive multiplicity.

theorem Hex.collectFactorMultiplicities_entry_shouldRecord (factors : Array ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ (collectFactorMultiplicities factors).toList) : shouldRecordPolynomialFactor entry.fst = true

Every collected factorization entry passed the recorded-factor filter.

theorem Hex.collectFactorMultiplicities_pairwise_first (factors : Array ZPoly) : List.Pairwise (fun (a b : ZPoly × Nat) => a.fst ≠ b.fst) (collectFactorMultiplicities factors).toList

The collector emits no duplicate polynomial keys.

theorem Hex.factorizationOfFactors_entry_mem_normalized_raw (f : ZPoly) (factors : Array ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ (factorizationOfFactors f factors).factors.toList) : ∃ (raw : ZPoly), raw ∈ factors.toList ∧ entry.fst = normalizeFactorSign raw

Membership in a Factorization built from a raw factor array descends to membership in that raw array, up to sign normalization.

theorem Hex.factorizationOfFactors_entry_multiplicity_pos (f : ZPoly) (factors : Array ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ (factorizationOfFactors f factors).factors.toList) : 0 < entry.snd

Entries in a Factorization built from raw factors have positive multiplicity.

theorem Hex.factorizationOfFactors_pairwise_first (f : ZPoly) (factors : Array ZPoly) : List.Pairwise (fun (a b : ZPoly × Nat) => a.fst ≠ b.fst) (factorizationOfFactors f factors).factors.toList

A Factorization built from raw factors has no duplicate polynomial keys.

theorem Hex.factorizationOfFactors_product_of_raw_product_of_all_recorded_normalized (f : ZPoly) (factors : Array ZPoly) (hraw : DensePoly.C (signedContentScalar f) * factors.polyProduct = f) (hnormalized : ∀ (factor : ZPoly), factor ∈ factors.toList → normalizeFactorSign factor = factor) (hrecorded : ∀ (factor : ZPoly), factor ∈ factors.toList → shouldRecordPolynomialFactor factor = true) : (factorizationOfFactors f factors).product = f

Packing a sign-normalized, fully recorded raw factor array preserves its known product.

theorem Hex.factorizationOfFactors_product_of_zero (factors : Array ZPoly) : (factorizationOfFactors 0 factors).product = 0

Packing any raw factor array against the zero input has product zero, because the packed scalar is zero.

theorem Hex.normalizeFactorSign_one : normalizeFactorSign 1 = 1

The sign-normalisation of 1 is 1. Exposed publicly so Mathlib-side per-branch umbrellas (in particular the fast-path constant arm, where the singleton primitive square-free part collapses to 1) can normalise the unit factor without re-deriving the leading-coefficient computation inline.

theorem Hex.shouldRecordPolynomialFactor_one : shouldRecordPolynomialFactor 1 = false

The shouldRecordPolynomialFactor filter rejects the unit 1. Exposed publicly so Mathlib-side per-branch umbrellas can contradict factorize_entry_shouldRecord directly when an entry collapses to a unit (in particular the fast-path constant arm, where the singleton primitive square-free part is 1).

theorem Hex.normalizeFactorSign_eq_self_of_leadingCoeff_nonneg (g : ZPoly) (h : 0 ≤ DensePoly.leadingCoeff g) : normalizeFactorSign g = g

Sign normalization fixes a polynomial with nonnegative leading coefficient.

theorem Hex.normalizeFactorSign_leadingCoeff_nonneg (g : ZPoly) : 0 ≤ DensePoly.leadingCoeff (normalizeFactorSign g)

Sign normalization produces a nonnegative leading coefficient.

theorem Hex.normalizeFactorSign_idem (g : ZPoly) : normalizeFactorSign (normalizeFactorSign g) = normalizeFactorSign g

Sign normalization is idempotent.

theorem Hex.normalizeFactorSign_primitive (f : ZPoly) (h : f.Primitive) : (normalizeFactorSign f).Primitive

Sign normalisation preserves primitivity: the if_neg branch is the identity, and the if_pos branch scales by -1, which preserves content by DensePoly.content_scale_neg_one.

theorem Hex.collectFactorMultiplicities_entry_normalizeFactorSign_id (factors : Array ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ (collectFactorMultiplicities factors).toList) : normalizeFactorSign entry.fst = entry.fst

Collected factor entries are fixed points of normalizeFactorSign.

theorem Hex.collectFactorMultiplicities_entry_leadingCoeff_pos (factors : Array ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ (collectFactorMultiplicities factors).toList) : 0 < DensePoly.leadingCoeff entry.fst

Collected factor entries have positive leading coefficient.

theorem Hex.factorizationOfFactors_entry_normalizeFactorSign_id (f : ZPoly) (factors : Array ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ (factorizationOfFactors f factors).factors.toList) : normalizeFactorSign entry.fst = entry.fst

Entries in a Factorization built from raw factors are fixed points of normalizeFactorSign.

theorem Hex.factorizationOfFactors_entry_leadingCoeff_pos (f : ZPoly) (factors : Array ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ (factorizationOfFactors f factors).factors.toList) : 0 < DensePoly.leadingCoeff entry.fst

Entries in a Factorization built from raw factors have positive leading coefficient.

theorem Hex.exactQuotient?_eq_some_of_mul_eq_monic_of_pos_degree {target candidate quotient : ZPoly} (hmonic : DensePoly.Monic candidate) (hdegree : 0 < DensePoly.natDegree candidate) (hmul : quotient * candidate = target) : exactQuotient? target candidate = some quotient

Converse to exactQuotient?_product: if candidate is monic with positive degree and quotient * candidate = target, then exactQuotient? target candidate returns some quotient.

theorem Hex.exactQuotient?_eq_some_of_divMod_eq_of_shouldRecord {target candidate quotient : ZPoly} (hrecord : shouldRecordPolynomialFactor candidate = true) (_hdivMod : DensePoly.divMod target candidate = (quotient, 0)) (hmul : quotient * candidate = target) : exactQuotient? target candidate = some quotient

Non-monic packaging companion for exactQuotient?_product.

For non-monic integer polynomials, an exact product equation alone does not identify the executable quotient: DensePoly.divMod performs coefficient division in ℤ, so downstream proofs must also supply the concrete divMod result. This lemma records the remaining wrapper logic of exactQuotient?: a recorded non-unit candidate with zero executable remainder and the checked product equation is accepted with the witnessed quotient.