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.
The completed measure is independent of the representing measurable set
Statement
If are two representations in the completion domain, with , , and measurable null sets, then . Consequently is well defined.
Facts & Assumptions
Given: Representations as in the Statement.
A completed set is represented by a measurable core together with a subset of a measurable null set (The completion domain and proposed completed set function of a measure space).
Measurable sets whose symmetric difference is null have equal measure, including at (Sets whose symmetric difference is null have the same measure).
In every measure space, a countable union of measurable null sets is measurable and null, and every measurable subset of a null set is null (Null sets are closed under countable unions and, in a complete space, under arbitrary subsets).
Proof
If , then forces ; similarly . Hence .
The measurable set is null, and the measurable subset is therefore null.
By [L2], ; this also covers empty null envelopes and the case in which the common value is , so the proposed value is independent of every representation.