def HexBerlekampZassenhausMathlib.liftedSubsetMask (d : Hex.LiftData) (S : LiftedFactorSubset d) : List Bool

Boolean indicator vector for S, indexed by the same Fin order as d.liftedFactors.toList.

Equations

• HexBerlekampZassenhausMathlib.liftedSubsetMask d S = List.map (fun (i : HexBerlekampZassenhausMathlib.LiftedFactorIndex d) => decide (i ∈ S)) (List.finRange d.liftedFactors.size)

theorem HexBerlekampZassenhausMathlib.liftedSubsetMask_length (d : Hex.LiftData) (S : LiftedFactorSubset d) : (liftedSubsetMask d S).length = d.liftedFactors.toList.length

The mask has one entry per lifted factor.

def HexBerlekampZassenhausMathlib.liftedSubsetSelectedList (d : Hex.LiftData) (S : LiftedFactorSubset d) : List Hex.ZPoly

The list of lifted factors selected by S, ordered by their original d.liftedFactors index.

Equations

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

def HexBerlekampZassenhausMathlib.liftedSubsetRejectedList (d : Hex.LiftData) (S : LiftedFactorSubset d) : List Hex.ZPoly

The list of lifted factors not selected by S, ordered by their original d.liftedFactors index.

Equations

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

theorem HexBerlekampZassenhausMathlib.subsetSplits_mem_exists_mask {xs selected rest : List Hex.ZPoly} : (selected, rest) ∈ Hex.subsetSplits xs → ∃ (mask : List Bool), mask.length = xs.length ∧ selected = List.filterMap (fun (p : Hex.ZPoly × Bool) => if p.2 = true then some p.1 else none) (xs.zip mask) ∧ rest = List.filterMap (fun (p : Hex.ZPoly × Bool) => if p.2 = true then none else some p.1) (xs.zip mask)

Converse to subsetSplits_zip_filterMap_partition: every executable subsetSplits member is induced by a Boolean mask over the input list.

theorem HexBerlekampZassenhausMathlib.subsetSplitsWithFirst_mem_exists_tail_mask {x : Hex.ZPoly} {xs selected rest : List Hex.ZPoly} (h : (selected, rest) ∈ Hex.subsetSplitsWithFirst (x :: xs)) : ∃ (mask : List Bool), mask.length = xs.length ∧ selected = x :: List.filterMap (fun (p : Hex.ZPoly × Bool) => if p.2 = true then some p.1 else none) (xs.zip mask) ∧ rest = List.filterMap (fun (p : Hex.ZPoly × Bool) => if p.2 = true then none else some p.1) (xs.zip mask)

Converse at the subsetSplitsWithFirst surface: every split comes from a Boolean mask over the tail, with the head forced into the selected side.

def HexBerlekampZassenhausMathlib.LiftedFactorListMatches (d : Hex.LiftData) (J : LiftedFactorSubset d) (localFactors : List Hex.ZPoly) : Prop

Predicate capturing that localFactors is the order-preserving list of lifted factors at the indices in J. This is the invariant preserved by the recursive recombination search: at every level the executable's running localFactors is exactly the list of lifted factors at the remaining unconsumed indices.

Used by the recursive coverage proof to connect the proof-side HenselSubsetCorrespondenceRest core d J target to the executable list threaded through Hex.recombinationSearchModAux.

Equations

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

theorem HexBerlekampZassenhausMathlib.LiftedFactorListMatches.univ (d : Hex.LiftData) : LiftedFactorListMatches d Finset.univ d.liftedFactors.toList

Initial-state instance: the full lifted-factor list matches the universe of indices. This pairs with henselSubsetCorrespondenceRest_initial at the start of the recursive coverage induction.

theorem HexBerlekampZassenhausMathlib.LiftedFactorListMatches.nodup_of_injOn {d : Hex.LiftData} {J : LiftedFactorSubset d} {localFactors : List Hex.ZPoly} (h : LiftedFactorListMatches d J localFactors) (hinj : Set.InjOn (liftedFactor d) ↑J) : localFactors.Nodup

