ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 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.

Constant coefficients and their affine solutions

Statement

Assume the Axiom of Choice. It implies Countable Choice (The Axiom of Choice, AC implies DC implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )). Fix $ν \in C$ with $∣ ν ∣ < 1$ , and let $μ$ be the sphere Beltrami coefficient whose finite-chart representative is the constant $ν$ (Measurable Beltrami coefficients and measurable conformal structures, The standard holomorphic charts on the Riemann sphere, with holomorphy and poles at infinity, The Riemann sphere is the published one-point compactification of the complex plane).

(a) Affine solution. The real-linear map $A (z) = z + ν \overset{ˉ}{z}$ is an orientation-preserving analytically quasiconformal homeomorphism of $C$ onto itself (Orientation-preserving homeomorphisms and the geometric definition of quasiconformality, The ACL and Sobolev analytic definition of quasiconformality). Its inverse, Wirtinger derivatives, Beltrami coefficient, and maximal dilatation are $A^{- 1} (w) = \frac{w - ν \overset{ˉ}{w}}{1 - ∣ ν ∣^{2}}, A_{z} \equiv 1, A_{\overset{ˉ}{z}} \equiv ν, μ_{A} \equiv ν, K_{A} = \frac{1 + ∣ ν ∣}{1 - ∣ ν ∣}$ (The Wirtinger derivatives $\partial_{z} f$ and $\partial_{\overset{ˉ}{z}} f$ , and antiholomorphic functions, The Beltrami coefficient and the maximal dilatation). More generally, every orientation-preserving real-affine solution $g (z) = a z + b \overset{ˉ}{z} + c$ of $g_{\overset{ˉ}{z}} = ν g_{z}$ on a complex domain has $b = ν a$ , $a \neq 0$ , and hence the form $g (z) = a (z + ν \overset{ˉ}{z}) + c$ (A complex domain is a nonempty connected open subset of $C$ ).

(b) Normalized sphere solution. The map $f^{ν} (z) : = \frac{z + ν \overset{ˉ}{z}}{1 + ν}, f^{ν} (\infty) : = \infty$ is an orientation-preserving quasiconformal homeomorphism and sphere weak solution: it fixes $0, 1, \infty$ and solves $f_{\overset{ˉ}{z}} = μ f_{z}$ in the sphere charts (Weak solutions of the Beltrami equation, The standard holomorphic charts on the Riemann sphere, with holomorphy and poles at infinity). It is unique among normalized orientation-preserving quasiconformal homeomorphic solutions. The full set of orientation-preserving quasiconformal homeomorphic sphere solutions is exactly ${M \circ f^{ν} : M is M \ddot{o} bius}$ (The measurable Riemann mapping theorem on the sphere, Möbius transformations of the Riemann sphere).

(c) Ellipse distortion. The ellipse $A (S^{1})$ has major-to-minor semiaxis ratio $K_{A} = (1 + ∣ ν ∣) / (1 - ∣ ν ∣)$ , equal to the ratio prescribed by the coefficient $ν$ (Measurable Beltrami coefficients and measurable conformal structures(b)). Multiplication by $(1 + ν)^{- 1}$ does not change that ratio, and when $ν = 0$ the normalized map is the identity.

Facts & Assumptions

Given: AC; $ν \in C$ with $∣ ν ∣ < 1$ ; and the sphere coefficient $μ$ with finite-chart representative $ν$ .

[F1]

AC implies Countable Choice, required by the measurable-coefficient, weak-solution and ACL interfaces (The Axiom of Choice, AC implies DC implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F2]

A sphere Beltrami coefficient is specified by its finite-chart representative; the infinity-chart expression is the holomorphic pullback and preserves its essential norm. The weak-solution equation is chart-independent under these pullbacks (Measurable Beltrami coefficients and measurable conformal structures, Weak solutions of the Beltrami equation, The standard holomorphic charts on the Riemann sphere, with holomorphy and poles at infinity, The Riemann sphere is the published one-point compactification of the complex plane).

[F3]

