Essential spectrum of the shift via index local constancy + connected balls

Clean Lean route to σₑ(S) = unit circle for the unilateral shift S, once you have: (a) π S unitary in a C*-algebra, so spectrum_subset_unitary_of_mem_unitary + CStarRing.norm_of_mem_unitary give σₑ ⊆ sphere 0 1; (b) μ ↦ index (algebraMap μ - S) is ContinuousOn the complement of σₑ (Mathlib's index_continuousOn_isFredholm composed). Then (convex_ball 0 1).isPreconnected.constant (hf.mono hsub) hx hy (ℤ is discrete) gives index -1 on the open disc, and invertibility gives index 0 for |μ| > 1. For λ on the circle, get a ball around λ inside σₑᶜ from Metric.isOpen_iff. Then compare the points ((1 ∓ δ : ℝ) : ℂ) * λ. Write (t:ℂ)*μ - μ = ((t-1 : ℝ) : ℂ) * μ with push_cast; ring before taking norms. Also, spectrum.norm_le_norm_of_mem on ℓ² needs NormOneClass, i.e. a Nontrivial (lp (fun _ ↦ ℂ) 2) instance. Prove it with lp.single 2 0 1 ≠ 0.