FullTarget.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Coordinate and ordinary-multiplicity assemblies of the full target

def OAI.Nagata.W13.FullNagataOrdinary line 27
Source documentation
The unchanged full baseline quantifier pattern, with each multiplicity lower bound written as an inequality between actual natural numbers.
```
def FullNagataOrdinary : Prop :=
…
```
theorem OAI.Nagata.W13.fullNagata_iff_ordinary line 41
Source documentation
Numerical ordinary multiplicity gives exactly the original lower-bound predicate at every point, hence exactly the full baseline proposition.
```
theorem fullNagata_iff_ordinary : Nagata.FullNagata ↔ FullNagataOrdinary := by
…
```
Mentions: OAI.Nagata.W13.FullNagataOrdinary
def OAI.Nagata.W13.FullNagataClassOrdinary line 63
Source documentation
The equivalent numerical formulation for projective classes of nonzero homogeneous equations. Classes identify only nonzero scalar multiples, not zero loci or radicals; reducible and nonreduced equations remain represented.
```
def FullNagataClassOrdinary : Prop :=
…
```
theorem OAI.Nagata.W13.ordinary_iff_classOrdinary line 77
Source documentation
Passing between a nonzero equation and its scalar class preserves its numerical ordinary multiplicity and the very same exceptional sequence.
```
theorem ordinary_iff_classOrdinary : FullNagataOrdinary ↔ FullNagataClassOrdinary := by
…
```
Mentions: OAI.Nagata.W13.FullNagataOrdinary, OAI.Nagata.W13.FullNagataClassOrdinary
theorem OAI.Nagata.W13.fullNagata_iff_classOrdinary line 94

theorem OAI.Nagata.W13.square_veryGeneral line 121

Source documentation

For k≥4, one proper closed exceptional sequence with nonempty complement handles all curves and unequal multiplicity vectors at k² projective points. This assembles the already-proved outside-union inequality without reproving it.

theorem square_veryGeneral (k : ℕ) (hk : 4 ≤ k) :
    ∃ E : ℕ → Set (OrderedDistinctPoints (k * k)),
      (∀ n, IsConfigurationZariskiClosed (E n) ∧ E n ≠ Set.univ) ∧
      (∃ p : OrderedDistinctPoints (k * k), ∀ n, p ∉ E n) ∧
      ∀ p : OrderedDistinctPoints (k * k), (∀ n, p ∉ E n) →
        ∀ (d : ℕ), 1 ≤ d →
        ∀ F : MvPolynomial (Fin 3) ℂ, F ≠ 0 → F.IsHomogeneous d →
        ∀ m : Fin (k * k) → ℕ,
          (∀ i, multiplicityAtLeast F (p.val i) (m i)) →
          (∑ i, (m i : ℝ)) < (d : ℝ) * Real.sqrt ((k * k : ℕ) : ℝ) := by
…

theorem OAI.Nagata.W13.square_veryGeneral_of_isSquare line 141

Source documentation

Exactly the original target's quantifiers, restricted explicitly to square r≥10; no restriction to uniform multiplicities or reduced equations appears.

theorem square_veryGeneral_of_isSquare (r : ℕ) (hr : 10 ≤ r) (hsquare : IsSquare 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) →
        ∀ (d : ℕ), 1 ≤ d →
        ∀ F : MvPolynomial (Fin 3) ℂ, F ≠ 0 → F.IsHomogeneous d →
        ∀ m : Fin r → ℕ,
          (∀ i, multiplicityAtLeast F (p.val i) (m i)) →
          (∑ i, (m i : ℝ)) < (d : ℝ) * Real.sqrt (r : ℝ) := by
…

theorem OAI.Nagata.W13.square_veryGeneral_ordinary line 158

Source documentation

The same square result using actual natural-number ordinary multiplicities, while preserving every raw polynomial and multiplicity-vector quantifier.

theorem square_veryGeneral_ordinary (r : ℕ) (hr : 10 ≤ r) (hsquare : IsSquare 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) →
        ∀ (d : ℕ), 1 ≤ d →
        ∀ (F : MvPolynomial (Fin 3) ℂ) (hFne : F ≠ 0) (hFhom : F.IsHomogeneous d),
        ∀ m : Fin r → ℕ,
          (∀ i, m i ≤ formOrdinaryMultiplicity ⟨F, hFhom, hFne⟩ (p.val i)) →
          (∑ i, (m i : ℝ)) < (d : ℝ) * Real.sqrt (r : ℝ) := by
…

theorem OAI.Nagata.W13.square_veryGeneral_classOrdinary line 178

Source documentation

The same strict square theorem for scalar classes of equations and numerical ordinary multiplicities. Classes identify scalar multiples, not radicals.

theorem square_veryGeneral_classOrdinary (r : ℕ) (hr : 10 ≤ r) (hsquare : IsSquare 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) →
        ∀ (d : ℕ), 1 ≤ d →
        ∀ C : W16.PlaneEquationClass d,
        ∀ m : Fin r → ℕ,
          (∀ i, m i ≤ classOrdinaryMultiplicity C (p.val i)) →
          (∑ i, (m i : ℝ)) < (d : ℝ) * Real.sqrt (r : ℝ) := by
…

Mentions: OAI.Nagata.W16.PlaneEquationClass

theorem OAI.Nagata.W13.fullNagata_of_nonsquare_interior_exclusion line 212
Source documentation
Once genuine universal systems in the nonsquare interior are excluded, the unchanged original full coordinate target follows. Every other branch and the single simultaneous exceptional sequence are supplied by checked proofs.
```
theorem fullNagata_of_nonsquare_interior_exclusion
    (hinterior : ∀ r : ℕ, 10 ≤ r → ¬ IsSquare r → ∀ d m : ℕ,
      0 < d → 0 < m → 3 < (d : ℝ) / m → (d : ℝ) / m < Real.sqrt r →
      ¬ UniversalSupport r d (fun _ => m)) : Nagata.FullNagata := by
…
```
Mentions: OAI.Nagata.W13.UniversalSupport
theorem OAI.Nagata.W13.fullNagataOrdinary_of_nonsquare_interior_exclusion line 227
Source documentation
The same conditional assembly concludes the proved-equivalent formulation with numerical ordinary multiplicities and identical original quantifiers.
```
theorem fullNagataOrdinary_of_nonsquare_interior_exclusion
    (hinterior : ∀ r : ℕ, 10 ≤ r → ¬ IsSquare r → ∀ d m : ℕ,
      0 < d → 0 < m → 3 < (d : ℝ) / m → (d : ℝ) / m < Real.sqrt r →
      ¬ UniversalSupport r d (fun _ => m)) : FullNagataOrdinary :=
…
```
Mentions: OAI.Nagata.W13.UniversalSupport, OAI.Nagata.W13.FullNagataOrdinary
theorem OAI.Nagata.W13.fullNagata_of_genuine_source_construction line 246