Incidence.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Projective incidence and closed multiplicity support loci; Geometric realization of universal multiplicity reduction

theorem OAI.Nagata.Workers.W25.guarded_chart_gluing line 20

Source documentation

Equations attached to an open-chart cover glue when each equation vanishes outside its own chart. No finiteness is needed for this logical step.

theorem guarded_chart_gluing {C X : Type*} {I : C → Type*}
    (U : C → X → Prop) (Z : (c : C) → I c → X → Prop) (S : X → Prop)
    (hcover : ∀ x, ∃ c, U c x)
    (houtside : ∀ c e x, ¬ U c x → Z c e x)
    (hlocal : ∀ c x, U c x → (S x ↔ ∀ e, Z c e x)) :
    ∀ x, S x ↔ ∀ c e, Z c e x := by
…

def OAI.Nagata.ProjectiveGeometry.guardedEquation line 53
Source documentation
An actual guarded multihomogeneous extension of an affine chart equation.
```
def guardedEquation {r : ℕ} (c : ConfigurationChart r)
    (f : MvPolynomial (Fin r × Fin 2) ℂ) : MultihomogeneousEquation r where
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.ConfigurationChart
theorem OAI.Nagata.ProjectiveGeometry.guardedEquation_vanishes_outside line 59
theorem OAI.Nagata.ProjectiveGeometry.guardedEquation_vanishes_iff line 69
Source documentation
Inside its own chart, the guarded homogeneous equation has exactly the same zeros as the original affine polynomial.
```
theorem guardedEquation_vanishes_iff {r : ℕ} (c : ConfigurationChart r)
    (f : MvPolynomial (Fin r × Fin 2) ℂ) (p : Fin r → PlanePoint)
    (hp : InConfigurationChart c p) :
    equationVanishes (guardedEquation c f) p ↔
      MvPolynomial.eval (configurationChartCoordinates₂ c p) f = 0 := by
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.ConfigurationChart, OAI.Nagata.ProjectiveGeometry.PlanePoint, OAI.Nagata.ProjectiveGeometry.InConfigurationChart, OAI.Nagata.ProjectiveGeometry.guardedEquation, OAI.Nagata.ProjectiveGeometry.configurationChartCoordinates₂
def OAI.Nagata.ProjectiveGeometry.productCommonZeroLocus line 78
theorem OAI.Nagata.ProjectiveGeometry.isProductZariskiClosed_commonZeroLocus line 82
theorem OAI.Nagata.ProjectiveGeometry.productClosed_of_chart_polynomial_equations line 96
Source documentation
The ambient version of chartwise polynomial closedness, needed to identify the multihomogeneous topology with the standard simultaneous affine charts.
```
theorem productClosed_of_chart_polynomial_equations {r : ℕ}
    {I : ConfigurationChart r → Type*}
    (f : (c : ConfigurationChart r) → I c → MvPolynomial (Fin r × Fin 2) ℂ)
    (S : Set (Fin r → PlanePoint))
    (hlocal : ∀ c p, InConfigurationChart c p →
      (p ∈ S ↔ ∀ e, MvPolynomial.eval (configurationChartCoordinates₂ c p) (f c e) = 0)) :
    IsProductZariskiClosed S := by
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.ConfigurationChart, OAI.Nagata.ProjectiveGeometry.PlanePoint, OAI.Nagata.ProjectiveGeometry.InConfigurationChart, OAI.Nagata.ProjectiveGeometry.configurationChartCoordinates₂

theorem OAI.Nagata.ProjectiveGeometry.configurationClosed_of_guarded_equations line 125

Source documentation

Guarded polynomial equations on all charts produce a relatively closed subset of the actual ordered configuration space. Each hypothesis is a concrete vanishing identity or chart membership statement.

theorem configurationClosed_of_guarded_equations {r : ℕ}
    {I : ConfigurationChart r → Type*}
    (G : (c : ConfigurationChart r) → I c → MultihomogeneousEquation r)
    (S : Set (OrderedDistinctPoints r))
    (houtside : ∀ c e (p : OrderedDistinctPoints r),
      ¬ InConfigurationChart c p.val → equationVanishes (G c e) p.val)
    (hlocal : ∀ c p, InConfigurationChart c p.val →
      (p ∈ S ↔ ∀ e, equationVanishes (G c e) p.val)) :
    IsConfigurationZariskiClosed S := by
…

Mentions: OAI.Nagata.ProjectiveGeometry.ConfigurationChart, OAI.Nagata.ProjectiveGeometry.InConfigurationChart

theorem OAI.Nagata.ProjectiveGeometry.configurationClosed_of_chart_polynomial_equations line 151
Source documentation
Polynomial equations in every simultaneous affine chart glue to the genuine multihomogeneous Zariski closedness definition. The guarding polynomials, boundary vanishing, and normalization factors are all constructed above.
```
theorem configurationClosed_of_chart_polynomial_equations {r : ℕ}
    {I : ConfigurationChart r → Type*}
    (f : (c : ConfigurationChart r) → I c → MvPolynomial (Fin r × Fin 2) ℂ)
    (S : Set (OrderedDistinctPoints r))
    (hlocal : ∀ c p, InConfigurationChart c p.val →
      (p ∈ S ↔ ∀ e, MvPolynomial.eval (configurationChartCoordinates₂ c p.val) (f c e) = 0)) :
    IsConfigurationZariskiClosed S := by
