Bounded primitive augmentation of any independent linear parameter tuple of the Hilbert dimension.

theorem CCDN.exists_bounded_linear_parameter_primitive {K : Type u_1} {F : Type u_2} [Field K] [CharZero K] [Field F] [Algebra K F] {n m : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) [I.IsPrime] [Algebra (MvPolynomial (Fin n) K ⧸ I) F] [IsScalarTower K (MvPolynomial (Fin n) K ⧸ I) F] [IsFractionRing (MvPolynomial (Fin n) K ⧸ I) F] (l : Fin (m + 1) → MvPolynomial (Fin n) K) (hl : ∀ (i : Fin (m + 1)), (l i).totalDegree ≤ 1) (hi : Function.Injective ⇑(projectionCoordinateMap I l)) (d : ℕ) (hdimdeg : HasProjectiveDimensionDegree I m d) : ∃ k ≤ n * d ^ 2, IntermediateField.adjoin K (Set.range fun (i : Fin (m + 2)) => (algebraMap (MvPolynomial (Fin n) K ⧸ I) F) ((Ideal.Quotient.mk I) (Fin.cases (momentCoordinate K n k) l i))) = ⊤

Given m + 1 linear forms algebraically independent modulo a prime I of projective dimension m and degree d (in characteristic zero), some moment coordinate with parameter k ≤ n * d ^ 2 together with these forms generates the function field of I.