Exact scale ratios and elementary bounds for the time scales.

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

The integer factor relating the three §2.1 time scales.

Equations

• AVenhance.Infra.Ingredients.tauCellFactor β Λ m = 4 * ↑⌈AVenhance.epsilon β Λ (m - 1) ^ (-AVenhance.delta β)⌉₊ + 1

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

Integer number of small time cells in a large time cell.

Equations

• AVenhance.Infra.Ingredients.tauCellCount β Λ m = (4 * ⌈AVenhance.epsilon β Λ (m - 1) ^ (-AVenhance.delta β)⌉₊ + 1) ^ 2

theorem AVenhance.Infra.Ingredients.tauCellFactor_sq_eq_count (β : ℝ) (Λ m : ℕ) : tauCellFactor β Λ m ^ 2 = ↑(tauCellCount β Λ m)

theorem AVenhance.Infra.Ingredients.tauP_eq_cellFactor_mul_tau {β : ℝ} {Λ m : ℕ} (hm : 1 ≤ m) : tauP β Λ m = tauCellFactor β Λ m * tau β Λ m

e.ratios.taum (1140-1147): τ'_m = (4⌈ε_{m-1}^{-δ}⌉+1) τ_m.

theorem AVenhance.Infra.Ingredients.tauPP_eq_cellFactor_sq_mul_tau {β : ℝ} {Λ m : ℕ} (hm : 1 ≤ m) : tauPP β Λ m = tauCellFactor β Λ m ^ 2 * tau β Λ m

e.ratios.taum (1140-1147): τ''_m = (4⌈ε_{m-1}^{-δ}⌉+1)^2 τ_m.

theorem AVenhance.Infra.Ingredients.tauPP_eq_cellFactor_mul_tauP {β : ℝ} {Λ m : ℕ} (hm : 1 ≤ m) : tauPP β Λ m = tauCellFactor β Λ m * tauP β Λ m

e.ratios.taum (1140-1147): τ''_m = (4⌈ε_{m-1}^{-δ}⌉+1) τ'_m.

theorem AVenhance.Infra.Ingredients.tauPP_eq_cellCount_mul_tau {β : ℝ} {Λ m : ℕ} (hm : 1 ≤ m) : tauPP β Λ m = ↑(tauCellCount β Λ m) * tau β Λ m

e.ratios.taum (1140-1147): the ratio τ''_m/τ_m is the odd integer (4⌈ε_{m-1}^{-δ}⌉+1)^2.