CubicEquations.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Degree, prime divisors, and universality of cubic equations; Regularity of the image of the cubic embedding

theorem OAI.Nagata.W03.polynomial_not_isUnit_of_eval_zero line 20

Source documentation

Vanishing at one actual vector makes a polynomial a nonunit.

theorem polynomial_not_isUnit_of_eval_zero
    (L : MvPolynomial (Fin 3) ℂ) (v : Fin 3 → ℂ)
    (hv : MvPolynomial.eval v L = 0) : ¬ IsUnit L := by
…

theorem OAI.Nagata.W03.prime_relation_divisor_mem line 27

Source documentation

A nonunit divisor of a prime relation vanishes on the whole parameter domain.

theorem prime_relation_divisor_mem
    (s : Fin 3 → ℂ → ℂ) (G L : MvPolynomial (Fin 3) ℂ)
    (hG : Prime G) (hrel : G ∈ polynomialRelationIdeal s)
    (hL : ¬ IsUnit L) (hdiv : L ∣ G) : L ∈ polynomialRelationIdeal s := by
…

theorem OAI.Nagata.W03.prime_relation_not_dvd_of_zero_and_nonzero line 38

Source documentation

A prime relation cannot be divisible by a polynomial which has one zero but also has a witnessed nonzero value on the parameterized image.

theorem prime_relation_not_dvd_of_zero_and_nonzero
    (s : Fin 3 → ℂ → ℂ) (G L : MvPolynomial (Fin 3) ℂ)
    (hG : Prime G) (hrel : G ∈ polynomialRelationIdeal s)
    (v : Fin 3 → ℂ) (hv : MvPolynomial.eval v L = 0)
    (hw : ∃ z : ℂ, z ≠ 0 ∧ MvPolynomial.eval (fun i => s i z) L ≠ 0) :
    ¬ L ∣ G := by
…

theorem OAI.Nagata.W03.actual_prime_relation_threePointLine line 63

Source documentation

Every prescribed image point lies on a three-point line that cannot divide a prime equation of the actual section map.

theorem actual_prime_relation_threePointLine {τ : ℝ}
    (hτ : 0 < τ) (hτone : τ < 1) {γ : ℂ} (hγ : γ ≠ 0)
    (G : MvPolynomial (Fin 3) ℂ) (hG : Prime G)
    (hhom : G.IsHomogeneous G.totalDegree)
    (hrel : G ∈ polynomialRelationIdeal
      (fun i => (actualCubicBasis hτ hτone hγ i).val))
    (q : TorusPoint (cubicPeriod hτ)) :
    ∃ (L : MvPolynomial (Fin 3) ℂ) (p : Fin 3 → PlanePoint),
      L ≠ 0 ∧ L.IsHomogeneous 1 ∧ Function.Injective p ∧
      p 0 = actualCubicMap hτ hτone hγ q ∧
      (∀ i, MvPolynomial.eval (p i).rep L = 0) ∧
      (∀ i, MvPolynomial.eval (p i).rep G = 0) ∧ ¬ L ∣ G := by
…

theorem OAI.Nagata.W03.actual_prime_relation_totalDegree_eq_three line 100

Source documentation

A prime homogeneous equation of the actual complete section map, with total degree at most three, has total degree exactly three.

theorem actual_prime_relation_totalDegree_eq_three {τ : ℝ}
    (hτ : 0 < τ) (hτone : τ < 1) {γ : ℂ} (hγ : γ ≠ 0)
    (G : MvPolynomial (Fin 3) ℂ) (hG : Prime G)
    (hhom : G.IsHomogeneous G.totalDegree) (hle : G.totalDegree ≤ 3)
    (hrel : G ∈ polynomialRelationIdeal
      (fun i => (actualCubicBasis hτ hτone hγ i).val)) :
    G.totalDegree = 3 := by
…

theorem OAI.Nagata.W03.exists_actual_prime_cubic_generator line 117

Source documentation

The pointwise ideal of all polynomial relations of the actual section map is generated by a genuine prime homogeneous cubic of exact total degree three.

