inductive Hex.FactorMethod : Type

Method that produced a public factorization result.

• constant : FactorMethod

  Constant-polynomial normalization.

• quadratic : FactorMethod

  Direct extraction of integer roots from a quadratic.

• classical : FactorMethod

  Exhaustive recombination of lifted modular factors.

• lattice : FactorMethod

  Lattice recombination using logarithmic derivatives.

• replay : FactorMethod

  Exact classical replay of a partition proposed by a small CLD lattice.

• trial : FactorMethod

  Trial division by bounded candidate factors.

• quadraticNorm : FactorMethod

  An iterated-quadratic-norm certificate proved the square-free core irreducible.

@[instance_reducible]

instance Hex.instDecidableEqFactorMethod : DecidableEq FactorMethod

Equations

• Hex.instDecidableEqFactorMethod x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hex.FactorMethod.name : FactorMethod → String

A short diagnostic name for a factorization method.

Equations

• Hex.FactorMethod.constant.name = "constant"
• Hex.FactorMethod.quadratic.name = "quadratic"
• Hex.FactorMethod.classical.name = "classical"
• Hex.FactorMethod.lattice.name = "lattice"
• Hex.FactorMethod.replay.name = "replay"
• Hex.FactorMethod.trial.name = "trial"
• Hex.FactorMethod.quadraticNorm.name = "quadraticNorm"

structure Hex.DirectFactorTrace : Type

Trace derived from the same factorization result used by the untraced API.

• method : FactorMethod

  The method that produced the returned factorization.

• classicalDecline : Option DeclineReason

  The reason classical recombination declined, when it did.

• classical : ClassicalStats

  Measurements from the classical recombination attempt.

@[instance_reducible]

instance Hex.instDecidableEqDirectFactorTrace : DecidableEq DirectFactorTrace

Equations

• Hex.instDecidableEqDirectFactorTrace = Hex.instDecidableEqDirectFactorTrace.decEq

def Hex.instDecidableEqDirectFactorTrace.decEq (x✝ x✝¹ : DirectFactorTrace) : Decidable (x✝ = x✝¹)

Equations

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

structure Hex.ClassicalRun (f : ZPoly) : Type

Result of normalization followed by classical recombination. A successful prime plan is retained even when recombination declines, so lattice recombination can consume the exact modular factorization already computed.

• factors : Option (Array ZPoly)

  The factors when classical recombination succeeded.

• trace : DirectFactorTrace

  The method and classical-search measurements.

• modular : Option (DirectPrimePlan (SquareFreeInput.ofNormalized (normalizeForFactor f)))

  The selected modular plan, retained for possible lattice recombination.

structure Hex.FactorRun : Type

Raw factors and trace produced by the total selector in one execution.

• factors : Array ZPoly

  The raw polynomial factors before multiplicities are collected.

• trace : DirectFactorTrace

  The method and classical-search measurements.

def Hex.instDecidableEqFactorRun.decEq (x✝ x✝¹ : FactorRun) : Decidable (x✝ = x✝¹)

Equations

