Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24
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.

βN as the free ultrafilter algebra

Example

The free algebra on N for the ultrafilter monad has carrier βN and structure map

μN:ββNβN.

For WββN and AN,

AμN(W){UβN:AU}W.

Facts & Assumptions

Given: The ultrafilter monad on Set.

[L1]

The free T-algebra on an object A is (TA,μA) (Free algebra for a monad).

[L2]

Ultrafilter multiplication is the displayed flattening membership formula (The ultrafilter endofunctor with principal unit and flattening multiplication).

[L3]

The ultrafilter endofunctor with principal unit and flattening multiplication is a monad (The ultrafilter endofunctor with principal unit and flattening multiplication is a monad).

[L4]

The ultrafilter extension principle says that every filter on a set is contained in an ultrafilter on that set (The ultrafilter extension principle (UL/BPI)).

Verification

technique · direct
1.1

Applying [L1] and [L3] at A=N gives the free algebra (βN,μN). Its unit includes every natural, including 0 and 1, as the corresponding principal ultrafilter.

L1L3
2.1

Specializing the multiplication formula [L2] to X=N gives the displayed membership equivalence.

step 1.1L2
2.2

The algebra unit equation μNηβN=1 and associativity equation μNβ(μN)=μNμβN are exactly the monad unit and associativity laws in [L3].

step 1.1L3algebra
3.1

Assuming UL/BPI, apply [L4] to extend the cofinite filter on N to an ultrafilter. It is free: if it were principal at n, it would contain both {n} and the cofinite set N{n}. Thus βN contains both the principal ultrafilters from step 1.1 and free ultrafilters, but no free ultrafilter is claimed without UL/BPI.

step 2.1L4

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources