Enclosure.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Enclosing polygons and real slice profiles

def OAI.Nagata.ExponentEnclosure.positivePart line 22
def OAI.Nagata.ExponentEnclosure.exponentPolygon line 24
def OAI.Nagata.ExponentEnclosure.enclosingPolygon line 29
lemma OAI.Nagata.ExponentEnclosure.positivePart_of_nonpos line 33
lemma OAI.Nagata.ExponentEnclosure.positivePart_of_nonneg line 36
theorem OAI.Nagata.ExponentEnclosure.polygon_containment line 41
Source documentation
The source polygon is contained in D_lam, including its upper-index tip. The hypotheses here are weaker than the manuscript's positive parameter bounds.
```
theorem polygon_containment {ρ a Δ lam X Y : ℝ}
    (hρ : 0 ≤ ρ) (hΔ : 0 ≤ Δ) (hlam : lam ≤ 1)
    (hslack : ρ + Δ * ρ / 9 < lam * a - 9 * (1 - lam))
    (h : exponentPolygon ρ a Δ X Y) : enclosingPolygon a lam X Y := by
…
```
Mentions: OAI.Nagata.ExponentEnclosure.exponentPolygon, OAI.Nagata.ExponentEnclosure.enclosingPolygon
theorem OAI.Nagata.ExponentEnclosure.degree_zero_tip line 64
Source documentation
The degree-zero block lies exactly on both boundary lines.
```
theorem degree_zero_tip {ρ a Δ : ℝ} (hρ : 0 ≤ ρ) :
    exponentPolygon ρ a Δ (1 + ρ / 9) (-a - ρ / 9 * (a - Δ)) := by
…
```
Mentions: OAI.Nagata.ExponentEnclosure.exponentPolygon

theorem OAI.Nagata.ExponentEnclosure.first_interval_normalized line 75

Source documentation

Normalization of a first-branch exponent interval, j ≤ m.

theorem first_interval_normalized {ρ a Δ m j K U : ℝ}
    (hm : 0 < m) (hρ : 0 ≤ ρ) (hj : 0 ≤ j) (hjm : j ≤ m)
    (hlo : U - a * j < K) (hhi : K < U - a * j + m * ρ) :
    exponentPolygon ρ a Δ (j / m) ((K - U) / m) := by
…

Mentions: OAI.Nagata.ExponentEnclosure.exponentPolygon

theorem OAI.Nagata.ExponentEnclosure.second_interval_normalized line 96

Source documentation

Normalization of a second-branch interval expressed relative to U_0.

theorem second_interval_normalized {ρ a Δ m j K U : ℝ}
    (hm : 0 < m) (hjm : m ≤ j) (hjtop : j ≤ m * (1 + ρ / 9))
    (hlo : U - a * j + Δ * (j - m) ≤ K)
    (hhi : K ≤ U - a * j + m * ρ + (Δ - 9) * (j - m)) :
    exponentPolygon ρ a Δ (j / m) ((K - U) / m) := by
…

Mentions: OAI.Nagata.ExponentEnclosure.exponentPolygon

theorem OAI.Nagata.ExponentEnclosure.second_lower_endpoint line 117
Source documentation
Algebraic identity identifying the lower interval endpoint in the second branch.
```
theorem second_lower_endpoint (a Δ m j h : ℝ) :
    (h - 9 * (j - m)) / 9 * (a - Δ) - (h / 9 * (a - Δ) + m * a) =
      -a * j + Δ * (j - m) := by ring
```

theorem OAI.Nagata.ExponentEnclosure.second_upper_endpoint line 122

Source documentation

The corresponding upper endpoint after adding the interval length n.

theorem second_upper_endpoint (a Δ m j h : ℝ) :
    (h - 9 * (j - m)) / 9 * (a - Δ) + (h - 9 * (j - m)) -
        (h / 9 * (a - Δ) + m * a) =
      -a * j + h + (Δ - 9) * (j - m) := by ring

def OAI.Nagata.ExponentEnclosure.rawExponent line 130
Source documentation
Raw exponent conditions of (exponent-set), using real indices so the numerical argument does not depend on integrality. d / 3 replaces its integer floor; for integral j the bounds are equivalent.
```
def rawExponent (d m h a Δ j K : ℝ) : Prop :=
…
```

theorem OAI.Nagata.ExponentEnclosure.rawExponent_normalized line 140

Source documentation

Every raw exponent obeys the manuscript's polygon inequalities.

theorem rawExponent_normalized {d m h ρ a Δ j K : ℝ}
    (hm : 0 < m) (hρ : 0 ≤ ρ) (hdegree : h = 3 * (d - 3 * m))
    (hratio : h = m * ρ) (hmem : rawExponent d m h a Δ j K) :
    exponentPolygon ρ a Δ (j / m)
      ((K - (h / 9 * (a - Δ) + m * a)) / m) := by