• Hex.instDecidableEqFactorRun.decEq { factors := a, trace := a_1 } { factors := b, trace := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.instDecidableEqFactorRun : DecidableEq FactorRun

Equations

• Hex.instDecidableEqFactorRun = Hex.instDecidableEqFactorRun.decEq

theorem Hex.bhksRecoveryCoreWithBound_ne_none_of_recovery_on_schedule (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) {start fuel target : Nat} {factors : Array ZPoly} (hfloor : bhksRecoveryFloor core ≤ target) (hmem : target ∈ henselPrecisionSchedule B start fuel) (hrecover : bhksRecover? core (core.directLiftData target primeData) = some factors) : bhksRecoveryCoreWithBound core B primeData start fuel ≠ none

A successful lift-and-recover at any scheduled precision at or above the recovery floor forces the bounded BHKS recovery loop to return a result.

def Hex.proposalLiftedFactorThreshold : Nat

Number of modular factors above which incremental partition replay is attempted before exhaustive direct recombination.

Equations

• Hex.proposalLiftedFactorThreshold = 24

def Hex.nonzeroCoefficientCount (f : ZPoly) : Nat

Number of nonzero coefficients in a polynomial.

Equations

• Hex.nonzeroCoefficientCount f = Array.foldl (fun (count : Nat) (coefficient : Int) => if coefficient = 0 then count else count + 1) 0 (Hex.DensePoly.toArray f)

def Hex.proposalEligible (f : ZPoly) (liftedFactorCount : Nat) : Prop

Cost predicate for the proposal tier. Large dense inputs may benefit from support peeling and, after an exact peel, a small CLD lattice on the residual; lacunary inputs retain the direct classical route, whose coefficient filters are especially effective there.

Equations

• Hex.proposalEligible f liftedFactorCount = (Hex.proposalLiftedFactorThreshold ≤ liftedFactorCount ∧ Hex.DensePoly.natDegree f < 4 * Hex.nonzeroCoefficientCount f)

@[instance_reducible]

instance Hex.instDecidableProposalEligible (f : ZPoly) (liftedFactorCount : Nat) : Decidable (proposalEligible f liftedFactorCount)

Equations

• Hex.instDecidableProposalEligible f liftedFactorCount = id inferInstance

inductive Hex.ClassicalInput (f : ZPoly) : Type

Normalization and prime selection for the classical engine. The selected plan carries its defining equality, so every later route consumes exactly the prime data computed here.

• answered {f : ZPoly} (factors : Array ZPoly) (trace : DirectFactorTrace) : ClassicalInput f

  A normalization or quadratic case answered before prime selection.

• noGoodPrime {f : ZPoly} : ClassicalInput f

  No admissible modular prime was found.

• planned {f : ZPoly} (modular : DirectPrimePlan (SquareFreeInput.ofNormalized (normalizeForFactor f))) (selected : directPrimePlan? (SquareFreeInput.ofNormalized (normalizeForFactor f)) = some modular) : ClassicalInput f

  A selected modular plan and its defining equation.

def Hex.classicalInput (f : ZPoly) : ClassicalInput f

Normalize and select the modular input for direct recombination.

Once the modular factorization is in hand its support width is known, and with it the size of the recombination walk that would follow. At or above Hex.QuadraticNormCertificate.widthFloor that walk is expensive enough to be worth one attempt at the iterated-quadratic-norm certificate, which answers the whole square-free core as a single irreducible factor. A success is an ordinary answered, reassembled by the same Hex.reassemblePolynomialFactors as the constant and quadratic cases, so it returns the same Hex.Factorization any other singleton proof would. A failure falls through to planned with no state carried, and every route below the floor is untouched.

Equations

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

def Hex.runClassicalPlan (f : ZPoly) (modular : DirectPrimePlan (SquareFreeInput.ofNormalized (normalizeForFactor f))) : ClassicalRun f

Execute direct recombination from an already selected modular plan.

Equations

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

def Hex.ClassicalInput.run {f : ZPoly} : ClassicalInput f → ClassicalRun f

Run the unrestricted classical method from a prepared input.

Equations

• (Hex.ClassicalInput.answered factors trace).run = { factors := some factors, trace := trace }
• Hex.ClassicalInput.noGoodPrime.run = { factors := none, trace := { method := Hex.FactorMethod.classical, classicalDecline := some Hex.DeclineReason.noGoodPrime } }
• (Hex.ClassicalInput.planned modular selected).run = Hex.runClassicalPlan f modular

def Hex.ClassicalInput.beforeProposal {f : ZPoly} : ClassicalInput f → ClassicalRun f

Route an eligible normalized large-support input to proposal replay before direct recombination. All other inputs run the unrestricted classical method.

Equations

• One or more equations did not get rendered due to their size.
• (Hex.ClassicalInput.answered factors trace).beforeProposal = { factors := some factors, trace := trace }
• Hex.ClassicalInput.noGoodPrime.beforeProposal = { factors := none, trace := { method := Hex.FactorMethod.classical, classicalDecline := some Hex.DeclineReason.noGoodPrime } }

def Hex.runClassical (f : ZPoly) : ClassicalRun f

Normalize once, select one modular plan, and execute the unrestricted direct-coordinate classical engine.

Equations

• Hex.runClassical f = (Hex.classicalInput f).run

def Hex.routeClassical (f : ZPoly) : ClassicalRun f

Cost-routed classical front end used by the total factorizer. A normalized eligible large-support input retains its plan and yields to proposal replay; every other input agrees with runClassical.

Equations

• Hex.routeClassical f = (Hex.classicalInput f).beforeProposal

def Hex.factorClassicalFactors (f : ZPoly) : Option (Array ZPoly)

Raw factor array for the sole production classical method.

Equations

• Hex.factorClassicalFactors f = (Hex.runClassical f).factors

def Hex.factorClassical (f : ZPoly) : Option Factorization

Factor via the direct-coordinate, size-ordered classical engine. Returns none only with a typed decline recorded by runClassical.

Equations

• Hex.factorClassical f = Option.map (Hex.factorizationOfFactors f) (Hex.factorClassicalFactors f)

def Hex.factorClassicalTraced (f : ZPoly) : Option Factorization × DirectFactorTrace

Classical factorization and typed trace derived from one shared execution.

Equations

• Hex.factorClassicalTraced f = (Option.map (Hex.factorizationOfFactors f) (Hex.runClassical f).factors, (Hex.runClassical f).trace)

structure Hex.CoordinateLatticeStats : Type

Measurements from one selected-coordinate CLD lattice.

• residualDegree : Nat

  Degree of the residual integer polynomial.

• liftedFactorCount : Nat

  Lifted local factors represented by indicator coordinates.

• coordinates : Array Nat

  Selected coefficient coordinates.

• cutThresholds : Array Nat

  Per-column coefficient cut thresholds.

• dimension : Nat

  Square lattice dimension.

• henselPrecision : Nat

  Hensel exponent used by the CLD rows.

• maxEntryBits : Nat

  Maximum bit length of an entry in the lattice basis.

• reducedRows : Nat

  Rows produced by the exact native LLL reducer.

• projectedRows : Nat

  Rows retained after exact LLL and the Gram-Schmidt cut.

• indicatorCount : Nat

  Support classes suggested by row reduction.

• supportSizes : Array Nat

  Sizes of the proposed lifted-factor support classes.

• candidateDegrees : Array Nat

  Degrees of exactly reconstructed candidate pieces.

• accepted : Bool

  Whether reconstruction produced an exact nontrivial partition.

@[instance_reducible]

instance Hex.instDecidableEqCoordinateLatticeStats : DecidableEq CoordinateLatticeStats

Equations

• Hex.instDecidableEqCoordinateLatticeStats = Hex.instDecidableEqCoordinateLatticeStats.decEq

def Hex.instDecidableEqCoordinateLatticeStats.decEq (x✝ x✝¹ : CoordinateLatticeStats) : Decidable (x✝ = x✝¹)

Equations

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

structure Hex.ProposalTrace : Type

Diagnostics for low-cardinality peeling, CLD partitioning, and replay.

• classical : ClassicalStats

  Classical measurements, including peeled degrees and residual support.

• lattices : Array CoordinateLatticeStats

  Selected-coordinate lattices tried in order.

• pieceDegrees : Array Nat

  Degrees of exact pieces presented to proved classical replay.

• factorDegrees : Array Nat

  Degrees returned by the proved replay calls.

@[instance_reducible]

instance Hex.instDecidableEqProposalTrace : DecidableEq ProposalTrace

Equations

• Hex.instDecidableEqProposalTrace = Hex.instDecidableEqProposalTrace.decEq

def Hex.instDecidableEqProposalTrace.decEq (x✝ x✝¹ : ProposalTrace) : Decidable (x✝ = x✝¹)

Equations

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

def Hex.coordinateLatticeWidths : List Nat

Deterministic incremental widths for selected-coordinate CLD lattices.

Equations

• Hex.coordinateLatticeWidths = [4, 8, 12, 16]

def Hex.proposalSubsetBudget : Nat

Candidate budget reserved for the proposal tier's complete low-cardinality levels. A later level that does not fit leaves the already peeled factors and exact residual intact.

Equations

• Hex.proposalSubsetBudget = 10000

def Hex.coordinateLatticeMaxEntryBits (L : BhksLatticeBasis) : Nat

Maximum bit length among entries of a square CLD lattice basis.

Equations

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

def Hex.indicatorSupportSizes (indicators : Array (Array Int)) : Array Nat

Cardinalities of proposed indicator support classes.

Equations

• Hex.indicatorSupportSizes indicators = Array.map (fun (row : Array Int) => Array.foldl (fun (count : Nat) (entry : Int) => if entry = 0 then count else count + 1) 0 row) indicators

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

Reduce a proposal lattice through the certified selector. Without an installed provider this is the exact native reducer; an installed external candidate is used only after Hex's certificate checks accept it.

Equations

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

def Hex.coordinateLatticeProposal (f : ZPoly) (d : LiftData) (prepared : BhksLeadingLogDerivativeData) (width : Nat) : Option (Array ZPoly) × CoordinateLatticeStats

Try one prefix of prepared selected-coordinate CLD data and reconstruct an exact candidate partition.

Equations

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

def Hex.proposeCoordinatePrefixes (f : ZPoly) (d : LiftData) (prepared : BhksLeadingLogDerivativeData) : List Nat → Array CoordinateLatticeStats → Option (Array ZPoly) × Array CoordinateLatticeStats

Replay an incremental selected-coordinate schedule against one shared maximum-width CLD preparation until an exact partition is reconstructed.

Equations

• One or more equations did not get rendered due to their size.
• Hex.proposeCoordinatePrefixes f d prepared [] x✝ = (none, x✝)

def Hex.coordinateLatticeProposals (f : ZPoly) (d : LiftData) (widths : List Nat) (attempts : Array CoordinateLatticeStats) : Option (Array ZPoly) × Array CoordinateLatticeStats

Prepare the largest requested CLD prefix once, then try its nested prefixes in order.

Equations

• Hex.coordinateLatticeProposals f d widths attempts = Hex.proposeCoordinatePrefixes f d (Hex.bhksLeadingLogDerivativeData f d.p d.k d.liftedFactors (List.foldl max 0 widths)) widths attempts

def Hex.replayClassicalList : List ZPoly → Option (Array ZPoly)

Replay the unrestricted proved classical factorizer on each exact proposal piece and concatenate the returned factor arrays.

Equations

• One or more equations did not get rendered due to their size.
• Hex.replayClassicalList [] = some #[]

def Hex.replayClassicalPieces (pieces : Array ZPoly) : Option (Array ZPoly)

Factor every proposed integer piece again with the existing proved classical factorizer.

Equations

• Hex.replayClassicalPieces pieces = Hex.replayClassicalList pieces.toList

structure Hex.ProposedFactorization (f : ZPoly) : Type

A self-contained successful proposal and replay result. The proof fields are erased at runtime; they expose exactly the checks used at the executable acceptance boundary.

• pieces : Array ZPoly

  Exact integer pieces before replay.

• factors : Array ZPoly

  Flattened factors returned by proved classical replay.

• core_eq : (normalizeForFactor f).squareFreeCore = f

  The proposal tier is entered only when normalization's square-free core is the input itself.

• pieces_product : self.pieces.polyProduct = f

  Proposed pieces reconstruct the input exactly.

• replay : replayClassicalPieces self.pieces = some self.factors

  Every factor comes from an existing classical factorization call.

• product : (factorizationOfFactors f self.factors).product = f

  The public factorization packing reconstructs the input exactly.

def Hex.proposeFactorization (f : ZPoly) (hcore : (normalizeForFactor f).squareFreeCore = f) (modular : DirectPrimePlan (SquareFreeInput.ofNormalized (normalizeForFactor f))) : Option (ProposedFactorization f) × ProposalTrace

Low-cardinality peeling, selected-coordinate CLD partitioning after exact progress, and proved classical replay from an existing modular plan. With no peeled factor, the proposal declines before building a lattice so production can proceed directly to its exact full-CLD fallback.

Equations

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

def Hex.factorProposedTraced (f : ZPoly) : Option (ProposedFactorization f) × ProposalTrace

Standalone proposal/replay entry. Production reuses the modular plan already selected by runClassical; this wrapper is retained for diagnostics.

Equations

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

def Hex.factorTrialFactorsWithBound (f : ZPoly) (B : Nat) : Array ZPoly

Raw factor array produced by the integer trial-division slow path.

Handles the deg-0 square-free part and integer-root cases up front via the same constant/quadratic-root short-circuits as the classical method; the residual exhaustive branch selects to the standalone integer trial-division algorithm (exhaustiveIntegerTrialCoreFactorsWithBound). This is the trial-division method of the three-method factorize combinator.

Equations

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

def Hex.factorTrialWithBound (f : ZPoly) (B : Nat) : Factorization

Factor using exhaustive recombination with the supplied coefficient bound.

Equations

• Hex.factorTrialWithBound f B = Hex.factorizationOfFactors f (Hex.factorTrialFactorsWithBound f B)

theorem Hex.factorTrialWithBound_eq_factorizationOfFactors (f : ZPoly) (B : Nat) : factorTrialWithBound f B = factorizationOfFactors f (factorTrialFactorsWithBound f B)

Characterise the bounded integer trial-division slow wrapper as the raw factor array packed into the public Factorization representation.

def Hex.factorTrial (f : ZPoly) : Factorization

Factor using the integer trial-division path at the default Mignotte coefficient bound. This is the trial-division method of the three-method factorize combinator.

Equations

• Hex.factorTrial f = Hex.factorTrialWithBound f f.defaultFactorCoeffBound

theorem Hex.factorTrial_eq (f : ZPoly) : factorTrial f = factorTrialWithBound f f.defaultFactorCoeffBound

Trial factorization uses the default coefficient bound.

def Hex.latticePrecisionCap (f : ZPoly) : Nat

Precision cap used by the public fast path.

The cap is the larger of the BHKS separation threshold bound of the primitive square-free part and the Mignotte coefficient bound of the input, so later termination proofs can use the same precision for both lattice separation and exact integer reconstruction.

The CLD lattice is built directly over (normalizeForFactor f).squareFreeCore. The square-free part remains explicit because it can have a larger coefficient norm than f (for f = (x¹⁸ - 1)(x¹⁹ - 1) the square-free part f / (x - 1) has coeffNormSq 36 against f's 4).

Equations

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

theorem Hex.bhksBound_squareFreeCore_le_latticePrecisionCap (f : ZPoly) : bhksBound (normalizeForFactor f).squareFreeCore ≤ latticePrecisionCap f

The cap dominates the BHKS resultant-precision bound of the primitive square-free part, the first of the four maxima defining it.

theorem Hex.cldCoeffFloor_squareFreeCore_le_latticePrecisionCap (f : ZPoly) : cldCoeffFloor (normalizeForFactor f).squareFreeCore ≤ latticePrecisionCap f

The cap clears the CLD column-adequacy floor of the primitive square-free part, so the lattice method's cap-precision run is column-adequate by construction.

theorem Hex.defaultFactorCoeffBound_le_latticePrecisionCap (f : ZPoly) : f.defaultFactorCoeffBound ≤ latticePrecisionCap f

The cap dominates the input polynomial's own Mignotte-style coefficient bound, so cap-precision recovery covers ordinary factor reconstruction.

theorem Hex.bhksRecoveryFloor_squareFreeCore_le_latticePrecisionCap (f : ZPoly) : bhksRecoveryFloor (normalizeForFactor f).squareFreeCore ≤ latticePrecisionCap f

The public precision cap clears the whole fast recovery acceptance floor, so the conditional loop always has admissible precisions on its schedule.

theorem Hex.defaultFactorCoeffBound_squareFreeCore_le_latticePrecisionCap (f : ZPoly) : (normalizeForFactor f).squareFreeCore.defaultFactorCoeffBound ≤ latticePrecisionCap f

The cap dominates the Mignotte bound of the primitive square-free part itself, needed by the true-support nonemptiness argument at cap precision.

theorem Hex.two_mul_bhksBound_squareFreeCore_lt_pow_cap (f : ZPoly) (primeData : PrimeChoiceData) (hp : 2 ≤ primeData.p) : 2 * bhksBound (normalizeForFactor f).squareFreeCore < primeData.p ^ ((normalizeForFactor f).squareFreeCore.directLiftData (latticePrecisionCap f) primeData).k

At the public precision cap, the monic lift for the primitive square-free part clears the BHKS separation threshold: 2 · bhksBound core < p ^ k. This is the hprec obligation of the lattice method's cap-precision irreducibility certification; it is what forces the cap's BHKS component to be computed from the square-free part rather than from f.

theorem Hex.two_mul_bhksBound_squareFreeCore_lt_pow_cap_of_choosePrimeData (f : ZPoly) (primeData : PrimeChoiceData) (hchoose : choosePrimeData? (normalizeForFactor f).squareFreeCore = some primeData) : 2 * bhksBound (normalizeForFactor f).squareFreeCore < primeData.p ^ ((normalizeForFactor f).squareFreeCore.directLiftData (latticePrecisionCap f) primeData).k

Variant of two_mul_bhksBound_squareFreeCore_lt_pow_cap keyed on the lattice method's prime-selection witness, matching the shape of the hprec side goal at the factorLatticeFactorsWithBound call site.

def Hex.bhksSingleAllOnesPartition (f : ZPoly) (d : LiftData) : Bool

The CLD recovery's equivalence-class partition at this precision is the single all-ones class; the signature of an irreducible input (all lifted mod-p factors form the one integer factor). At column-adequate precision (bhksRecoveryFloor core ≤ k) this certifies irreducibility; the proven count lower bound forces a reducible square-free part to exhibit ≥ 2 classes there (squareFreeCore_irreducible_of_bhksSingleAllOnes in the Mathlib layer); while below the floor it may instead mean the lattice has not separated the factors yet, so callers must only trust it at k ≥ bhksRecoveryFloor core. (A cap-free CLD path would treat this partition as degenerate and decline, which is why such a path "misses" on Swinnerton-Dyer inputs; the lattice method uses this predicate, both in latticeCoreLoop's early stop and in the trailing cap check, to turn the declined-but-certified case into a positive irreducibility verdict.)

Equations

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

def Hex.latticeCoreWithBound (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) (k fuel : Nat) : Option (Array ZPoly)

Lattice factorization loop entry: bhksRecoveryCoreWithBound with certificate-backed early termination on the single all-ones partition. Computes the CLD column-adequacy floor once (through the irreducible bhksRecoveryThreshold) and runs latticeCoreLoop.

Equations

• Hex.latticeCoreWithBound core B primeData k fuel = Hex.latticeCoreLoop✝ core B (Hex.bhksRecoveryThreshold core) primeData k fuel

theorem Hex.latticeCoreWithBound_ne_none_of_recovery_on_schedule (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) {start fuel target : Nat} {factors : Array ZPoly} (hfloor : bhksRecoveryFloor core ≤ target) (hmem : target ∈ henselPrecisionSchedule B start fuel) (hrecover : bhksRecover? core (core.directLiftData target primeData) = some factors) : latticeCoreWithBound core B primeData start fuel ≠ none

A successful fixed-precision recovery on the scheduled lattice path forces the certificate-aware lattice recovery loop to return some result.

theorem Hex.latticeCoreWithBound_some_spec {core : ZPoly} {B : Nat} {primeData : PrimeChoiceData} {k fuel : Nat} {cf : Array ZPoly} (h : latticeCoreWithBound core B primeData k fuel = some cf) : bhksRecoveryCoreWithBound core B primeData k fuel = some cf ∨ cf = #[core] ∧ ∃ (k' : Nat), bhksRecoveryFloor core ≤ k' ∧ bhksSingleAllOnesPartition core (core.directLiftData k' primeData) = true

A successful latticeCoreWithBound call is either a bhksRecoveryCoreWithBound success or the early irreducibility certificate; the singleton #[core] with a witness precision k' clearing bhksRecoveryFloor core whose partition is the single all-ones class. The witness pair is exactly the hB_floor/hbhks input of the Mathlib layer's squareFreeCore_irreducible_of_bhksSingleAllOnes.

def Hex.latticeCoreFactorsWithBound (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) : Option (Array ZPoly)

Large-r lattice factorization factorisation: the van Hoeij CLD recovery, plus irreducibility certification. When the recovery splits core, use its factors; when the loop's certificate-backed early stop fires (single all-ones partition at column-adequate precision), core is irreducible (#[core]); when the loop declines all the way to the cap, check the cap-precision partition once more: the single all-ones class means core is irreducible (#[core]), anything else is a genuine failure (none).

Both certification arms are conditional on the column-adequacy floor: the loop's early stop only examines the partition at k ≥ bhksRecoveryThreshold core, and the trailing cap check requires bhksRecoveryThreshold core ≤ B; below the floor the all-ones partition may merely mean the lattice has not separated the factors yet, so certifying there would be unsound. The public factorLattice supplies latticePrecisionCap, which clears the floor by construction.

Equations

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

def Hex.factorLatticeFactorsWithPlan (normalized : FactorNormalizationData) (B : Nat) (modular : DirectPrimePlan (SquareFreeInput.ofNormalized normalized)) : Option (Array ZPoly)

Reassemble a lattice result from an existing direct prime plan. The plan is indexed by the normalized polynomial, so callers cannot reuse modular factors for a different polynomial.

Equations

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

def Hex.factorLatticeFactorsWithBound (f : ZPoly) (B : Nat) : Option (Array ZPoly)

Raw factor array for the large-r lattice method: the CLD lattice recovery, certifying irreducibility at the cap so that Swinnerton-Dyer / high-r irreducibles return some #[f] instead of none.

Equations

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

theorem Hex.factorLatticeFactorsWithBound_zero (B : Nat) : factorLatticeFactorsWithBound 0 B = some (reassemblePolynomialFactors (normalizeForFactor 0) #[(normalizeForFactor 0).squareFreeCore])

The bounded lattice method represents the zero polynomial by its normalized zero factor.

def Hex.factorLatticeWithBound (f : ZPoly) (B : Nat) : Option Factorization

Attempt lattice recombination with the supplied coefficient bound.

Equations

• Hex.factorLatticeWithBound f B = Option.map (Hex.factorizationOfFactors f) (Hex.factorLatticeFactorsWithBound f B)

def Hex.factorLattice (f : ZPoly) : Option Factorization

Van Hoeij CLD lattice method (large-r) at the full BHKS precision cap. Certifies irreducibility (unlike a cap-free CLD path), so it returns some on Swinnerton-Dyer and cyclotomic high-r irreducibles.

Equations

• Hex.factorLattice f = Hex.factorLatticeWithBound f (Hex.latticePrecisionCap f)

def Hex.runLatticePlan (f : ZPoly) (trace : DirectFactorTrace) (modular : DirectPrimePlan (SquareFreeInput.ofNormalized (normalizeForFactor f))) : FactorRun

Package the CLD result from an existing modular plan, retaining the trial factorizer as the total backstop.

Equations

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

def Hex.runFactor (f : ZPoly) : FactorRun

Total integer-polynomial factorization with bounded fast paths.

Small modular supports use the proved size-ordered classical search directly. Large supports first search support sizes one through three, then reuse the same Hensel lift to keep peeling factors of support size one or two. After at least one exact peel, the residual and its complementary lifted support pass to a small leading-column CLD lattice for partitioning. Without exact progress, production skips that speculative lattice and proceeds directly to the full CLD fallback. The small lattice is only a proposal: exact product checks and proved classical factorization of every proposed piece decide acceptance. If that composition declines, the full proved CLD method remains the fallback, followed by trial division when necessary.

Returns the chosen Factorization and a DirectFactorTrace whose method records which method answered. A classical decline retains its direct prime plan, and the lattice fallback consumes that plan without repeating modular factorization.

Self-certifying. Each non-backstop method's Factorization is accepted only when it reconstructs the input (Factorization.product φ = f, decidable on ZPoly); on the (corpus-never) miss it falls through to the proven factorTrial backstop. This makes Factorization.product (ZPoly.factorize f) = f provable unconditionally without yet proving the classical recombination loop reconstructs (that, with per-factor irreducibility, is the separate re-proof step). Proposal irreducibility comes solely from the proved replay calls, not from trusting the selected-column lattice.

The raw factors and trace are retained together so every public view observes the same selection execution.

Equations

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

def Hex.factorTraced (f : ZPoly) : Factorization × DirectFactorTrace

Factor an integer polynomial and return a trace of the selected method.

Equations

• Hex.factorTraced f = (Hex.factorizationOfFactors f (Hex.runFactor f).factors, (Hex.runFactor f).trace)

def Hex.ZPoly.factorize (f : ZPoly) : Factorization

The public total factorisation of a Hex.ZPoly.

Small modular supports use Hex.factorClassical. Large supports reuse one Hensel lift for repeated exact low-cardinality peeling. Once peeling makes exact progress, a selected-column CLD proposal partitions the hard residual; otherwise the speculative tier is skipped. Every proposed piece is checked and factored again by the proved classical method. If the proposal declines, Hex.factorLattice tries full CLD recombination. Hex.factorTrial is the total backstop. It does not depend on Hex.choosePrimeData?, so this function still returns a factorisation when prime selection fails.

This definition lives in the Hex.ZPoly namespace, so it can be called with dot notation as f.factorize.

Equations

• f.factorize = (Hex.factorTraced f).fst

def Hex.ZPoly.factors (f : ZPoly) : Array (ZPoly × Nat)

The irreducible factors of f with their multiplicities: the factors field of the full factorisation f.factorize.

Equations

• f.factors = f.factorize.factors

theorem Hex.factorLattice_eq_map (f : ZPoly) : factorLattice f = Option.map (factorizationOfFactors f) (factorLatticeFactorsWithBound f (latticePrecisionCap f))

The CLD lattice method's Factorization is the raw lattice factor array packed through factorizationOfFactors f.

def Hex.factorFactors (f : ZPoly) : Array ZPoly

Raw factor array produced by the same total-selection execution as ZPoly.factorize.

Equations

• Hex.factorFactors f = (Hex.runFactor f).factors

theorem Hex.factorize_eq_factorizationOfFactors (f : ZPoly) : f.factorize = factorizationOfFactors f (factorFactors f)

The cost-based hybrid factorisation is the factorizationOfFactors-packed form of its raw factor array factorFactors. Every method (classical / lattice / trial) assembles via factorizationOfFactors f, so this correspondence lets the structural factorizationOfFactors_entry_* lemmas apply to every entry of the hybrid result.

theorem Hex.runClassicalPlan_modular (f : ZPoly) (modular : DirectPrimePlan (SquareFreeInput.ofNormalized (normalizeForFactor f))) : (runClassicalPlan f modular).modular = some modular

A modular plan retained by the classical run is exactly the plan selected for the normalized polynomial.

theorem Hex.runClassical_plan (f : ZPoly) {modular : DirectPrimePlan (SquareFreeInput.ofNormalized (normalizeForFactor f))} (hmodular : (runClassical f).modular = some modular) : directPrimePlan? (SquareFreeInput.ofNormalized (normalizeForFactor f)) = some modular

A modular plan retained by the full classical run is exactly the plan the direct prime selector chose for the normalized polynomial.

theorem Hex.routeClassical_plan (f : ZPoly) {modular : DirectPrimePlan (SquareFreeInput.ofNormalized (normalizeForFactor f))} (hmodular : (routeClassical f).modular = some modular) : directPrimePlan? (SquareFreeInput.ofNormalized (normalizeForFactor f)) = some modular

A modular plan retained by the cost router is the unique plan selected in its classical input.

theorem Hex.routeClassical_success (f : ZPoly) {factors : Array ZPoly} (h : (routeClassical f).factors = some factors) : factorClassicalFactors f = some factors

A successful cost-routed classical run is the same success returned by the unrestricted public classical method.

theorem Hex.runLatticePlan_mem_source (f : ZPoly) (trace : DirectFactorTrace) (modular : DirectPrimePlan (SquareFreeInput.ofNormalized (normalizeForFactor f))) {raw : ZPoly} (hmem : raw ∈ (runLatticePlan f trace modular).factors.toList) : (∃ (cf : Array ZPoly), factorLatticeFactorsWithPlan (normalizeForFactor f) (latticePrecisionCap f) modular = some cf ∧ raw ∈ cf.toList) ∨ raw ∈ (factorTrialFactorsWithBound f f.defaultFactorCoeffBound).toList

Every factor returned by a planned CLD run comes from its successful lattice result or from the trial-factorization backstop.

theorem Hex.runFactor_mem_source (f : ZPoly) {raw : ZPoly} (hmem : raw ∈ (runFactor f).factors.toList) : (∃ (result : ProposedFactorization f), raw ∈ result.factors.toList) ∨ (∃ (cf : Array ZPoly), factorClassicalFactors f = some cf ∧ raw ∈ cf.toList) ∨ (∃ (modular : DirectPrimePlan (SquareFreeInput.ofNormalized (normalizeForFactor f))), ∃ (cf : Array ZPoly), directPrimePlan? (SquareFreeInput.ofNormalized (normalizeForFactor f)) = some modular ∧ factorLatticeFactorsWithPlan (normalizeForFactor f) (latticePrecisionCap f) modular = some cf ∧ raw ∈ cf.toList) ∨ raw ∈ (factorTrialFactorsWithBound f f.defaultFactorCoeffBound).toList

Every raw factor of the total selector comes from proposal replay, the classical method, the CLD lattice method, or the trial backstop.

theorem Hex.factorFactors_mem_source (f : ZPoly) {raw : ZPoly} (hmem : raw ∈ (factorFactors f).toList) : (∃ (result : ProposedFactorization f), raw ∈ result.factors.toList) ∨ (∃ (cf : Array ZPoly), factorClassicalFactors f = some cf ∧ raw ∈ cf.toList) ∨ (∃ (modular : DirectPrimePlan (SquareFreeInput.ofNormalized (normalizeForFactor f))), ∃ (cf : Array ZPoly), directPrimePlan? (SquareFreeInput.ofNormalized (normalizeForFactor f)) = some modular ∧ factorLatticeFactorsWithPlan (normalizeForFactor f) (latticePrecisionCap f) modular = some cf ∧ raw ∈ cf.toList) ∨ raw ∈ (factorTrialFactorsWithBound f f.defaultFactorCoeffBound).toList

Every raw factor of the total selector comes from proposal replay or one of the established classical, lattice, and trial branches.

theorem Hex.factorizationOfFactors_scalar (f : ZPoly) (rawFactors : Array ZPoly) : (factorizationOfFactors f rawFactors).scalar = if f = 0 then 0 else if DensePoly.leadingCoeff f < 0 then -f.content else f.content

Scalar contract for a factorization assembled from a raw factor array. The public statement exposes the signed-content convention without exposing the private helper used to compute it.

@[simp]

theorem Hex.factorizationOfFactors_scalar_zero (rawFactors : Array ZPoly) : (factorizationOfFactors 0 rawFactors).scalar = 0

Packing raw factors of the zero polynomial records the zero scalar.

theorem Hex.factorizationOfFactors_scalar_of_leadingCoeff_neg {f : ZPoly} (rawFactors : Array ZPoly) (hf : f ≠ 0) (hneg : DensePoly.leadingCoeff f < 0) : (factorizationOfFactors f rawFactors).scalar = -f.content

A nonzero input with negative leading coefficient records the negated content as its scalar.

theorem Hex.factorizationOfFactors_scalar_of_leadingCoeff_pos {f : ZPoly} (rawFactors : Array ZPoly) (hf : f ≠ 0) (hpos : 0 < DensePoly.leadingCoeff f) : (factorizationOfFactors f rawFactors).scalar = f.content

A nonzero input with positive leading coefficient records its content as its scalar.

theorem Hex.factorizationOfFactors_scalar_eq_zero_iff (f : ZPoly) (rawFactors : Array ZPoly) : (factorizationOfFactors f rawFactors).scalar = 0 ↔ f = 0

The packed scalar vanishes exactly on the zero input.

theorem Hex.factorize_scalar (f : ZPoly) : f.factorize.scalar = if f = 0 then 0 else if DensePoly.leadingCoeff f < 0 then -f.content else f.content

Scalar contract for the default public factorization entry point.

@[simp]

theorem Hex.factorize_scalar_zero : (ZPoly.factorize 0).scalar = 0

The default factorization of 0 records the zero scalar.

theorem Hex.factorize_zero_factors : (ZPoly.factorize 0).factors = #[]

The default factorization of 0 records no polynomial factors: the primitive square-free part of 0 is the unit 1, so every reassembled raw factor is dropped by the shouldRecordPolynomialFactor filter. This lets factorize_irreducible_of_nonUnit discharge the degenerate f = 0 case vacuously, without a nonzero hypothesis.

theorem Hex.factorize_scalar_of_leadingCoeff_neg {f : ZPoly} (hf : f ≠ 0) (hneg : DensePoly.leadingCoeff f < 0) : f.factorize.scalar = -f.content

A nonzero polynomial with negative leading coefficient records the negated content as its scalar, keeping every stored factor's leading coefficient positive.

theorem Hex.factorize_scalar_of_leadingCoeff_pos {f : ZPoly} (hf : f ≠ 0) (hpos : 0 < DensePoly.leadingCoeff f) : f.factorize.scalar = f.content

A nonzero polynomial with positive leading coefficient keeps its content as scalar factor.

theorem Hex.factorize_scalar_eq_zero_iff (f : ZPoly) : f.factorize.scalar = 0 ↔ f = 0

The public scalar vanishes exactly on the zero input.

theorem Hex.factorize_entry_multiplicity_pos (f : ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ f.factorize.factors.toList) : 0 < entry.snd

Every recorded entry of the default public factorization has positive multiplicity.

theorem Hex.factorize_entry_normalizeFactorSign_id (f : ZPoly) (entry : ZPoly × Nat) (hmem : entry ∈ f.factorize.factors.toList) : normalizeFactorSign entry.fst = entry.fst

Every recorded entry of the default public factorization is fixed by normalizeFactorSign.