Scaling the defining equation by a nonzero constant preserves the matrix rank. This permits monic normalization over fields without enlarging integer coefficients or clearing extra denominators.

The closed-form coefficient matrix has corank at most one for a monic irreducible equation of outer degree d whose coefficients have degree at most D, in characteristic zero or larger than 2dD. This supplies the rank input to effective Bertini.

theorem CCDN.closedForm_coefficient_rank_lower {F : Type u_1} [Field F] [IsAlgClosed F] (d : ℕ) (f : Polynomial (Polynomial F)) (hf : Irreducible f) (hm : f.Monic) (hdeg : f.degree = ↑d) (D : ℕ) (htotal : bivariateTotalDegree f ≤ D) (hchar : CharZeroOrGT F (2 * d * D)) : 2 * d ^ 2 ≤ (closedFormCoefficientMatrix d f).rank + 1

The matrix on the 2d² unknown coefficients has rank at least 2d²-1.

theorem CCDN.closedFormOperator_smul_equation {R : Type u_1} [CommRing R] (a : R) (f : Polynomial (Polynomial R)) (u : Polynomial (Polynomial R) × Polynomial (Polynomial R)) : (closedFormOperator (a • f)) u = a • (closedFormOperator f) u

The closed-form operator is linear in the equation: scaling the equation by a scales the operator by a.

theorem CCDN.closedFormCoefficientMatrix_smul {R : Type u_1} [CommRing R] (a : R) (d : ℕ) (f : Polynomial (Polynomial R)) : closedFormCoefficientMatrix d (a • f) = a • closedFormCoefficientMatrix d f

Scaling the equation by a scales its closed-form coefficient matrix by a.

theorem CCDN.bivariate_smul_eq_constant_mul {R : Type u_1} [CommRing R] (a : R) (f : Polynomial (Polynomial R)) : a • f = Polynomial.C (Polynomial.C a) * f

Scalar multiplication of a bivariate polynomial by a is multiplication by the constant polynomial a.

theorem CCDN.bivariate_irreducible_smul_iff {F : Type u_1} [Field F] (a : F) (ha : a ≠ 0) (f : Polynomial (Polynomial F)) : Irreducible (a • f) ↔ Irreducible f

Over a field, multiplying a bivariate polynomial by a nonzero scalar preserves irreducibility.

theorem CCDN.bivariateTotalDegree_smul_le {R : Type u_1} [CommRing R] (a : R) (f : Polynomial (Polynomial R)) : bivariateTotalDegree (a • f) ≤ bivariateTotalDegree f

Scalar multiplication does not increase the total degree.

theorem CCDN.bivariate_monic_normalize {F : Type u_1} [Field F] (a : F) (ha : a ≠ 0) (f : Polynomial (Polynomial F)) (hl : f.leadingCoeff = Polynomial.C a) : (a⁻¹ • f).Monic

If the outer leading coefficient of f is the nonzero constant a, then a⁻¹ • f is monic. Normalizing over the coefficient field means no integer denominators need to be cleared in the original coefficient matrix.

theorem CCDN.closedForm_rank_lower_of_constant_leading {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] (d : ℕ) (a : F) (ha : a ≠ 0) (f : Polynomial (Polynomial F)) (hl : f.leadingCoeff = Polynomial.C a) (hf : Irreducible f) (hdeg : f.natDegree = d) : 2 * d ^ 2 ≤ (closedFormCoefficientMatrix d f).rank + 1

Over an algebraically closed field of characteristic zero, an irreducible f of outer degree d whose outer leading coefficient is a nonzero constant has closed-form coefficient matrix of rank at least 2 * d ^ 2 - 1; the equation need not be monic.

theorem CCDN.closedForm_rank_drop_of_constant_leading {F : Type u_1} [Field F] (d : ℕ) (hd : 0 < d) (hchar : CharZeroOrGT F d) (a : F) (ha : a ≠ 0) (f : Polynomial (Polynomial F)) (hl : f.leadingCoeff = Polynomial.C a) (hred : ¬Irreducible f) (hdeg : f.natDegree = d) (htotal : bivariateTotalDegree f ≤ d) : (closedFormCoefficientMatrix d f).rank + 2 ≤ 2 * d ^ 2

A reducible f of outer degree and total degree d, whose outer leading coefficient is a nonzero constant, has closed-form coefficient matrix of rank at most 2 * d ^ 2 - 2, in characteristic zero or greater than d.