…
```
Mentions: OAI.Nagata.ProjectiveGeometry.ConfigurationChart, OAI.Nagata.ProjectiveGeometry.InConfigurationChart, OAI.Nagata.ProjectiveGeometry.configurationChartCoordinates₂
theorem OAI.Nagata.ProjectiveGeometry.multiplicityAtLeast_iff_directChart line 187
theorem OAI.Nagata.ProjectiveGeometry.supportLocus_iff_chart_minors line 198
Source documentation
On any containing simultaneous chart the genuine projective support locus is exactly the zero set of the actual global-form matrix minors.
```
theorem supportLocus_iff_chart_minors (r : ℕ) (index : Workers.W25.IncidenceIndex r)
    (c : ConfigurationChart r) (p : OrderedDistinctPoints r)
    (hp : InConfigurationChart c p.val) :
    p ∈ W13.supportLocus r index ↔
      ∀ s : W27.HomogeneousMonomial index.1.val → W27.PlaneJet r index.2,
        MvPolynomial.eval (configurationChartCoordinates₂ c p.val)
          (W27.minorPolynomial (W27.chartPlaneJetMatrix (R := ℂ) c index.1.val index.2) s) = 0 := by
…
```
Mentions: OAI.Nagata.Workers.W25.IncidenceIndex, OAI.Nagata.ProjectiveGeometry.ConfigurationChart, OAI.Nagata.ProjectiveGeometry.InConfigurationChart, OAI.Nagata.W13.supportLocus, OAI.Nagata.W27.HomogeneousMonomial, OAI.Nagata.W27.PlaneJet, OAI.Nagata.ProjectiveGeometry.configurationChartCoordinates₂, OAI.Nagata.W27.minorPolynomial, OAI.Nagata.W27.chartPlaneJetMatrix
theorem OAI.Nagata.ProjectiveGeometry.supportLocus_isConfigurationZariskiClosed line 228
Source documentation
Closedness required by manuscript §1, Lemma lem:universal, for every positive degree and every unequal nonnegative multiplicity vector.
```
theorem supportLocus_isConfigurationZariskiClosed (r : ℕ)
    (index : Workers.W25.IncidenceIndex r) :
    IsConfigurationZariskiClosed (W13.supportLocus r index) := by
…
```
Mentions: OAI.Nagata.Workers.W25.IncidenceIndex, OAI.Nagata.W13.supportLocus

theorem OAI.Nagata.W13.universal_reduction line 264

Source documentation

The full source universal reduction for genuine projective configurations, actual homogeneous forms, and ordinary chart ideal-power conditions.

theorem universal_reduction (r : ℕ) (hr : 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) →
        ∀ (d : ℕ), 1 ≤ d →
        ∀ F : MvPolynomial (Fin 3) ℂ, F ≠ 0 → F.IsHomogeneous d →
        ∀ m : Fin r → ℕ,
          (∀ i, multiplicityAtLeast F (p.val i) (m i)) →
          (d : ℝ) * Real.sqrt r ≤ ∑ i, (m i : ℝ) →
          ∃ D M : ℕ, 0 < D ∧ 0 < M ∧ (D : ℝ) / M ≤ Real.sqrt r ∧
            UniversalSupport r D (fun _ => M) :=
…

Mentions: OAI.Nagata.W13.UniversalSupport

theorem OAI.Nagata.W13.strict_bound_of_no_universal line 282

Source documentation

Conditional consequence: actual projective closedness is supplied, but excluding all positive equal-multiplicity universal systems remains an explicit input, including the square-case equality boundary.

theorem strict_bound_of_no_universal (r : ℕ) (hr : 10 ≤ r)
    (hno : ∀ D M : ℕ, 0 < D → 0 < M →
      (D : ℝ) / M ≤ Real.sqrt r → ¬ UniversalSupport r D (fun _ => M)) :
    ∃ 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 :=
…

Mentions: OAI.Nagata.W13.UniversalSupport