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.
Balogh combinatorial map
Statement
Assume AC. Put and . There is a map , written , such that for every
there exist with , and for every .
Facts & Assumptions
Given: The set , continuum cardinal and the fixed regular rank level of the restriction data.
The countable model pair, all tuple types, finite-set and evaluation closure, countable-element inclusion, and trace injectivity on hold as proved in Balogh finite restriction data.
Realizable tuples have labels above their supports , and disjoint petals on supply infinitely many witnesses for every eligible root triple (Balogh countable restriction enumeration).
Specified rules admit transfinite recursion (Transfinite recursion).
AC is assumed for the preceding data, well-orders and model/witness selections (The Axiom of Choice).
Proof
Fix the enumeration and thinning in F2 under A1. For and set if and ; set if , that trace is outside , and it belongs to for some ; in every other case set . By disjointness of the petals in F2 the second clause has at most one such . The first two clauses have disjoint trace conditions, and all values are in . Thus these rules define a function and hence a fixed map , before any test functions are supplied. Empty contributes only the first or default clause.
Now fix arbitrary test functions of the stated types. F1 supplies countable with the parameters in , and F2 gives the label of their tuple. Write ; since , the ordinal is outside and . Put , , and for . The finite set and finite function belong to by its finite-set closure in F1; their binary values and ordered-pair codings belong there too. The set belongs to by definability and uniqueness. These bounded conditions on graphs are absolute in the transitive rank level of F1, and has low rank there. We have . It is uncountable: if it were countable, F1 would imply , contradicting .
There exists a maximal such that for distinct members. Indeed use A1 to well-order , and F3 to scan it, accepting a point exactly when it is compatible with all earlier accepted points. Every rejected point remains incompatible with an accepted point, so the resulting set is maximal. All subsets of and the finite intersection tests have rank below , as in F1. Consequently the existential assertion has its real meaning in , and elementarity gives such a , with actual maximality. If were countable, F1 would imply . For , the finite set would then be a subset of , and : it contains by and can meet only in . Thus could be adjoined, a contradiction. Therefore is uncountable.
If and some , then is the unique member of with , because two would violate the root-intersection equation. Since , uniqueness and elementarity put by F1. Hence implies . The set is uncountable by step 2.1 and countability of . Both , so it belongs to . Its intersection with is infinite: after any finite list of distinct members in , elementarity gives another member outside that finite list, using finite-set closure F1. For , one has and . Set and . Trace injectivity F1 makes well-defined. The trace test gives , and gives and . Injectivity also transfers the pairwise root intersections of to . Thus this infinite reflected set witnesses .
F2 now supplies a point with . It is in , and . Moreover is a finite subset of by F1, whereas , so . If , its trace lies in . Trace injectivity identifies it with the member of having that trace. Therefore , and the first defining clause gives . If instead , F1 says its trace is outside ; it lies in , so the second clause gives . These cases exhaust , including the empty case where no equations are required.
The map in step 1.1 is fixed independently of the arbitrary test functions, and step 4.1 provides their required pair with every listed property. Thus it satisfies the full quantified statement. QED.
Depends on
Used by
- Balogh continuum topology Definition
- Balogh failure of countable shrinking Lemma
Dependency tree · two levels
15 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.