Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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 B=P({0,1,2}) and I=P({2})={,{2}}. Restriction to {0,1} identifies B/I with P({0,1}). The dual map is the inclusion of points 0,1 into the three-point Stone space. This calculation is in ZF.

Facts & Assumptions

[F1]

Boolean homomorphisms and quotient relation defines the ideal equivalence using symmetric difference.

[F2]

Quotient operations are well defined supplies the Boolean quotient and its factorization.

[F3]

Finite Boolean algebras are powersets of their atoms describes the finite ultrafilters by atoms.

[F4]

Stone ultrafilter space and its clopen basis defines the basic clopens of the ultrafilter space.

Verification

Given: The displayed algebra B and ideal I.

1.1

The family I contains zero, is downward closed and is closed under union; it omits {0,1,2}, so is proper. The condition AA{2} is equivalent to A{0,1}=A{0,1}: membership at 0,1 must agree, while membership at 2 is unrestricted. The four classes are {,{2}}, {{0},{0,2}}, {{1},{1,2}} and {{0,1},{0,1,2}}.

F1givenalgebra
2.1

Define r(A)=A{0,1}. It preserves unions and intersections, sends the two bounds to and {0,1}, and satisfies r({0,1,2}A)={0,1}r(A). Its zero fibre is I. F2 factors it through B/I; step 1.1 shows the factor sends the four classes bijectively to ,{0},{1},{0,1}. Thus it is the asserted Boolean isomorphism.

F2step 1.1algebra
3.1

The atoms of each powerset algebra are its singletons, so F3 identifies its ultrafilters with point filters. For i=0,1, the inverse image of the point filter Vi in P({0,1}) is r1[Vi]={A:ir(A)}={A:iA}=Ui in B. Its image contains exactly U0,U1, omitting U2. By F4 the preimage of any basic clopen [A] is the set of those Vi with iA{0,1}, explicitly the clopen [r(A)]. This is the stated two-point inclusion with its discrete topology. QED.

F3F4step 2.1algebra

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