The Schwarz reflection principle across the real axis

This file proves the summit of the conformal-mapping roadmap's Schwarz-reflection layer (L4 in ConformalMapping/README.md, the sorry-goal stated in ConformalMapping/Suggested.lean): on a conjugation-symmetric open set Ω, a function that is continuous on the closed upper part, holomorphic on the open upper part, and real on Ω ∩ ℝ extends holomorphically across the real axis. The extension is the explicit witness schwarzReflection f from Reflection/Basic.lean, whose gluing calculus (continuity on all of Ω, holomorphy off the axis, the derivative formulas and the conjugation symmetry) is already established there. What remains — and is proved here — is holomorphy at the axis — and that is exactly Painlevé removability of the real axis, TauCeti.differentiableOn_of_continuousOn_of_differentiableOn_im_ne_zero from Conformal/Removability/Basic.lean, where the Morera argument that supplies it is proved. So the reflection principle is now a two-line consequence of the two halves of its input: continuity of the extension across the axis, and holomorphy off it.

As with the rest of the L0–L3/L4 conformal-mapping material, this is coordinated with the upstream Mathlib Riemann-mapping effort leanprover-community/mathlib4#33505; L4 (reflection) is not part of that draft, so this is genuinely new Lean formalization, but any shared foundational API should be refactored to Mathlib's once it lands.

theorem TauCeti.differentiableOn_schwarzReflection_of_symmetric {f : ℂ → ℂ} {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hreal : ∀ z ∈ Ω, z.im = 0 → (f z).im = 0) : DifferentiableOn ℂ (schwarzReflection f) Ω

Schwarz reflection principle (real axis). On a conjugation-symmetric open set Ω, if f is continuous on the closed upper part, holomorphic on the open upper part, and real-valued on the real axis of Ω, then the explicit reflection extension schwarzReflection f is holomorphic on all of Ω — in particular across the real axis.

The gluing calculus (continuity everywhere, holomorphy off the axis, the conjugation symmetry) is Reflection/Basic.lean; the missing holomorphy at the axis is Painlevé removability, differentiableOn_of_continuousOn_of_differentiableOn_im_ne_zero.

theorem TauCeti.exists_differentiableOn_eqOn_conj_of_symmetric {f : ℂ → ℂ} {Ω : Set ℂ} (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hreal : ∀ z ∈ Ω, z.im = 0 → (f z).im = 0) : ∃ (F : ℂ → ℂ), DifferentiableOn ℂ F Ω ∧ Set.EqOn F f (Ω ∩ {z : ℂ | 0 ≤ z.im}) ∧ ∀ z ∈ Ω, F ((starRingEnd ℂ) z) = (starRingEnd ℂ) (F z)

Schwarz reflection principle, packaged existential form (the L4 milestone of ConformalMapping/Suggested.lean). On a conjugation-symmetric open Ω, a function continuous on the closed upper part, holomorphic on the open upper part, and real on the real axis extends to a function holomorphic on all of Ω that agrees with f on the closed upper part and satisfies the reflection symmetry F (conj z) = conj (F z). The explicit witness is schwarzReflection f.