RationalSeparation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Rational separation survives the real drift

The proofs use real representative differences and integral errors directly. They do not assume a separation property of labels: it is deduced from the primitive rational path and the proved width bound on a label's first intervals.

theorem OAI.QuantitativeVanDerWaerden.return_separation_margin line 20
Source documentation
The scale inequalities from the closest-return argument leave enough space between distinct rational residues for an entire first-coordinate box.
```
theorem return_separation_margin {h : ℕ} {M H W : ℝ}
    (hh : 0 < h) (hperiod : (h : ℝ) ≤ 2 * M)
    (hW : 0 ≤ W) (hWH : W ≤ H) (hsmall : 4 * M * H < 1) :
    W + (2 * M * W) / h < 1 / (h : ℝ) := by
…
```
theorem OAI.QuantitativeVanDerWaerden.index_drift_le line 35
Source documentation
The drift accumulated between two indices in the progression is at most the full-length drift divided by the return denominator.
```
theorem index_drift_le {a b k h : ℕ} {u U : ℝ}
    (ha : a < k) (hb : b < k) (hh : 0 < h)
    (hu : (k : ℝ) * |u| ≤ U) :
    |((a : ℝ) - b) / h * u| ≤ U / h := by
…
```

theorem OAI.QuantitativeVanDerWaerden.rational_path_coordinate_separation line 55

Source documentation

Indices incongruent modulo the primitive denominator have a separated coordinate, even after adding the actual small drift and choosing representatives.

theorem rational_path_coordinate_separation {ι : Type uIndex} [Fintype ι]
    {k h a b : ℕ} {W U : ℝ} {t : ι → ℤ}
    (X : ℕ → ι → ℝ) (A u : ι → ℝ)
    (hh : 0 < h) (hp : PrimitiveVector h t)
    (hpath : ∀ n, n < k → ∀ i, ∃ z : ℤ,
      X n i - A i - (n : ℝ) / h * ((t i : ℝ) + u i) = z)
    (hdrift : ∀ i, (k : ℝ) * |u i| ≤ U)
    (hmargin : W + U / h < 1 / (h : ℝ))
    (ha : a < k) (hb : b < k) (hab : ¬ (h : ℤ) ∣ (a : ℤ) - b) :
    ∃ i, W < |X a i - X b i| := by
…

Mentions: OAI.QuantitativeVanDerWaerden.PrimitiveVector

theorem OAI.QuantitativeVanDerWaerden.same_label_divisible_index_difference line 88

Source documentation

Every occurrence of one label lies in one residue class. The label hypothesis is only its actual coordinate-width bound.

theorem same_label_divisible_index_difference {ι : Type uIndex} {L : Type uL} [Fintype ι]
    {k h a b : ℕ} {W U : ℝ} {t : ι → ℤ}
    (X : ℕ → ι → ℝ) (A u : ι → ℝ) (label : ℕ → L)
    (hh : 0 < h) (hp : PrimitiveVector h t)
    (hpath : ∀ n, n < k → ∀ i, ∃ z : ℤ,
      X n i - A i - (n : ℝ) / h * ((t i : ℝ) + u i) = z)
    (hdrift : ∀ i, (k : ℝ) * |u i| ≤ U)
    (hmargin : W + U / h < 1 / (h : ℝ))
    (hwidth : ∀ n, n < k → ∀ m, m < k → label n = label m →
      ∀ i, |X n i - X m i| ≤ W)
    (ha : a < k) (hb : b < k) (hlab : label a = label b) :
    (h : ℤ) ∣ (a : ℤ) - b := by
…

Mentions: OAI.QuantitativeVanDerWaerden.PrimitiveVector