Bridge single singularity base — task verification #
bridge_single_singularity_base is a proved theorem in Lecture14.lean (line 615),
reduced from circleIntegral_eq_sum_of_singularities with Fin 1.
The underlying axiom for the multi-singularity bridge construction is
circleIntegral_eq_sum_of_singularities_bridge (line 559), which requires
the Jordan curve theorem / piecewise smooth contour integration not in Mathlib.