def HexBerlekampZassenhausMathlib.BHKS.liftedSubsetOfClass (d : Hex.LiftData) (members : List ℕ) : LiftedFactorSubset d

Proof-side lifted support selected by one canonical signature class.

Equations

• HexBerlekampZassenhausMathlib.BHKS.liftedSubsetOfClass d members = {i : HexBerlekampZassenhausMathlib.LiftedFactorIndex d | ↑i ∈ members}

@[simp]

theorem HexBerlekampZassenhausMathlib.BHKS.mem_liftedSubsetOfClass (d : Hex.LiftData) (members : List ℕ) (i : LiftedFactorIndex d) : i ∈ liftedSubsetOfClass d members ↔ ↑i ∈ members

Membership rule for liftedSubsetOfClass.

def HexBerlekampZassenhausMathlib.BHKS.selectedFactorsOfClass (liftedFactors : Array Hex.ZPoly) (members : List ℕ) : Array Hex.ZPoly

Executable selected-factor array for one canonical signature class.

Equations

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

theorem HexBerlekampZassenhausMathlib.BHKS.selectedFactorsOfClass_polyProduct (d : Hex.LiftData) (members : List ℕ) : (selectedFactorsOfClass d.liftedFactors members).polyProduct = liftedFactorProduct d (liftedSubsetOfClass d members)

Executable and proof-side selected products agree.

theorem HexBerlekampZassenhausMathlib.BHKS.liftedSubsetOfClass_mem {r : ℕ} (trueSupports : Set (Set (Fin r))) (hcover : ∀ (i : Fin r), ∃ S ∈ trueSupports, i ∈ S) (hdisjoint : ∀ S ∈ trueSupports, ∀ T ∈ trueSupports, ∀ i ∈ S, i ∈ T → S = T) (d : Hex.LiftData) (hr : d.liftedFactors.size = r) {members : List ℕ} (hmem : members ∈ supportPartitionByMinColumn trueSupports) : ↑(liftedSubsetOfClass d members) ∈ ⋯ ▸ trueSupports

A canonical signature class is the carrier of one member of a genuine support partition.

