The closed-form coefficient matrix commutes with coefficient ring maps, including passage from integers to characteristic zero and reduction modulo p.

Reconstruct bounded polynomial closed forms inside the matrix kernel. Two independent forms force the rank drop used by the integer minor.

noncomputable def CCDN.bivariateMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) : Polynomial (Polynomial R) →+* Polynomial (Polynomial S)

Apply a ring map to both levels of bivariate coefficients.

Equations

• CCDN.bivariateMap φ = Polynomial.mapRingHom (Polynomial.mapRingHom φ)

@[simp]

theorem CCDN.bivariateMap_coeff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (f : Polynomial (Polynomial R)) (i j : ℕ) : (((bivariateMap φ) f).coeff i).coeff j = φ ((f.coeff i).coeff j)

The coefficients of bivariateMap φ f are the images under φ of those of f.

theorem CCDN.bivariateMap_derivative {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (f : Polynomial (Polynomial R)) : (bivariateMap φ) (Polynomial.derivative f) = Polynomial.derivative ((bivariateMap φ) f)

Applying a coefficient ring homomorphism commutes with the outer derivative.

theorem CCDN.bivariateMap_coefficientDerivative {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (f : Polynomial (Polynomial R)) : (bivariateMap φ) ((bivariateCoefficientDerivative R) f) = (bivariateCoefficientDerivative S) ((bivariateMap φ) f)

Applying a coefficient ring homomorphism commutes with the inner derivative.

theorem CCDN.bivariateMap_closedFormOperator {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (f : Polynomial (Polynomial R)) (u : Polynomial (Polynomial R) × Polynomial (Polynomial R)) : (bivariateMap φ) ((closedFormOperator f) u) = (closedFormOperator ((bivariateMap φ) f)) ((bivariateMap φ) u.1, (bivariateMap φ) u.2)

Applying a coefficient ring homomorphism commutes with the closed-form operator, applied to the equation and to both unknowns.

theorem CCDN.closedFormCoefficientMatrix_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (d : ℕ) (f : Polynomial (Polynomial R)) : (closedFormCoefficientMatrix d f).map ⇑φ = closedFormCoefficientMatrix d ((bivariateMap φ) f)

Matrix entries base-change exactly; no injectivity or characteristic hypothesis on the coefficient map is needed.

def CCDN.InBivariateGrid {R : Type u_1} [CommRing R] (d : ℕ) (f : Polynomial (Polynomial R)) : Prop

All coefficients outside the strict rectangular grid vanish.

Equations

• CCDN.InBivariateGrid d f = ∀ (i j : ℕ), d ≤ i ∨ d ≤ j → (f.coeff i).coeff j = 0

theorem CCDN.bivariateGridPolynomial_coeff_zero {R : Type u_1} [CommRing R] (d : ℕ) (v : BivariateGrid d → R) (i j : ℕ) (h : d ≤ i ∨ d ≤ j) : (((bivariateGridPolynomial R d) v).coeff i).coeff j = 0

The polynomial with coefficients on the grid BivariateGrid d has zero coefficient at every monomial with outer exponent i and inner exponent j such that d ≤ i or d ≤ j.

theorem CCDN.bivariateGridPolynomial_reconstruct {R : Type u_1} [CommRing R] (d : ℕ) (f : Polynomial (Polynomial R)) (hf : InBivariateGrid d f) : ((bivariateGridPolynomial R d) fun (i : BivariateGrid d) => (f.coeff ↑i.1).coeff ↑i.2) = f

Coefficient extraction followed by decoding recovers every polynomial supported on the grid.

theorem CCDN.closedFormOperator_gradient {F : Type u_1} [Field F] (f : Polynomial (Polynomial F)) : (closedFormOperator f) (Polynomial.derivative f, (bivariateCoefficientDerivative F) f) = 0

The gradient itself satisfies the closed-form equation in every field.

theorem CCDN.closedForm_rank_drop_of_two_forms {F : Type u_1} [Field F] (d : ℕ) (f : Polynomial (Polynomial F)) (u w : Polynomial (Polynomial F) × Polynomial (Polynomial F)) (hu₁ : InBivariateGrid d u.1) (hu₂ : InBivariateGrid d u.2) (hw₁ : InBivariateGrid d w.1) (hw₂ : InBivariateGrid d w.2) (hu : (closedFormOperator f) u = 0) (hw : (closedFormOperator f) w = 0) (hu0 : u ≠ 0) (hind : ∀ (a : F), a • u ≠ w) : (closedFormCoefficientMatrix d f).rank + 2 ≤ 2 * d ^ 2

Two polynomial solutions, one not a scalar multiple of the other, give a rank drop of at least two.