TorusConfigurations.lean`

50 declarations, 0 contain sorry, 0 declared as axioms

Distinct embedded torus configurations and affine avoidance; Nonintegral differences of normalized marked parameters

theorem OAI.Nagata.W06.finite_affine_integer_preimages line 26
Source documentation
Integer preimages of a nonconstant real affine map in a bounded interval are finite.
```
theorem finite_affine_integer_preimages (a b R : ℝ) (ha : a ≠ 0) :
    {x : ℝ | |x| ≤ R ∧ ∃ k : ℤ, a * x + b = k}.Finite := by
…
```

theorem OAI.Nagata.W06.exists_delta_avoiding_affine_integers line 50

Source documentation

Simultaneous delta choice, with no additional finiteness hypothesis.

theorem exists_delta_avoiding_affine_integers {ι : Type*} [Finite ι]
    (a b : ι → ℝ) (ha : ∀ i, a i ≠ 0)
    {ρ B : ℝ} (hρ : 0 < ρ) (hB : ρ < B) :
    ∃ Δ : ℝ, 0 < Δ ∧ Δ < 1 / 2 ∧ ρ + Δ * ρ / 9 < B ∧
      ∀ i (k : ℤ), a i * Δ + b i ≠ k := by
…

theorem OAI.Nagata.W06.exists_source_nonintegral_delta line 77

Source documentation

The simultaneous nonintegrality requirements in the source, together with delta slack. The relation h = 3*(d-3*m) and positivity of d-3*j are retained explicitly.

theorem exists_source_nonintegral_delta {m u₀ : ℕ} {h d ρ ρstar B : ℝ}
    (hh : 0 < h) (hdegree : h = 3 * (d - 3 * (m : ℝ)))
    (hρ : 0 < ρ) (hB : ρ < B) :
    ∃ Δ : ℝ, 0 < Δ ∧ Δ < 1 / 2 ∧ ρ + Δ * ρ / 9 < B ∧
      (∀ (j : Fin (m + 1)) (k : ℤ),
        h / 9 * (ρstar - Δ) + ((m : ℝ) - (j.val : ℝ)) * ρstar ≠ k) ∧
      (∀ (j : Fin (u₀ + 1)), m < j.val → 0 < d - 3 * (j.val : ℝ) →
        ∀ k : ℤ, (h - 9 * ((j.val : ℝ) - (m : ℝ))) / 9 * (ρstar - Δ) ≠ k) := by
…

theorem OAI.Nagata.W06.TorusConfiguration.rayTorusPoint_injective_on_unit_interval line 141

Source documentation

Distinct exponents inside (0,1) define distinct actual torus points.

theorem rayTorusPoint_injective_on_unit_interval {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1) :
    Set.InjOn (fun s : ℝ => torusPointMk (positivePeriod τ hτ) (rayPoint τ s))
      (Set.Ioo 0 1) := by
…

def OAI.Nagata.W06.TorusConfiguration.coverTuple line 162
Source documentation
The fixed lifts followed by the q moving lifts in the common exponential chart.
```
def coverTuple (τ x0 : ℝ) (xi : Fin 9 → ℝ) {q : ℕ} (ξ : Fin q → ℂ) :
    Fin (9 + q) → ℂˣ :=
