Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-09
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.

Two finite disjoint petals can be made cross-incomparable

Statement

In ZFC, if T is an Aronszajn tree and W is an uncountable family of pairwise disjoint finite subsets of T, then distinct S,RW satisfy: every node in S is incomparable with every node in R.

Facts & Assumptions

Given: Such T and W; assume AC. Here a family is a set of distinct finite subsets, and “comparable” includes equality.

[F1]

Aronszajn trees have height ω1, countable levels and no cofinal branch. Aronszajn, Suslin and special trees

[F2]

On every uncountable set there is an ultrafilter all of whose members are uncountable and containing every cocountable subset. An ultrafilter containing all cocountable subsets

[F3]

If a finite union belongs to an ultrafilter, one of its terms belongs to it. Ultrafilters are prime: a union in U has a member in U

[F4]

Nodes with a common tree extension are comparable, and strict tree order strictly increases height; predecessors at a specified smaller height are unique. Tree predecessors and compatibility

[F5]

Countable unions of countable sets are countable under countable choice. Countable unions of at most countable sets, assuming ACω

[F6]

Filters are closed under pairwise intersections, omit the empty set, and are upward closed. Filter on a set

[A1]

Proof

1.1

If W, pair it with any other member; the conclusion is vacuous and there is another member because W is uncountable. Otherwise every member has positive size. Partition W by its finite sizes. F5 and A1 imply that some size m>0 occurs uncountably often; restrict to that subfamily, still denoted W. Use AC to fix for each SW an enumeration (xiS)i<m.

F5A1given
2.1

Fix an ultrafilter U on W as in F2. Suppose the conclusion fails. For xT and i<m let Y(x,i)={RW:x is comparable with xiR}. For fixed SW, failure supplies a comparable pair between S and every RS, so the finite union of Y(x,i) over xS,i<m contains W{S}. This cocountable set belongs to U, and upward closure F6 puts the union in U. F3 gives a pair (xS,iS) with xSS and Y(xS,iS)U. Use the already fixed finite enumeration and the usual order on m×m to take its first such pair.

F2F3F6step 1.1
3.1

Some k<m occurs as iS on an uncountable subfamily Z: otherwise its finitely many fibers would all be countable and F5 would make W countable. For distinct S,RZ, F6 gives V=Y(xS,k)Y(xR,k)U, so F2 says V is uncountable. Put γ=max{ht(xS),ht(xR)}+1<ω1. The set T<γ is countable by F1 and F5, since γ is countable. The map HxkH is injective on W because its members are disjoint. Consequently only countably many HV can have xkHT<γ. Choose an H outside those exceptions. Its kth node is comparable with xS,xR and strictly higher than both, so F4 forces it to extend both. Hence xS,xR are comparable.

F1F2F4F5F6A1step 1.1step 2.1
4.1

The set C={xS:SZ} is therefore an uncountable chain: injectivity follows from disjointness, and comparability from step 3.1. Its heights are unbounded in ω1, since any bounded collection of levels is countable by the same F1/F5 argument. Its downward closure B={t:cC (tTc)} is a chain: compare two witnesses in C and use F4 to compare both predecessors below the higher witness. It is cofinal. It is also maximal: if a node u is comparable with every member of B, take cC of height above u; F4 forces u<Tc, whence uB. Thus B is a cofinal branch, contradicting F1. The failure assumed in step 2.1 is impossible, proving the assertion.

F1F4F5A1step 2.1step 3.1

Depends on

Used by

Dependency tree · two levels

28 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