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.
Elementary sets: the finite unions of half-open boxes in
Definition
Fix . A subset is an elementary set when there are a natural number and a list of half-open boxes (Half-open boxes in and their volume), that is a function on whose values are half-open boxes, with
Write for the family of all elementary subsets of .
The list is part of the data of the presentation and not of the set: one elementary set has many presentations, and nothing below reads a presentation off a set. At the union is empty, so ; at every half-open box is elementary, included. The boxes of a presentation are not required to be disjoint or nonempty.
Remarks
-
Every elementary set does admit a disjoint presentation, by a common coordinate grid built from the parameters of the given list (Every elementary set is a finite disjoint union of half-open boxes, and any finitely many boxes admit a common grid refinement). That is a theorem about , not part of the definition, and keeping it out of the definition is what lets a presentation be produced by hand wherever one is convenient.
-
is an algebra and not merely a ring of sets (The elementary sets form an algebra of subsets of containing every half-open box), and that is exactly what the infinite parameters of Half-open boxes in and their volume buy: with real parameters only, every member of would be bounded and the family would not contain .