…
```

def OAI.Nagata.W06.TorusConfiguration.torusTuple line 168

Source documentation

The corresponding actual torus tuple.

def torusTuple (τ : ℝ) (hτ : 0 < τ) (x0 : ℝ) (xi : Fin 9 → ℝ)
    {q : ℕ} (ξ : Fin q → ℂ) : Fin (9 + q) → TorusPoint (positivePeriod τ hτ) :=
…

theorem OAI.Nagata.W06.TorusConfiguration.coverTuple_left line 172
theorem OAI.Nagata.W06.TorusConfiguration.coverTuple_right line 177
theorem OAI.Nagata.W06.TorusConfiguration.torusTuple_left line 182
theorem OAI.Nagata.W06.TorusConfiguration.torusTuple_right line 189
theorem OAI.Nagata.W06.TorusConfiguration.torusTuple_eq_sum line 195

theorem OAI.Nagata.W06.TorusConfiguration.torusTuple_injective line 206

Source documentation

Pairwise distinctness of the complete source tuple, with every quantitative common-chart bound explicit. No cubic embedding is assumed in this theorem.

theorem torusTuple_injective {τ R : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    (xi : Fin 9 → ℝ) (hxi : Function.Injective xi)
    (hxi_bounds : ∀ i, 0 < xi i ∧ xi i < 1 / 2)
    (hR : 0 < R) (hRpi : R < Real.pi / 2) (hlog : 2 * R < |Real.log τ|)
    (hmargin : R < markedGap (1 / 2) xi * |Real.log τ|)
    {q : ℕ} (ξ : Fin q → ℂ) (hξ : Function.Injective ξ) (hξR : ∀ j, ‖ξ j‖ < R) :
    Function.Injective (torusTuple τ hτ (1 / 2) xi ξ) := by
…

Mentions: OAI.Nagata.W06.TorusConfiguration.torusTuple

theorem OAI.Nagata.W06.TorusConfiguration.exists_eventual_injective_torusTuple line 250

Source documentation

One common disk works for every q and every distinct q-tuple in that disk, uniformly for all sufficiently small positive τ.

theorem exists_eventual_injective_torusTuple (xi : Fin 9 → ℝ) (hxi : Function.Injective xi)
    (hxi_bounds : ∀ i, 0 < xi i ∧ xi i < 1 / 2) :
    ∃ R : ℝ, 0 < R ∧ R < Real.pi / 2 ∧
      ∀ᶠ τ : ℝ in 𝓝[>] 0, 0 < τ ∧ τ < 1 ∧
        ∀ (hτ : 0 < τ) (q : ℕ) (ξ : Fin q → ℂ),
          Function.Injective ξ → (∀ j, ‖ξ j‖ < R) →
          Function.Injective (torusTuple τ hτ (1 / 2) xi ξ) := by
…

Mentions: OAI.Nagata.W06.TorusConfiguration.torusTuple

def OAI.Nagata.W06.TorusConfiguration.embeddedConfiguration line 286

Source documentation

Composition with a supplied genuine injective projective map.

def embeddedConfiguration {τ : ℝ} (hτ : 0 < τ) (x0 : ℝ) (xi : Fin 9 → ℝ)
    {q : ℕ} (ξ : Fin q → ℂ)
    (hinj : Function.Injective (torusTuple τ hτ x0 xi ξ))
    (embed : TorusPoint (positivePeriod τ hτ) → PlanePoint)
    (hembed : Function.Injective embed) : OrderedDistinctPoints (9 + q) :=
…

Mentions: OAI.Nagata.W06.TorusConfiguration.torusTuple

theorem OAI.Nagata.W06.TorusConfiguration.embeddedConfiguration_apply line 293
def OAI.Nagata.W06.TorusConfiguration.reindexConfiguration line 302
Source documentation
Reindexing preserves the actual points and changes only the tuple's index type.
```
def reindexConfiguration {r s : ℕ} (hrs : r = s) (p : OrderedDistinctPoints s) :
    OrderedDistinctPoints r :=
