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

Sweet density transfers along complete suborders

Statement

Assume ZFC. Let P be a complete suborder of B+=BA(Q)∖{0B} (write B=BA(Q)), let (Q,D,(En)) be a sweetness model, and let (Aj)j<ω be subsets of P whose union is dense in P. Write e:Q→B∖{0B} for the canonical dense completion map, and use Shelah's quotient convention

p⊩Pq∈Q/P⟺every p0∈P with p0≤p is compatible in B with e(q).

Suppose q∈D and p∈P forces q∈Q/P. Then some j,k<ω have the following uniform property: for every q′Ekq there is p′∈Aj with p′≤p which forces q′∈Q/P. Moreover, the union of all Aj for which such a k exists is dense below p. This is the full two-part conclusion of Claim 7.4 of the source, in the library order.

Facts & Assumptions

Given: ZFC and the objects and quotient convention in the Statement.

[F1]

Shelah sweetness models for forcing: (Q,D,(En)) satisfies the sequential clause and the transfer clause, and its En-classes are downward directed. The same definition says that P is a complete suborder of B when its order and incompatibility are inherited from B+ and every maximal antichain of P remains maximal in B+.

[F2]

Choice-free regular open completion of forcing preorders (with forcing equivalence as in Forcing equivalence and Boolean completion) and Completeness, regular opens, and order continuity: the canonical map e:Q→B∖{0B} preserves order, preserves and reflects compatibility, and has order-dense image. It need not be injective or reflect the original order.

[F3]

By the displayed quotient convention, p⊩Pq∈Q/P is monotone in p and upward closed in q: if p′≤p and q′≤q, then p⊩Pq′∈Q/P implies p′⊩Pq∈Q/P.

[F4]

The Axiom of Choice supplies choices from nonempty witness sets. Under this assumption Zorn's lemma gives a maximal element of any nonempty poset in which every chain has an upper bound.

[F5]

N×N≈N gives the unique decomposition of every positive natural into 2m(2r+1). Thus define n(i)=m from i+1=2m(2r+1) for every i∈N.

Proof

1.1F5

Fix the canonical surjection n(i)=m where i+1=2m(2r+1), For fixed m, the indices i=2m(2r+1)−1 as r varies are unbounded, so m occurs arbitrarily late; in particular n(0)=0.

1.2F3

The Boolean conditions p and e(q) are compatible in B: the quotient hypothesis applied to p0=p says exactly that they are compatible.

2.1F1F4step 1.1

For each i<ω, use [F4] to choose qi∈D with qiEiq so that, whenever there exists q′Eiq for which no p′∈An(i) satisfies p′≤p and p′⊩q′∈Q/P, the chosen qi has that property. The admissible set is nonempty: choose a bad witness if one exists, and otherwise use q itself.

2.2F1F2step 1.2

There is r∈D with r≤q and e(r)≤p. Indeed step 1.2 gives a nonzero b≤p∧e(q) in B. Density of e[Q] supplies s∈Q with e(s)≤b. Then e(s) and e(q) are compatible, so compatibility reflection in [F2] supplies a common strengthening t≤s,q in Q. Finally density of D supplies r∈D with r≤t. Order preservation gives e(r)≤e(s)≤p, while r≤q.

3.1F1F2step 2.2

There is k<ω such that every q′Ekq has e(q′) compatible with p. Apply the comparable form of the transfer clause to r≤q at n=0. It supplies k such that every q′Ekq has some r′E0r with r′≤r,q′. Hence e(r′)≤e(r)≤p and e(r′)≤e(q′), so e(r′) witnesses the required Boolean compatibility.

3.2F1step 2.1

The sequence (qi) extends to the diagonal witness: since qiEiq and Ei refines Ek for all i≥k, the sequential clause applied to the sequence with last term q gives q∗∈D with q∗Ekq and q∗≤qi for every i≥k.

4.1F1F3F4step 3.1step 3.2

Since q∗Ekq, step 3.1 makes e(q∗) compatible with p. We claim that some p′′≤p in P forces q∗∈Q/P. Otherwise the quotient convention makes C={s∈P:s≤p and s⊥Be(q∗)} dense below p in P. Apply [F4] to the poset of antichains contained in C, ordered by inclusion: the empty antichain is present and unions bound chains because any two elements of a chain union occur together in one antichain. Obtain a maximal such A. It is predense below p: otherwise a condition below p incompatible with all of A has a strengthening in C that could be added. Apply the same argument to antichains of P containing A to obtain a maximal antichain M of P. Every member of M∖A is incompatible with p: if such an m were compatible with p, a common strengthening in P would be compatible with some member of the predense antichain A below p, contradicting that M is an antichain. By completeness of the suborder [F1], M is maximal in B. But a common Boolean strengthening of p and e(q∗) is incompatible with every member of A (by the definition of C) and every member of M∖A (because they are incompatible with p), contradicting maximality in B. This proves the claim. Now choose p′∈Aj below p′′ from the dense union of the Aj. Then p′≤p and p′⊩q∗∈Q/P; by upward closure in [F3], it also forces every q′∈Q with q∗≤q′ into the quotient.

5.1step 1.1step 2.1step 4.1

Choose i≥k with n(i)=j, possible by step 1.1. Then p′∈An(i) satisfies p′≤p and, since q∗≤qi, forces qi∈Q/P; so qi is not bad at level i. By step 2.1 the existence of a bad witness at level i would have forced qi to be bad, hence no q′Eiq is bad for An(i): for every q′Eiq there is p′∈Aj with p′≤p and p′⊩q′∈Q/P. Thus the pair (Aj,i) has the uniform property required in part (1) of the Statement.

6.1F3step 5.1

Let A∗=⋃{Aj:for some k, Aj has the uniform property for k}. Given p0≤p, the hypothesis p0⊩q∈Q/P holds by monotonicity [F3], so the argument of steps 1.2 through 5.1 with p0 in place of p produces j,k such that every q′Ekq, in particular q′=q, has a condition p′∈Aj below p0 forcing q′∈Q/P; The uniform property below p0 implies the one below p since every witness below p0 is below p, so this Aj is included in A∗. Hence A∗ meets every strengthening of p and is dense below p.

7.1step 5.1step 6.1∎

The steps above establish both conclusions of the Statement.

Depends on

Used by

Dependency tree · two levels

48 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