ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The identity welding of the round circle

Example

Assume the Axiom of Choice. Let $D = {z \in C : ∣ z ∣ < 1}$ and $T = \partial D$ , with $D^{*} = \hat{C} ∖ \overline{D}$ . Set $Γ = T$ , $Ω_{0} = D$ , $Ω_{1} = D^{*}$ , and take $f = {i d}_{D}$ and $g = {i d}_{D^{*}}$ . In the library convention $h = f^{- 1} \circ g ∣_{T}$ , this gives $h = {i d}_{T}$ , so the identity circle homeomorphism is welded by the round circle.

More generally, for $A, B \in Aut (D)$ let $\tilde{A}, \tilde{B}$ be their standard Möbius extensions to the sphere, and set $f = A : D \to D$ and $g = \tilde{B} ∣_{D^{*}} : D^{*} \to D^{*}$ . Then the welding is the Möbius circle homeomorphism $h = {\tilde{A}}^{- 1} \circ \tilde{B} ∣_{T}$ , and $h = {i d}_{T}$ if and only if $A = B$ .

Every welding of ${i d}_{T}$ has a generalized round circle as its welding curve: it is the image of $T$ under a Möbius transformation, hence is either a Euclidean circle or a straight line together with $\infty$ .

Facts & Assumptions

Given: AC, the unit disc $D$ , its exterior $D^{*}$ , and the round boundary $T$ .

[F1]

A conformal welding is a triple of complementary Jordan-domain parameter maps whose boundary extensions define $h = (\overline{f} ∣_{T})^{- 1} \circ (\overline{g} ∣_{T})$ (The welding homeomorphism of a Jordan curve). This is the library convention; Bishop's source convention is its inverse.

[F2]

The biholomorphic self-maps of $D$ form $Aut (D)$ ; each has the form $e^{i θ} (a - z) / (1 - \overline{a} z)$ and therefore extends to a Möbius transformation of the sphere preserving $D$ , $T$ , and $D^{*}$ (Conformal equivalence and the automorphism group of a domain, The unit disc, the upper half-plane, and Blaschke factors, Every automorphism of the disc is a rotated Blaschke factor, Möbius transformations of the Riemann sphere).

[F3]

The round circle $T$ is globally conformally removable (Round circles and straight lines are conformally removable).

[F4]

If the first welding curve is globally conformally removable, any second welding of the same homeomorphism is obtained by Möbius postcomposition of both parameter maps (Welding uniqueness for conformally removable curves, part (a)).

[F5]

A Möbius transformation $M (z) = (a z + b) / (c z + d)$ has $a d - b c \neq 0$ and maps $T$ to a generalized circle: for $w = M (z)$ , the condition $∣ z ∣ = 1$ becomes $∣ d w - b ∣ = ∣ a - c w ∣$ , a circle or line equation, with $\infty$ included in the line case (Möbius transformations of the Riemann sphere).

[F6]

The AC hypothesis of the welding definition and the round-circle and uniqueness suppliers is recorded by The Axiom of Choice.

Proof

technique · compute the boundary compositions directly, then apply conditional welding uniqueness to the removable round-circle example

1.1F1givenalgebra

The identity maps on $D$ and $D^{*}$ are conformal bijections, and their boundary extensions are both ${i d}_{T}$ . By [F1], their welding is ${i d}_{T}^{- 1} \circ {i d}_{T} = {i d}_{T}$ .

1.2F1F2given

By [F2], $\tilde{A}$ and $\tilde{B}$ preserve $D$ and $D^{*}$ , so the restrictions in the statement are conformal bijections of the two sides and extend to $T$ . Applying [F1] gives $h = {\tilde{A}}^{- 1} \circ \tilde{B} ∣_{T}$ . Its factors preserve the orientation of $T$ , so $h$ is an orientation-preserving Möbius circle homeomorphism.

2.1F2F5step 1.2algebra

If $A = B$ , their sphere extensions agree and the formula in step 1.2 gives $h = {i d}_{T}$ . Conversely, if $h = {i d}_{T}$ , the Möbius transformation $M = {\tilde{A}}^{- 1} \circ \tilde{B}$ fixes every $ζ \in T$ . Write $M (z) = (a z + b) / (c z + d)$ with $a d - b c \neq 0$ . Its denominator has no zero on $T$ , and each fixed point satisfies $c ζ^{2} + (d - a) ζ - b = 0$ . A polynomial of degree at most two that vanishes at three distinct points of $T$ is the zero polynomial; hence $c = b = 0$ and $d = a$ , so $M$ is the identity. Thus $\tilde{A} = \tilde{B}$ and $A = B$ .

3.1F3F4F5F6step 1.1∎

Let $(Γ^{'}, f^{'}, g^{'})$ be any other welding of ${i d}_{T}$ . By step 1.1, $(T, {i d}_{D}, {i d}_{D^{*}})$ is a welding of the same homeomorphism, and [F3] makes its first curve removable. Apply [F4] with this round welding first: a Möbius transformation $M$ satisfies $f^{'} = M \circ {i d}_{D}$ and $g^{'} = M \circ {i d}_{D^{*}}$ , so $Γ^{'} = M (T)$ . By [F5], this is a generalized round circle. The inherited AC premise is recorded in [F6].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Christopher J. Bishop, Conformal welding and Koebe's theorem, Ann. of Math. 166 (2007) 613-656 (standard reference, not scraped)
Malik Younsi, On removable sets for holomorphic functions, EMS Surv. Math. Sci. 2 (2015) 219-254 (standard reference, not scraped)
Mikhail Lyubich, Conformal Geometry and Dynamics of Quadratic Polynomials, vol. I (book draft, Stony Brook) (standard reference, not scraped)