Upper cardinality bound for a product partition in a UFD.
If a non-zero element f is associated to the product of a list of non-zero
non-unit factors, then that list cannot have more entries than the multiset of
normalized irreducible factors of f. Each list entry contributes at least one
normalized factor. The bound requires product preservation and
shouldRecord/non-unit facts, but does not assume irreducibility of the
emitted factors.
If a list of irreducible factors has product associated to f, then the
multiset of normalized factors of f has exactly the length of the list.
This is the converse cardinality direction to
length_le_normalizedFactors_card for the already-certified irreducible
partition case.
The normalized factors of a list product of irreducibles are exactly the normalizations of the list entries, viewed as a multiset.
Use this when a uniqueness or scalar-splitting proof needs to replace the abstract UFD factor multiset of a certified product by the concrete flattened list of factors.
Uniqueness for scalar-prefixed products of flattened monic irreducible integer polynomial factors.
If two nonzero integer scalars multiply products of monic irreducible factors to the same polynomial, the scalars agree and the flattened products have the same normalized-factor multiset. This is the Mathlib/UFD result needed by the factorization uniqueness theorem after executable factor entries have been expanded by multiplicity. The theorem stays public as the clean monic specialization; current BZ factorization uniqueness uses the normalize-fixed variant below because executable factors are not necessarily monic.
Variant of scalar_eq_and_normalizedFactors_eq_of_monic_irreducible_product_eq
for nonconstant normalize-fixed irreducible integer polynomial factors, which
is what the BZ uniqueness theorem actually has (the executable
normalizeFactorSign only enforces a nonnegative leading coefficient, not a
unit leading coefficient).
If two nonzero integer scalars multiply products of nonconstant normalize-fixed
irreducible integer polynomial factors to the same polynomial, the scalars
agree and the flattened factor lists agree as multisets. Constant factors are
ruled out by the natDegree ≠ 0 hypothesis, so they cannot leak between the
scalar prefix and the factor list. This is the exported shape used by
Factorization uniqueness after translating executable factors to
Polynomial ℤ.
Group B partition-cardinality bound (Mathlib-only UFD argument).
In any unique factorization monoid, a non-zero element f admitting a list of
non-unit divisors gs whose product is associated to f and whose length
equals the cardinality of normalizedFactors f must consist entirely of
irreducible elements.
This isolates the UFD half of the BHKS Group B / B8 certification theorem:
the algorithm-specific work (establishing the cardinality equality from BHKS
lattice success state) is handled separately and supplies the hcount
hypothesis to this lemma. Fast and exhaustive branch lemmas should use this
once they have product preservation, non-unit entries, and the final count
equality.
UFD subset-factor lemma.
In a unique factorization monoid, if a non-zero element g divides the
product of a multiset of irreducibles qs, then the normalized factorization
of g is a sub-multiset of qs up to normalization.
This is the UFD half of the BZ certificate degree-obstruction argument: once an integer factor reduces to a divisor of the recorded modular factor product, its modular factorization is drawn from the recorded irreducibles. The polynomial degree lemma below is the usual public caller-facing package; this theorem remains available for callers that need the raw sub-multiset relation.
UFD subset existence and uniqueness for squarefree-product divisors.
In a unique factorization monoid, if factors is a Nodup multiset of
normalize-fixed irreducibles and d is a normalize-fixed divisor of
factors.prod, then there is a unique sub-multiset S ≤ factors whose
product equals d. The witness is normalizedFactors d; uniqueness uses
normalizedFactors_prod_eq to recover any candidate from its product.
This is the abstract Mathlib half of the
existsUnique_modPFactorSubset_of_choosePrimeData assembly: the final
caller instantiates α := Polynomial (ZMod p) and transports the
resulting sub-multiset through an executable factor-list indexing.
Polynomial subset-degree lemma.
Over a field K, if g : K[X] is non-zero and divides the product of a
multiset of irreducible polynomials qs, then g.natDegree is the sum of
some sub-multiset of qs.map natDegree.
This is the degree-subset-sum packaging of
normalizedFactors_le_map_normalize_of_dvd_prod_irreducibles that the BZ
certificate degree-obstruction caller needs: the recorded modular factor
degrees are the qs.map natDegree values, and the contradiction with a
"no subset sums to g.natDegree" obstruction comes from this lemma.