Integer-ratio consequences for the time scales.

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

Natural ceiling entering the first time-scale definition.

Equations

• AVenhance.Infra.Ingredients.TimeScaleArithmetic.tauCeil β Λ m = ⌈AVenhance.epsilon β Λ (m - 1) ^ (-AVenhance.delta β)⌉₊

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

Natural ceiling entering the finer time-scale definition.

Equations

• AVenhance.Infra.Ingredients.TimeScaleArithmetic.tauPPceil β Λ m = ⌈AVenhance.a β Λ (m - 1) / AVenhance.epsilon β Λ (m - 1) ^ (2 * AVenhance.delta β)⌉₊

theorem AVenhance.Infra.Ingredients.TimeScaleArithmetic.tauPP_reciprocal_exact {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : 1 / tauPP β Λ m = 2 ^ 25 * ↑(tauPPceil β Λ m)

theorem AVenhance.Infra.Ingredients.TimeScaleArithmetic.tauFactor_cast {β : ℝ} {Λ m : ℕ} : tauCellFactor β Λ m = ↑(4 * tauCeil β Λ m + 1)

theorem AVenhance.Infra.Ingredients.tauPP_reciprocal_multiple_four {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (_hm : 1 ≤ m) : ∃ (n : ℕ), 1 / tauPP β Λ m = ↑(4 * n)

e.ratios.taum (1140-1147): 1/τ''_m is an integer multiple of four.

theorem AVenhance.Infra.Ingredients.tauPP_ratio_and_tau_reciprocal {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hm : 1 ≤ m) : tauPP β Λ m / tau β Λ m = ↑(tauCellCount β Λ m) ∧ ∃ (n : ℕ), 1 / tau β Λ m = ↑(4 * n)

e.ratios.taum (1140-1147): τ''_m/τ_m is an integer congruent to one modulo four, and 1/τ_m is an integer multiple of four.