LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13

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.

Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive

Statement

Complex conjugation is a real-field automorphism satisfying $\overline{z + w} = \overline{z} + \overline{w}, \overline{z w} = \overline{z} \overline{w}, \overline{\overline{z}} = z .$ For every $z, w \in C$ , $z \overline{z} = ∣ z ∣^{2}, ∣ z ∣ \geq 0, ∣ z ∣ = 0 ⟺ z = 0,$ $∣ z w ∣ = ∣ z ∣ ∣ w ∣, ∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣ .$

Facts & Assumptions

Given: $z = a + b i$ and $w = u + v i$ .

[F1]

Complex numbers have unique real coordinates and the coordinate addition and multiplication formulas ( $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})$ ).

[F2]

Conjugation and modulus are defined by $\overline{a + b i} = a - b i$ and $∣ a + b i ∣ = \sqrt{a^{2} + b^{2}}$ (Real and imaginary parts, complex conjugation, and modulus).

[F3]

The real numbers are a complete ordered field (The Cauchy-sequence reals have the least-upper-bound property), and every nonnegative element of a complete ordered field has a unique nonnegative square root (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[F4]

For nonnegative elements $r, s$ of an ordered field, $r \leq s$ if and only if $r^{2} \leq s^{2}$ (Squaring is monotone on the nonnegatives).

[F5]

The square of every nonzero element of an ordered field is positive (Squares of nonzero elements are positive).

Proof

technique · direct

1.1F1F2algebra

Coordinate expansion using [F1] and [F2] proves the two homomorphism laws, that conjugation fixes every real number, and that applying it twice is the identity. Thus conjugation is an involutive real-field automorphism.

1.2F1F2algebra

Direct multiplication gives $z \overline{z} = a^{2} + b^{2} = ∣ z ∣^{2}$ .

1.3F5algebra

Lagrange's identity gives $(a^{2} + b^{2}) (u^{2} + v^{2}) - (a u + b v)^{2} = (a v - b u)^{2} \geq 0.$ The final inequality follows from [F5], with the zero case included.

2.1F2F3F5step 1.2

By [F2] and [F3], $∣ z ∣ \geq 0$ . If $z = 0$ , then $∣ z ∣ = 0$ ; conversely, $∣ z ∣ = 0$ makes $a^{2} + b^{2} = 0$ , and [F5] forces $a = b = 0$ .

3.1F3step 1.1step 1.2step 2.1

Apply step 1.2 to $z w$ and use step 1.1: $∣ z w ∣^{2} = (z w) \overline{z w} = (z \overline{z}) (w \overline{w}) = ∣ z ∣^{2} ∣ w ∣^{2}$ . Both sides of $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ are nonnegative, so uniqueness in [F3] proves multiplicativity.

3.2F4step 2.1step 1.3

Hence $a u + b v \leq ∣ z ∣ ∣ w ∣$ : if $a u + b v \leq 0$ this follows from $∣ z ∣ ∣ w ∣ \geq 0$ ; otherwise both quantities are nonnegative, step 1.3 and [F4] give the inequality after squaring.

4.1F1F2step 1.2step 3.2algebra

Expanding with [F1] and [F2], then using step 3.2, gives $∣ z + w ∣^{2} = a^{2} + b^{2} + u^{2} + v^{2} + 2 (a u + b v) \leq (∣ z ∣ + ∣ w ∣)^{2} .$

5.1F4step 2.1step 4.1∎

Both sides of $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ are nonnegative, so [F4] turns the squared inequality in step 4.1 into the triangle inequality.

Depends on

Used by

Buffered certified rational phase approximation Algorithm
Certified complex-polynomial root isolation in exact algebraic arithmetic Algorithm
A holomorphic function of constant modulus on a domain is constant Corollary
exp(x+iy)=eˣ(cos y+i sin y), |exp(x+iy)|=eˣ, and e^iπ+1=0 Corollary
Orthogonal and unitary operators form groups, and their determinants have modulus one Corollary
The index of a cycle is locally constant off its trace and vanishes far from it Corollary
The induced length is a norm Corollary
The Jacobian determinant of a holomorphic map is |f'|² and is positive exactly where f'≠0 Corollary
The modulus of a holomorphic function on a closed polydisc is bounded by its supremum on the distinguished boundary Corollary
The unital algebra generated by a separating complex family and its conjugates is dense Corollary
A complete domain is necessary for sequential uniform boundedness Counterexample
A connected complex domain need not be star-shaped Counterexample
A connected plane domain that is not homologically simply connected Counterexample
A divergent Blaschke sum: no nonzero Hardy function has these zeros Counterexample
A holomorphic function on an annulus can have a nonzero closed-contour integral Counterexample
A nonconstant Blaschke factor has constant boundary modulus Counterexample
Boundary-scale derivative blowup despite bounded ball data Counterexample
The complement property is not sufficient for complex phase retrieval Counterexample
The disc algebra is unital and separating but not self-adjoint or dense Counterexample
The integers do not have property (T) Counterexample
Uniform convergence on the closed unit disc does not give a holomorphic extension to a larger disc Counterexample
z↦|z| is nowhere complex differentiable Counterexample
z↦|z|² is complex differentiable exactly at 0, with derivative 0, but is holomorphic on no neighbourhood of 0 Counterexample
zⁿ tends locally uniformly to zero on the unit disc but not uniformly on the closed disc Counterexample
Balls, polydiscs and the distinguished boundary in ℂᵐ Definition
Blaschke factors and Blaschke products Definition
Chebyshev constant of a compact planar set Definition
Complex L^∞ space of a locally compact group Definition
Direct integral of a measurable Hilbert field Definition
Fekete points and the transfinite diameter of a compact set Definition
Filled complex triangles, their oriented three-edge boundary contours, diameter, and perimeter Definition
Finite complex-array norms used by the NUFFT certificates Definition
Fourier coefficients and trigonometric polynomials on the torus Definition
Left-invariant means on L^∞ of a locally compact group Definition
Measurable and decomposable operator fields Definition
Measurable Beltrami coefficients and measurable conformal structures Definition
Positive definite functions on an abelian group Definition
Self-adjoint complex function algebras, unitality, and point separation Definition
Square-summable families on an arbitrary index set and the space ℓ²(I) Definition
The counting inner product on ℂ^ℤ/Nℤ Definition

…and 251 more results.

Dependency tree · two levels

23 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, Basic Analysis I: Complex Numbers and the Complex Exponential (standard reference, not scraped)

Conjugation is an involutive real-field automorphism, zz‾=∣z∣2zz=∣z∣2, and modulus is definite, multiplicative, and subadditive