Alphabeta MathHow 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.
How universal regularity excludes the classical Choice pathologies
Example
Compare the four distinct obstruction calculations.
Facts & Assumptions
Given: Universal LM and PSP in the Solovay model.
The Solovay model has no Vitali or Bernstein set: supplies the translate and perfect-set contradictions.
The Solovay model has no Hamel basis and no discontinuous additive real function: supplies the kernel and bounded-level-set contradictions.
Verification
For a Vitali selector, rational translates are disjoint: measure zero makes their countable cover null, and positive measure makes finitely many translates exceed a containing interval.
For a Bernstein set, it and its complement contain no perfect subset; at least one is uncountable, contradicting PSP.
For a Hamel basis, one coefficient kernel is a proper measurable subgroup: positive measure makes it all of , while measure zero makes its rational-coset cover null.
For an additive map, a positive-measure bounded level set exists; Steinhaus makes the map bounded near zero and hence continuous and linear.
These are exactly the four named cases and use, respectively, translation invariance, PSP, subgroup rigidity, and Cauchy regularity; only countable ideal closure uses DC.
The comparison follows in all four cases.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
21 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.