noncomputable def HexBerlekampZassenhausMathlib.BHKS.recoveredClassFactor (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (members : List ℕ) : Hex.ZPoly

The executable direct candidate attached to one signature class.

Equations

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

noncomputable def HexBerlekampZassenhausMathlib.BHKS.recoveredClassFactors (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) : Array Hex.ZPoly

Recovered factors in canonical signature-class order.

Equations

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

structure HexBerlekampZassenhausMathlib.BHKS.RecoveredClassCertificate (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (members : List ℕ) : Type

Certificate selected by one canonical signature class.

• support : ModPFactorSubset data

  The modular support represented by the signature class.

• certificate : DirectFactorCertificate core B data self.support

  The recovered irreducible factor and its direct-support proof.

• support_eq : directLiftedSupport core B data self.support = liftedSubsetOfClass (core.directLiftData B data) members

  The direct lifted support is exactly the selected signature class.

noncomputable def HexBerlekampZassenhausMathlib.BHKS.recoveredClassCertificate {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (hcover : ∀ (i : LiftedFactorIndex (core.directLiftData B data)), ∃ U ∈ directTrueSupports core B data, i ∈ U) (hdisjoint : ∀ U ∈ directTrueSupports core B data, ∀ V ∈ directTrueSupports core B data, ∀ i ∈ U, i ∈ V → U = V) {members : List ℕ} (hmem : members ∈ supportPartitionByMinColumn (directTrueSupports core B data)) : RecoveredClassCertificate core B data members

Select the unique direct factor certificate carried by a canonical class.

Equations

• HexBerlekampZassenhausMathlib.BHKS.recoveredClassCertificate hcover hdisjoint hmem = { support := Classical.choose ⋯, certificate := Classical.choice ⋯, support_eq := ⋯ }

theorem HexBerlekampZassenhausMathlib.BHKS.recoveredClassFactor_eq {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (hcover : ∀ (i : LiftedFactorIndex (core.directLiftData B data)), ∃ U ∈ directTrueSupports core B data, i ∈ U) (hdisjoint : ∀ U ∈ directTrueSupports core B data, ∀ V ∈ directTrueSupports core B data, ∀ i ∈ U, i ∈ V → U = V) {members : List ℕ} (hmem : members ∈ supportPartitionByMinColumn (directTrueSupports core B data)) : recoveredClassFactor core B data members = (recoveredClassCertificate hcover hdisjoint hmem).certificate.factor

The executable factor of a signature class is exactly the normalized irreducible factor in its direct certificate.

theorem HexBerlekampZassenhausMathlib.BHKS.recoveredClassFactors_polyProduct {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (hcore_ne : core ≠ 0) (_hcore_primitive : core.Primitive) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hpartition : DirectSupportPartition core B data Finset.univ core) (hcover : ∀ (i : LiftedFactorIndex (core.directLiftData B data)), ∃ U ∈ directTrueSupports core B data, i ∈ U) (hdisjoint : ∀ U ∈ directTrueSupports core B data, ∀ V ∈ directTrueSupports core B data, ∀ i ∈ U, i ∈ V → U = V) (hcard : (directTrueSupports core B data).ncard = (UniqueFactorizationMonoid.normalizedFactors (HexPolyZMathlib.toPolynomial core)).card) : (recoveredClassFactors core B data).polyProduct = core

Canonical recovered class factors multiply back to the primitive, positive-leading primitive square-free part.

theorem HexBerlekampZassenhausMathlib.BHKS.bhksIndicatorCandidates_eq_some_of_span_eq {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (hcore_primitive : core.Primitive) (hcover : ∀ (i : LiftedFactorIndex (core.directLiftData B data)), ∃ U ∈ directTrueSupports core B data, i ∈ U) (hdisjoint : ∀ U ∈ directTrueSupports core B data, ∀ V ∈ directTrueSupports core B data, ∀ i ∈ U, i ∈ V → U = V) (hrows : 1 ≤ (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors).factorCount + (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors).coeffWidth) (hspan : projectedRowSpanInt (Hex.bhksProjectedRows (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors) hrows) = trueSupportSpanInt (directTrueSupports core B data)) : Hex.bhksIndicatorCandidates? core (core.directLiftData B data) (Hex.bhksEquivalenceClassIndicators (Hex.bhksProjectedRows (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors) hrows)) = some (recoveredClassFactors core B data)

Exact projected span makes every executable signature-class candidate the factor in its direct certificate.

theorem HexBerlekampZassenhausMathlib.BHKS.projectedRows_isEmpty_eq_false_of_span_eq (L : Hex.BhksProjectedRows) (trueSupports : Set (Set (Fin L.factorCount))) (hspan : projectedRowSpanInt L = trueSupportSpanInt trueSupports) (hcover : ∀ (i : Fin L.factorCount), ∃ S ∈ trueSupports, i ∈ S) (hclasses : supportPartitionByMinColumn trueSupports ≠ []) : L.projectedRows.isEmpty = false

A nonempty genuine support partition cannot have exact projected span with an empty executable row array.

theorem HexBerlekampZassenhausMathlib.BHKS.bhksRecover_eq_some_of_span_eq {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (hcore_ne : core ≠ 0) (hcore_primitive : core.Primitive) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hpartition : DirectSupportPartition core B data Finset.univ core) (hcover : ∀ (i : LiftedFactorIndex (core.directLiftData B data)), ∃ U ∈ directTrueSupports core B data, i ∈ U) (hdisjoint : ∀ U ∈ directTrueSupports core B data, ∀ V ∈ directTrueSupports core B data, ∀ i ∈ U, i ∈ V → U = V) (hcard : (directTrueSupports core B data).ncard = (UniqueFactorizationMonoid.normalizedFactors (HexPolyZMathlib.toPolynomial core)).card) (hrows : 1 ≤ (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors).factorCount + (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors).coeffWidth) (hspan : projectedRowSpanInt (Hex.bhksProjectedRows (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors) hrows) = trueSupportSpanInt (directTrueSupports core B data)) (hclasses : 2 ≤ (supportPartitionByMinColumn (directTrueSupports core B data)).length) : Hex.bhksRecover? core (core.directLiftData B data) = some (recoveredClassFactors core B data)

With at least two true supports, exact span recovery passes every fixed-precision BHKS check.

theorem HexBerlekampZassenhausMathlib.BHKS.bhksSingleAllOnesPartition_eq_true_of_span_eq {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (hcover : ∀ (i : LiftedFactorIndex (core.directLiftData B data)), ∃ U ∈ directTrueSupports core B data, i ∈ U) (hdisjoint : ∀ U ∈ directTrueSupports core B data, ∀ V ∈ directTrueSupports core B data, ∀ i ∈ U, i ∈ V → U = V) (hrows : 1 ≤ (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors).factorCount + (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors).coeffWidth) (hspan : projectedRowSpanInt (Hex.bhksProjectedRows (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors) hrows) = trueSupportSpanInt (directTrueSupports core B data)) (hclasses : (supportPartitionByMinColumn (directTrueSupports core B data)).length = 1) : Hex.bhksSingleAllOnesPartition core (core.directLiftData B data) = true

With exactly one true support, exact span recovery yields the executable single-all-ones irreducibility certificate.