…
```
theorem OAI.Nagata.W06.TorusConfiguration.reindexConfiguration_apply line 306

def OAI.Nagata.W06.TorusConfiguration.embeddedConfigurationOfEq line 311

Source documentation

The source equality r=9+q is retained exactly, with no unused or repeated points.

def embeddedConfigurationOfEq {r q : ℕ} (hr : r = 9 + q)
    {τ : ℝ} (hτ : 0 < τ) (x0 : ℝ) (xi : Fin 9 → ℝ) (ξ : Fin q → ℂ)
    (hinj : Function.Injective (torusTuple τ hτ x0 xi ξ))
    (embed : TorusPoint (positivePeriod τ hτ) → PlanePoint)
    (hembed : Function.Injective embed) : OrderedDistinctPoints r :=
…

Mentions: OAI.Nagata.W06.TorusConfiguration.torusTuple

def OAI.Nagata.W06.TorusConfiguration.embeddedConfigurationForR line 319

Source documentation

For every r≥9 the literal choice q=r−9 gives an actual r-tuple.

def embeddedConfigurationForR (r : ℕ) (hr : 9 ≤ r)
    {τ : ℝ} (hτ : 0 < τ) (x0 : ℝ) (xi : Fin 9 → ℝ) (ξ : Fin (r - 9) → ℂ)
    (hinj : Function.Injective (torusTuple τ hτ x0 xi ξ))
    (embed : TorusPoint (positivePeriod τ hτ) → PlanePoint)
    (hembed : Function.Injective embed) : OrderedDistinctPoints r :=
…

Mentions: OAI.Nagata.W06.TorusConfiguration.torusTuple

theorem OAI.Nagata.W06.TorusConfiguration.collisionTorusTuple_injective line 328

Source documentation

Explicit colliding q-tuples remain distinct from each other and all nine fixed marks at every sequence index, under the same source common-chart bounds.

theorem collisionTorusTuple_injective {τ R : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    (xi : Fin 9 → ℝ) (hxi : Function.Injective xi)
    (hxi_bounds : ∀ i, 0 < xi i ∧ xi i < 1 / 2)
    (hR : 0 < R) (hRpi : R < Real.pi / 2) (hlog : 2 * R < |Real.log τ|)
    (hmargin : R < markedGap (1 / 2) xi * |Real.log τ|) (q n : ℕ) :
    Function.Injective (torusTuple τ hτ (1 / 2) xi (Nagata.W20.collisionCenters q R n)) := by
…

Mentions: OAI.Nagata.W06.TorusConfiguration.torusTuple, OAI.Nagata.W20.collisionCenters

theorem OAI.Nagata.W06.TorusConfiguration.exists_eventual_collisionConfiguration line 342

Source documentation

One disk and one explicit collision family work uniformly for all q and all sufficiently small periods; every center tends to zero in the genuine complex chart.

theorem exists_eventual_collisionConfiguration (xi : Fin 9 → ℝ)
    (hxi : Function.Injective xi) (hxi_bounds : ∀ i, 0 < xi i ∧ xi i < 1 / 2) :
    ∃ R : ℝ, 0 < R ∧ R < Real.pi / 2 ∧
      (∀ q i, Tendsto (fun n => Nagata.W20.collisionCenters q R n i) atTop (𝓝 0)) ∧
      ∀ᶠ τ : ℝ in 𝓝[>] 0, 0 < τ ∧ τ < 1 ∧
        ∀ (hτ : 0 < τ) (q n : ℕ), Function.Injective
          (torusTuple τ hτ (1 / 2) xi (Nagata.W20.collisionCenters q R n)) := by
…

Mentions: OAI.Nagata.W20.collisionCenters, OAI.Nagata.W06.TorusConfiguration.torusTuple

def OAI.Nagata.W06.LineArrangement.extraPoint line 377
Source documentation
A countably infinite explicit sequence of extra points on component zero.
```
def extraPoint (K : Type*) [Field K] (k t : ℕ) : K × K :=
…
```
theorem OAI.Nagata.W06.LineArrangement.extraPoint_zero line 383
theorem OAI.Nagata.W06.LineArrangement.extraPoint_injective line 386
theorem OAI.Nagata.W06.LineArrangement.extraPoint_ne_mark line 391
theorem OAI.Nagata.W06.LineArrangement.extraPoint_not_mem_markedPoints line 399
theorem OAI.Nagata.W06.LineArrangement.extraPoint_on_zero line 407

theorem OAI.Nagata.W06.LineArrangement.extraPoint_nonsingular_certificate line 412

Source documentation

Every extra point has a concrete nonzero Y-partial derivative.

theorem extraPoint_nonsingular_certificate (k : ℕ) (hk : 0 < k) (t : ℕ) :
    planeEval (Nagata.Workers.W24.lineUnionEquation K k)
        (extraPoint K k t).1 (extraPoint K k t).2 = 0 ∧
      planeEval (Nagata.Workers.W24.lineUnionEquation K k).derivative
        (extraPoint K k t).1 (extraPoint K k t).2 ≠ 0 := by
…

Mentions: OAI.Nagata.W06.LineArrangement.planeEval, OAI.Nagata.Workers.W24.lineUnionEquation, OAI.Nagata.W06.LineArrangement.extraPoint

def OAI.Nagata.W06.LineArrangement.manyMarkedPoints line 424
Source documentation
The finite set of k² original marks and n distinct extra points.
```
def manyMarkedPoints (K : Type*) [Field K] (k n : ℕ) : Finset (K × K) := by
…
```
theorem OAI.Nagata.W06.LineArrangement.card_manyMarkedPoints line 428
theorem OAI.Nagata.W06.LineArrangement.markedPoint_mem_manyMarkedPoints line 441
theorem OAI.Nagata.W06.LineArrangement.extraPoint_mem_manyMarkedPoints line 448
theorem OAI.Nagata.W06.LineArrangement.manyMarkedPoints_nonsingular line 454
theorem OAI.Nagata.W06.LineArrangement.exists_vertical_displacement_many line 466
Source documentation
Every target scalar of the vertical differential is attainable at every selected point.
```
theorem exists_vertical_displacement_many (k : ℕ) (hk : 0 < k) (n : ℕ)
    (p : K × K) (hp : p ∈ manyMarkedPoints K k n) (c : K) :
    ∃ t : K, planeEval (Nagata.Workers.W24.lineUnionEquation K k).derivative p.1 p.2 * t = c := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.manyMarkedPoints, OAI.Nagata.W06.LineArrangement.planeEval, OAI.Nagata.Workers.W24.lineUnionEquation

theorem OAI.Nagata.W06.LineArrangement.triangle_configuration_every_r line 474

Source documentation

Exactly r certified nonsingular affine points for every r≥9 on the triangle.

