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.

Extremal length of a rectangle and of a round annulus by hand

Sources

Christopher J. Bishop, Quasiconformal Mappings, Ch. 1 §1, printed pp. 4–5 (PDF pp. 9–10). Lemmas 1.6 and 1.7 give the rectangle and round-annulus constants by explicit test metrics and Cauchy–Schwarz on the respective foliations.
Mikhail Lyubich, Conformal Geometry and Dynamics of Quadratic Polynomials, vol. I, Ch. 1 §6.3.1, printed pp. 121–122. Proposition 6.6 computes the vertical family of an annulus, and Exercise 6.8 gives its dual circular family.

Example

Assume Countable Choice and use the conventions of Extremal length and the curve-family modulus of a path family.

(a) For $Π = (0, 2) \times (0, 1)$ and the family $Γ$ of paths joining the two vertical sides, $λ (Γ) = 2, μ (Γ) = \frac{1}{2} .$ The constant density $ρ = \frac{1}{2}$ gives $ℓ_{ρ} (Γ) \geq 1$ , has area $\frac{1}{2}$ , and has quotient $2$ . For every finite-positive-area Borel density, the horizontal slices and Cauchy–Schwarz give the matching upper bound.

(b) For $A = A (1, e^{2 π})$ , the connecting family $Γ_{A}$ has $λ (Γ_{A}) = 1, μ (Γ_{A}) = 1.$ The density $ρ (z) = 1 / (2 π ∣ z ∣)$ gives every connecting path length at least $1$ and has area $1$ . The radial Cauchy–Schwarz estimate gives the matching upper bound.

(c) Let $Θ_{A}$ be the family of closed paths in $A$ with winding number $1$ about $0$ . For every $0 < r < R$ , $λ (Γ_{A (r, R)}) λ (Θ_{A (r, R)}) = 1.$ For $A (1, e^{2 π})$ , both values are $1$ ; for $A (1, 2)$ , they are $\log 2 / (2 π)$ and $2 π / \log 2$ , respectively.

(d) Similarities $z \mapsto c z$ with $c \neq 0$ preserve the connecting-family extremal length of round annuli. In particular, $z \mapsto z / r$ sends $A (r, R)$ to $A (1, R / r)$ , and the conformal parameter $M$ defined in The conformal parameter of a round annulus is a complete invariant is $(2 π)^{- 1} \log (R / r)$ .

Facts & Assumptions

Given: Countable Choice; the rectangle and annulus curve families, and their Borel densities and area conventions.

[F1]

Borel densities are extended by zero outside their domain; nonrectifiable paths have infinite length. The path length equals the integral against arc length, is additive on subpath intervals, and agrees with the absolute line integral for continuous densities (Extremal length and the curve-family modulus of a path family, The rho-length and the extremal length are well defined).

[F2]

A Borel function on an open subspace extends by zero as a Borel function; Borel sets in a Euclidean product are product-measurable, and the product of the one-dimensional Lebesgue measures agrees with planar Lebesgue measure on Borel sets (The Borel sigma-algebra of a subspace is the trace of the ambient Borel sigma-algebra, The Borel product of R^m and R^n is the Borel sigma-algebra of R^{m+n}, On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}, A continuous map has Borel preimages of Borel sets, Arithmetic and lattice operations preserve measurability whenever they are defined).

[F3]

Tonelli interchanges nonnegative product integrals, and Cauchy–Schwarz applies to square-integrable slices (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Cauchy-Schwarz inequality for $L^{2}$ ).

[F4]

