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.
A finite quotient and its dual inclusion
Example
Let and . Restriction to identifies with . The dual map is the inclusion of points into the three-point Stone space. This calculation is in ZF.
Facts & Assumptions
Boolean homomorphisms and quotient relation defines the ideal equivalence using symmetric difference.
Quotient operations are well defined supplies the Boolean quotient and its factorization.
Finite Boolean algebras are powersets of their atoms describes the finite ultrafilters by atoms.
Stone ultrafilter space and its clopen basis defines the basic clopens of the ultrafilter space.
Verification
Given: The displayed algebra and ideal .
The family contains zero, is downward closed and is closed under union; it omits , so is proper. The condition is equivalent to : membership at must agree, while membership at is unrestricted. The four classes are , , and .
Define . It preserves unions and intersections, sends the two bounds to and , and satisfies . Its zero fibre is . F2 factors it through ; step 1.1 shows the factor sends the four classes bijectively to . Thus it is the asserted Boolean isomorphism.
The atoms of each powerset algebra are its singletons, so F3 identifies its ultrafilters with point filters. For , the inverse image of the point filter in is in . Its image contains exactly , omitting . By F4 the preimage of any basic clopen is the set of those with , explicitly the clopen . This is the stated two-point inclusion with its discrete topology. QED.
Used by
Nothing in the library uses this result yet.
Dependency tree · 0 levels
Nothing. This result depends on no other item in the library.
Sources
- Tressl, Stone Duality for Boolean Algebras, 4.1 (inverse-image map); local three-point quotient calculation (standard reference, not scraped)