Parameters.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Real and integral parameter choices and scaling

theorem OAI.Nagata.Workers.W05.rhoStar_identity line 16
Source documentation
Equation (rho): the boundary parameter satisfies the quadratic identity.
```
theorem rhoStar_identity (r : ℝ) (hr : 0 ≤ r) :
    2 * (3 * (Real.sqrt r - 3)) + (3 * (Real.sqrt r - 3)) ^ 2 / 9 = r - 9 := by
…
```

theorem OAI.Nagata.Workers.W05.rho_bounds line 22

Source documentation

The inequalities preceding equation (rho), with positive multiplicity.

theorem rho_bounds (r d m : ℝ) (_hm : 0 < m)
    (hlow : 3 < d / m) (hupp : d / m < Real.sqrt r) :
    0 < 3 * (d / m - 3) ∧
      3 * (d / m - 3) < 3 * (Real.sqrt r - 3) ∧
      0 < 3 * (Real.sqrt r - 3) := by
…

theorem OAI.Nagata.Workers.W05.exists_contraction line 32

Source documentation

Equation (lambda), proved using an explicit open interval for lambda.

theorem exists_contraction (rho a : ℝ) (hrho : 0 ≤ rho) (hgap : rho < a) :
    ∃ lam : ℝ, 0 < lam ∧ lam < 1 ∧ rho < lam * a - 9 * (1 - lam) := by
…

theorem OAI.Nagata.Workers.W05.exists_positive_scaling line 44

Source documentation

Equation (scaling): a common positive integral multiple supplies the slack.

theorem exists_positive_scaling (q lam m : ℝ)
    (hq : 0 < q) (hlam : lam < 1) (hm : 0 < m) :
    ∃ n : ℕ, 0 < n ∧ 1 ≤ q * (1 - lam) * ((n : ℝ) * m) := by
…

theorem OAI.Nagata.Workers.W05.ratio_scale line 55
Source documentation
Common scaling leaves d/m, hence rho, unchanged.
```
theorem ratio_scale (d m : ℝ) (n : ℕ) (hn : 0 < n) :
    ((n : ℝ) * d) / ((n : ℝ) * m) = d / m := by
…
```
theorem OAI.Nagata.Workers.W05.degree_eq_mul_rho line 61
Source documentation
The integer degree h agrees with m rho after viewing the data as reals.
```
theorem degree_eq_mul_rho (d m : ℝ) (hm : 0 < m) :
    3 * (d - 3 * m) = m * (3 * (d / m - 3)) := by
…
```
theorem OAI.Nagata.Workers.W05.q_pos line 66
Source documentation
Positivity of the number of nonzero displacements.
```
theorem q_pos (r : ℝ) (hr : 10 ≤ r) : 0 < r - 9 := by linarith
…
```
theorem OAI.Nagata.Workers.W05.natural_integer_floor line 80
theorem OAI.Nagata.Workers.W05.coefficient_index_iff line 84
Source documentation
The finite natural coefficient index type enumerates the exact integer range.
```
theorem coefficient_index_iff (D : ℕ) (j : ℤ) :
    0 ≤ j ∧ j ≤ (D : ℤ) / 3 ↔
      ∃ i : Fin (D / 3 + 1), (i.val : ℤ) = j := by
…
```
theorem OAI.Nagata.Workers.W05.exponentSet_index_bounds line 98
Source documentation
No column in the actual exponent set has a negative polynomial exponent, and every exponent lies below the same integer floor bound.
```
theorem exponentSet_index_bounds {D M j K : ℤ} {a Δ : ℝ}
    (hM : 0 ≤ M) (hD : 3 * M < D)
    (hp : (j, K) ∈ exponentSet D M a Δ) : 0 ≤ j ∧ j ≤ D / 3 := by
…
```
theorem OAI.Nagata.Workers.W05.sourceDegree_nonnegative line 109
Source documentation
All source degrees up to the floor cutoff are nonnegative integers.
```
theorem sourceDegree_nonnegative {D j : ℤ} (hj : j ≤ D / 3) :
    0 ≤ sourceDegree D j := by
…
```
theorem OAI.Nagata.Workers.W05.commonDegree_positive line 116
Source documentation
The first blocks have positive common degree under the source's strict ratio.
```
theorem commonDegree_positive {D M : ℤ} (hD : 3 * M < D) :
    0 < commonDegree D M := by
…
```

theorem OAI.Nagata.Workers.W05.first_block_index_count line 122

Source documentation

Exact integer index count for every first coefficient block.

theorem first_block_index_count (D M j : ℤ) (a Δ : ℝ)
    (hU : firstLower D M j a Δ ∉ Set.range (Int.cast : ℤ → ℝ)) :
    (openIntegerInterval (firstLower D M j a Δ)
      (firstLower D M j a Δ + (commonDegree D M : ℝ))).card =
        (commonDegree D M).toNat := by
