SquareNormal.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Normal evaluation and obstructions for square line arrangements

theorem OAI.Nagata.Workers.W24.exists_displacement_outside_homogeneousEvaluation line 18
Source documentation
At any k² chosen coordinate representatives, degree-k plane forms have an evaluation image of dimension strictly below k² for k≥4.
```
theorem exists_displacement_outside_homogeneousEvaluation {ι : Type*} [Fintype ι]
    (k : ℕ) (hk : 4 ≤ k) (hcard : Fintype.card ι = k * k)
    (a : ι → Fin 3 → ℂ) :
    ∃ c : ι → ℂ, c ∉ (homogeneousEvaluation k a).range := by
…
```
Mentions: OAI.Nagata.Workers.W24.homogeneousEvaluation
theorem OAI.Nagata.Workers.W24.exists_grid_displacement line 30
Source documentation
The precise ordered grid of k marks on each of k lines.
```
theorem exists_grid_displacement (k : ℕ) (hk : 4 ≤ k)
    (a : Fin k × Fin k → Fin 3 → ℂ) :
    ∃ c : Fin k × Fin k → ℂ, c ∉ (homogeneousEvaluation k a).range := by
…
```
Mentions: OAI.Nagata.Workers.W24.homogeneousEvaluation

theorem OAI.Nagata.Workers.W24.normal_top_coefficients_zero line 50

Source documentation

Local surface orders at arbitrary normal displacements force the highest coefficient to vanish on every component when its index is below m.

