NegativePathWords.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Unit-step words remain in the negative halfspace

This is the concrete subdivision needed for quotient-boundary independence. The logarithmic mesh error is absorbed into half of the negative height gap.

theorem OAI.PolycyclicRecognition.one_parameter_nat_dist_le line 25
Source documentation
Integer points of an actual one-parameter subgroup lie in a linear ball. This supplies the absolute radius of the negative-height ray pivots.
```
theorem one_parameter_nat_dist_le
    (d : ℝ → G) (hzero : d 0 = 1) (hmul : ∀ s t, d (s + t) = d s * d t)
    (n : ℕ) : dist 1 (d n) ≤ (n : ℝ) * dist 1 (d 1) := by
…
```

theorem OAI.PolycyclicRecognition.exists_negative_word_prefix_chains line 38

Source documentation

Retain the actual prefixes of an eventually specified unit-step word. Their absolute radius follows by adding the radius of the starting point.

theorem exists_negative_word_prefix_chains
    (height : G → ℝ) (base target : ℕ → G) {C D gap : ℝ} {q : ℕ}
    (hbase : ∀ n : ℕ, dist 1 (base n) ≤ D * n)
    (hwords : ∀ᶠ n : ℕ in atTop, ∃ w : List G,
      (∀ g ∈ w, g ∈ closedBall (1 : G) 1) ∧ w.prod = (base n)⁻¹ * target n ∧
      (w.length : ℝ) ≤ C * (1 + n) ^ q ∧ ∀ i : ℕ,
        height (base n * (w.take i).prod) ≤ -gap * n ∧
        dist (base n) (base n * (w.take i).prod) ≤ C * n) :
    ∃ (m : ℕ → ℕ) (z : ℕ → ℕ → G),
      (∀ n, z n 0 = base n) ∧
      (∀ᶠ n in atTop, z n (m n) = target n) ∧
      (∀ᶠ n in atTop, (m n : ℝ) ≤ C * (1 + n) ^ q) ∧
…

theorem OAI.PolycyclicRecognition.eventually_negative_path_unit_words line 92

Source documentation

Subdivision can start at any point of the actual negative-height path. Every resulting prefix stays nearby, has negative linear height, and the number of unit steps is bounded by a fixed quadratic.

theorem eventually_negative_path_unit_words
    (hpath : ∀ g : G, ∃ γ : ℝ → G, γ 0 = 1 ∧ γ 1 = g ∧
      ∀ t ∈ Icc (0 : ℝ) 1, ∀ u ∈ Icc (0 : ℝ) 1,
        dist (γ t) (γ u) ≤ dist 1 g * |t - u|)
    (height : G → ℝ) {K C a : ℝ} (hK : 0 ≤ K) (hC : 0 ≤ C) (ha : 0 < a)
    (hheight : ∀ x y, |height x - height y| ≤ K * dist x y)
    (source target : ℕ → G)
    (hγ : ∀ᶠ n : ℕ in atTop, ∃ γ : Path (source n) (target n),
      PathMetricBound γ (C * n) (C * (1 + Real.log (2 + n))) ∧
      ∀ t, height (γ t) ≤ -a * n) :
    ∀ᶠ n : ℕ in atTop, ∃ w : List G,
      (∀ x ∈ w, x ∈ closedBall (1 : G) 1) ∧
…

Mentions: OAI.PolycyclicRecognition.PathMetricBound