The polar map $P (s, θ) = s e^{i θ}$ is $C^{1}$ with determinant $s > 0$ . The Euclidean inverse-function theorem gives local $C^{1}$ inverses; uniqueness of the polar angle, shifted to the branch $0 < θ < 2 π$ , makes $P$ a global diffeomorphism onto the annulus with its positive radial cut removed (The Euclidean inverse function theorem, Every nonzero complex number has a unique polar form $r (\cos θ + i \sin θ)$ with $r > 0$ and $- π < θ \leq π$ ). The cut is a planar null set under Countable Choice (A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in $R^{n}$ ). The Borel change-of-variables theorem therefore gives, for every nonnegative Borel $g$ on $A (1, e^{2 π})$ , $\int_{A (1, e^{2 π})} g d A = \int_{0}^{2 π} \int_{1}^{e^{2 π}} g (s e^{i θ}) s d s d θ .$ (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions, A continuous map has Borel preimages of Borel sets, Arithmetic and lattice operations preserve measurability whenever they are defined)

[F5]

A rectifiable path crossing the two circles of a round annulus has $\int_{γ} ∣ d z ∣ / ∣ z ∣ \geq \log (R / r)$ . To prove this, cover its compact trace by discs avoiding zero, subdivide so each subpath lies in one disc, take a holomorphic logarithm of $z$ on each disc, and add the primitive integrals of $1 / z$ ; the real endpoint increment is $\log R - \log r$ . The modulus of a complex line integral is bounded by the absolute line integral (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset, Every open cover of a compact metric space has a Lebesgue number: a $δ > 0$ such that every nonempty subset of diameter less than $δ$ lies inside a single member of the cover, A nonvanishing holomorphic function on a disc has a holomorphic logarithm, A holomorphic logarithm is a primitive of the logarithmic derivative, The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path, The fundamental inequality: the modulus of the integral is at most the absolute line integral for rectifiable contours, Complex line integrals change sign under reversal and add under concatenation, The complex line integral over a rectifiable path as a componentwise Riemann–Stieltjes integral, The absolute line integral over a rectifiable path using its arc-length function, Continuous integrands have complex and absolute line integrals along every rectifiable path, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , The natural logarithm as the inverse of the exponential function).

[F6]

For the Borel test density $ρ (z) = 1 / (2 π ∣ z ∣)$ on $A (1, e^{2 π})$ , the Cauchy–Schwarz upper bound on radial slices is computed by $\int_{1}^{e^{2 π}} d s / s = 2 π$ ; also $\log (e^{2 π}) = 2 π$ and $π > 0$ (The natural logarithm as the inverse of the exponential function, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , Pi as twice the smallest positive zero of cosine).

[F7]

The round-annulus connecting-family extremal length is the conformal parameter $M (A (r, R)) = (2 π)^{- 1} \log (R / r)$ , and the winding-one closed-family value is its reciprocal (Extremal length of the rectangle and of the round annulus, The conformal parameter of a round annulus is a complete invariant). Similarities preserve the connecting-family value by the Borel change-of-variables formula and arc-length scaling (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions, A $C$ -Lipschitz map multiplies path length by at most $C$ ; isometries preserve length and scalar dilation multiplies it by the absolute scale).

Verification

technique · explicit test densities, slice estimates and the annulus formula

1.1F2F3F4given

For a Borel density on $Π$ , extend $ρ^{2} 1_{Π}$ by zero to $R^{2}$ . [F2] makes it product-measurable, and [F3] gives $A (ρ) = \int_{0}^{1} \int_{0}^{2} ρ (x, y)^{2} d x d y .$ For the annulus, [F4] gives the displayed polar area formula for arbitrary nonnegative Borel functions, not just continuous densities.

1.2F1F2F3givenalgebra

The constant rectangle density $ρ = \frac{1}{2}$ gives every crossing path Euclidean length at least $2$ , hence $ℓ_{ρ} (Γ) \geq 1$ . The box area formula gives $A (ρ) = 2 \cdot 1 \cdot (1 / 2)^{2} = 1 / 2$ , so the quotient is $2$ . For an arbitrary Borel density with $0 < A (ρ) < \infty$ , put $L = ℓ_{ρ} (Γ)$ . Each horizontal segment belongs to $Γ$ , so for every $y \in (0, 1)$ , $L \leq \int_{0}^{2} ρ (x, y) d x$ . Finite area and Tonelli give a full-measure set of $y$ with finite square integral; choosing one such $y$ first shows $L < \infty$ . On almost every such slice, [F3] gives $L^{2} \leq 2 \int_{0}^{2} ρ (x, y)^{2} d x$ . Integrating in $y$ gives $L^{2} \leq 2 A (ρ)$ . Thus every quotient is at most $2$ , and $λ (Γ) = 2$ , $μ (Γ) = 1 / 2$ .