…

Mentions: OAI.Nagata.ExponentEnclosure.rawExponent, OAI.Nagata.ExponentEnclosure.exponentPolygon

theorem OAI.Nagata.ExponentEnclosure.integer_exponent_enclosure line 171

Source documentation

The integer exponent-set arithmetic maps into the enclosing polygon. This uses actual integer indices, without assuming any analytic/geometric bridge.

theorem integer_exponent_enclosure {d m h ρ a Δ lam : ℝ} {j K : ℤ}
    (hm : 0 < m) (hρ : 0 ≤ ρ) (hΔ : 0 ≤ Δ) (hlam : lam ≤ 1)
    (hdegree : h = 3 * (d - 3 * m)) (hratio : h = m * ρ)
    (hslack : ρ + Δ * ρ / 9 < lam * a - 9 * (1 - lam))
    (hmem : rawExponent d m h a Δ (j : ℝ) (K : ℝ)) :
    enclosingPolygon a lam ((j : ℝ) / m)
      (((K : ℝ) - (h / 9 * (a - Δ) + m * a)) / m) :=
…

Mentions: OAI.Nagata.ExponentEnclosure.rawExponent, OAI.Nagata.ExponentEnclosure.enclosingPolygon

def OAI.Nagata.W04.InPolygon line 192
Source documentation
Membership in the enclosing polygon D_lambda, with a left explicit.
```
def InPolygon (a lam x y : ℝ) : Prop :=
…
```
theorem OAI.Nagata.W04.polygon_dilation line 196
Source documentation
Dilation by any positive real factor preserves the actual inequalities.
```
theorem polygon_dilation (a lam scale x y : ℝ) (hscale : 0 < scale) :
    InPolygon a (scale * lam) (scale * x) (scale * y) ↔ InPolygon a lam x y := by
…
```
Mentions: OAI.Nagata.W04.InPolygon
theorem OAI.Nagata.W04.polygon_scaling line 210
Source documentation
Positive coordinate dilation gives exactly D_lambda = lambda D_1.
```
theorem polygon_scaling (a lam x y : ℝ) (hlam : 0 < lam) :
    InPolygon a lam (lam * x) (lam * y) ↔ InPolygon a 1 x y := by
…
```
Mentions: OAI.Nagata.W04.InPolygon
theorem OAI.Nagata.W04.le_one_sub_div_iff line 214
theorem OAI.Nagata.W04.positive_slice line 221
Source documentation
Exact horizontal slice above the horizontal axis; empty cases are included.
```
theorem positive_slice (a x y : ℝ) (ha : 0 < a) (hy : 0 ≤ y) :
    InPolygon a 1 x y ↔ 0 ≤ x ∧ x ≤ 1 - y / a := by
…
```
Mentions: OAI.Nagata.W04.InPolygon
theorem OAI.Nagata.W04.negative_slice line 239
Source documentation
Exact horizontal slice below the horizontal axis; empty cases are included.
```
theorem negative_slice (a x y : ℝ) (ha : 0 < a) (hy : y ≤ 0) :
    InPolygon a 1 x y ↔ -y / a ≤ x ∧ x ≤ 1 - y / (a + 9) := by
…
```
Mentions: OAI.Nagata.W04.InPolygon
theorem OAI.Nagata.W04.negative_width_identity line 259
Source documentation
The negative-height interval width in the manuscript has the asserted slope.
```
theorem negative_width_identity (a y : ℝ) (ha : 0 < a) :
    (1 - y / (a + 9)) - (-y / a) = 1 + y / (a * (1 + a / 9)) := by
…
```
def OAI.Nagata.W04.UnitSliceWidth line 270
Source documentation
Canonical width formula; negative values signify an empty slice.
```
def UnitSliceWidth (a y : ℝ) : ℝ :=
…
```
def OAI.Nagata.W04.SliceLower line 274
Source documentation
Left endpoint of the affine horizontal slice.
```
def SliceLower (a y : ℝ) : ℝ := if 0 ≤ y then 0 else -y / a
```
def OAI.Nagata.W04.SliceUpper line 277
Source documentation
Right endpoint of the affine horizontal slice.
```
def SliceUpper (a y : ℝ) : ℝ :=
…
```
theorem OAI.Nagata.W04.unit_slice_width line 281
Source documentation
The width formula is the actual difference of interval endpoints.
```
theorem unit_slice_width (a y : ℝ) (ha : 0 < a) :
    SliceUpper a y - SliceLower a y = UnitSliceWidth a y := by
…
```
Mentions: OAI.Nagata.W04.SliceUpper, OAI.Nagata.W04.SliceLower, OAI.Nagata.W04.UnitSliceWidth
theorem OAI.Nagata.W04.unit_slice_interval line 289
Source documentation
The endpoint functions describe the polygon's actual slice exactly.
```
theorem unit_slice_interval (a x y : ℝ) (ha : 0 < a) :
    InPolygon a 1 x y ↔ SliceLower a y ≤ x ∧ x ≤ SliceUpper a y := by
…
```
Mentions: OAI.Nagata.W04.InPolygon, OAI.Nagata.W04.SliceLower, OAI.Nagata.W04.SliceUpper
theorem OAI.Nagata.W04.unit_slice_nonempty line 298
Source documentation
Nonnegative width is exactly nonemptiness; both endpoint tips are retained.
```
theorem unit_slice_nonempty (a y : ℝ) (ha : 0 < a) :
    (∃ x, InPolygon a 1 x y) ↔ 0 ≤ UnitSliceWidth a y := by
…
```
Mentions: OAI.Nagata.W04.InPolygon, OAI.Nagata.W04.UnitSliceWidth
theorem OAI.Nagata.W04.unit_width_le_one line 311
Source documentation
No horizontal slice has width greater than one.
```
theorem unit_width_le_one (a y : ℝ) (ha : 0 < a) : UnitSliceWidth a y ≤ 1 := by
…
```
Mentions: OAI.Nagata.W04.UnitSliceWidth

