theorem HexBerlekampZassenhausMathlib.irreducible_of_directSingleton (core : Hex.ZPoly) (data : Hex.PrimeChoiceData) (prime : DirectPrimeFacts core data) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (hcore_prim : core.Primitive) (hsmall : data.factorsModP.size ≤ 1) : core.Irreducible

A one-factor direct modular plan certifies irreducibility of a primitive positive-degree input.

theorem HexBerlekampZassenhausMathlib.bhksRecoveryCoreWithBound_factorCount (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (hcore_prim : core.Primitive) (hcore_sqfree : Squarefree (HexPolyZMathlib.toPolynomial core)) (hval : ModPFactorization core data) (coreFactors : Array Hex.ZPoly) (hfast : Hex.bhksRecoveryCoreWithBound core B data (Hex.initialHenselPrecision B) (Hex.ZPoly.quadraticDoublingSteps B + 2) = some coreFactors) : (List.map HexPolyZMathlib.toPolynomial coreFactors.toList).length = (UniqueFactorizationMonoid.normalizedFactors (HexPolyZMathlib.toPolynomial core)).card

A successful forward-adequate CLD split emits exactly one candidate for each normalized irreducible factor.

theorem HexBerlekampZassenhausMathlib.irreducible_of_directSingleClass (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (hcore_prim : core.Primitive) (hcore_sqfree : Squarefree (HexPolyZMathlib.toPolynomial core)) (hval : ModPFactorization core data) (hB_floor : Hex.bhksRecoveryFloor core ≤ B) (hB_ne : B ≠ 0) (hsingle : Hex.bhksSingleAllOnesPartition core (core.directLiftData B data) = true) : core.Irreducible

At a forward-adequate precision, the executable single-all-ones certificate implies that the primitive square-free part is irreducible.

theorem HexBerlekampZassenhausMathlib.latticeCoreFactorsWithBound_factor_irreducible (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (prime : DirectPrimeFacts core data) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (hcore_prim : core.Primitive) (hcore_sqfree : Squarefree (HexPolyZMathlib.toPolynomial core)) (hB_floor : Hex.bhksRecoveryFloor core ≤ B) (hB_ne : B ≠ 0) {coreFactors : Array Hex.ZPoly} (hlattice : Hex.latticeCoreFactorsWithBound core B data = some coreFactors) (factor : Hex.ZPoly) : factor ∈ coreFactors.toList → factor.Irreducible

Every factor returned by the direct-coordinate CLD method is irreducible. Split success uses the forward count theorem; either all-ones arm uses the forward irreducibility certificate.

theorem HexBerlekampZassenhausMathlib.latticeCoreFactorsWithBound_ne_none (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (prime : DirectPrimeFacts core data) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (hcore_prim : core.Primitive) (hcore_sqfree : Squarefree (HexPolyZMathlib.toPolynomial core)) (hB_floor : Hex.bhksRecoveryFloor core ≤ B) (hB_ne : B ≠ 0) (hresultant : 2 * Hex.bhksBound core < (core.directLiftData B data).p ^ (core.directLiftData B data).k) : Hex.latticeCoreFactorsWithBound core B data ≠ none

At full resultant-adequate precision, the direct-coordinate CLD method is total for every successful prime plan. Exact span yields either a genuine multi-class recovery on the scheduled cap visit or the single-all-ones certificate.

theorem HexBerlekampZassenhausMathlib.reassemblyExpansionComplete_latticeCore (f : Hex.ZPoly) (hf : f ≠ 0) (B : ℕ) (data : Hex.PrimeChoiceData) (prime : DirectPrimeFacts (Hex.normalizeForFactor f).squareFreeCore data) (hcore_pos : 0 < Hex.DensePoly.natDegree (Hex.normalizeForFactor f).squareFreeCore) (hB_floor : Hex.bhksRecoveryFloor (Hex.normalizeForFactor f).squareFreeCore ≤ B) (hB_ne : B ≠ 0) {coreFactors : Array Hex.ZPoly} (hlattice : Hex.latticeCoreFactorsWithBound (Hex.normalizeForFactor f).squareFreeCore B data = some coreFactors) : Hex.reassemblyExpansionComplete (Hex.normalizeForFactor f) coreFactors

Reassembling a successful direct CLD factorization of the square-free part covers the original input exactly.

theorem HexBerlekampZassenhausMathlib.factorLatticeFactorsWithPlan_factor_irreducible (f : Hex.ZPoly) (hf : f ≠ 0) (modular : Hex.DirectPrimePlan { poly := (Hex.normalizeForFactor f).squareFreeCore }) (hplan : Hex.directPrimePlan? { poly := (Hex.normalizeForFactor f).squareFreeCore } = some modular) {factors : Array Hex.ZPoly} (hresult : Hex.factorLatticeFactorsWithPlan (Hex.normalizeForFactor f) (Hex.latticePrecisionCap f) modular = some factors) {raw : Hex.ZPoly} (hraw : raw ∈ factors.toList) (hrecord : Hex.shouldRecordPolynomialFactor (Hex.normalizeFactorSign raw) = true) : raw.Irreducible

Every recorded raw factor returned by CLD from a selected direct prime is irreducible.

theorem HexBerlekampZassenhausMathlib.factorLatticeFactorsWithBound_factor_irreducible (f : Hex.ZPoly) (hf : f ≠ 0) {factors : Array Hex.ZPoly} (hresult : Hex.factorLatticeFactorsWithBound f (Hex.latticePrecisionCap f) = some factors) {raw : Hex.ZPoly} (hraw : raw ∈ factors.toList) (hrecord : Hex.shouldRecordPolynomialFactor (Hex.normalizeFactorSign raw) = true) : raw.Irreducible

Every recorded raw factor returned by the standalone direct CLD branch is irreducible.