The corrected floor index and its cell-containment property.

noncomputable def AVenhance.Infra.Ingredients.LIdxConsequences.tauCellHalfCount (β : ℝ) (Λ m : ℕ) : ℕ

Half-count of time cells used in the coarse time-index arithmetic.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Ingredients.LIdxConsequences.tauCellCount_eq_two_mul_half_add_one (β : ℝ) (Λ m : ℕ) : tauCellCount β Λ m = 2 * tauCellHalfCount β Λ m + 1

theorem AVenhance.Infra.Ingredients.tau_pos {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : 0 < tau β Λ m

Positivity of all time cells from e.taum.def and e.taum.primeprime.def (1108-1136).

theorem AVenhance.Infra.Ingredients.taum_prime_supp {β : ℝ} {Λ m : ℕ} (k : ℤ) (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : Set.Icc (↑k * tau β Λ m - tau β Λ m / 2) (↑k * tau β Λ m + tau β Λ m / 2) ⊆ Set.Icc (↑(lIdx β Λ m k) * tauPP β Λ m - tauPP β Λ m / 2) (↑(lIdx β Λ m k) * tauPP β Λ m + tauPP β Λ m / 2)

e.taum.prime.supp (1179-1187), using the corrected floor index: the small time cell centered at k τ_m lies in its assigned large cell.