For a real-differentiable map, $f_{z}$ and $f_{\overset{ˉ}{z}}$ are the two Wirtinger coefficients of its real differential; for $A (z) = z + ν \overset{ˉ}{z}$ , they are $1$ and $ν$ (The Wirtinger derivatives $\partial_{z} f$ and $\partial_{\overset{ˉ}{z}} f$ , and antiholomorphic functions).

[F4]

For a real-affine map, coordinate-line restrictions are absolutely continuous with constant derivatives, so the ACL characterization The ACL characterisation of $W^{1, p}$ gives local $W^{1, 2}$ membership. An analytic quasiconformal homeomorphism has $W_{l o c}^{1, 2}$ regularity and satisfies $∣ f_{\overset{ˉ}{z}} ∣ \leq k ∣ f_{z} ∣$ for $k = (K - 1) / (K + 1)$ ; its maximal dilatation is determined by its Beltrami coefficient (The ACL and Sobolev analytic definition of quasiconformality, The Beltrami coefficient and the maximal dilatation).

[F5]

A real-linear isomorphism preserves orientation exactly when its determinant is positive; for $A$ the determinant is $1 - ∣ ν ∣^{2}$ (A real linear isomorphism preserves or reverses orientation according to the sign of its determinant).

[F6]

A positive real determinant gives the positive local orientation sign; the sign of a homeomorphism is locally constant, and the holomorphic sphere-chart transition preserves orientation. Thus the positive finite-chart sign gives the same sphere orientation at infinity (A real linear isomorphism preserves or reverses orientation according to the sign of its determinant, Orientation-preserving homeomorphisms and the geometric definition of quasiconformality, The standard holomorphic charts on the Riemann sphere, with holomorphy and poles at infinity).

[F7]

On the sphere, holomorphic source and target chart changes transport both the coefficient and weak equation; a locally Lipschitz chart expression with bounded classical derivatives away from one point is in $W_{l o c}^{1, 2}$ by the ACL characterization The ACL characterisation of $W^{1, p}$ , and its value at one point does not affect the a.e. equation. Since every chart expression of $μ$ has modulus $∣ ν ∣$ , the weak equation gives the analytic quasiconformal inequality in each chart (The standard holomorphic charts on the Riemann sphere, with holomorphy and poles at infinity, Measurable Beltrami coefficients and measurable conformal structures, Weak solutions of the Beltrami equation, The ACL and Sobolev analytic definition of quasiconformality).

[F8]

Among orientation-preserving quasiconformal homeomorphic sphere solutions, the normalized measurable Riemann mapping theorem gives existence and uniqueness of the three-point normalized solution and identifies all such solutions as its Möbius postcompositions (The measurable Riemann mapping theorem on the sphere).

[F9]

The ellipse-field definition assigns axis ratio $(1 + ∣ ν ∣) / (1 - ∣ ν ∣)$ to coefficient $ν$ (Measurable Beltrami coefficients and measurable conformal structures(b)).

Proof

technique · compute the real-linear map and extend its normalized multiple to the sphere

1.1F1F3F4F5givenalgebra

Put $s : = ∣ ν ∣ < 1$ . The inverse formula follows from $w - ν \overset{ˉ}{w} = (1 - ∣ ν ∣^{2}) z$ . By [F3], $A_{z} = 1$ and $A_{\overset{ˉ}{z}} = ν$ , so $J_{A} = 1 - ∣ ν ∣^{2} > 0$ ; the inverse makes $A$ a homeomorphism. By [F4], it is analytically $K_{A}$ -quasiconformal with coefficient $ν$ , where $K_{A} = (1 + s) / (1 - s)$ ; [F5] gives orientation preservation.

1.2F3F5givenalgebra

If $g (z) = a z + b \overset{ˉ}{z} + c$ , then $g_{z} = a$ and $g_{\overset{ˉ}{z}} = b$ . Thus the equation is equivalent to $b = ν a$ . Its Jacobian is $∣ a ∣^{2} - ∣ b ∣^{2} = (1 - ∣ ν ∣^{2}) ∣ a ∣^{2}$ , so an orientation-preserving solution has $a \neq 0$ ; conversely any such $a$ gives the stated real-affine solution.

