theorem Hex.subsetsOfSizeWithComplement_mem {α : Type} (l : List α) (d : Nat) (sc : List α × List α) : sc ∈ subsetsOfSizeWithComplement l d → (∀ (x : α), x ∈ sc.fst → x ∈ l) ∧ ∀ (x : α), x ∈ sc.snd → x ∈ l

Every selected and rejected entry emitted by the extensional combination specification comes from its input list.

structure Hex.DirectSplit (basis : LiftData) : Type

A dividing candidate and the exact unused support complement.

• selected : List (DirectLiftedIndex basis)

  The lifted factors used in the candidate product.

• remaining : List (DirectLiftedIndex basis)

  The exact complementary lifted factors.

• candidate : ZPoly

  The primitive normalized integer candidate.

• quotient : ZPoly

  The exact quotient of the current target by candidate.

inductive Hex.DirectLevelResult (basis : LiftData) : Type

Result of streaming one complete subset-cardinality level.

• found {basis : LiftData} (split : DirectSplit basis) (tried : Nat) : DirectLevelResult basis

  A candidate divides the target; tried records the work performed.

• exhausted {basis : LiftData} (tried : Nat) : DirectLevelResult basis

  Every candidate at this cardinality was tested without success.

def Hex.directSelectedFactors (basis : LiftData) (selected : List (DirectLiftedIndex basis)) : List ZPoly

Lifted polynomials selected by an indexed support list.

Equations

• Hex.directSelectedFactors basis selected = List.map (Hex.directLiftedFactor basis) selected

def Hex.directSelectedDegree (basis : LiftData) (selected : List (DirectLiftedIndex basis)) : Nat

Cached degree statistic evaluated before candidate construction.

Equations

• Hex.directSelectedDegree basis selected = List.foldl (fun (sum : Nat) (factor : Hex.ZPoly) => sum + Hex.DensePoly.natDegree factor) 0 (Hex.directSelectedFactors basis selected)

def Hex.directSelectedTrail (basis : LiftData) (selected : List (DirectLiftedIndex basis)) : Int

Cached trailing-coefficient residue evaluated before candidate construction.

Equations

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

def Hex.tryDirectSplit (coreLc : Int) (target : ZPoly) (basis : LiftData) (selected : List (DirectLiftedIndex basis)) : Option (ZPoly × ZPoly)

Evaluate one indexed direct split after its cheap cached statistics.

Equations

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

structure Hex.LiftSupport (basis : LiftData) : Type

The traversal data of one lifted basis.

Nothing here mentions a target: the lift modulus and the lifted factors are what a Hensel lift produced, so one of these is reusable for as long as the basis is, across every residual polynomial searched against it. The proposal traversal takes that reuse (peelDirect prepares one per peel run); the head-forced traversal still prepares one per cardinality level.

The lift modulus is basis.p ^ basis.k, which at recovery precision is wide enough to need several limbs, and rebuilding it at every traversal step is the dominant cost of a support that no candidate test ever sees. It is recorded prepared, in every representation the traversal reduces against: the residue update multiplies modulo its integer form and the trailing filter compares against its halfway threshold, so neither derives anything from the modulus at a leaf. The proof fields pin the arrays to the lifted factors elementwise and to their length, so a traversal reading this is interchangeable with one reading the factors directly.

• modulus : LiftModulus

  The lift modulus basis.p ^ basis.k, prepared for centred reduction.

• degrees : Array Nat

  Degree of each lifted factor, in basis order.

• trails : Array Int

  Trailing coefficient of each lifted factor, in basis order.

• modulus_eq : self.modulus = LiftModulus.ofNat (liftModulus basis)

  The recorded modulus is the prepared lift modulus.

• degrees_size : self.degrees.size = basis.liftedFactors.size

  There is one recorded degree per lifted factor.

• trails_size : self.trails.size = basis.liftedFactors.size

  There is one recorded trailing coefficient per lifted factor.

• degrees_eq (i : DirectLiftedIndex basis) : self.degrees.getD (↑i) 0 = DensePoly.natDegree (directLiftedFactor basis i)

  Each recorded degree is its lifted factor's degree.

• trails_eq (i : DirectLiftedIndex basis) : self.trails.getD (↑i) 0 = DensePoly.coeff (directLiftedFactor basis i) 0

  Each recorded trailing coefficient is its lifted factor's constant term.

