A primitive coordinate pair generates the function field over the constant field. Every finite family of functions then has polynomial reconstruction identities with one nonzero denominator. No bound on its degree is asserted.

theorem CCDN.adjoin_top_polynomial_fraction {K : Type u_1} {F : Type u_2} {σ : Type u_3} [Field K] [Field F] [Algebra K F] (a : σ → F) (ha : IntermediateField.adjoin K (Set.range a) = ⊤) (x : F) : ∃ (r : MvPolynomial σ K) (s : MvPolynomial σ K), (MvPolynomial.aeval a) s ≠ 0 ∧ x = (MvPolynomial.aeval a) r / (MvPolynomial.aeval a) s

A generating polynomial tuple expresses any field element as a quotient with a nonzero evaluated denominator.

theorem CCDN.exists_common_polynomial_reconstruction {K : Type u_1} {F : Type u_2} {σ : Type u_3} {ι : Type u_4} [Field K] [Field F] [Algebra K F] [Finite ι] (a : σ → F) (ha : IntermediateField.adjoin K (Set.range a) = ⊤) (x : ι → F) : ∃ (Q : MvPolynomial σ K) (P : ι → MvPolynomial σ K), (MvPolynomial.aeval a) Q ≠ 0 ∧ ∀ (i : ι), (MvPolynomial.aeval a) Q * x i = (MvPolynomial.aeval a) (P i)

A finite family of field elements has a common polynomial denominator in any generating tuple, with polynomial reconstruction identities.