LowDegree.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Nonzero low-degree homogeneous equations and configurations

def OAI.Nagata.W03.LowDegree.lineNormalPolynomial line 27
Source documentation
Actual normal polynomial restricted to component i, with coefficients in its affine coordinate ring K[U]. The outer polynomial variable is the fiber.
```
def lineNormalPolynomial (R : ℕ → MvPolynomial (Fin 3) K) (d i : ℕ) :
    Polynomial (Polynomial K) :=
…
```
def OAI.Nagata.W03.LowDegree.fiberPolynomial line 33
Source documentation
The ordinary fiber polynomial above the affine point with parameter U.
```
def fiberPolynomial (R : ℕ → MvPolynomial (Fin 3) K) (d i : ℕ) (U : K) : K[X] :=
…
```

theorem OAI.Nagata.W03.LowDegree.lower_coefficient_restrictions_zero line 38

Source documentation

Nine marked multiplicity conditions annihilate every coefficient below m when d≤3m, including the equality-degree case on the reduced triangle.

theorem lower_coefficient_restrictions_zero [CharZero K]
    (R : ℕ → MvPolynomial (Fin 3) K) (d m : ℕ) (hdm : d ≤ 3 * m)
    (hdegree : ∀ j ≤ d / 3, ∀ i : ℕ, i < 3 →
      (lineRestriction (i : K) (R j)).natDegree ≤ d - 3 * j)
    (hfirst : ∀ j ≤ d / 3, j < m → ∀ i : ℕ, i < 3 →
      (X + C ((firstMark 3 i : ℕ) : K)) ^ (m - j) ∣ lineRestriction (i : K) (R j))
    (htail : ∀ j ≤ d / 3, j < m → ∀ i : ℕ, i < 3 → ∀ s < 2,
      (X + C ((s + 2 : ℕ) : K)) ^ (m - j) ∣ lineRestriction (i : K) (R j)) :
    ∀ j ≤ d / 3, j < m → ∀ i : ℕ, i < 3 → lineRestriction (i : K) (R j) = 0 := by
…

theorem OAI.Nagata.W03.LowDegree.strict_low_degree_lineNormal_zero line 56

Source documentation

If d<3m all component normal polynomials vanish. This conclusion involves actual polynomials, not a formal coefficient-vanishing predicate.

theorem strict_low_degree_lineNormal_zero
    (R : ℕ → MvPolynomial (Fin 3) K) (d m : ℕ) (hdm : d < 3 * m)
    (hlower : ∀ j ≤ d / 3, j < m → ∀ i : ℕ, i < 3 →
      lineRestriction (i : K) (R j) = 0) :
    ∀ i : ℕ, i < 3 → lineNormalPolynomial R d i = 0 := by
…

Mentions: OAI.Nagata.W03.LowDegree.lineNormalPolynomial

theorem OAI.Nagata.W03.LowDegree.equality_lineNormal_shape line 70

Source documentation

At d=3m, vanishing of all lower coefficients leaves the actual top monomial.

theorem equality_lineNormal_shape
    (R : ℕ → MvPolynomial (Fin 3) K) (m : ℕ) (a : K)
    (hlower : ∀ j < m, ∀ i : ℕ, i < 3 → lineRestriction (i : K) (R j) = 0)
    (htop : R m = MvPolynomial.C a) :
    ∀ i : ℕ, i < 3 → lineNormalPolynomial R (3 * m) i = Polynomial.monomial m (C a) := by
…

Mentions: OAI.Nagata.W03.LowDegree.lineNormalPolynomial

