structure Hex.DirectPrimeProbe (core : SquareFreeInput) : Type

One good-prime factorization computed while planning. The candidate is retained with its result so proof provenance and diagnostics never need to recover it by searching the candidate table.

• candidate : SmallPrimeCandidate

  The candidate prime and its primality witness.

• data : PrimeChoiceData

  The modular image and its factorization.

• factorDegrees : Array Nat

  Degrees of the cached modular factors.

• reachableDegrees : Array Bool

  Subset-degree reachability bitset, indexed from zero through degree core. This is computed once with the modular factorization and is reused by planning and optional degree-obstruction checks.

structure Hex.DirectPrimePlan (core : SquareFreeInput) : Type

Cached direct-coordinate modular plan. Every successful trial performed by the planner is retained. The selected trial is stored separately from the other successful trials, so it is structurally impossible for the choice to refer to an uncached factorization.

• selected : DirectPrimeProbe core

  The successful trial chosen for Hensel lifting and recombination.

• otherProbes : Array (DirectPrimeProbe core)

  Other successful trials retained for degree-obstruction certificates.

def Hex.DirectPrimePlan.ofSelection {core : SquareFreeInput} (selected : DirectPrimeProbe core) (otherProbes : Array (DirectPrimeProbe core)) : DirectPrimePlan core

Build a plan from its selected successful trial and all other successful trials. This is the only constructor exposed outside this module.

Equations

• Hex.DirectPrimePlan.ofSelection selected otherProbes = { selected := selected, otherProbes := otherProbes }

def Hex.DirectPrimePlan.probes {core : SquareFreeInput} (plan : DirectPrimePlan core) : Array (DirectPrimeProbe core)

All cached successful trials, with the selected value first.

Equations

• plan.probes = #[plan.selected] ++ plan.otherProbes

def Hex.DirectPrimePlan.data {core : SquareFreeInput} (plan : DirectPrimePlan core) : PrimeChoiceData

Selected modular factorization.

Equations

• plan.data = plan.selected.data

def Hex.DirectPrimePlan.prime {core : SquareFreeInput} (plan : DirectPrimePlan core) : Nat

Selected prime.

Equations

• plan.prime = plan.data.p

def Hex.DirectPrimePlan.width {core : SquareFreeInput} (plan : DirectPrimePlan core) : Nat

Number of local factors at the selected prime.

Equations

• plan.width = plan.data.factorsModP.size

def Hex.directFactorDegrees (data : PrimeChoiceData) : Array Nat

Degree list retained beside a direct modular factorization.

Equations

• Hex.directFactorDegrees data = Array.map (fun (g : Hex.FpPoly data.p) => Hex.DensePoly.natDegree g) data.factorsModP

def Hex.directDegreeBitsStep (maxDegree : Nat) (reachable : Array Bool) (degree : Nat) : Array Bool

One subset-sum DP step. The returned Boolean array records whether each degree at most maxDegree can be formed after admitting degree.

Equations

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

def Hex.directDegreeBits (maxDegree : Nat) (degrees : Array Nat) : Array Bool

Predictable O(number of factors × degree) subset-degree bitset.

Unlike the former recursive degree-subset enumeration, this has no width cap. Index i is true exactly when the planner has found a modular-factor subset whose degrees sum to i; the Mathlib side supplies the semantic theorem.

Equations

