Translation identities at the large Section 3 time scale.

theorem AVenhance.Infra.Section3.tauCellCount_mod_four (β : ℝ) (Λ m : ℕ) : Ingredients.tauCellCount β Λ m % 4 = 1

The number of small cells in a large cell is congruent to one modulo four.

theorem AVenhance.Infra.Section3.lIdx_add_twoCellCount {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) : lIdx β I.Λ m (k + 2 * ↑(Ingredients.tauCellCount β I.Λ m)) = lIdx β I.Λ m k + 2

Shifting the small integer index by two large cells advances the large cutoff index by exactly two.

theorem AVenhance.Infra.Section3.zetaProd_add_twoCellCount {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (t : ℝ) : I.zetaProd m (k + 2 * ↑(Ingredients.tauCellCount β I.Λ m)) (t + 2 * tauPP β I.Λ m) = I.zetaProd m k t

The product of the two time cutoffs is invariant when time and its small index are shifted together by two large cells.