A matched localFactors is Nodup whenever liftedFactor d is injective on the index set J.

Discharges the hlocal_nodup hypothesis of liftedSubsetSplit_prefix_exists_mem_sdiff_of_matches and liftedFactorSubsetPartition_prefix_none. The Set.InjOn premise is a Hensel-coprimality fact about the local factors of d: distinct lifted factors are pairwise coprime, so when monic they are not equal as polynomials. Producing the injectivity witness from partition data (or directly from henselLiftData invariants) is the caller's responsibility and this theorem covers only the pure list-level step.

theorem HexBerlekampZassenhausMathlib.liftedSubsetRejectedList_eq_liftedSubsetSelectedList_sdiff (d : Hex.LiftData) (S : LiftedFactorSubset d) : liftedSubsetRejectedList d S = liftedSubsetSelectedList d (Finset.univ \ S)

The rejected list of a subset S is exactly the selected list of the complementary universe minus S. This is the executable-side identity that matches liftedSubsetRejectedList d S to Finset.univ \ S.

theorem HexBerlekampZassenhausMathlib.LiftedFactorListMatches.head?_eq_liftedFactor_min' {d : Hex.LiftData} {J : LiftedFactorSubset d} {localFactors : List Hex.ZPoly} (h : LiftedFactorListMatches d J localFactors) (hne : Finset.Nonempty J) : localFactors.head? = some (liftedFactor d (Finset.min' J hne))

Head identification for a non-empty matching state: the head of localFactors is the lifted factor at J.min'. Used by the recursive coverage proof to connect the proof-side "first remaining index of J" to the executable-side head of localFactors.