• Hex.directDegreeBits maxDegree degrees = Array.foldl (Hex.directDegreeBitsStep maxDegree) (#[true] ++ Array.replicate maxDegree false) degrees

def Hex.DirectPrimeProbe.ofData (core : SquareFreeInput) (candidate : SmallPrimeCandidate) (data : PrimeChoiceData) : DirectPrimeProbe core

Build the indexed cached trial and its degree DP in one place.

Equations

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

def Hex.reachableProperCount (reachable : Array Bool) : Nat

Number of proper degrees a subset-degree bitset still admits.

Equations

• Hex.reachableProperCount reachable = List.count true (List.drop 1 reachable.toList).dropLast

def Hex.directReachableProperCount {core : SquareFreeInput} (probe : DirectPrimeProbe core) : Nat

Number of proper degrees still possible at a modular trial. Fewer reachable degrees means more cheap degree rejections during recombination.

Equations

• Hex.directReachableProperCount probe = Hex.reachableProperCount probe.reachableDegrees

def Hex.directSubsetCost (factorCount : Nat) : Nat

Candidate count of a complete head-forced subset search.

Equations

• Hex.directSubsetCost factorCount = if factorCount = 0 then 0 else 2 ^ (factorCount - 1)

def Hex.directDegreeScore (core : SquareFreeInput) (p : Nat) (degrees : Array Nat) : Nat × Nat × Nat × Nat

Lexicographic downstream score of a modular factorization known only by its prime and its factor degrees: complete subset work first, then degree-obstruction opportunities, lift precision, and prime as a stable tie breaker. Width is already reflected exponentially by directSubsetCost.

Every key is a function of the degree multiset and the prime, so a scouted degree pattern scores exactly as the factorization it predicts would.

Equations

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

def Hex.directProbeScore (core : SquareFreeInput) (probe : DirectPrimeProbe core) : Nat × Nat × Nat × Nat

Score of a computed modular factorization.

Equations

• Hex.directProbeScore core probe = Hex.directDegreeScore core probe.data.p probe.factorDegrees

def Hex.scoreBetter (a b : Nat × Nat × Nat × Nat) : Bool

Strict lexicographic order on downstream scores; true when b is the cheaper plan.

Equations

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

def Hex.scoutFuel : Nat

Hard bound on the good primes a plan scouts, so the walk terminates in a fixed number of modular observations however cheap the next one looks. A scout costs one Frobenius power and one gcd per separated factor degree, and is abandoned as soon as the factors it has separated show the candidate cannot win, so the walk's whole modular budget is one full split, at most scoutFuel bounded scouts, and one further full split for the scouted winner. Bad primes do not spend the allowance: they never reach a scout.

Which of those scouts are actually performed is decided by scoutPays, not by this bound.

Equations

• Hex.scoutFuel = 2

def Hex.liftWords (core : SquareFreeInput) (p : Nat) : Nat

Machine words in the Hensel lift modulus a plan at p needs. A recombination candidate's product and trial division run over integers of this width, so this is the part of a candidate's cost that the prime, rather than the input, decides.

The modulus is formed rather than estimated from precision * bitLen p, which overshoots by up to one bit per power and so crosses word boundaries the real modulus does not.

Equations

• Hex.liftWords core p = max 1 ((Hex.ZPoly.bitLen (p ^ Hex.precisionForCoeffBound core.poly.defaultFactorCoeffBound p) + 63) / 64)

def Hex.scoutRoundCost : Nat

Cost of one bounded-scout word operation, in recombination word operations.

A scout round works modulo a word-sized prime with a polynomial division in its inner loop; a recombination candidate multiplies and divides multiword integers in a tighter loop. Over the recorded per-candidate prices the scout's word operation runs about ten times the recombination one.

Equations

• Hex.scoutRoundCost = 10

def Hex.splitColumnCost : Nat

Cost of one Berlekamp-split word operation, in recombination word operations. The fixed-space matrix and its row reduction are the tightest modular loop the planner runs, about half a scout round's.

Equations

• Hex.splitColumnCost = 5

structure Hex.ScoutIncumbent : Type

The plan a scouting walk is trying to beat: its prime, the degrees of its modular factors, and its downstream score. Width and largest factor degree are read off the degrees, so this carries everything both the comparison and the pricing need and nothing else.

• prime : Nat

  The prime the incumbent plan uses.

• degrees : Array Nat

  Degrees of the incumbent plan's modular factors.

• score : Nat × Nat × Nat × Nat

  The incumbent plan's lexicographic downstream score.

def Hex.ScoutIncumbent.maxDegree (inc : ScoutIncumbent) : Nat

Largest modular factor degree of the incumbent plan. A bounded scout stops at the largest factor degree of the image it separates, so this stands in for the round count a scout of the next candidate would run. A proxy, not a bound: a narrower candidate tends to have larger factor degrees, and the walk has not seen them.

Equations

• inc.maxDegree = Array.foldl max 0 inc.degrees

def Hex.ScoutIncumbent.candidatesLeft (inc : ScoutIncumbent) : Nat

Recombination candidates the incumbent plan may still have to visit: the complete head-forced count, capped where the direct engine abandons the search.

Equations

• inc.candidatesLeft = min (Hex.directSubsetCost inc.degrees.size) Hex.defaultSubsetBudget

def Hex.scoutPays (core : SquareFreeInput) (inc : ScoutIncumbent) (q fuel : Nat) : Bool

Whether the walk can still afford one more modular observation: the recombination work the incumbent plan may have left, against the scouts and split the rest of the walk may spend.

This is the walk's only stopping decision. It governs the first good prime and every scouted candidate alike, and it depends on nothing but the degree of the input, the primes involved, and the degree patterns already observed.

Both sides are worst cases, so passing means the remaining walk could pay for itself, not that it will.

Equations

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

structure Hex.PrimeDegreePattern : Type

A candidate prime together with the modular degree pattern a scout established for it. This carries no factorization: the degrees are a prediction, and the plan splits the winner to obtain the factors.

• candidate : SmallPrimeCandidate

  The candidate prime and its primality witness.

• degrees : Array Nat

  Degrees of the irreducible factors of the modular image.

def Hex.probeDegreePattern? (f : ZPoly) (c : SmallPrimeCandidate) (target : Nat) : Option Berlekamp.DegreePattern

Scout one candidate's modular degree pattern, without splitting it.

none when the candidate is not a good prime -- the only case a scout declines. A complete pattern records the candidate's exact factor degrees; an incomplete one records that the candidate has more than target local factors, which is all a wider candidate needs to be discarded.

Equations

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

def Hex.scoutBetterPattern (core : SquareFreeInput) : Nat → List SmallPrimeCandidate → ScoutIncumbent → Option PrimeDegreePattern → Option PrimeDegreePattern

Scout further good primes for a cheaper plan than the incumbent's.

Nothing is split here. The walk stops as soon as scoutPays says the incumbent has too little recombination work left to repay another observation. Otherwise a candidate is discarded as soon as its separated factors reach the incumbent's width, since a wider image can only score worse; and a candidate whose pattern completes is scored exactly as the factorization it predicts would be, and becomes the incumbent if it wins -- which both tightens the target width and reprices the next observation against the plan now held.

Returns the best scouted pattern strictly cheaper than the incumbent's score, if any.

Equations

• One or more equations did not get rendered due to their size.
• Hex.scoutBetterPattern core 0 x✝² x✝¹ x✝ = x✝
• Hex.scoutBetterPattern core x✝² [] x✝¹ x✝ = x✝

def Hex.planOfScout (core : SquareFreeInput) (first : DirectPrimeProbe core) : Option PrimeDegreePattern → DirectPrimePlan core

Split the scouted winner and keep the plan it improves on.

The scout predicted this candidate's factor degrees but computed no factors, so the plan takes them from the Berlekamp split here. If that split declines -- which a good prime does not -- the first probe stands.

Equations

• One or more equations did not get rendered due to their size.
• Hex.planOfScout core first none = Hex.DirectPrimePlan.ofSelection first #[]

def Hex.firstDirectPlan? (core : SquareFreeInput) : List SmallPrimeCandidate → Option (DirectPrimePlan core)

Select the first good prime, then let the walk price further observations against the recombination work that plan has left.

Equations

• One or more equations did not get rendered due to their size.
• Hex.firstDirectPlan? core [] = none

def Hex.directPrimePlan? (core : SquareFreeInput) : Option (DirectPrimePlan core)

Plan and cache a good direct-coordinate modular factorization.

Equations

• Hex.directPrimePlan? core = Hex.firstDirectPlan? core (Hex.smallPrimeCandidates ++ Hex.extendedSmallPrimeCandidates)

def Hex.DirectPrimeProbe.Trial {core : SquareFreeInput} (probe : DirectPrimeProbe core) : Prop

A probe is its own good-prime trial: the recorded factorization is what the explicit trial at its candidate returned, and every derived field -- the factor degrees and the subset-degree bitset -- was computed from that factorization by DirectPrimeProbe.ofData.

The planner retains probes it did not select, and a consumer that reads their degree data needs both halves: without the first it does not know the factorization is a factorization of this input at all, and without the second the cached Booleans are unrelated to the recorded degrees.

Equations

• probe.Trial = (Hex.probePrimeData? core.poly probe.candidate = some probe.data ∧ probe = Hex.DirectPrimeProbe.ofData core probe.candidate probe.data)

theorem Hex.DirectPrimeProbe.trial_ofData {core : SquareFreeInput} {candidate : SmallPrimeCandidate} {data : PrimeChoiceData} (h : probePrimeData? core.poly candidate = some data) : (ofData core candidate data).Trial

A trial built by ofData from a successful explicit trial is one.

theorem Hex.directPrimePlan?_selected_spec (core : SquareFreeInput) (plan : DirectPrimePlan core) (h : directPrimePlan? core = some plan) : probePrimeData? core.poly plan.selected.candidate = some plan.selected.data

The selected cached value is exactly the result of its retained explicit prime trial.

theorem Hex.directPrimePlan?_probes_trial (core : SquareFreeInput) (plan : DirectPrimePlan core) (h : directPrimePlan? core = some plan) (probe : DirectPrimeProbe core) : probe ∈ plan.probes → probe.Trial

Every retained cached trial -- the selected one and each other successful trial the planner kept -- is exactly the result of its own explicit good-prime trial, with its degree data computed from that result.

theorem Hex.DirectPrimePlan.selected_mem_probes {core : SquareFreeInput} (plan : DirectPrimePlan core) : plan.selected ∈ plan.probes

The selected trial is one of the retained trials.

theorem Hex.directPrimePlan?_probes_p_le_500 (core : SquareFreeInput) (plan : DirectPrimePlan core) (h : directPrimePlan? core = some plan) (probe : DirectPrimeProbe core) : probe ∈ plan.probes → probe.data.p ≤ 500

Every retained cached trial uses a prime from the fixed [3, 500] hot-path candidate list.

theorem Hex.directPrimePlan?_selected_p_le_500 (core : SquareFreeInput) (plan : DirectPrimePlan core) (h : directPrimePlan? core = some plan) : plan.prime ≤ 500

The direct planner selects only from the fixed [3, 500] hot-path candidate list.