CoverNormal.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Universal normal polynomials on line and smooth curve coverings

theorem OAI.Nagata.Workers.W17.indexedPlaneFamily_chart_orders line 21

Source documentation

A polynomial kernel family specializes to actual chart ideal powers.

theorem indexedPlaneFamily_chart_orders {r d : ℕ} (m : Fin r → ℕ)
    (c : Fin r → Fin 3) (p : Fin r × Fin 2 → Polynomial ℂ)
    (q : HomogeneousMonomial d → Polynomial ℂ)
    (hq : (parameterMatrix (chartPlaneJetMatrix c d m) p).mulVec q = 0)
    (s : ℂ) :
    ∀ i, Nagata.AffineMultiplicity.orderAtLeast (fun j => (p (i,j)).eval s) (m i)
      (directChartHom (c i) ((indexedPlaneFamily d q).eval (MvPolynomial.C s))) := by
…

Mentions: OAI.Nagata.Workers.W17.indexedPlaneFamily

theorem OAI.Nagata.Workers.W17.universalSupport_polynomial_family line 41

Source documentation

The actual family is nonzero at parameter zero and homogeneous of degree d; all moving-configuration ordinary orders hold without a genericity assumption on the parameter after the polynomial kernel identity is established.

theorem universalSupport_polynomial_family {r d : ℕ} {m : Fin r → ℕ}
    (hU : Nagata.W13.UniversalSupport r d m)
    (c : Fin r → Fin 3) (p : Fin r × Fin 2 → Polynomial ℂ)
    (hbase : Function.Injective
      (configurationChartEmbedding c (fun ij => (p ij).eval 0))) :
    ∃ S : Polynomial (MvPolynomial (Fin 3) ℂ),
      S.coeff 0 ≠ 0 ∧ (∀ α, (S.coeff α).IsHomogeneous d) ∧
      ∀ s i, Nagata.AffineMultiplicity.orderAtLeast (fun j => (p (i,j)).eval s) (m i)
        (directChartHom (c i) (S.eval (MvPolynomial.C s))) := by
…

Mentions: OAI.Nagata.W13.UniversalSupport

theorem OAI.Nagata.Workers.W17.universalSupport_degree_bounded_normal_data line 66

Source documentation

The complete algebraic input to normal specialization comes from actual universal homogeneous equations along any distinct-based polynomial motion.

theorem universalSupport_degree_bounded_normal_data {r d : ℕ} {m : Fin r → ℕ}
    (hU : Nagata.W13.UniversalSupport r d m)
    (c : Fin r → Fin 3) (p : Fin r × Fin 2 → Polynomial ℂ)
    (hbase : Function.Injective
      (configurationChartEmbedding c (fun ij => (p ij).eval 0)))
    (G : MvPolynomial (Fin 3) ℂ) (k : ℕ)
    (hG : G.IsHomogeneous k) (hunit : ¬IsUnit G) (hk : 0 < k) :
    ∃ (I : Finset ℕ) (j : ℕ → ℕ) (T : ℕ → MvPolynomial (Fin 3) ℂ) (u : ℕ),
      (∀ α ∈ I, ¬G ∣ T α) ∧
      (∀ α ∈ I, j α ≤ d / k ∧ (T α).IsHomogeneous (d - k * j α)) ∧
      (∀ α ∈ I, u ≤ α + j α) ∧ u ≤ d / k ∧
      (I.filter (fun α => α + j α = u)).Nonempty ∧
…

Mentions: OAI.Nagata.W13.UniversalSupport

def OAI.Nagata.Workers.W17.planeCoordinate line 108
Source documentation
Ordered affine coordinates of an actual complex-plane point.
```
def planeCoordinate (p : ComplexPlane) (a : Fin 2) : ℂ := if a = 0 then p.1 else p.2
```
def OAI.Nagata.Workers.W17.affineCoordinateMotion line 111
Source documentation
A literal polynomial affine motion, valid for every parameter.
```
def affineCoordinateMotion (p V : ComplexPlane) (a : Fin 2) : Polynomial ℂ :=
…
```
theorem OAI.Nagata.Workers.W17.affineCoordinateMotion_eval line 114
def OAI.Nagata.Workers.W17.coveringNormalVelocity line 122
Source documentation
Vertical velocity lifting a prescribed covering-frame normal coordinate.
```
def coveringNormalVelocity (G : MvPolynomial (Fin 3) ℂ) (k : ℕ)
    (X : Fin 3 → ℂ → ℂ) (c : Fin 3) (z w : ℂ) : ComplexPlane :=
…
```
theorem OAI.Nagata.Workers.W17.coveringNormalVelocity_derivative line 128