def Hex.LiftSupport.degree {basis : LiftData} (lift : LiftSupport basis) (i : DirectLiftedIndex basis) : Nat

The recorded degree of a lifted factor.

Equations

• lift.degree i = lift.degrees.getD (↑i) 0

def Hex.LiftSupport.trail {basis : LiftData} (lift : LiftSupport basis) (i : DirectLiftedIndex basis) : Int

The recorded trailing coefficient of a lifted factor.

Equations

• lift.trail i = lift.trails.getD (↑i) 0

@[simp]

theorem Hex.LiftSupport.degree_spec {basis : LiftData} (lift : LiftSupport basis) (i : DirectLiftedIndex basis) : lift.degree i = DensePoly.natDegree (directLiftedFactor basis i)

A recorded degree is the degree of the lifted factor it indexes.

@[simp]

theorem Hex.LiftSupport.trail_spec {basis : LiftData} (lift : LiftSupport basis) (i : DirectLiftedIndex basis) : lift.trail i = DensePoly.coeff (directLiftedFactor basis i) 0

A recorded trailing coefficient is the constant term of the lifted factor it indexes.

@[simp]

theorem Hex.LiftSupport.modulus_spec {basis : LiftData} (lift : LiftSupport basis) : lift.modulus = LiftModulus.ofNat (liftModulus basis)

The recorded modulus is the prepared lift modulus.

theorem Hex.LiftSupport.modulusNat_spec {basis : LiftData} (lift : LiftSupport basis) : lift.modulus.nat = liftModulus basis

The recorded modulus records the lift modulus. Not @[simp]: simp already closes this via modulus_spec and LiftModulus.nat_ofNat.

theorem Hex.LiftSupport.modulusInt_spec {basis : LiftData} (lift : LiftSupport basis) : lift.modulus.int = ↑(liftModulus basis)

The recorded integer modulus is the lift modulus. Not @[simp]: simp already closes this via modulus_spec and LiftModulus.int_ofNat.

def Hex.liftSupport (basis : LiftData) : LiftSupport basis

Compute the traversal data of a lifted basis.

Equations

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

def Hex.directLeaf (coreLc : Int) (target : ZPoly) (cached : TargetImage target) (basis : LiftData) (modulus : LiftModulus) (head : DirectLiftedIndex basis) (xs selectedRev rejectedRev : List (DirectLiftedIndex basis)) (selectedDegree : Nat) (selectedTrail : Int) : DirectLevelResult basis

Evaluate one traversal leaf.

The degree and trailing-coefficient filters read only the incrementally maintained statistics, so a support they reject never reverses the selected indices, never maps them to lifted polynomials, and never builds a candidate. The complementary support is concatenated only after an exact divisor is found. The prefilter runs once: a surviving leaf continues with directCandidateAfterPrefilter rather than re-entering tryDirectCandidate.

Equations

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

theorem Hex.directLeaf_eq (coreLc : Int) (target : ZPoly) (cached : TargetImage target) (basis : LiftData) (modulus : LiftModulus) (head : DirectLiftedIndex basis) (xs selectedRev rejectedRev : List (DirectLiftedIndex basis)) (selectedDegree : Nat) (selectedTrail : Int) : directLeaf coreLc target cached basis modulus head xs selectedRev rejectedRev selectedDegree selectedTrail = match tryDirectCandidate coreLc target modulus (directSelectedFactors basis (head :: selectedRev.reverse)) selectedDegree selectedTrail with | some (candidate, quotient) => DirectLevelResult.found { selected := head :: selectedRev.reverse, remaining := rejectedRev.reverse ++ xs, candidate := candidate, quotient := quotient } 1 | none => DirectLevelResult.exhausted 1

The guarded leaf agrees with evaluating the candidate test directly. The prefilter is tryDirectCandidate's own first step, so guarding on it changes only when the arguments are built, and every field of the result -- including the tried count -- is unchanged.

def Hex.scanDirectCombinations (coreLc : Int) (target : ZPoly) (basis : LiftData) (lift : LiftSupport basis) (image : TargetImage target) (head : DirectLiftedIndex basis) (xs : List (DirectLiftedIndex basis)) (choose : Nat) (selectedRev rejectedRev : List (DirectLiftedIndex basis)) (selectedDegree : Nat) (selectedTrail : Int) : DirectLevelResult basis

