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.
John domains and the John constant
Definition
Assume Countable Choice. Let and let be open, bounded and nonempty. Its boundary is then a nonempty compact subset of contained in a sufficiently large closed ball (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space, For , every Euclidean closed ball and every Euclidean sphere of positive radius is compact), and the distance is defined for every and is a -Lipschitz function of (, so the distance to a fixed nonempty set is -Lipschitz).
Rectifiable curves, their arclength functions are used with the conventions of The arc-length function of a rectifiable path.
John domain and John constant. A pair with satisfies the John condition with constant if for every there is a rectifiable curve parametrised by arclength, with , and Write for the infimum of the admissible constants ; with the convention , this value belongs to . The domain is a John domain if for some , and is the John constant of the pair . The estimates below use an admissible constant, never the finiteness of the infimum alone, and whether the infimum is attained is immaterial.
Arclength form. If is arclength parametrised from , then for , because the straight segment from to is no longer than the curve. Hence a curve satisfying the arclength normalisation for all also satisfies the displayed relative-distance condition with the same constant . Only this implication is used here; the chain construction below uses the displayed relative-distance condition.
Connectedness. A John domain is path-connected and hence connected: given , choose curves from to and from to as in the definition (under Countable Choice the two curves may be chosen simultaneously) and traverse followed by the reverse of . No regularity of is assumed beyond what the definition uses.
Depends on
The arc-length function of a rectifiable path
The absolute line integral over a rectifiable path using its arc-length function
Interior, closure, boundary, limit point, isolated point and dense subset of a metric space
For , every Euclidean closed ball and every Euclidean sphere of positive radius is compact
, so the distance to a fixed nonempty set is -Lipschitz
The Axiom of Countable Choice ()