Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-14
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.

Random and Cohen generics over an intermediate model are conull and comeagre

Statement

If an intermediate transitive N has countably many reals in V[G], the N-random reals are conull and the N-Cohen-generic reals are comeagre in V[G].

Facts & Assumptions

Given: Such an intermediate N.

[F2]

Borel-code, measure, category, and perfect-set absoluteness: coded null/meagre witnesses and their countable unions are absolute.

[F3]

The Axiom of Choice: ambient AC enumerates the codes.

Proof

1.1

Borel codes are reals, so F1 and ambient AC enumerate all N-coded Borel null sets as (Cn). A real is not random over N exactly when it belongs to one of these null sets (every random-algebra dense failure has such a coded null witness). Thus the nonrandom reals lie in C=nCn, which is null by F2.

F1F2F3
2.1

Similarly enumerate the N-coded closed nowhere-dense sets. A real failing Cohen genericity misses an N-coded dense open set, hence belongs to its closed nowhere-dense complement. Their union is meagre by F2, so its complement, the N-Cohen generics, is comeagre. Empty coded exceptions and a model with finitely many codes are covered by repeating codes in the enumeration.

F1F2F3

Depends on

Used by

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.

Sources