theorem Hex.densePoly_int_scale_one (p : ZPoly) : DensePoly.scale 1 p = p

Scaling an integer polynomial by one is a no-op.

theorem Hex.reassemblePolynomialFactors_product_eq_input (f : ZPoly) (coreFactors : Array ZPoly) (hcore : coreFactors.polyProduct = (normalizeForFactor f).squareFreeCore) : DensePoly.C (signedContentScalar f) * (reassemblePolynomialFactors (normalizeForFactor f) coreFactors).polyProduct = f

The full normalized reassembly: combining the array-product layout from polyProduct_reassemblePolynomialFactors with the signed content reconstruction recovers the original polynomial exactly. Handles f = 0 separately because signedContentScalar 0 = 0 collapses the scalar prefix.

theorem Hex.subsetSplitsWithFirst_mem_cons {factor : ZPoly} {factors selected rest : List ZPoly} (hmem : (selected, rest) ∈ subsetSplits factors) : (factor :: selected, rest) ∈ subsetSplitsWithFirst (factor :: factors)

A subset split extends to the corresponding split after adjoining a required head.

theorem Hex.subsetSplits_nil_mem : ([], []) ∈ subsetSplits []

Constructor for subsetSplits membership on the empty list: the only partition of the empty list is ([], []).

theorem Hex.subsetSplits_cons_left_mem {factor : ZPoly} {factors selected rest : List ZPoly} (h : (selected, rest) ∈ subsetSplits factors) : (factor :: selected, rest) ∈ subsetSplits (factor :: factors)

Constructor for subsetSplits membership on a cons list, head selected: prepending factor to the selected side preserves enumerability.

theorem Hex.subsetSplits_cons_right_mem {factor : ZPoly} {factors selected rest : List ZPoly} (h : (selected, rest) ∈ subsetSplits factors) : (selected, factor :: rest) ∈ subsetSplits (factor :: factors)

Constructor for subsetSplits membership on a cons list, head unselected: prepending factor to the rest side preserves enumerability.

theorem Hex.firstSome_isSome_of_mem {α β : Type} {xs : List α} {f : α → Option β} {x : α} {y : β} (hmem : x ∈ xs) (hxy : f x = some y) : (firstSome xs f).isSome = true

Existence companion to firstSome_some: if f x = some y for some x ∈ xs, then firstSome xs f is itself some _. Used to chain executable completeness arguments: showing the search at the current step can succeed reduces to exhibiting a single subset whose candidate works.

theorem Hex.recombinationSearch_product (f : ZPoly) (localFactors factors : List ZPoly) (hsearch : recombinationSearch f localFactors = some factors) : factors.toArray.polyProduct = f

A successful exhaustive recombination search preserves the target product.

theorem Hex.recombinationSearchModAux_one (modulus : Nat) (localFactors : List ZPoly) (fuel : Nat) : recombinationSearchModAux 1 modulus localFactors (fuel + 1) = some []

Base case for the exhaustive recombination search: when the running target has already been reduced to 1, the search terminates and returns the empty factor list.

theorem Hex.recombinationSearchModAux_isSome_of_step {target candidate quotient : ZPoly} {modulus fuel : Nat} {localFactors selected rest : List ZPoly} (htarget_ne_one : target ≠ 1) (hsplit : (selected, rest) ∈ subsetSplitsWithFirst localFactors) (hcandidate_def : candidate = normalizeFactorSign (centeredLiftPoly selected.toArray.polyProduct modulus).primitivePart) (hrecord : shouldRecordPolynomialFactor candidate = true) (hquot : exactQuotient? target candidate = some quotient) (hsearch_rest : (recombinationSearchModAux quotient modulus rest fuel).isSome = true) : (recombinationSearchModAux target modulus localFactors (fuel + 1)).isSome = true

Executable completeness of recombinationSearchModAux: if a single exhaustive-search step can pick the candidate produced by centred-lifting selected (a subset of localFactors whose order-preserving partition has rest as complement), and the recursive search on the residual (quotient, rest) succeeds with the supplied fuel, then the search at the current step also succeeds.

This is the Mathlib-free step lemma underpinning Group A coverage proofs: it exposes that any subset of the lifted local factors with a working candidate is enumerated by subsetSplitsWithFirst, and that the search descends through that candidate to the residual problem.

theorem Hex.recombinationSearchMod_isSome_of_step {target candidate quotient : ZPoly} {modulus : Nat} {localFactors selected rest : List ZPoly} (htarget_ne_one : target ≠ 1) (hsplit : (selected, rest) ∈ subsetSplitsWithFirst localFactors) (hcandidate_def : candidate = normalizeFactorSign (centeredLiftPoly selected.toArray.polyProduct modulus).primitivePart) (hrecord : shouldRecordPolynomialFactor candidate = true) (hquot : exactQuotient? target candidate = some quotient) (hsearch_rest : (recombinationSearchModAux quotient modulus rest localFactors.length).isSome = true) : (recombinationSearchMod target modulus localFactors).isSome = true

