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.
Van Hove sequence of bounded regions
Definition
Assume countable choice, fix an integer , and use the Euclidean norm from The Euclidean inner product on and the -dimensional Lebesgue measure from Lebesgue measurable sets, the family , and the restricted set function . Countable choice ensures the stated Lebesgue set function is a measure and every Borel set is Lebesgue measurable (The Axiom of Countable Choice (), Assuming countable choice, every Borel subset of is Lebesgue measurable). For , define , with . The topological boundary of is For a Lebesgue-measurable set , write . For a bounded set and , define its two-sided boundary layer where is the Euclidean distance just defined. A van Hove sequence is a sequence of bounded Lebesgue-measurable sets with , , and The boundary is closed, distance to a nonempty set is continuous, and for bounded its -neighborhood is bounded; hence each is Borel and has finite Lebesgue measure (Lebesgue measure is sigma-finite, and every metrically bounded subset of has finite outer measure). The condition controls both inner and outer boundary neighborhoods. It does not impose connectedness, a bounded aspect ratio, smooth boundaries, or a periodic identification.
Depends on
The Axiom of Countable Choice ()
The Euclidean inner product on
Lebesgue measurable sets, the family , and the restricted set function
The Borel sigma-algebra of a topological space
Assuming countable choice, every Borel subset of is Lebesgue measurable
Lebesgue measure is sigma-finite, and every metrically bounded subset of has finite outer measure