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.
Balls, polydiscs and the distinguished boundary in
Definition
Fix and read through Complex -space and its real coordinate dictionary. A polyradius is a function with for every ; a single positive real abbreviates the constant polyradius with every .
For and a polyradius , the open polydisc, the closed polydisc and the distinguished boundary are
Thus is the set of points all of whose coordinates lie on their own circle: it is the product of the circles .
The open ball and closed ball of centre and radius are those of the norm of the dictionary, that is the sets and of Open ball, closed ball and sphere in a metric space and Euclidean spheres and closed balls as subspaces of .
Remarks
The distinguished boundary is not the topological boundary when . The topological boundary of consists of the points where at least one coordinate satisfies , whereas requires every coordinate to do so. For the two coincide. For the inclusion is proper: the point whose first coordinate is and whose remaining coordinates are lies in the topological boundary and not in .
Polydiscs are open and convex. Openness is coordinatewise: if for every , then for , because by the dictionary. Convexity in the sense of A convex subset of contains every line segment between two of its points is also coordinatewise: for in and , by Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive. Hence a polydisc is star-shaped with respect to each of its points (Star-shaped open subsets of Euclidean space). The same computation gives convexity of the closed polydisc.
Slices are discs. Fixing all coordinates but the th at values with , the set of with the resulting point in is exactly the open disc ; this is what makes the one-variable theory applicable one coordinate at a time. Moduli, real and imaginary parts are those of Real and imaginary parts, complex conjugation, and modulus.
Depends on
Complex -space and its real coordinate dictionary
Open ball, closed ball and sphere in a metric space
Euclidean spheres and closed balls as subspaces of
A convex subset of contains every line segment between two of its points
Star-shaped open subsets of Euclidean space
Real and imaginary parts, complex conjugation, and modulus
Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive