theorem HexBerlekampZassenhausMathlib.directDegreeBits_getElem?_iff (maxDegree : ℕ) (degrees : Array ℕ) (i : ℕ) (hi : i ≤ maxDegree) : (Hex.directDegreeBits maxDegree degrees)[i]?.getD false = true ↔ ∃ S ≤ ↑degrees.toList, S.sum = i

Hex.directDegreeBits means what its name says: index i is true exactly when some sub-multiset of the recorded degrees sums to i.

The bound i ≤ maxDegree is the array's own range; outside it the fold records nothing, and no degree of a divisor of a degree-maxDegree polynomial lands there.

theorem HexBerlekampZassenhausMathlib.exists_subMultiset_directFactorDegrees_of_dvd {core : Hex.ZPoly} {data : Hex.PrimeChoiceData} (hval : ModPFactorization core data) {c : Hex.ZPoly} (hdvd : c ∣ core) : ∃ S ≤ ↑(Hex.directFactorDegrees data).toList, S.sum = Hex.DensePoly.natDegree c

Reduction at a good prime sends an integer divisor of the input to a subproduct of that prime's modular irreducible factors and preserves its degree, so the divisor's degree is one of the subset sums of the recorded modular factor degrees.

This is the whole content of a degree filter that consults a prime other than the one recombination enumerates: a support whose degree is not such a subset sum cannot be the support of a genuine integer factor.

theorem HexBerlekampZassenhausMathlib.reachableDegrees_of_dvd {core : Hex.SquareFreeInput} {probe : Hex.DirectPrimeProbe core} (hrec : probe = Hex.DirectPrimeProbe.ofData core probe.candidate probe.data) (hval : ModPFactorization core.poly probe.data) {c : Hex.ZPoly} (hdvd : c ∣ core.poly) : probe.reachableDegrees[Hex.DensePoly.natDegree c]?.getD false = true

No false rejection. A probe that is its own good-prime trial marks the degree of every genuine integer divisor of the input as reachable, so a traversal that discards a support whose degree is not marked discards no genuine factor.

structure HexBerlekampZassenhausMathlib.DirectPrimeFacts (core : Hex.ZPoly) (data : Hex.PrimeChoiceData) : Prop

The complete proof-facing contract of a direct prime probe. Consumers need the semantic factorization, the cached Berlekamp form for the singleton certificate, and the small-prime bound used by the CLD resultant estimate.

• factorization : ModPFactorization core data

  The cached modular factorization is mathematically valid.

• berlekampForm : Hex.factorsModPBerlekampForm core data

  The cached factors have the required Berlekamp certificate form.

• p_le : data.p ≤ 500

  The prime lies within the range used by the resultant estimate.

theorem HexBerlekampZassenhausMathlib.directPrimePlan_probes_modPFactorization (core : Hex.SquareFreeInput) (plan : Hex.DirectPrimePlan core) (hplan : Hex.directPrimePlan? core = some plan) (hprim : core.poly.Primitive) (hlc_pos : 0 < Hex.DensePoly.leadingCoeff core.poly) (hpos : 0 < Hex.DensePoly.natDegree core.poly) (probe : Hex.DirectPrimeProbe core) : probe ∈ plan.probes → ModPFactorization core.poly probe.data

Every retained trial -- not only the selected one -- describes the normalized modular image of the plan's own indexed polynomial.

theorem HexBerlekampZassenhausMathlib.directPrimePlan_probes_facts (core : Hex.SquareFreeInput) (plan : Hex.DirectPrimePlan core) (hplan : Hex.directPrimePlan? core = some plan) (hprim : core.poly.Primitive) (hlc_pos : 0 < Hex.DensePoly.leadingCoeff core.poly) (hpos : 0 < Hex.DensePoly.natDegree core.poly) (probe : Hex.DirectPrimeProbe core) : probe ∈ plan.probes → DirectPrimeFacts core.poly probe.data

Every retained trial supplies exactly the modular facts the classical and lattice proof cones consume.

theorem HexBerlekampZassenhausMathlib.directPrimePlan_probes_reachableDegrees (core : Hex.SquareFreeInput) (plan : Hex.DirectPrimePlan core) (hplan : Hex.directPrimePlan? core = some plan) (hprim : core.poly.Primitive) (hlc_pos : 0 < Hex.DensePoly.leadingCoeff core.poly) (hpos : 0 < Hex.DensePoly.natDegree core.poly) {c : Hex.ZPoly} (hdvd : c ∣ core.poly) (probe : Hex.DirectPrimeProbe core) : probe ∈ plan.probes → probe.reachableDegrees[Hex.DensePoly.natDegree c]?.getD false = true

The statement a degree filter over a whole plan consumes: the degree of a genuine integer divisor of the input is marked reachable at every trial the planner retained, so intersecting the retained bitsets rejects no genuine factor.

theorem HexBerlekampZassenhausMathlib.directPrimePlan_modPFactorization (core : Hex.SquareFreeInput) (plan : Hex.DirectPrimePlan core) (hplan : Hex.directPrimePlan? core = some plan) (hprim : core.poly.Primitive) (hlc_pos : 0 < Hex.DensePoly.leadingCoeff core.poly) (hpos : 0 < Hex.DensePoly.natDegree core.poly) : ModPFactorization core.poly plan.data

A selected direct plan describes the normalized modular image of its own indexed polynomial.

theorem HexBerlekampZassenhausMathlib.directPrimePlan_facts (core : Hex.SquareFreeInput) (plan : Hex.DirectPrimePlan core) (hplan : Hex.directPrimePlan? core = some plan) (hprim : core.poly.Primitive) (hlc_pos : 0 < Hex.DensePoly.leadingCoeff core.poly) (hpos : 0 < Hex.DensePoly.natDegree core.poly) : DirectPrimeFacts core.poly plan.data

A successful direct plan supplies exactly the modular facts used by the classical and lattice proof cones.