SquareReduction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Universal and very general square-configuration reduction

theorem OAI.Nagata.Workers.W24.marked_directChart_partial_ne_zero line 17
theorem OAI.Nagata.Workers.W24.square_universalSupport_degree_gt line 27
Source documentation
Strict square-case degree bound, including all nonzero reducible and nonreduced homogeneous equations in the genuine universal-system definition.
```
theorem square_universalSupport_degree_gt (k d m : ℕ) (hk : 4 ≤ k) (hm : 0 < m)
    (hU : Nagata.W13.UniversalSupport (k * k) d (fun _ => m)) : k * m < d := by
…
```
Mentions: OAI.Nagata.W13.UniversalSupport

theorem OAI.Nagata.Workers.W24.square_strict_inequality_outside_supportExceptionalUnion line 72

Source documentation

All unequal multiplicity vectors simultaneously satisfy the strict square bound outside the one actual support exceptional union.

theorem square_strict_inequality_outside_supportExceptionalUnion
    (k : ℕ) (hk : 4 ≤ k) (p : OrderedDistinctPoints (k * k))
    (hp : p ∉ Nagata.W13.supportExceptionalUnion (k * k))
    (d : ℕ) (hd : 0 < d) (m : Fin (k * k) → ℕ)
    (F : MvPolynomial (Fin 3) ℂ) (hne : F ≠ 0) (hhom : F.IsHomogeneous d)
    (hmult : ∀ i, multiplicityAtLeast F (p.val i) (m i)) :
    (d : ℝ) * Real.sqrt ((k * k : ℕ) : ℝ) > ∑ i, (m i : ℝ) := by
…

Mentions: OAI.Nagata.W13.supportExceptionalUnion