1.3F1F4F5F6givenalgebra

Let $γ$ be any rectifiable path joining the boundary circles of $A (1, e^{2 π})$ . By [F5], $ℓ_{ρ} (γ) = \frac{1}{2 π} \int_{γ} ∣ d z ∣ / ∣ z ∣ \geq 1$ for $ρ (z) = 1 / (2 π ∣ z ∣)$ ; nonrectifiable paths have infinite length by [F1]. The polar area formula [F4] gives $A (ρ) = \int_{0}^{2 π} \int_{1}^{e^{2 π}} \frac{1}{4 π^{2} s^{2}} s d s d θ = 1.$ Hence this explicit metric gives quotient $1$ .

1.4F6F7algebra

For every $0 < r < R$ , [F7] gives $λ (Γ_{A (r, R)}) = (2 π)^{- 1} \log (R / r)$ and $λ (Θ_{A (r, R)}) = 2 π / \log (R / r)$ . Their product is $1$ . Substituting $R / r = e^{2 π}$ gives both values $1$ ; substituting $R / r = 2$ gives $\log 2 / (2 π)$ and $2 π / \log 2$ .

1.5F1F7givenalgebra

If $c \in C^{\times}$ , the similarity $f (z) = c z$ maps $A (r, R)$ bijectively onto $A (∣ c ∣ r, ∣ c ∣ R)$ . For a Borel density $τ$ on the target, $ρ (z) = ∣ c ∣ τ (c z)$ has the same $ρ$ -lengths on source paths as $τ$ has on their images, because arc length scales by $∣ c ∣$ ; its area is unchanged by the Jacobian $∣ c ∣^{2}$ and the Borel change-of-variables formula. The inverse similarity gives a bijection of the finite-positive-area metrics, so the extremal lengths agree. Taking $c = 1 / r$ and applying [F7] gives $M (A (r, R)) = (2 π)^{- 1} \log (R / r)$ .

2.1F1F3F4F6step 1.3given

For any Borel density $σ$ on the annulus with $0 < A (σ) < \infty$ , put $L = ℓ_{σ} (Γ_{A})$ . Every radial segment is in $Γ_{A}$ , so $L \leq \int_{1}^{e^{2 π}} σ (s e^{i θ}) d s$ for every $θ$ . By [F3, F4], a full-measure set of angles has finite weighted square integral; choosing one first shows $L < \infty$ . For almost every $θ$ , weighted Cauchy–Schwarz gives $L^{2} \leq (\int_{1}^{e^{2 π}} \frac{d s}{s}) \int_{1}^{e^{2 π}} σ (s e^{i θ})^{2} s d s = 2 π \int_{1}^{e^{2 π}} σ (s e^{i θ})^{2} s d s .$ Integrating in $θ$ and using [F3, F4] gives $2 π L^{2} \leq 2 π A (σ)$ , so every quotient is at most $1$ . With step 1.3, this proves $λ (Γ_{A}) = 1$ and $μ (Γ_{A}) = 1$ .

3.1F1F4F6given∎

The hypotheses always have $w = 2$ , $h = 1$ , and $1 < e^{2 π} < \infty$ ; the horizontal rectangle segments, radial annulus segments, and once-traversed circle show the assigned families are nonempty. All testing densities have positive finite area, all stated endpoints are boundary endpoints with zero arc-length mass, and no empty, zero-area, or degenerate-radius case is included. Countable Choice is used only through the explicitly declared measure and length interfaces; no full AC is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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