noncomputable def FrameSingularity.angularCoord (p : ℝ × ℝ) : ℝ

structure FrameSingularity.IsOrthonormalTangentFrame (f : ℝ × ℝ → EuclideanSpace ℝ (Fin 3)) (X : ℝ × ℝ → Fin 2 → EuclideanSpace ℝ (Fin 3)) (S : Set (ℝ × ℝ)) : Prop

• tangent (p : ℝ × ℝ) : p ∈ S → ∀ (i : Fin 2), ∃ (a : ℝ) (b : ℝ), X p i = a • (fderiv ℝ f p) (1, 0) + b • (fderiv ℝ f p) (0, 1)
• orthonormal (p : ℝ × ℝ) : p ∈ S → ∀ (i j : Fin 2), inner ℝ (X p i) (X p j) = if i = j then 1 else 0

structure FrameSingularity.HasFrameSingularity (m : ℤ) (X : ℝ × ℝ → Fin 2 → EuclideanSpace ℝ (Fin 3)) (U : Set (ℝ × ℝ)) : Type

• f : ℝ × ℝ → EuclideanSpace ℝ (Fin 3)
• f_smooth : ContDiffOn ℝ ⊤ self.f U
• f_immersion (p : ℝ × ℝ) : p ∈ U → Function.Injective ⇑(fderiv ℝ self.f p)
• hU : (0, 0) ∈ U
• frame_tangent : IsOrthonormalTangentFrame self.f X (U \ {(0, 0)})
• smoothFrame : ℝ × ℝ → Fin 2 → EuclideanSpace ℝ (Fin 3)
• smooth_extends : ContDiffOn ℝ ⊤ (fun (p : ℝ × ℝ) => (self.smoothFrame p 0, self.smoothFrame p 1)) U
• smoothFrame_tangent : IsOrthonormalTangentFrame self.f self.smoothFrame U
• rotation_eq_fst (p : ℝ × ℝ) : p ∈ U \ {(0, 0)} → let θ := angularCoord p; X p 0 = Real.cos (↑m * θ) • self.smoothFrame p 0 - Real.sin (↑m * θ) • self.smoothFrame p 1
• rotation_eq_snd (p : ℝ × ℝ) : p ∈ U \ {(0, 0)} → let θ := angularCoord p; X p 1 = Real.sin (↑m * θ) • self.smoothFrame p 0 + Real.cos (↑m * θ) • self.smoothFrame p 1

noncomputable def FrameSingularity.dTheta (p : ℝ × ℝ) : ℝ × ℝ

noncomputable def FrameSingularity.circleIntegral1Form (α : ℝ × ℝ → ℝ × ℝ) (ρ : ℝ) : ℝ

theorem FrameSingularity.connection_integral_singularity (m : ℤ) (X : ℝ × ℝ → Fin 2 → EuclideanSpace ℝ (Fin 3)) (U : Set (ℝ × ℝ)) (α : ℝ × ℝ → ℝ × ℝ) (hsing : HasFrameSingularity m X U) (α' : ℝ × ℝ → ℝ × ℝ) (hα'_cont : ContinuousOn α' U) (hα_decomp : ∀ p ∈ U \ {(0, 0)}, α p = α' p - ↑m • dTheta p) : Filter.Tendsto (fun (ρ : ℝ) => circleIntegral1Form α ρ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-2 * Real.pi * ↑m))