Companion to recombinationSearchModAux_isSome_of_step at the recombinationSearchMod surface. Hides the fuel parameter, requiring the caller to supply the recursive isSome witness already specialised to fuel localFactors.length. Useful for downstream callers that want to chain step lemmas with a fixed shared fuel budget.

theorem Hex.recombinationSearchModAux_eq_some_of_step_of_prefix_none {target candidate quotient : ZPoly} {modulus fuel : Nat} {localFactors selected rest restFactors : List ZPoly} {pre suffix : List (List ZPoly × List ZPoly)} (htarget_ne_one : target ≠ 1) (hsplits : subsetSplitsWithFirst localFactors = pre ++ (selected, rest) :: suffix) (hprefix : ∀ (split : List ZPoly × List ZPoly), split ∈ pre → (have candidate' := normalizeFactorSign (centeredLiftPoly split.fst.toArray.polyProduct modulus).primitivePart; if shouldRecordPolynomialFactor candidate' = true then match exactQuotient? target candidate' with | none => none | some quotient' => match recombinationSearchModAux quotient' modulus split.snd fuel with | none => none | some r => some (candidate' :: r) else none) = none) (hcandidate_def : candidate = normalizeFactorSign (centeredLiftPoly selected.toArray.polyProduct modulus).primitivePart) (hrecord : shouldRecordPolynomialFactor candidate = true) (hquot : exactQuotient? target candidate = some quotient) (hsearch_rest : recombinationSearchModAux quotient modulus rest fuel = some restFactors) : recombinationSearchModAux target modulus localFactors (fuel + 1) = some (candidate :: restFactors)

Exact-output version of recombinationSearchModAux_isSome_of_step.

The earlier completeness lemma is intentionally weak: it only proves that the search succeeds when a particular split would work. This theorem is the concrete-output companion used by coverage proofs: if that split is positioned after a prefix whose recombination attempts all fail, then the executable firstSome traversal returns the candidate from this split as the head of the resulting factor list.

theorem Hex.recombinationSearchMod_eq_some_of_step_of_prefix_none {target candidate quotient : ZPoly} {modulus : Nat} {localFactors selected rest restFactors : List ZPoly} {pre suffix : List (List ZPoly × List ZPoly)} (htarget_ne_one : target ≠ 1) (hsplits : subsetSplitsWithFirst localFactors = pre ++ (selected, rest) :: suffix) (hprefix : ∀ (split : List ZPoly × List ZPoly), split ∈ pre → (have candidate' := normalizeFactorSign (centeredLiftPoly split.fst.toArray.polyProduct modulus).primitivePart; if shouldRecordPolynomialFactor candidate' = true then match exactQuotient? target candidate' with | none => none | some quotient' => match recombinationSearchModAux quotient' modulus split.snd localFactors.length with | none => none | some r => some (candidate' :: r) else none) = none) (hcandidate_def : candidate = normalizeFactorSign (centeredLiftPoly selected.toArray.polyProduct modulus).primitivePart) (hrecord : shouldRecordPolynomialFactor candidate = true) (hquot : exactQuotient? target candidate = some quotient) (hsearch_rest : recombinationSearchModAux quotient modulus rest localFactors.length = some restFactors) : recombinationSearchMod target modulus localFactors = some (candidate :: restFactors)

Surface exact-output companion for recombinationSearchMod.

This hides the fuel parameter in the same way as recombinationSearchMod_isSome_of_step, while retaining the returned factor list when the selected split is the first successful split.

theorem Hex.recombineExhaustive_eq_of_recombinationSearchMod_some {f : ZPoly} {d : LiftData} {factors : List ZPoly} (h : recombinationSearchMod f (liftModulus d) d.liftedFactors.toList = some factors) : recombineExhaustive f d = factors.toArray

When recombinationSearchMod succeeds on the lifted-factor list, the recombineExhaustive wrapper returns exactly the array of recovered factors. This is the equality lemma that lets downstream irreducibility proofs replace a recombineExhaustive term with a concrete factor list once the search is known to succeed.

theorem Hex.bhksRecoveryCoreWithBound_product (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) (k fuel : Nat) (coreFactors : Array ZPoly) : bhksRecoveryCoreWithBound core B primeData k fuel = some coreFactors → coreFactors.polyProduct = core

A successful fixed-precision BHKS fast-recombination loop preserves the polynomial product: every success branch comes from the classified BHKS recovery success case, which already certifies Array.polyProduct = core.

