ShortPeriodLift.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The short-period branch of the outer-color dichotomy

A cut crossed by the unreduced real path is close to every sample. The actual adaptive mesh then makes every sampled interval narrower than the nonzero step. Two equal labels contradict this, forcing one global real affine lift.

theorem OAI.QuantitativeVanDerWaerden.rho_eq_of_integer_difference line 20
theorem OAI.QuantitativeVanDerWaerden.rho_half line 26
theorem OAI.QuantitativeVanDerWaerden.rho_le_distance_to_cut line 33
Source documentation
The circle distance to the cut is at most the real distance to any lift of that cut. This includes equality at either endpoint.
```
theorem rho_le_distance_to_cut (x : ℝ) (z : ℤ) :
    rho x ≤ |x - (1 / 2 + z)| := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.rho

theorem OAI.QuantitativeVanDerWaerden.short_segment_cut_rho line 41

Source documentation

Once the closed real segment hits a cut, every sample is cut-near. The congruences connect the real path with the actual centered samples.

theorem short_segment_cut_rho {Y : ℕ → ℝ} {A w t : ℝ} {k : ℕ} {z : ℤ}
    (hcongr : ∀ j, j < k → ∃ m : ℤ, Y j - (A + (j : ℝ) * w) = (m : ℝ))
    (ht0 : 0 ≤ t) (htk : t ≤ (k : ℝ))
    (hcut : A + t * w = 1 / 2 + z) :
    ∀ j, j < k → rho (Y j) ≤ (k : ℝ) * |w| := by
…

Mentions: OAI.QuantitativeVanDerWaerden.rho

theorem OAI.QuantitativeVanDerWaerden.short_period_affine_lift line 59

Source documentation

A repeated interval forces every centered sample onto the same real lift. Only the width at one of the repeated samples is needed.

theorem short_period_affine_lift {Y : ℕ → ℝ} {A w H α width : ℝ} {k a b : ℕ}
    (hrep : ∀ j, j < k → -(1 / 2 : ℝ) ≤ Y j ∧ Y j < 1 / 2)
    (hbase : Y 0 = A)
    (hcongr : ∀ j, j < k → ∃ z : ℤ, Y j - (A + (j : ℝ) * w) = (z : ℝ))
    (hH : 0 ≤ H) (hmotion : (k : ℝ) * |w| < 1 / 2)
    (hsep : w ≠ 0 → α ≤ |w|) (hsmall : 2 * H * ((k : ℝ) + 1) < 1)
    (hab : a ≠ b) (hak : a < k) (hbk : b < k)
    (hsame : |Y a - Y b| ≤ width)
    (hwidth : width ≤ 2 * H * (rho (Y a) + α)) :
    ∀ j, j < k → Y j = A + (j : ℝ) * w := by
…

Mentions: OAI.QuantitativeVanDerWaerden.rho

theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.short_period_affine_lift line 84

theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.short_period_vector_lift line 106

Source documentation

The coordinatewise conclusion gives a single vector affine lift.

theorem AdaptiveMesh.short_period_vector_lift (M : AdaptiveMesh)
    {ι : Type uIndex} {Y : ℕ → ι → ℝ} {w : ι → ℝ} {k a b : ℕ}
    (hrep : ∀ i j, j < k → -(1 / 2 : ℝ) ≤ Y j i ∧ Y j i < 1 / 2)
    (hcongr : ∀ i j, j < k →
      ∃ z : ℤ, Y j i - (Y 0 i + (j : ℝ) * w i) = (z : ℝ))
    (hmotion : ∀ i, (k : ℝ) * |w i| < 1 / 2)
    (hsep : ∀ i, w i ≠ 0 → M.alpha ≤ |w i|)
    (hsmall : 2 * M.H * ((k : ℝ) + 1) < 1)
    (hab : a ≠ b) (hak : a < k) (hbk : b < k)
    (hsame : ∀ i, M.meshLabel (Y a i) = M.meshLabel (Y b i)) :
    ∀ j, j < k → Y j = fun i => Y 0 i + (j : ℝ) * w i := by
…

Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh

theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.short_period_cyclic_lift line 125

Source documentation

Short-period lifting for the actual cyclic representatives and actual adaptive labels. The only remaining inputs are the numerical short-motion bounds, a congruent step, and a repeated label.

theorem AdaptiveMesh.short_period_cyclic_lift (M : AdaptiveMesh)
    {q D dilation k a b : ℕ} (hq : 0 < q)
    (n d : CyclicGroup q D) (w : Fin D → ℝ)
    (hstep : ∀ i, ∃ z : ℤ, yRep q D dilation d i - w i = (z : ℝ))
    (halpha : M.alpha ≤ 1 / (q : ℝ) ^ D)
    (hmotion : ∀ i, (k : ℝ) * |w i| < 1 / 2)
    (hsmall : 2 * M.H * ((k : ℝ) + 1) < 1)
    (hab : a ≠ b) (hak : a < k) (hbk : b < k)
    (hsame : ∀ i, M.meshLabel (yRep q D dilation (n + a • d) i) =
      M.meshLabel (yRep q D dilation (n + b • d) i)) :
    ∀ j, j < k → yRep q D dilation (n + j • d) =
      fun i => yRep q D dilation n i + (j : ℝ) * w i := by
…

Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.dilation, OAI.QuantitativeVanDerWaerden.CyclicGroup, OAI.QuantitativeVanDerWaerden.yRep