theorem OAI.Nagata.W03.LowDegree.equality_fiber_shape line 89
Source documentation
Evaluation in the base coordinate preserves the top monomial and its scalar.
```
theorem equality_fiber_shape
    (R : ℕ → MvPolynomial (Fin 3) K) (m i : ℕ) (U a : K)
    (hshape : lineNormalPolynomial R (3 * m) i = Polynomial.monomial m (C a)) :
    fiberPolynomial R (3 * m) i U = Polynomial.monomial m a := by
…
```
Mentions: OAI.Nagata.W03.LowDegree.lineNormalPolynomial, OAI.Nagata.W03.LowDegree.fiberPolynomial
theorem OAI.Nagata.W03.LowDegree.pure_fiber_root_forces_scalar_zero line 97
Source documentation
A pure nonzero top monomial cannot have positive root order at a nonzero fiber displacement. The divisibility premise is ordinary polynomial multiplicity.
```
theorem pure_fiber_root_forces_scalar_zero (m : ℕ) (hm : 0 < m) (a c : K)
    (hc : c ≠ 0) (hroot : (X - C c) ^ m ∣ Polynomial.monomial m a) : a = 0 := by
…
```
theorem OAI.Nagata.W03.LowDegree.equality_low_degree_contradiction line 104

theorem OAI.Nagata.W03.LowDegree.degree_gt_three_mul_of_normal_polynomial line 121

Source documentation

Combined low-degree branch: these actual coefficient and fiber conditions force d>3m. The top-constant condition follows from homogeneous degree zero.

theorem degree_gt_three_mul_of_normal_polynomial [CharZero K]
    (R : ℕ → MvPolynomial (Fin 3) K) (d m : ℕ) (hm : 0 < m) (U c : K)
    (hdegree : ∀ j ≤ d / 3, ∀ i : ℕ, i < 3 →
      (lineRestriction (i : K) (R j)).natDegree ≤ d - 3 * j)
    (hfirst : ∀ j ≤ d / 3, j < m → ∀ i : ℕ, i < 3 →
      (X + C ((firstMark 3 i : ℕ) : K)) ^ (m - j) ∣ lineRestriction (i : K) (R j))
    (htail : ∀ j ≤ d / 3, j < m → ∀ i : ℕ, i < 3 → ∀ s < 2,
      (X + C ((s + 2 : ℕ) : K)) ^ (m - j) ∣ lineRestriction (i : K) (R j))
    (htop : d = 3 * m → ∃ a : K, R m = MvPolynomial.C a)
    (hnonzero : ∃ i < 3, lineNormalPolynomial R d i ≠ 0)
    (hc : c ≠ 0)
    (hroot : (X - C c) ^ m ∣ fiberPolynomial R d 0 U) : 3 * m < d := by
…

Mentions: OAI.Nagata.W03.LowDegree.lineNormalPolynomial, OAI.Nagata.W03.LowDegree.fiberPolynomial

theorem OAI.Nagata.W03.LowDegree.degree_gt_three_mul_of_ambient_normal_polynomial line 148

Source documentation

The ambient total-degree bounds discharge both the component-degree premise and the common constant leading coefficient. Genuine homogeneous degree bounds imply these total-degree bounds; no smooth-curve section theorem is used.

theorem degree_gt_three_mul_of_ambient_normal_polynomial [CharZero K]
    (R : ℕ → MvPolynomial (Fin 3) K) (d m : ℕ) (hm : 0 < m) (U c : K)
    (hdegree : ∀ j ≤ d / 3, (R j).totalDegree ≤ d - 3 * j)
    (hfirst : ∀ j ≤ d / 3, j < m → ∀ i : ℕ, i < 3 →
      (X + C ((firstMark 3 i : ℕ) : K)) ^ (m - j) ∣ lineRestriction (i : K) (R j))
    (htail : ∀ j ≤ d / 3, j < m → ∀ i : ℕ, i < 3 → ∀ s < 2,
      (X + C ((s + 2 : ℕ) : K)) ^ (m - j) ∣ lineRestriction (i : K) (R j))
    (hnonzero : ∃ i < 3, lineNormalPolynomial R d i ≠ 0)
    (hc : c ≠ 0)
    (hroot : (X - C c) ^ m ∣ fiberPolynomial R d 0 U) : 3 * m < d := by
…

Mentions: OAI.Nagata.W03.LowDegree.lineNormalPolynomial, OAI.Nagata.W03.LowDegree.fiberPolynomial

def OAI.Nagata.W03.LowDegree.quotientNormalPolynomial line 183

