Nagata.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Nagata's inequality for very general complex plane configurations; Equivalence of homogeneous-coordinate and effective-cycle statements

def OAI.Nagata.Workers.W10.FullNagataCurves line 19
Source documentation
Full strict simultaneous target on genuine nonzero effective curve cycles. No square-only, equal-multiplicity, degree, or reducedness restriction is added.
```
def FullNagataCurves : Prop :=
…
```
theorem OAI.Nagata.Workers.W10.fullNagata_iff_effectiveCurves line 31
Source documentation
Both full statements use exactly the same simultaneous exceptional union. The proof transports degree and all local orders through the proved cycle bridge.
```
theorem fullNagata_iff_effectiveCurves : Nagata.FullNagata ↔ FullNagataCurves := by
…
```
Mentions: OAI.Nagata.Workers.W10.FullNagataCurves
def OAI.Nagata.Workers.W10.FullNagataEffectiveCurves line 68
Source documentation
One exceptional union handles every genuine effective curve and every unequal nonnegative multiplicity vector. All positive degrees, reducible curves and repeated components remain quantified.
```
def FullNagataEffectiveCurves : Prop :=
…
```
theorem OAI.Nagata.Workers.W10.fullNagataCurves_iff_ordinary line 78
theorem OAI.Nagata.Workers.W10.fullNagata_iff_genuineEffectiveCurves line 82
theorem OAI.Nagata.W13.nagata_full line 102
Source documentation
The unchanged full coordinate statement, for every square and nonsquare r≥10, all positive degrees, and all nonnegative unequal multiplicity vectors. No geometric construction or universal-exclusion premise remains.
```
theorem nagata_full : Nagata.FullNagata := by
…
```
theorem OAI.Nagata.W13.nagata_full_ordinary line 113
Source documentation
Full numerical ordinary-multiplicity formulation for nonzero homogeneous plane equations; the same simultaneous quantifier pattern is retained.
```
theorem nagata_full_ordinary : FullNagataOrdinary :=
…
```
Mentions: OAI.Nagata.W13.FullNagataOrdinary
theorem OAI.Nagata.W13.nagata_full_classOrdinary line 118
Source documentation
Full numerical ordinary-multiplicity statement for scalar classes of nonzero equations, retaining reducible and nonreduced structure.
```
theorem nagata_full_classOrdinary : FullNagataClassOrdinary :=
…
```
Mentions: OAI.Nagata.W13.FullNagataClassOrdinary
theorem OAI.Nagata.W13.nagata_full_effectiveCurves line 123
Source documentation
The full strict theorem for genuine nonzero effective plane-curve cycles, with their actual degree and numerical ordinary multiplicities.
```
theorem nagata_full_effectiveCurves : Workers.W10.FullNagataEffectiveCurves :=
…
```
Mentions: OAI.Nagata.Workers.W10.FullNagataEffectiveCurves

theorem OAI.Nagata.nagata_conjecture line 148

Source documentation

One countable proper closed exceptional union works simultaneously for all nonzero effective plane curves and all unequal nonnegative multiplicities.

Distinct definitions of this name: ComparatorChallenges/Nagata.lean:352 (different declaration text). Qualify references as OAI.Nagata.nagata_conjecture@path.

theorem nagata_conjecture :
    ∀ r : ℕ, 10 ≤ r →
      ∃ E : ℕ → Set (OrderedDistinctPoints r),
        (∀ n, IsConfigurationZariskiClosed (E n) ∧ E n ≠ Set.univ) ∧
        (∃ p : OrderedDistinctPoints r, ∀ n, p ∉ E n) ∧
        ∀ p : OrderedDistinctPoints r, (∀ n, p ∉ E n) →
          ∀ C : Workers.W10.EffectivePlaneCurve, ∀ m : Fin r → ℕ,
            (∀ i, m i ≤ W15.curveOrdinaryMultiplicity C (p.val i)) →
            (∑ i, (m i : ℝ)) <
              (Workers.W10.curveDegree C : ℝ) * Real.sqrt (r : ℝ) :=
…

theorem OAI.Nagata.nagata_conjecture_coordinates line 162
Source documentation
The original complete coordinate statement, including every degree d≥1, all nonzero homogeneous equations and all nonnegative multiplicity bounds.
Distinct definitions of this name: ComparatorChallenges/Nagata.lean:365 (same statement text; different proof or body). Qualify references as OAI.Nagata.nagata_conjecture_coordinates@path.
```
theorem nagata_conjecture_coordinates : FullNagata := W13.nagata_full
…
```
Mentions: OAI.Nagata.W13.nagata_full