Stream the choose-element subsets of xs. selectedRev and rejectedRev are prefixes already decided by the caller. Inclusion is visited before exclusion, matching the ordinary lexicographic combination order.

Equations

• One or more equations did not get rendered due to their size.
• Hex.scanDirectCombinations coreLc target basis lift image head x✝⁴ 0 x✝³ x✝² x✝¹ x✝ = Hex.directLeaf coreLc target image basis lift.modulus head x✝⁴ x✝³ x✝² x✝¹ x✝
• Hex.scanDirectCombinations coreLc target basis lift image head [] n.succ x✝³ x✝² x✝¹ x✝ = Hex.DirectLevelResult.exhausted 0

def Hex.scanDirectLevel (coreLc : Int) (target : ZPoly) (basis : LiftData) (head : DirectLiftedIndex basis) (tail : List (DirectLiftedIndex basis)) (tailCard : Nat) : DirectLevelResult basis

Stream one head-forced level.

Both prepared objects are built here, so a head search that runs several cardinalities rebuilds the whole lift support -- modulus, degree array and trail array -- and reduces the target again at each one. That is where the mixed object left them; giving them the lifetimes their dependencies describe, as the proposal traversal now has, means threading them through findDirectHead and searchDirectAux, which the classical completeness and correctness proofs quantify over.

Equations

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

structure Hex.DirectCandidateStats : Type

Stage counters for the unforced low-cardinality candidate sweep.

• leaves : Nat

  Combinatorial leaves visited.

• degreeSurvivors : Nat

  Leaves surviving the cached degree bound.

• trailingSurvivors : Nat

  Leaves also surviving the trailing-coefficient divisibility test.

• constructed : Nat

  Integer candidate polynomials constructed.

• recordable : Nat

  Constructed candidates passing the nonunit recording filter.

• exactDivisions : Nat

  Candidates sent to exact polynomial division.

def Hex.instDecidableEqDirectCandidateStats.decEq (x✝ x✝¹ : DirectCandidateStats) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hex.instDecidableEqDirectCandidateStats : DecidableEq DirectCandidateStats

Equations

• Hex.instDecidableEqDirectCandidateStats = Hex.instDecidableEqDirectCandidateStats.decEq

def Hex.DirectCandidateStats.add (left right : DirectCandidateStats) : DirectCandidateStats

Add candidate-stage counters componentwise.

Equations

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

inductive Hex.DirectSubsetLevelResult (basis : LiftData) : Type

Result of one instrumented unforced subset-cardinality level.

• found {basis : LiftData} (split : DirectSplit basis) (stats : DirectCandidateStats) : DirectSubsetLevelResult basis

  A candidate divides the target.

• exhausted {basis : LiftData} (stats : DirectCandidateStats) : DirectSubsetLevelResult basis

  Every candidate at this cardinality was rejected.

def Hex.scanDirectSubsets (coreLc : Int) (target : ZPoly) (basis : LiftData) (lift : LiftSupport basis) (image : TargetImage target) (xs : List (DirectLiftedIndex basis)) (choose : Nat) (selectedRev rejectedRev : List (DirectLiftedIndex basis)) (selectedDegree : Nat) (selectedTrail : Int) : DirectSubsetLevelResult basis

Stream the choose-element subsets of the complete lifted support.

Unlike scanDirectCombinations, no distinguished factor is forced into every candidate. This is the low-cardinality iterator: it visits each subset once, retains the exact complementary support, and never materializes the family of subsets.

Equations

• One or more equations did not get rendered due to their size.
• Hex.scanDirectSubsets coreLc target basis lift image [] n.succ x✝³ x✝² x✝¹ x✝ = Hex.DirectSubsetLevelResult.exhausted { }

def Hex.scanDirectSubsetLevel (coreLc : Int) (target : ZPoly) (basis : LiftData) (lift : LiftSupport basis) (image : TargetImage target) (support : List (DirectLiftedIndex basis)) (cardinality : Nat) : DirectSubsetLevelResult basis

Stream one unforced subset-cardinality level.

Both prepared objects are supplied by the caller: the lift data is constant for the peel run, and the target image belongs to the residual whose cardinality schedule this level is one step of.

Equations

• Hex.scanDirectSubsetLevel coreLc target basis lift image support cardinality = Hex.scanDirectSubsets coreLc target basis lift image support cardinality [] [] 0 1