Source documentation

Normal polynomial with coefficients in the actual coordinate ring modulo G.

def quotientNormalPolynomial (R : ℕ → MvPolynomial (Fin 3) K) (d : ℕ)
    (G : MvPolynomial (Fin 3) K) :
    Polynomial (MvPolynomial (Fin 3) K ⧸ Ideal.span ({G} : Set (MvPolynomial (Fin 3) K))) :=
…

theorem OAI.Nagata.W03.LowDegree.exists_nondivisible_coefficient_of_quotientNormal_ne_zero line 190
Source documentation
A nonzero quotient normal polynomial has an actual nonzero residue coefficient.
```
theorem exists_nondivisible_coefficient_of_quotientNormal_ne_zero
    (R : ℕ → MvPolynomial (Fin 3) K) (d : ℕ) (G : MvPolynomial (Fin 3) K)
    (hN : quotientNormalPolynomial R d G ≠ 0) :
    ∃ j ≤ d / 3, ¬ G ∣ R j := by
…
```
Mentions: OAI.Nagata.W03.LowDegree.quotientNormalPolynomial
theorem OAI.Nagata.W03.LowDegree.coeff_lineNormalPolynomial line 206
Source documentation
The j-th coefficient of the actual component polynomial is its line restriction.
```
theorem coeff_lineNormalPolynomial
    (R : ℕ → MvPolynomial (Fin 3) K) (d i j : ℕ) (hj : j ≤ d / 3) :
    (lineNormalPolynomial R d i).coeff j = lineRestriction (i : K) (R j) := by
…
```
Mentions: OAI.Nagata.W03.LowDegree.lineNormalPolynomial

theorem OAI.Nagata.W03.LowDegree.exists_nonzero_lineNormal_of_quotientNormal_ne_zero line 215

Source documentation

A proved component-noncancellation bridge transports the genuine quotient nonzero condition to a nonzero component normal polynomial.

theorem exists_nonzero_lineNormal_of_quotientNormal_ne_zero
    (R : ℕ → MvPolynomial (Fin 3) K) (d : ℕ) (G : MvPolynomial (Fin 3) K)
    (hN : quotientNormalPolynomial R d G ≠ 0)
    (hcomponents : ∀ j ≤ d / 3, ¬ G ∣ R j →
      ∃ i : ℕ, i < 3 ∧ lineRestriction (i : K) (R j) ≠ 0) :
    ∃ i < 3, lineNormalPolynomial R d i ≠ 0 := by
…

Mentions: OAI.Nagata.W03.LowDegree.quotientNormalPolynomial, OAI.Nagata.W03.LowDegree.lineNormalPolynomial

theorem OAI.Nagata.W03.LowDegree.quotientNormalPolynomial_coeff_eq_map line 230

Source documentation

The finite quotient sum agrees with mapping the actual normal polynomial when its coefficient support obeys the source exponent bound.

theorem quotientNormalPolynomial_coeff_eq_map
    (F : Polynomial (MvPolynomial (Fin 3) K)) (d : ℕ) (G : MvPolynomial (Fin 3) K)
    (hbound : ∀ j, d / 3 < j → F.coeff j = 0) :
    quotientNormalPolynomial F.coeff d G =
      F.map (Ideal.Quotient.mk (Ideal.span ({G} : Set (MvPolynomial (Fin 3) K)))) := by
…

Mentions: OAI.Nagata.W03.LowDegree.quotientNormalPolynomial

theorem OAI.Nagata.W03.LowDegree.quotientNormalPolynomial_ne_zero_of_map_ne_zero line 244

theorem OAI.Nagata.W03.LowDegree.marked_factors_of_zero_surface_orders line 270

Source documentation

The marked surface orders at zero displacement give the exact first and tail root-factor conditions needed by the triangle coefficient obstruction.

