theorem HexBerlekampZassenhausMathlib.subsetsOfSizeWithComplement_structure {α : Type} [DecidableEq α] (xs selected remaining : List α) (choose : ℕ) : xs.Nodup → (selected, remaining) ∈ Hex.subsetsOfSizeWithComplement xs choose → selected.Nodup ∧ remaining.Nodup ∧ Disjoint selected.toFinset remaining.toFinset ∧ selected.toFinset ∪ remaining.toFinset = xs.toFinset ∧ selected.length = choose

Structural facts for a size-indexed selected/rejected partition.

theorem HexBerlekampZassenhausMathlib.filter_split_mem_subsetsOfSizeWithComplement {α : Type} (P : α → Bool) (xs : List α) : (List.filter P xs, List.filter (fun (x : α) => !P x) xs) ∈ Hex.subsetsOfSizeWithComplement xs (List.filter P xs).length

Filtering a list by a predicate produces the corresponding member of the size-indexed selected/rejected enumerator.

theorem HexBerlekampZassenhausMathlib.scanDirectCombinations_found (coreLc : ℤ) (target : Hex.ZPoly) (basis : Hex.LiftData) (lift : Hex.LiftSupport basis) (image : Hex.TargetImage target) (head : Hex.DirectLiftedIndex basis) (xs : List (Hex.DirectLiftedIndex basis)) (choose : ℕ) (selectedRev rejectedRev : List (Hex.DirectLiftedIndex basis)) (selectedDegree : ℕ) (selectedTrail : ℤ) (split : Hex.DirectSplit basis) (tried : ℕ) : selectedDegree = Hex.directSelectedDegree basis (head :: selectedRev.reverse) → selectedTrail = Hex.directSelectedTrail basis (head :: selectedRev.reverse) → Hex.scanDirectCombinations coreLc target basis lift image head xs choose selectedRev rejectedRev selectedDegree selectedTrail = Hex.DirectLevelResult.found split tried → ∃ (selected : List (Hex.DirectLiftedIndex basis)) (remaining : List (Hex.DirectLiftedIndex basis)), (selected, remaining) ∈ Hex.subsetsOfSizeWithComplement xs choose ∧ split.selected = head :: (selectedRev.reverse ++ selected) ∧ split.remaining = rejectedRev.reverse ++ remaining ∧ Hex.tryDirectSplit coreLc target basis split.selected = some (split.candidate, split.quotient)

A successful leaf exposes its exact indexed split and candidate check.

theorem HexBerlekampZassenhausMathlib.scanDirectCombinations_finds (coreLc : ℤ) (target : Hex.ZPoly) (basis : Hex.LiftData) (lift : Hex.LiftSupport basis) (image : Hex.TargetImage target) (head : Hex.DirectLiftedIndex basis) (xs : List (Hex.DirectLiftedIndex basis)) (choose : ℕ) (selectedRev rejectedRev : List (Hex.DirectLiftedIndex basis)) (selectedDegree : ℕ) (selectedTrail : ℤ) (selected remaining : List (Hex.DirectLiftedIndex basis)) (candidate quotient : Hex.ZPoly) : selectedDegree = Hex.directSelectedDegree basis (head :: selectedRev.reverse) → selectedTrail = Hex.directSelectedTrail basis (head :: selectedRev.reverse) → (selected, remaining) ∈ Hex.subsetsOfSizeWithComplement xs choose → Hex.tryDirectSplit coreLc target basis (head :: (selectedRev.reverse ++ selected)) = some (candidate, quotient) → ∃ (split : Hex.DirectSplit basis) (tried : ℕ), Hex.scanDirectCombinations coreLc target basis lift image head xs choose selectedRev rejectedRev selectedDegree selectedTrail = Hex.DirectLevelResult.found split tried

Every extensionally specified working split is reached by the streaming iterator (possibly after an earlier working split).

theorem HexBerlekampZassenhausMathlib.tryDirectSplit_some {coreLc : ℤ} {target : Hex.ZPoly} {basis : Hex.LiftData} {selected : List (Hex.DirectLiftedIndex basis)} {candidate quotient : Hex.ZPoly} (h : Hex.tryDirectSplit coreLc target basis selected = some (candidate, quotient)) : candidate = Hex.directCandidate coreLc (Hex.liftModulus basis) (Hex.directSelectedFactors basis selected) ∧ quotient * candidate = target

Successful exact quotient and candidate identities at a checked leaf.