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 Luzin cylinder set gives a tight strongly unbounded coloring
Statement
Assume AC. If has size and the Luzin cylinder property, there is an injective-column tight strongly unbounded coloring . In fact has a countable downward cofinal family.
Facts & Assumptions
Given: Such a set and .
Every uncountable subset of is dense in some cylinder (Luzin sets, stick, and almost-disjoint guessing at omega one, clause 1).
Strong unboundedness, , and tightness have the quantified definitions of Tight strongly unbounded colorings.
Assume The Axiom of Choice; in particular countable choice is available.
Under countable choice a countable union of countable sets is countable (Countable unions of at most countable sets, assuming ).
Proof
Enumerate bijectively as and define . For an uncountable , injectivity makes uncountable. Choose its cylinder witness from F1 and put . For each , the extension is a prefix of some with . Hence , proving strong unboundedness, including when is empty.
Fix and . For each finite string set . Finite strings form a countable set: their length plus sum of entries stratifies them into finite sets. Remove from . By F3, using precisely the countable-choice consequence of A1, is countable; therefore is uncountable.
Apply F1 to the columns indexed by and choose such that every extension of occurs among them. Put . Every extension of belongs to , being a prefix of a column in . Every prefix of also belongs to , by taking one such column extending . Thus , without requiring that itself be prefix-closed.
Some has . Since , is uncountable. Every column extending has all its prefixes comparable with , so and . The fixed family is countable, and the inclusion and uncountability just proved show it is downward cofinal. This proves tightness with the stated stronger countable bound; injectivity was built into step 1.1.
Depends on
Used by
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
- Rinot–Shalev–Todorcevic, A new small Dowker space, Lemma 2.12 and Claims 2.12.1–2, p.5 (standard reference, not scraped)