theorem marked_factors_of_zero_surface_orders
    (R : ℕ → MvPolynomial (Fin 3) K) (d m : ℕ)
    (hfirst : ∀ i < 3, lineNormalPolynomial R d i ∈
      (nestedPointIdeal (-((firstMark 3 i : ℕ) : K)) 0) ^ m)
    (htail : ∀ i < 3, ∀ s < 2, lineNormalPolynomial R d i ∈
      (nestedPointIdeal (-((s + 2 : ℕ) : K)) 0) ^ m) :
    (∀ j ≤ d / 3, ∀ i : ℕ, i < 3 →
      (X + C ((firstMark 3 i : ℕ) : K)) ^ (m - j) ∣ lineRestriction (i : K) (R j)) ∧
    (∀ j ≤ d / 3, ∀ i : ℕ, i < 3 → ∀ s < 2,
      (X + C ((s + 2 : ℕ) : K)) ^ (m - j) ∣ lineRestriction (i : K) (R j)) := by
…

Mentions: OAI.Nagata.W03.LowDegree.lineNormalPolynomial

theorem OAI.Nagata.W03.LowDegree.degree_gt_three_mul_of_surface_orders line 290
theorem OAI.Nagata.W03.LowDegree.exists_nonzero_lineNormal_of_homogeneous_quotient line 318
Source documentation
Homogeneous noncancellation turns the genuine quotient normal polynomial into a nonzero polynomial on at least one actual affine line component.
```
theorem exists_nonzero_lineNormal_of_homogeneous_quotient
    (R : ℕ → MvPolynomial (Fin 3) ℂ) (d : ℕ)
    (hhom : ∀ j ≤ d / 3, (R j).IsHomogeneous (d - 3 * j))
    (hN : quotientNormalPolynomial R d (Nagata.Workers.W24.homogeneousLineUnion ℂ 3) ≠ 0) :
    ∃ i < 3, lineNormalPolynomial R d i ≠ 0 := by
…
```
Mentions: OAI.Nagata.W03.LowDegree.quotientNormalPolynomial, OAI.Nagata.Workers.W24.homogeneousLineUnion, OAI.Nagata.W03.LowDegree.lineNormalPolynomial

theorem OAI.Nagata.W03.LowDegree.degree_gt_three_mul_of_homogeneous_normal_polynomial line 333

Source documentation

The complete algebraic low-degree branch over the genuine three-line homogeneous curve. The first nine multiplicity conditions are actual root factors; the tenth condition is ordinary fiber-polynomial root multiplicity.

theorem degree_gt_three_mul_of_homogeneous_normal_polynomial
    (R : ℕ → MvPolynomial (Fin 3) ℂ) (d m : ℕ) (hm : 0 < m) (U c : ℂ)
    (hhom : ∀ j ≤ d / 3, (R j).IsHomogeneous (d - 3 * j))
    (hfirst : ∀ j ≤ d / 3, j < m → ∀ i : ℕ, i < 3 →
      (X + C ((firstMark 3 i : ℕ) : ℂ)) ^ (m - j) ∣ lineRestriction (i : ℂ) (R j))
    (htail : ∀ j ≤ d / 3, j < m → ∀ i : ℕ, i < 3 → ∀ s < 2,
      (X + C ((s + 2 : ℕ) : ℂ)) ^ (m - j) ∣ lineRestriction (i : ℂ) (R j))
    (hN : quotientNormalPolynomial R d (Nagata.Workers.W24.homogeneousLineUnion ℂ 3) ≠ 0)
    (hc : c ≠ 0)
    (hroot : (X - C c) ^ m ∣ fiberPolynomial R d 0 U) : 3 * m < d := by
…

Mentions: OAI.Nagata.W03.LowDegree.quotientNormalPolynomial, OAI.Nagata.Workers.W24.homogeneousLineUnion, OAI.Nagata.W03.LowDegree.fiberPolynomial

theorem OAI.Nagata.W03.LowDegree.degree_gt_three_mul_of_grouped_homogeneous_normal_polynomial line 347

theorem OAI.Nagata.W03.LowDegree.degree_gt_three_mul_of_homogeneous_surface_orders line 366

Source documentation