theorem Hex.bhksRecoveryCoreWithBound_some_indicatorCandidates {core : ZPoly} {B : Nat} {primeData : PrimeChoiceData} {k fuel : Nat} {coreFactors : Array ZPoly} (h : bhksRecoveryCoreWithBound core B primeData k fuel = some coreFactors) : ∃ (k' : Nat), ∃ (hrows : 1 ≤ (bhksLatticeBasis core (core.directLiftData k' primeData).p (core.directLiftData k' primeData).k (core.directLiftData k' primeData).liftedFactors).factorCount + (bhksLatticeBasis core (core.directLiftData k' primeData).p (core.directLiftData k' primeData).k (core.directLiftData k' primeData).liftedFactors).coeffWidth), bhksIndicatorCandidates? core (core.directLiftData k' primeData) (bhksEquivalenceClassIndicators (bhksProjectedRows (bhksLatticeBasis core (core.directLiftData k' primeData).p (core.directLiftData k' primeData).k (core.directLiftData k' primeData).liftedFactors) hrows)) = some coreFactors ∧ bhksDegenerateIndicatorPartition (bhksProjectedRows (bhksLatticeBasis core (core.directLiftData k' primeData).p (core.directLiftData k' primeData).k (core.directLiftData k' primeData).liftedFactors) hrows) (bhksEquivalenceClassIndicators (bhksProjectedRows (bhksLatticeBasis core (core.directLiftData k' primeData).p (core.directLiftData k' primeData).k (core.directLiftData k' primeData).liftedFactors) hrows)) = false ∧ coreFactors.polyProduct = core ∧ bhksRecoveryFloor core ≤ k'

Proof-facing recovery-data extractor for the fast-recombination loop, stated without reference to the private bhksRecoverClassified. A successful bhksRecoveryCoreWithBound call is witnessed by a concrete precision-schedule index k': at the toMonicLiftData for that precision there is a positive-dimension witness hrows whose equivalence-class indicator candidates reconstruct exactly to coreFactors, the indicator partition is non-degenerate, and the candidates multiply back to core. This is the correspondence-side entry point used to rebuild the forward-recovery package (and hence the selected support/subset witnesses) that the per-factor success lemmas discard.

theorem Hex.bhksRecoveryCoreWithBound_some_normalizeFactorSign {core : ZPoly} {B : Nat} {primeData : PrimeChoiceData} {k fuel : Nat} {coreFactors : Array ZPoly} (h : bhksRecoveryCoreWithBound core B primeData k fuel = some coreFactors) (factor : ZPoly) : factor ∈ coreFactors.toList → normalizeFactorSign factor = factor

Successful lattice recovery returns factors with normalized signs.

theorem Hex.bhksRecoveryCoreWithBound_some_shouldRecord {core : ZPoly} {B : Nat} {primeData : PrimeChoiceData} {k fuel : Nat} {coreFactors : Array ZPoly} (h : bhksRecoveryCoreWithBound core B primeData k fuel = some coreFactors) (factor : ZPoly) : factor ∈ coreFactors.toList → shouldRecordPolynomialFactor factor = true

Successful lattice recovery returns only nonconstant polynomial factors.

theorem Hex.bhksRecoveryCoreWithBound_some_degree_pos {core : ZPoly} {B : Nat} {primeData : PrimeChoiceData} {k fuel : Nat} {coreFactors : Array ZPoly} (h : bhksRecoveryCoreWithBound core B primeData k fuel = some coreFactors) (factor : ZPoly) : factor ∈ coreFactors.toList → 0 < DensePoly.natDegree factor

Every factor returned by successful lattice recovery has positive degree.

theorem Hex.bhksRecoveryCoreWithBound_some_dvd (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) (k fuel : Nat) (coreFactors : Array ZPoly) : bhksRecoveryCoreWithBound core B primeData k fuel = some coreFactors → ∀ (factor : ZPoly), factor ∈ coreFactors.toList → factor ∣ core

Every factor emitted by the BHKS fast-recombination loop divides the input polynomial. The success branch is the only branch that exits with some coreFactors, and bhksRecoverClassified_success_dvd certifies divisibility for each candidate at that exit.

theorem Hex.degree_pos_of_primitive_norm_record (q : ZPoly) (hq_primitive : q.Primitive) (hq_norm : normalizeFactorSign q = q) (hq_record : shouldRecordPolynomialFactor q = true) : 0 < DensePoly.natDegree q

A primitive, sign-normalized ZPoly that passes shouldRecordPolynomialFactor has positive degree?. A size-1 such polynomial combines Primitive q (forcing |q.coeff 0| = 1) with normalizeFactorSign q = q (forcing 0 ≤ q.coeff 0) to conclude q = 1, which shouldRecord excludes.