Gelfand–Naimark norming states in Lean on top of Mathlib's GNS file

Mathlib's GelfandNaimarkSegal.lean gives f.gnsStarAlgHom but has no cyclic vector or states. Short route: (1) ζ := coe (f.toPreGNS 1). Then ⟪ζ, π a ζ⟫ = f a via Completion.inner_coe + preGNS_inner_def. GNS uniqueness: build [a] ↦ π a ξ with LinearMap.isometryOfInner and extend with LinearIsometry.fromCompletion (import Mathlib.Analysis.Normed.Operator.Extend explicitly; it is not re-exported). (2) ‖φ‖ ≤ 1 and φ 1 = 1 imply φ is positive: show φ(h) is real by bounding ‖h + algebraMap (t*I)‖² = ‖h*h + t²‖, then use CStarAlgebra.norm_le_iff_le_algebraMap to get ‖1 - b‖ ≤ 1 for 0 ≤ b ≤ 1. (3) A norming state for b ≥ 0: CStarAlgebra.nnnorm_mem_spectrum_of_nonneg, then StarSubalgebra.spectrum_eq (needs an IsClosed instance in context) on StarAlgebra.elemental ℂ b, which is a CommCStarAlgebra. Next WeakDual.CharacterSpace.mem_spectrum_iff_exists, then exists_extension_norm_eq; the character bound is AlgHom.norm_apply_le_self. Gotcha: rw [← inner_self_eq_norm_sq_to_K] fails because the RCLike vs Complex ofReal casts differ. Use have e := inner_self_eq_norm_sq_to_K (𝕜 := ℂ) v; refine e.symm.trans ?_.