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.
An event of positive probability in a finite probability space is nonempty
Statement
If an event in a finite probability space has , then is nonempty.
Facts & Assumptions
Given: An event in a finite probability space.
The empty event has probability zero (Normalization, nonnegativity, monotonicity, complements, and differences in a finite probability space).
Proof
Assume is empty.
Then by [L1], so is not positive.
The contrapositive proves that positive probability implies nonemptiness. It asserts existence of an outcome, not a canonical choice of one.
Depends on
Used by
- A parameter ledger for the high-girth, high-chromatic alteration proof Example
- The random-colouring proof of R(k,k)>2^k/2 Example
- A k-uniform hypergraph is 2-colourable when every edge meets at most d other edges and e(d+1)≤2ᵏ⁻¹ Theorem
- For all positive k,ℓ, some finite graph has girth greater than ℓ and chromatic number greater than k Theorem
- If k≥1 and n≥3k² 2ᵏ, an n-vertex tournament with property Sₖ exists Theorem
- The first-moment method for avoiding or forcing a finite count of bad events Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 22 results over 8 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- J. Matousek and J. Vondrak, The Probabilistic Method, Chapter 2 (standard reference, not scraped)
- Y. Zhao, MIT 18.218 Probabilistic Method in Combinatorics, Section 2.1 (standard reference, not scraped)