…

theorem OAI.Nagata.Workers.W05.second_block_index_count line 136

Source documentation

Exact integer index count for every positive-degree second coefficient block.

theorem second_block_index_count (D j : ℤ) (a Δ : ℝ)
    (hU : secondLower D j a Δ ∉ Set.range (Int.cast : ℤ → ℝ)) :
    (openIntegerInterval (secondLower D j a Δ)
      (secondLower D j a Δ + (sourceDegree D j : ℝ))).card =
        (sourceDegree D j).toNat := by
…

theorem OAI.Nagata.Workers.W05.zero_source_degree_last line 150
Source documentation
A zero source degree is exactly the final index and forces divisibility by 3.
```
theorem zero_source_degree_last {D j : ℤ} (hz : sourceDegree D j = 0) :
    j = D / 3 ∧ 3 ∣ D := by
…
```

theorem OAI.Nagata.Workers.W05.exists_numeric_choices line 169

Source documentation

Simultaneously choose the contraction, integral scaling, nonintegral delta, and nine marked real exponents required before the elliptic construction.

theorem exists_numeric_choices (r d m : ℕ) (hr : 10 ≤ r) (hm : 0 < m)
    (hlow : 3 < (d : ℝ) / (m : ℝ))
    (hupp : (d : ℝ) / (m : ℝ) < Real.sqrt (r : ℝ)) :
    ∃ (n : ℕ) (lam Δ : ℝ) (x : Fin 9 → ℝ),
      0 < n ∧ 0 < lam ∧ lam < 1 ∧
      1 ≤ ((r : ℝ) - 9) * (1 - lam) * ((n * m : ℕ) : ℝ) ∧
      0 < Δ ∧ Δ < 1 / 2 ∧
      (3 * ((d : ℝ) / (m : ℝ) - 3)) +
          Δ * (3 * ((d : ℝ) / (m : ℝ) - 3)) / 9 <
        lam * (3 * (Real.sqrt (r : ℝ) - 3)) - 9 * (1 - lam) ∧
      Function.Injective x ∧ (∀ i, 0 < x i ∧ x i < 1 / 2) ∧
      (∑ i : Fin 9, (1 / 2 - x i)) = Δ ∧
…

theorem OAI.Nagata.Workers.W05.firstLower_nonintegral_of_fin line 225
theorem OAI.Nagata.Workers.W05.secondLower_nonintegral_of_fin line 240

theorem OAI.Nagata.Workers.W05.exists_scaled_parameters line 274

Source documentation

All fixed scalar choices from equations rho/lambda/scaling/delta/nonintegral/ marked-parameters, with actual scaled natural degrees and multiplicities.

theorem exists_scaled_parameters (r d m : ℕ) (hr : 10 ≤ r) (hm : 0 < m)
    (hlow : 3 < (d : ℝ) / m) (hupp : (d : ℝ) / m < Real.sqrt r) :
    ∃ (n D M q : ℕ) (rho a h lam Δ eta : ℝ) (x : Fin 9 → ℝ),
      0 < n ∧ D = n * d ∧ M = n * m ∧ q = r - 9 ∧
      0 < D ∧ 0 < M ∧ 0 < q ∧ M ≤ D / 3 ∧
      (D : ℝ) / M = (d : ℝ) / m ∧
      rho = 3 * ((D : ℝ) / M - 3) ∧ a = 3 * (Real.sqrt r - 3) ∧
      h = 3 * ((D : ℝ) - 3 * M) ∧ h = (M : ℝ) * rho ∧
      0 < rho ∧ rho < a ∧ 0 < a ∧ 0 < h ∧
      2 * a + a ^ 2 / 9 = (q : ℝ) ∧
      0 < lam ∧ lam < 1 ∧ rho < lam * a - 9 * (1 - lam) ∧
      1 ≤ (q : ℝ) * (1 - lam) * M ∧
…

theorem OAI.Nagata.Workers.W05.exists_fixed_period_radius line 361
Source documentation
Every fixed real period in (0,1) admits a positive exponential chart radius.
```
theorem exists_fixed_period_radius {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1) :
    ∃ R : ℝ, 0 < R ∧ R < Real.pi / 2 ∧ 2 * R < |Real.log τ| := by
…
```
theorem OAI.Nagata.Workers.W05.chartPoint_identity line 371
theorem OAI.Nagata.Workers.W05.positivePeriod_action_free line 376
Source documentation
The period action is free on all actual nonzero complex points.
```
theorem positivePeriod_action_free {τ : ℝ} (hτ : 0 < τ) (hτ1 : τ < 1)
    (k : ℤ) (z : ℂˣ) (hk : positivePeriod τ hτ ^ k * z = z) : k = 0 := by
…
```
Mentions: OAI.Nagata.Workers.W05.positivePeriod
theorem OAI.Nagata.Workers.W05.exists_injective_identity_slice line 387