theorem HexBerlekampZassenhausMathlib.liftedSubsetSplit_mem_subsetSplitsWithFirst_of_matches {d : Hex.LiftData} {J : LiftedFactorSubset d} {localFactors : List Hex.ZPoly} (h : LiftedFactorListMatches d J localFactors) {S : LiftedFactorSubset d} (hSJ : S ⊆ J) (hne : Finset.Nonempty J) (hmin : Finset.min' J hne ∈ S) : (liftedSubsetSelectedList d S, liftedSubsetSelectedList d (J \ S)) ∈ Hex.subsetSplitsWithFirst localFactors

Generalised partition lemma at the subsetSplitsWithFirst surface: for any matching state and any S ⊆ J containing J.min', the order-preserving (selected, rest) partition of localFactors by S lies in subsetSplitsWithFirst localFactors.

The selected component is liftedSubsetSelectedList d S (since S ⊆ J) and the rest component is liftedSubsetSelectedList d (J \ S).

theorem HexBerlekampZassenhausMathlib.liftedSubsetSelectedList_eq_mask_partition_of_matches {d : Hex.LiftData} {J : LiftedFactorSubset d} {localFactors : List Hex.ZPoly} (hmatches : LiftedFactorListMatches d J localFactors) (hne : Finset.Nonempty J) {head : Hex.ZPoly} {tail : List Hex.ZPoly} (hloc : localFactors = head :: tail) (mask : List Bool) (hmask_len : mask.length = tail.length) : ∃ T ⊆ J, Finset.min' J hne ∈ T ∧ liftedSubsetSelectedList d T = head :: List.filterMap (fun (p : Hex.ZPoly × Bool) => if p.2 = true then some p.1 else none) (tail.zip mask) ∧ liftedSubsetSelectedList d (J \ T) = List.filterMap (fun (p : Hex.ZPoly × Bool) => if p.2 = true then none else some p.1) (tail.zip mask)

Mask-to-subset lemma: given a Boolean mask of matching length over the tail of a matched localFactors list, there is a LiftedFactorSubset d (containing J.min' and contained in J) whose (selected, rest) list partition equals the matched-list mask partition. The natural converse of liftedSubsetSplit_mem_subsetSplitsWithFirst_of_matches, used to recover a proof-side lifted-factor subset from an arbitrary executable split.

theorem HexBerlekampZassenhausMathlib.liftedSubsetSplit_prefix_mem_of_matches {d : Hex.LiftData} {J S : LiftedFactorSubset d} {localFactors : List Hex.ZPoly} {pre suffix : List (List Hex.ZPoly × List Hex.ZPoly)} (hmatches : LiftedFactorListMatches d J localFactors) (hne : Finset.Nonempty J) (hsplits : Hex.subsetSplitsWithFirst localFactors = pre ++ (liftedSubsetSelectedList d S, liftedSubsetSelectedList d (J \ S)) :: suffix) {split : List Hex.ZPoly × List Hex.ZPoly} (hsplit : split ∈ pre) : ∃ T ⊆ J, Finset.min' J hne ∈ T ∧ split = (liftedSubsetSelectedList d T, liftedSubsetSelectedList d (J \ T))

Prefix characterization at the matched-state subsetSplitsWithFirst surface: given an arbitrary executable split split ∈ pre appearing before a chosen matched S-split in Hex.subsetSplitsWithFirst localFactors, there is a proof-side lifted-factor subset T ⊆ J containing J.min' whose order-preserving (selected, rest) partition equals split.

Combines the executable-enumeration mask converse subsetSplitsWithFirst_mem_exists_tail_mask with the mask-to-subset lemma liftedSubsetSelectedList_eq_mask_partition_of_matches. Used by the prefix-none discharge in the recursive coverage proof.

The conclusion is independent of the S-side shape constraints (S ⊆ J and J.min' hne ∈ S) that the caller typically has in scope: the prefix characterization is a structural property of the executable enumeration. The caller call site keeps those hypotheses for the suffix (S, J \ S) entry itself, but does not need to thread them through this lemma.

theorem HexBerlekampZassenhausMathlib.liftedSubsetSplit_prefix_exists_mem_sdiff_of_matches {d : Hex.LiftData} {J S : LiftedFactorSubset d} {localFactors : List Hex.ZPoly} {pre suffix : List (List Hex.ZPoly × List Hex.ZPoly)} (hlocal_nodup : localFactors.Nodup) (hmatches : LiftedFactorListMatches d J localFactors) (hSJ : S ⊆ J) (hne : Finset.Nonempty J) (hmin : Finset.min' J hne ∈ S) (hsplits : Hex.subsetSplitsWithFirst localFactors = pre ++ (liftedSubsetSelectedList d S, liftedSubsetSelectedList d (J \ S)) :: suffix) {split : List Hex.ZPoly × List Hex.ZPoly} (hsplit : split ∈ pre) : ∃ T ⊆ J, Finset.min' J hne ∈ T ∧ split = (liftedSubsetSelectedList d T, liftedSubsetSelectedList d (J \ T)) ∧ ∃ i ∈ J, i ∈ S ∧ i ∉ T

Strengthening of liftedSubsetSplit_prefix_mem_of_matches: when the matched localFactors is Nodup and the boundary split is the canonical (S, J \ S) partition, every prefix split ∈ pre admits a witness index i ∈ J ∩ S that is not in the recovered subset T.

The Nodup hypothesis is required to lift the executable mask-level bit difference (provided by subsetSplits_prefix_exists_bit_diff_aux) back to a proof-side LiftedFactorIndex d difference, since liftedFactor d is otherwise allowed to collide on distinct indices. Callers thread this hypothesis from a Hensel-coprimality fact at the recombination call site (liftedFactor d injective on the J-filter index list).

Used by the recursive coverage assembler for the prefix-none case: an arbitrary executable split appearing before the S-split must miss at least one of the S-indices, witnessing recombination-search progress.

theorem HexBerlekampZassenhausMathlib.polyProduct_liftedSubsetSelectedList_eq_liftedFactorProduct (d : Hex.LiftData) (S : LiftedFactorSubset d) : (liftedSubsetSelectedList d S).toArray.polyProduct = liftedFactorProduct d S

The transported recombination candidate product equals the proof-side lifted-factor product: both factor lists are permutations of each other in Polynomial ℤ, so commutativity collapses the order difference.