Uniform continuity of normalized phase shifts

Slicing.IsLocallyFinite (WeakStabilityCondition/StabilityCondition/Foundation/StabilityCondition.lean) quantifies one radius η over all centres t: every window (t - η, t + η) must have finite-length objects. A normalized shift distorts windows, so transporting local finiteness across the action needs a uniform bound on that distortion, not a pointwise one.

Uniform continuity is not automatic for a continuous bijection of ℝ. It holds here because of map_add_one: f commutes with x ↦ x + 1, so its behaviour on all of ℝ is determined by a compact window, and the modulus obtained there transfers everywhere by integer translation. map_add_int is that transfer, and uniformContinuous is the argument.

exists_radius packages the uniform window estimate needed to transport local finiteness.

Integer translation

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.NormalizedShift.map_add_nat (f : NormalizedShift) (n : ℕ) (x : ℝ) : f.toOrderIso (x + ↑n) = f.toOrderIso x + ↑n

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.NormalizedShift.map_sub_nat (f : NormalizedShift) (m : ℕ) (x : ℝ) : f.toOrderIso (x - ↑m) = f.toOrderIso x - ↑m

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.NormalizedShift.map_add_int (f : NormalizedShift) (n : ℤ) (x : ℝ) : f.toOrderIso (x + ↑n) = f.toOrderIso x + ↑n

f commutes with translation by any integer, not just by 1.

Uniform continuity

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.NormalizedShift.uniformContinuous (f : NormalizedShift) : UniformContinuous ⇑f.toOrderIso

A normalized shift is uniformly continuous.

Continuity alone is free (OrderIso.continuous); uniformity is not, and a general continuous bijection of ℝ does not have it. The +1-equivariance is what buys it: fix a modulus on the compact window [-1, 2], then move any pair of nearby points into that window by an integer translation, which map_add_int says f respects exactly.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.NormalizedShift.exists_radius (f : NormalizedShift) {w M : ℝ} (hw : 0 < w) (hM : 0 < M) : ∃ (η : ℝ), 0 < η ∧ η < M ∧ ∀ (t : ℝ), f.toOrderIso (t + η) - f.toOrderIso (t - η) < w

Windows can be shrunk uniformly: given a target width w and a ceiling M, there is a radius η < M such that f carries every window (t - η, t + η) into an interval of width < w.

The quantifier order is the whole point — one η for all centres t. That is what IsLocallyFinite demands and what pointwise continuity would not give.