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.
Real and imaginary parts, complex conjugation, and modulus
Definition
Every has unique coordinates ( is a field, every element is uniquely , and every nonzero element has inverse ). Define and define its modulus by The real numbers are least-upper-bound complete (The Cauchy-sequence reals have the least-upper-bound property), so the nonnegative square root exists and is unique by Square roots exist: a unique with ; the positives are .
Depends on
- $\mathbb C=\mathbb R[x]/(x^2+1)$ is a field, every element is uniquely $a+bi$, and every nonzero element has inverse $(a-bi)/(a^2+b^2)$
- Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$; the positives are $\{x^2 : x \neq 0\}$
- The Cauchy-sequence reals have the least-upper-bound property
Used by
- Certified complex-polynomial root isolation in exact algebraic arithmetic Algorithm
- A holomorphic function with continuous complex derivative has C¹ real and imaginary components Corollary
- A positive reaction term restores coercivity without Poincar'e Corollary
- An inverse-error chain obeys Minkowski in L²; root-sum-square is equivalent to aggregate cross-term cancellation Corollary
- Eigenfunctions for distinct symmetric elliptic eigenvalues are L²-orthogonal Corollary
- Symmetric Lax--Milgram is energy minimisation Corollary
- The induced length is a norm Corollary
- The inner-product norm is definite, homogeneous, and satisfies the triangle inequality Corollary
- The principal logarithm is the normalised holomorphic branch on the slit plane Corollary
- The winding number is the increment of a continuous argument divided by 2π Corollary
- A bounded form without coercivity need not be solvable Counterexample
- A coercive form need not be symmetric Counterexample
- Boundary-scale derivative blowup despite bounded ball data Counterexample
- The absolute-value extension gives a zero complex-step quotient despite its real derivative 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
- The Neumann Poisson problem is not coercive on all of H¹ Counterexample
- Admissible polynomial pair for Hermitian-reflection QSP Definition
- Balls, polydiscs and the distinguished boundary in ℂᵐ Definition
- Blaschke factors and Blaschke products Definition
- Bounded, coercive and symmetric sesquilinear forms Definition
- C star algebra Definition
- Closed sectorial form and its associated operator Definition
- Complex associative algebra with involution Definition
- Complex L^∞ space of a locally compact group Definition
- Complex Lp classes and Euclidean test-function conventions Definition
- Complex norm and complex normed space Definition
- Continuous logarithms and continuous arguments along a contour Definition
- Dirac Notation Conversion Definition
- Direct integral of a measurable Hilbert field Definition
- Finite complex-array norms used by the NUFFT certificates Definition
- Green function with a pole at infinity Definition
- Holomorphic and antiholomorphic discrete-series models Definition
- Integrable real and complex functions, and their integrals Definition
- ℓ2 sample/query access to vectors and matrices Definition
- Left-invariant means on L^∞ of a locally compact group Definition
- Linear multistep methods, consistency, order, and the root condition Definition
- Logarithmic embedding of a number field Definition
- QSP signal matrix and ordered phase sequence Definition
…and 160 more results.
Dependency tree · two levels
19 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)