theorem normal_top_coefficients_zero {K : Type*} [Field K] [CharZero K]
    (k m J : ℕ) (hk : 3 ≤ k) (hJm : J < m)
    (H : ℕ → Polynomial (Polynomial K))
    (cFirst : ℕ → K) (cTail : ℕ → ℕ → K)
    (hdegree : ∀ i < k, (H i).natDegree ≤ J)
    (hbase : ∀ i < k, ((H i).coeff J).natDegree ≤ k * (m - J))
    (hfirst : ∀ i < k, H i ∈
      (nestedPointIdeal (-((firstMark k i : ℕ) : K)) (cFirst i)) ^ m)
    (htail : ∀ i < k, ∀ s < k - 1, H i ∈
      (nestedPointIdeal (-((s + 2 : ℕ) : K)) (cTail i s)) ^ m)
    (hglue : ∀ i < k, ∀ j < k,
      ((H i).coeff J).eval ((i + j : ℕ) : K) =
…

theorem OAI.Nagata.Workers.W24.normal_top_index_eq_and_degree_eq line 78

Source documentation

A nonzero highest component, together with the degree-weight bound, forces the last possible index and the square equality d=k*m.

theorem normal_top_index_eq_and_degree_eq {K : Type*} [Field K] [CharZero K]
    (k d m J : ℕ) (hk : 3 ≤ k) (hd : d ≤ k * m) (hweight : k * J ≤ d)
    (H : ℕ → Polynomial (Polynomial K))
    (cFirst : ℕ → K) (cTail : ℕ → ℕ → K)
    (hdegree : ∀ i < k, (H i).natDegree ≤ J)
    (hbase : ∀ i < k, ((H i).coeff J).natDegree ≤ d - k * J)
    (hfirst : ∀ i < k, H i ∈
      (nestedPointIdeal (-((firstMark k i : ℕ) : K)) (cFirst i)) ^ m)
    (htail : ∀ i < k, ∀ s < k - 1, H i ∈
      (nestedPointIdeal (-((s + 2 : ℕ) : K)) (cTail i s)) ^ m)
    (hglue : ∀ i < k, ∀ j < k,
      ((H i).coeff J).eval ((i + j : ℕ) : K) =
…

theorem OAI.Nagata.Workers.W24.normal_evaluation_contradiction line 117

Source documentation

A constant nonzero highest coefficient turns the local order equations into an impossible evaluation vector when the displacement is outside the image.

theorem normal_evaluation_contradiction {K V ι : Type*} [Field K] [CharZero K]
    [AddCommGroup V] [Module K V]
    (E : V →ₗ[K] (ι → K)) (c : ι → K) (hc : c ∉ E.range)
    (m : ℕ) (hm : 0 < m) (a : K) (ha : a ≠ 0)
    (H : ι → Polynomial (Polynomial K)) (base : ι → K)
    (hdegree : ∀ i, (H i).natDegree ≤ m)
    (horder : ∀ i, H i ∈ (nestedPointIdeal (base i) (c i)) ^ m)
    (htop : ∀ i, ((H i).coeff m).eval (base i) = a)
    (s : V) (hprevious : ∀ i, E s i = ((H i).coeff (m - 1)).eval (base i)) :
    False := by
…

def OAI.Nagata.Workers.W24.planeNormalOnLine line 149
Source documentation
The literal normal polynomial restricted coefficientwise to component i.
```
def planeNormalOnLine (F : Polynomial (MvPolynomial (Fin 3) ℂ)) (i : ℕ) :
    Polynomial (Polynomial ℂ) := F.map (Nagata.W04.ReducibleSquare.lineRestriction (i : ℂ))
```
Mentions: OAI.Nagata.W04.ReducibleSquare.lineRestriction
theorem OAI.Nagata.Workers.W24.planeNormalOnLine_coeff line 152
theorem OAI.Nagata.Workers.W24.lineRestriction_union_zero line 157

theorem OAI.Nagata.Workers.W24.plane_normal_top_index_eq_and_degree_eq line 164

Source documentation

A nonzero quotient normal polynomial with actual homogeneous plane lifts and local marked orders has last index m and exact equality degree k*m.

theorem plane_normal_top_index_eq_and_degree_eq
    (k d m : ℕ) (hk : 3 ≤ k) (hd : d ≤ k * m)
    (F : Polynomial (MvPolynomial (Fin 3) ℂ))
    (hhom : ∀ j, (F.coeff j).IsHomogeneous (d - k * j))
    (hweight : ∀ j, F.coeff j ≠ 0 → k * j ≤ d)
    (hne : normalResiduePolynomial (homogeneousLineUnion ℂ k) F ≠ 0)
    (cFirst : ℕ → ℂ) (cTail : ℕ → ℕ → ℂ)
    (hfirst : ∀ i < k, planeNormalOnLine F i ∈
      (nestedPointIdeal (-((firstMark k i : ℕ) : ℂ)) (cFirst i)) ^ m)
    (htail : ∀ i < k, ∀ s < k - 1, planeNormalOnLine F i ∈
      (nestedPointIdeal (-((s + 2 : ℕ) : ℂ)) (cTail i s)) ^ m) :
    (normalResiduePolynomial (homogeneousLineUnion ℂ k) F).natDegree = m ∧ d = k * m := by
…

Mentions: OAI.Nagata.Workers.W24.normalResiduePolynomial, OAI.Nagata.Workers.W24.homogeneousLineUnion, OAI.Nagata.Workers.W24.planeNormalOnLine

def OAI.Nagata.Workers.W24.componentCoordinates line 212
Source documentation
Literal normalized homogeneous coordinates on a selected line.
```
def componentCoordinates (i : ℕ) (a : ℂ) : Fin 3 → ℂ :=
…
```

theorem OAI.Nagata.Workers.W24.plane_normal_equality_contradiction line 218

Source documentation

The square equality case is impossible for an outside-image displacement. The central object is an actual polynomial with homogeneous plane coefficients; only its local normal-point orders are an input from specialization.

theorem plane_normal_equality_contradiction {ι : Type*}
    (k m : ℕ) (hm : 0 < m)
    (component : ι → Fin k) (base c : ι → ℂ)
    (hc : c ∉ (homogeneousEvaluation k
      (fun i => componentCoordinates (component i).val (base i))).range)
    (F : Polynomial (MvPolynomial (Fin 3) ℂ))
    (hhom : ∀ j, (F.coeff j).IsHomogeneous (k * m - k * j))
    (hne : normalResiduePolynomial (homogeneousLineUnion ℂ k) F ≠ 0)
    (hindex : (normalResiduePolynomial (homogeneousLineUnion ℂ k) F).natDegree = m)
    (horder : ∀ i, planeNormalOnLine F (component i).val ∈
      (nestedPointIdeal (base i) (c i)) ^ m) : False := by
…

Mentions: OAI.Nagata.Workers.W24.homogeneousEvaluation, OAI.Nagata.Workers.W24.componentCoordinates, OAI.Nagata.Workers.W24.normalResiduePolynomial, OAI.Nagata.Workers.W24.homogeneousLineUnion, OAI.Nagata.Workers.W24.planeNormalOnLine

def OAI.Nagata.Workers.W24.squareMarkedBase line 275
def OAI.Nagata.Workers.W24.squareMarkedCoordinates line 278
theorem OAI.Nagata.Workers.W24.squareMarkedCoordinates_eq line 282
Source documentation
The base points are exactly the actual marked affine configuration.
```
theorem squareMarkedCoordinates_eq (k : ℕ) (p : Fin k × Fin k) :
    squareMarkedCoordinates k p =
      ![(markedPoint ℂ k p.1 p.2).1, (markedPoint ℂ k p.1 p.2).2, 1] := rfl
```
Mentions: OAI.Nagata.Workers.W24.squareMarkedCoordinates

theorem OAI.Nagata.Workers.W24.square_normal_obstruction line 289

Source documentation

All source-constructed homogeneous lifts are excluded by a single outside-image displacement. The local multiplicity condition is an actual ideal-power condition on literal coefficientwise line restrictions.

theorem square_normal_obstruction (k d m : ℕ) (hk : 4 ≤ k) (hm : 0 < m)
    (hd : d ≤ k * m) (c : Fin k × Fin k → ℂ)
    (hc : c ∉ (homogeneousEvaluation k (squareMarkedCoordinates k)).range)
    (F : Polynomial (MvPolynomial (Fin 3) ℂ))
    (hhom : ∀ j, (F.coeff j).IsHomogeneous (d - k * j))
    (hweight : ∀ j, F.coeff j ≠ 0 → k * j ≤ d)
    (hne : normalResiduePolynomial (homogeneousLineUnion ℂ k) F ≠ 0)
    (horder : ∀ p : Fin k × Fin k, planeNormalOnLine F p.1.val ∈
      (nestedPointIdeal (squareMarkedBase k p) (c p)) ^ m) : False := by
…

Mentions: OAI.Nagata.Workers.W24.homogeneousEvaluation, OAI.Nagata.Workers.W24.squareMarkedCoordinates, OAI.Nagata.Workers.W24.normalResiduePolynomial, OAI.Nagata.Workers.W24.homogeneousLineUnion, OAI.Nagata.Workers.W24.planeNormalOnLine, OAI.Nagata.Workers.W24.squareMarkedBase

theorem OAI.Nagata.Workers.W24.exists_square_normal_obstruction line 322

Source documentation

One displacement excludes all degrees and positive multiplicities in the square slope range at once, for genuine normal polynomials with plane lifts.

theorem exists_square_normal_obstruction (k : ℕ) (hk : 4 ≤ k) :
    ∃ c : Fin k × Fin k → ℂ, ∀ d m : ℕ, 0 < m → d ≤ k * m →
      ∀ F : Polynomial (MvPolynomial (Fin 3) ℂ),
      (∀ j, (F.coeff j).IsHomogeneous (d - k * j)) →
      (∀ j, F.coeff j ≠ 0 → k * j ≤ d) →
      normalResiduePolynomial (homogeneousLineUnion ℂ k) F ≠ 0 →
      ¬ (∀ p : Fin k × Fin k, planeNormalOnLine F p.1.val ∈
        (nestedPointIdeal (squareMarkedBase k p) (c p)) ^ m) := by
…

Mentions: OAI.Nagata.Workers.W24.normalResiduePolynomial, OAI.Nagata.Workers.W24.homogeneousLineUnion, OAI.Nagata.Workers.W24.planeNormalOnLine, OAI.Nagata.Workers.W24.squareMarkedBase