CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

A nonconstant Blaschke factor has constant boundary modulus

Statement refuted

A function holomorphic on the unit disc and continuous on its closure must be constant whenever its modulus is constant on the unit circle.

Facts & Assumptions

Given: A parameter $a \in C$ with $∣ a ∣ < 1$ and the Blaschke factor $B_{a} (z) : = \frac{z - a}{1 - \overline{a} z} .$ Complex conjugation and modulus obey $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ and $∣ z ∣^{2} = z \overline{z}$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive), and $C$ is a field ( $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ ).

[L1]

If a holomorphic function has constant modulus on the boundary of a bounded domain, then it is constant or has a zero in the domain (Constant boundary modulus forces an interior zero or constancy).

[L2]

A quotient of holomorphic functions is holomorphic wherever its denominator is nonzero (Linearity, product, reciprocal, and quotient rules for complex derivatives).

Counterexample

technique · direct

1.1

If $a = 0$ , the denominator is $1$ . If $a \neq 0$ , choose $R$ with $1 < R < 1 / ∣ a ∣$ ; for $∣ z ∣ < R$ one has $∣ \overline{a} z ∣ < 1$ , so $1 - \overline{a} z \neq 0$ . Thus [L2] makes $B_{a}$ holomorphic on a neighbourhood of the closed unit disc, and hence continuous there.

L2givenalgebra

2.1

When $∣ z ∣ = 1$ , direct expansion gives $∣ z - a ∣^{2} = 1 - z \overline{a} - a \overline{z} + ∣ a ∣^{2} = ∣ 1 - \overline{a} z ∣^{2} .$ The denominator is nonzero by step 1.1, so $∣ B_{a} (z) ∣ = 1$ on the entire unit circle.

step 1.1givenalgebra

3.1

Since $B_{a} (a) = 0$ and its boundary modulus is $1$ , the function is nonconstant. It therefore realizes the zero alternative in [L1] and refutes the proposed implication, including the case $a = 0$ , where $B_{0} (z) = z$ .

step 1.1step 2.1L1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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

J. Lebl, Guide to Cultivating Complex Analysis, Proposition 3.5.2 (standard reference, not scraped)