Final reduced-triangle algebraic low-degree statement: actual homogeneous coefficient lifts, actual quotient nonzero polynomial, and ordinary point-ideal powers at the nine zero and one nonzero normal displacements imply d>3m.

theorem degree_gt_three_mul_of_homogeneous_surface_orders
    (R : ℕ → MvPolynomial (Fin 3) ℂ) (d m : ℕ) (hm : 0 < m) (U c : ℂ)
    (hhom : ∀ j ≤ d / 3, (R j).IsHomogeneous (d - 3 * j))
    (hfirst : ∀ i < 3, lineNormalPolynomial R d i ∈
      (Nagata.W18.nestedPointIdeal (-((firstMark 3 i : ℕ) : ℂ)) 0) ^ m)
    (htail : ∀ i < 3, ∀ s < 2, lineNormalPolynomial R d i ∈
      (Nagata.W18.nestedPointIdeal (-((s + 2 : ℕ) : ℂ)) 0) ^ m)
    (hN : quotientNormalPolynomial R d (Nagata.Workers.W24.homogeneousLineUnion ℂ 3) ≠ 0)
    (hc : c ≠ 0)
    (htenth : lineNormalPolynomial R d 0 ∈ (Nagata.W18.nestedPointIdeal U c) ^ m) :
    3 * m < d :=
…

Mentions: OAI.Nagata.W03.LowDegree.lineNormalPolynomial, OAI.Nagata.W18.nestedPointIdeal, OAI.Nagata.W03.LowDegree.quotientNormalPolynomial, OAI.Nagata.Workers.W24.homogeneousLineUnion

abbrev OAI.Nagata.W03.LowDegree.TriangleIndex line 396
def OAI.Nagata.W03.LowDegree.triangleComponent line 398
def OAI.Nagata.W03.LowDegree.triangleBasePoint line 401
def OAI.Nagata.W03.LowDegree.triangleDisplacement line 404
theorem OAI.Nagata.W03.LowDegree.triangle_configuration_count_and_injective line 408
Source documentation
This actual ordered index set has exactly r distinct base points.
```
theorem triangle_configuration_count_and_injective (r : ℕ) (hr : 9 ≤ r) :
    Fintype.card (TriangleIndex r) = r ∧ Function.Injective (triangleBasePoint r) := by
…
```
Mentions: OAI.Nagata.W03.LowDegree.TriangleIndex, OAI.Nagata.W03.LowDegree.triangleBasePoint
theorem OAI.Nagata.W03.LowDegree.degree_gt_three_mul_on_triangle_configuration line 417
Source documentation
On the actual r-point configuration, surface orders of the normal polynomial force d>3m; the case r=10 and all larger r are treated uniformly.
```
theorem degree_gt_three_mul_on_triangle_configuration
    (r d m : ℕ) (hr : 10 ≤ r) (hm : 0 < m)
    (R : ℕ → MvPolynomial (Fin 3) ℂ)
    (hhom : ∀ j ≤ d / 3, (R j).IsHomogeneous (d - 3 * j))
    (hN : quotientNormalPolynomial R d (Nagata.Workers.W24.homogeneousLineUnion ℂ 3) ≠ 0)
    (horder : ∀ p : TriangleIndex r,
      lineNormalPolynomial R d (triangleComponent p) ∈
        (Nagata.W18.nestedPointIdeal (triangleBasePoint r p).1 (triangleDisplacement p)) ^ m) :
    3 * m < d := by
…
```
Mentions: OAI.Nagata.W03.LowDegree.quotientNormalPolynomial, OAI.Nagata.Workers.W24.homogeneousLineUnion, OAI.Nagata.W03.LowDegree.TriangleIndex, OAI.Nagata.W03.LowDegree.lineNormalPolynomial, OAI.Nagata.W03.LowDegree.triangleComponent, OAI.Nagata.W18.nestedPointIdeal, OAI.Nagata.W03.LowDegree.triangleBasePoint, OAI.Nagata.W03.LowDegree.triangleDisplacement
theorem OAI.Nagata.W03.LowDegree.degree_gt_three_mul_of_selected_lifts_on_triangle line 441