theorem triangle_configuration_every_r (r : ℕ) (hr : 9 ≤ r) :
    (manyMarkedPoints K 3 (r - 9)).card = r ∧
      ∀ p ∈ manyMarkedPoints K 3 (r - 9),
        planeEval (Nagata.Workers.W24.lineUnionEquation K 3) p.1 p.2 = 0 ∧
        planeEval (Nagata.Workers.W24.lineUnionEquation K 3).derivative p.1 p.2 ≠ 0 := by
…

Mentions: OAI.Nagata.W06.LineArrangement.manyMarkedPoints, OAI.Nagata.W06.LineArrangement.planeEval, OAI.Nagata.Workers.W24.lineUnionEquation

theorem OAI.Nagata.W06.LineArrangement.triangle_additionalPoint_mem line 486
Source documentation
For every r≥10, the point (-5,0) is present alongside the original nine marks.
```
theorem triangle_additionalPoint_mem (r : ℕ) (hr : 10 ≤ r) :
    additionalPoint K 3 ∈ manyMarkedPoints K 3 (r - 9) := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.additionalPoint, OAI.Nagata.W06.LineArrangement.manyMarkedPoints
def OAI.Nagata.W06.LineArrangement.mixedPoint line 492
Source documentation
A direct index type for the ordered original and additional points.
```
def mixedPoint (K : Type*) [Field K] (k n : ℕ) : (Fin k × Fin k) ⊕ Fin n → K × K :=
…
```
theorem OAI.Nagata.W06.LineArrangement.mixedPoint_injective line 495
def OAI.Nagata.W06.LineArrangement.pairCoordinates line 522
Source documentation
The two affine coordinates of a point, enumerated by Fin 2.
```
def pairCoordinates (p : ℂ × ℂ) : Fin 2 → ℂ := ![p.1, p.2]
```
theorem OAI.Nagata.W06.LineArrangement.pairCoordinates_injective line 524
def OAI.Nagata.W06.LineArrangement.liftAffine line 531
Source documentation
The genuine projective point [U:Y:1].
```
def liftAffine (p : ℂ × ℂ) : PlanePoint := chartPoint₂ 2 (pairCoordinates p)
```
Mentions: OAI.Nagata.W06.LineArrangement.pairCoordinates
theorem OAI.Nagata.W06.LineArrangement.liftAffine_injective line 533
theorem OAI.Nagata.W06.LineArrangement.liftAffine_vector line 537
Source documentation
Explicit verification of the homogeneous-coordinate convention.
```
theorem liftAffine_vector (p : ℂ × ℂ) :
    chartVector₂ 2 (pairCoordinates p) = ![p.1, p.2, 1] := by
…
```
Mentions: OAI.Nagata.W06.LineArrangement.pairCoordinates
theorem OAI.Nagata.W06.LineArrangement.liftAffine_chartCoordinates line 542
def OAI.Nagata.W06.LineArrangement.configurationIndexEquiv line 547
Source documentation
Explicit enumeration of the k² original marks followed by n extra marks.
```
def configurationIndexEquiv (k n : ℕ) :
    ((Fin k × Fin k) ⊕ Fin n) ≃ Fin (k * k + n) :=
…
```
def OAI.Nagata.W06.LineArrangement.orderedAffinePoint line 552
theorem OAI.Nagata.W06.LineArrangement.orderedAffinePoint_injective line 555
def OAI.Nagata.W06.LineArrangement.orderedProjectiveConfiguration line 559
Source documentation
An actual element of U_(k²+n), with all projective points explicitly constructed.
```
def orderedProjectiveConfiguration (k n : ℕ) : OrderedDistinctPoints (k * k + n) :=
…
```

theorem OAI.Nagata.W06.LineArrangement.orderedAffinePoint_nonsingular line 564

Source documentation

Every ordered point retains the verified affine equation and derivative certificate.

theorem orderedAffinePoint_nonsingular (k : ℕ) (hk : 0 < k) (n : ℕ)
    (t : Fin (k * k + n)) :
    planeEval (Nagata.Workers.W24.lineUnionEquation ℂ k)
        (orderedAffinePoint k n t).1 (orderedAffinePoint k n t).2 = 0 ∧
      planeEval (Nagata.Workers.W24.lineUnionEquation ℂ k).derivative
        (orderedAffinePoint k n t).1 (orderedAffinePoint k n t).2 ≠ 0 := by
…

Mentions: OAI.Nagata.W06.LineArrangement.planeEval, OAI.Nagata.Workers.W24.lineUnionEquation, OAI.Nagata.W06.LineArrangement.orderedAffinePoint

def OAI.Nagata.W06.LineArrangement.triangleOrderedConfiguration line 576
Source documentation
Every r≥9 has the concrete r-point triangle configuration in the genuine U_r.
```
def triangleOrderedConfiguration (r : ℕ) (hr : 9 ≤ r) : OrderedDistinctPoints r := by
…
```