theorem OAI.Nagata.W04.unit_width_threshold line 323

Source documentation

The width threshold yields a single closed interval of heights.

theorem unit_width_threshold (a y s : ℝ) (ha : 0 < a)
    (hs : 0 ≤ s) (hs1 : s ≤ 1) :
    s ≤ UnitSliceWidth a y ↔
      -a * (1 + a / 9) * (1 - s) ≤ y ∧ y ≤ a * (1 - s) := by
…

Mentions: OAI.Nagata.W04.UnitSliceWidth

def OAI.Nagata.W04.ScaledSliceWidth line 350
Source documentation
Width after positive dilation and arbitrary vertical translation.
```
def ScaledSliceWidth (a scale U y : ℝ) : ℝ :=
…
```
theorem OAI.Nagata.W04.scaled_width_le_scale line 354
Source documentation
Every scaled horizontal slice has width at most the dilation factor.
```
theorem scaled_width_le_scale (a scale U y : ℝ) (ha : 0 < a) (hscale : 0 ≤ scale) :
    ScaledSliceWidth a scale U y ≤ scale := by
…
```
Mentions: OAI.Nagata.W04.ScaledSliceWidth

theorem OAI.Nagata.W04.scaled_slice_interval line 360

Source documentation

Positive scaling and translation preserve the exact endpoint description.

theorem scaled_slice_interval (a scale U x y : ℝ) (ha : 0 < a) (hscale : 0 < scale) :
    InPolygon a scale x (y - U) ↔
      scale * SliceLower a ((y - U) / scale) ≤ x ∧
      x ≤ scale * SliceUpper a ((y - U) / scale) := by
…

Mentions: OAI.Nagata.W04.InPolygon, OAI.Nagata.W04.SliceLower, OAI.Nagata.W04.SliceUpper

theorem OAI.Nagata.W04.scaled_slice_width line 371
Source documentation
The scaled width also equals the difference of its actual endpoints.
```
theorem scaled_slice_width (a scale U y : ℝ) (ha : 0 < a) :
    scale * SliceUpper a ((y - U) / scale) -
      scale * SliceLower a ((y - U) / scale) = ScaledSliceWidth a scale U y := by
…
```
Mentions: OAI.Nagata.W04.SliceUpper, OAI.Nagata.W04.SliceLower, OAI.Nagata.W04.ScaledSliceWidth

theorem OAI.Nagata.W04.scaled_width_threshold line 378

Source documentation

The exact closed height interval, including both zero-width tips.

theorem scaled_width_threshold (a scale U y s : ℝ)
    (ha : 0 < a) (hscale : 0 < scale) (hs : 0 ≤ s) (hsupper : s ≤ scale) :
    s ≤ ScaledSliceWidth a scale U y ↔
      U - a * (1 + a / 9) * (scale - s) ≤ y ∧
      y ≤ U + a * (scale - s) := by
…

Mentions: OAI.Nagata.W04.ScaledSliceWidth

theorem OAI.Nagata.W04.height_interval_length line 400

Source documentation

Length of the interval of heights in the threshold theorem.

theorem height_interval_length (a scale U s : ℝ) :
    (U + a * (scale - s)) - (U - a * (1 + a / 9) * (scale - s)) =
      (2 * a + a ^ 2 / 9) * (scale - s) := by ring
…