theorem OAI.Nagata.Workers.W17.coveringMotion_base_injective line 140

Source documentation

The parameter-zero tuple of these motions is exactly the given genuine projective tuple in its selected affine charts.

theorem coveringMotion_base_injective {r : ℕ}
    (c : Fin r → Fin 3) (p V : Fin r → ComplexPlane)
    (hbase : Function.Injective (fun b => chartPoint₂ (c b) (planeCoordinate (p b)))) :
    Function.Injective (configurationChartEmbedding c
      (fun ba => (affineCoordinateMotion (p ba.1) (V ba.1) ba.2).eval 0)) := by
…

Mentions: OAI.Nagata.Workers.W17.planeCoordinate, OAI.Nagata.Workers.W17.affineCoordinateMotion

theorem OAI.Nagata.Workers.W17.universalSupport_selected_line_data line 166

Source documentation

Actual universal plane equations give selected homogeneous lifts with ordinary surface orders at every prescribed normal displacement.

theorem universalSupport_selected_line_data {r d : ℕ} {m : Fin r → ℕ}
    (hU : Nagata.W13.UniversalSupport r d m)
    (G : MvPolynomial (Fin 3) ℂ) (k : ℕ)
    (hG : G.IsHomogeneous k) (hk : 0 < k)
    (line ξ displacement : Fin r → ℂ)
    (hbase : Function.Injective (fun b : Fin r => (ξ b, (line b)^2 - line b * ξ b)))
    (hline : ∀ b, Nagata.W04.ReducibleSquare.lineRestriction (line b) G = 0)
    (hpartial : ∀ b, planePolynomialEval
      (MvPolynomial.pderiv 1 (Nagata.W27.directChartHom (2 : Fin 3) G))
      (ξ b, (line b)^2 - line b * ξ b) ≠ 0) :
    ∃ (indices : Finset ℕ) (j : ℕ → ℕ) (T : ℕ → MvPolynomial (Fin 3) ℂ) (u : ℕ),
      indices.Nonempty ∧ (∀ α ∈ indices, α + j α = u) ∧
…

Mentions: OAI.Nagata.W13.UniversalSupport, OAI.Nagata.W04.ReducibleSquare.lineRestriction, OAI.Nagata.W27.directChartHom

theorem OAI.Nagata.Workers.W17.universalSupport_covering_normal_polynomial line 260

theorem OAI.Nagata.Workers.W17.universalSupport_line_normal_polynomial line 337

Source documentation

Full literal normal-polynomial conclusion on finitely many smooth line components, with all multiplicity and prescribed-displacement quantifiers.

theorem universalSupport_line_normal_polynomial {r d : ℕ} {m : Fin r → ℕ}
    (hU : Nagata.W13.UniversalSupport r d m)
    (G : MvPolynomial (Fin 3) ℂ) (k : ℕ)
    (hG : G.IsHomogeneous k) (hk : 0 < k)
    (line ξ displacement : Fin r → ℂ)
    (hbase : Function.Injective (fun b : Fin r => (ξ b, (line b)^2 - line b * ξ b)))
    (hline : ∀ b, Nagata.W04.ReducibleSquare.lineRestriction (line b) G = 0)
    (hpartial : ∀ b, planePolynomialEval
      (MvPolynomial.pderiv 1 (Nagata.W27.directChartHom (2 : Fin 3) G))
      (ξ b, (line b)^2 - line b * ξ b) ≠ 0) :
    ∃ F : Polynomial (MvPolynomial (Fin 3) ℂ),
      (∀ n, (F.coeff n).IsHomogeneous (d - k*n)) ∧
…

Mentions: OAI.Nagata.W13.UniversalSupport, OAI.Nagata.W04.ReducibleSquare.lineRestriction, OAI.Nagata.W27.directChartHom

theorem OAI.Nagata.Workers.W17.universalSupport_smooth_covering_normal_polynomial line 379