LongPeriodEligibility.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Literal eligibility of a heavy long-period block

The actual interval labels are injective along a primitive short-drift block. The regular-position count and stationary drift conditions are proved from the rational grid and adaptive mesh, respectively.

theorem OAI.QuantitativeVanDerWaerden.full_block_fullLabel_injective line 20

Source documentation

Primitive rational motion separates the literal first-coordinate mesh labels throughout a full block, including all irregular positions.

theorem full_block_fullLabel_injective {D h : ℕ}
    (n : ℕ) (hn : 0 < n) (A : AdaptiveMesh) (R : Realization D)
    (lambda : ℕ) (t : Fin D → Fin h) (hh : 0 < h)
    (hprimitive : PrimitiveVector h (fun i => ((t i).val : ℤ)))
    (hfirst : ∀ i, |R.u i| ≤ 1 / (n : ℝ))
    (hscale : 2 * (h : ℝ) * (1 / (n : ℝ)) < 1) :
    Function.Injective (fullLabel n hn A R lambda t) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.PrimitiveVector

theorem OAI.QuantitativeVanDerWaerden.heavy_long_block_eligible line 74

Source documentation

Every actual block satisfying the return-path bounds and containing a heavy anchor is eligible for the recorded-pattern family. Neither half-block regularity, distinct labels, nor stationary widths are assumed.

theorem heavy_long_block_eligible {D h : ℕ}
    (n : ℕ) (hn : 0 < n) (A : AdaptiveMesh) (R : Realization D)
    (lambda : ℕ) (t : Fin D → Fin h) (hh : 0 < h) (hD : 3 ≤ D)
    (hprimitive : PrimitiveVector h (fun i => ((t i).val : ℤ)))
    (hfirst : ∀ i, |R.u i| ≤ 1 / (n : ℝ))
    (hscale : 2 * (h : ℝ) * (1 / (n : ℝ)) < 1)
    (hrotating : ∀ i, ¬ stationary lambda t i → |R.v i| ≤ A.H)
    (hnear : ∀ i, ¬ stationary lambda t i → |R.v i| < 1 / (1000 * (D : ℝ)))
    (hperiod : ∀ i, ¬ stationary lambda t i →
      D ^ 2 < h / Nat.gcd h (lambda * (t i).val))
    (anchor : Fin h) (M k : ℝ) (hsmall : 2 * M / k ≤ 1 / 16)
    (hheavy : ∀ i, stationary lambda t i → |R.v i| ≤
…

Mentions: OAI.QuantitativeVanDerWaerden.AdaptiveMesh, OAI.QuantitativeVanDerWaerden.PrimitiveVector