theorem exists_actual_prime_cubic_generator {τ : ℝ}
    (hτ : 0 < τ) (hτone : τ < 1) {γ : ℂ} (hγ : γ ≠ 0) :
    ∃ G : MvPolynomial (Fin 3) ℂ,
      Prime G ∧ G.IsHomogeneous 3 ∧ G.totalDegree = 3 ∧
      polynomialRelationIdeal
        (fun i => (actualCubicBasis hτ hτone hγ i).val) = Ideal.span {G} ∧
      (∀ z : ℂ, z ≠ 0 →
        MvPolynomial.eval (cubicEvaluationVector (actualCubicBasis hτ hτone hγ) z) G = 0) ∧
      (∀ P : MvPolynomial (Fin 3) ℂ, ¬ G ∣ P →
        ∃ z : ℂ, z ≠ 0 ∧
          MvPolynomial.eval (cubicEvaluationVector (actualCubicBasis hτ hτone hγ) z) P ≠ 0) := by
…

theorem OAI.Nagata.W21.actual_prime_cubic_regular_at_image line 150

theorem OAI.Nagata.W21.exists_actual_regular_prime_cubic line 173

Source documentation

A genuine prime cubic with the exact relation ideal, noncancellation, and nonzero homogeneous gradient at every actual section evaluation vector.

 theorem exists_actual_regular_prime_cubic {τ : ℝ}
    (hτ : 0 < τ) (hτone : τ < 1) {γ : ℂ} (hγ : γ ≠ 0) :
    ∃ G : MvPolynomial (Fin 3) ℂ,
      Prime G ∧ G.IsHomogeneous 3 ∧ G.totalDegree = 3 ∧
      polynomialRelationIdeal
        (fun i => (actualCubicBasis hτ hτone hγ i).val) = Ideal.span {G} ∧
      (∀ z : ℂ, z ≠ 0 →
        MvPolynomial.eval (cubicEvaluationVector (actualCubicBasis hτ hτone hγ) z) G = 0) ∧
      (∀ z : ℂ, z ≠ 0 → ∃ j,
        MvPolynomial.eval (cubicEvaluationVector (actualCubicBasis hτ hτone hγ) z)
          (MvPolynomial.pderiv j G) ≠ 0) ∧
      (∀ P : MvPolynomial (Fin 3) ℂ, ¬ G ∣ P → ∃ z : ℂ, z ≠ 0 ∧
…

theorem OAI.Nagata.W03.LowDegree.lineNormalPolynomial_coeff_eq_map line 211
Source documentation
Coefficientwise component restriction agrees with the finite normal sum when the actual polynomial has no terms above floor(d/3).
```
theorem lineNormalPolynomial_coeff_eq_map
    (F : Polynomial (MvPolynomial (Fin 3) ℂ)) (d i : ℕ)
    (hbound : ∀ j, d / 3 < j → F.coeff j = 0) :
    lineNormalPolynomial F.coeff d i = F.map (lineRestriction (i : ℂ)) := by
…
```
Mentions: OAI.Nagata.W03.LowDegree.lineNormalPolynomial
theorem OAI.Nagata.W03.LowDegree.cubic_universalSupport_degree_gt line 226
Source documentation
For every r≥10, genuine universal equal-multiplicity plane systems have degree strictly greater than 3m. Both d<3m and d=3m are excluded. No positivity assumption on d is needed for this stronger statement.
```
theorem cubic_universalSupport_degree_gt (r d m : ℕ) (hr : 10 ≤ r) (hm : 0 < m)
    (hU : Nagata.W13.UniversalSupport r d (fun _ => m)) : 3 * m < d := by
…
```
Mentions: OAI.Nagata.W13.UniversalSupport
theorem OAI.Nagata.W03.LowDegree.cubic_low_degree line 260
Source documentation
The exact positive-degree manuscript formulation.
```
theorem cubic_low_degree (r d m : ℕ) (hr : 10 ≤ r) (_hd : 0 < d) (hm : 0 < m)
    (hU : Nagata.W13.UniversalSupport r d (fun _ => m)) : 3 * m < d :=
…
```
Mentions: OAI.Nagata.W13.UniversalSupport