2.1F2F3F6F7step 1.1given

Since $∣ ν ∣ < 1$ , $1 + ν \neq 0$ and $f^{ν} = (1 + ν)^{- 1} A$ is invertible on $C$ . Its lower bound $∣ f^{ν} (z) ∣ \geq (1 - ∣ ν ∣) ∣ z ∣ / ∣ 1 + ν ∣$ shows it extends continuously by $f^{ν} (\infty) = \infty$ , and its inverse extends likewise. In the source and target infinity coordinates $w = 1 / z$ and $η = 1 / f^{ν} (z)$ , the expression is $η (w) = \frac{(1 + ν) w \overset{ˉ}{w}}{\overset{ˉ}{w} + ν w}, η (0) = 0.$ For $w \neq 0$ , $∣ \overset{ˉ}{w} + ν w ∣ \geq (1 - ∣ ν ∣) ∣ w ∣$ ; the expression is homogeneous of degree one and smooth on the punctured disk, so its derivative is bounded there by its bound on the unit circle, while $∣ η (w) ∣ = O (∣ w ∣)$ . The bounded derivative gives a Lipschitz bound along segments avoiding $0$ , and continuity extends that bound across $0$ . Its coordinate-line restrictions are therefore absolutely continuous: the sum of their increments is bounded by the Lipschitz constant times the total interval length. Their derivatives are bounded off $0$ , hence locally square-integrable, so the ACL characterization in [F7] gives $W_{l o c}^{1, 2}$ at $0$ . In the finite chart, $f_{\overset{ˉ}{z}}^{ν} = ν f_{z}^{ν}$ ; the coefficient pullback in [F7] gives the same weak equation in the infinity chart, with the point $w = 0$ immaterial. The local orientation sign remains positive by [F6]. Hence $f^{ν}$ is a sphere weak solution and orientation-preserving quasiconformal homeomorphism. Direct substitution gives $f^{ν} (0) = 0$ and $f^{ν} (1) = 1$ .

3.1F1F8step 2.1given

The Axiom of Choice permits use of [F8]. Step 2.1 proves that $f^{ν}$ is a normalized orientation-preserving quasiconformal homeomorphic solution, so uniqueness in [F8] identifies it with the normalized MRMT solution. Every other orientation-preserving quasiconformal homeomorphic sphere solution is its Möbius postcomposition by [F8], and every such postcomposition is a solution.

4.1F9step 1.1givenalgebra∎

If $ν = 0$ , then $A$ and $f^{0}$ are the identity and the ellipse ratio is $1$ . Otherwise write $ν = s e^{i θ}$ and set $z = e^{i θ / 2} (x + i y)$ . Then $A (z) = e^{i θ / 2} ((1 + s) x + i (1 - s) y) .$ Thus $A (S^{1})$ has semiaxes $1 + s$ and $1 - s$ , so its ratio is $(1 + s) / (1 - s) = K_{A}$ , which also equals the coefficient ellipse ratio by [F9]. Multiplication by $(1 + ν)^{- 1}$ scales and rotates both axes equally.

Source notes

Bishop, Ch. 2 §1, printed pp. 49–51, was read in full. It derives the real-linear form $α z + β \overset{ˉ}{z}$ , the complex dilatation $μ = β / α$ , the ratio $D = (1 + ∣ μ ∣) / (1 - ∣ μ ∣)$ , and the major-axis direction. The Step 1 locator “Ch. 3 §1, p. 85” was corrected to this exact passage. Lyubich §14.1, printed p. 196, was read in full for uniqueness up to conformal postcomposition.

Supplier reconciliation

The explicit maps and calculations above remain unchanged. Their exact normalized uniqueness and solution-family uses now consume the complete stable MRMT proof, and their analytic conventions consume the earlier12 definitions/equivalence. Root decisions and full-run certification are separate.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

125 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, Quasiconformal Mappings (Stony Brook Math 627 course notes) (standard reference, not scraped)
Mikhail Lyubich, Conformal Geometry and Dynamics of Quadratic Polynomials, vol. I (book draft, Stony Brook) (standard reference, not scraped)