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

Pcf cofinality ideals and cutoff conventions

Statement

Assume AC. For a set A of infinite regular cardinals and a cardinal λ, put

J<λ[A]={EA:pcf(E)λ},Jλ[A]=J<λ+[A].

The first condition means that every member of pcf(E) is strictly less than λ. These are possibly improper ideals, increasing with the cutoff, and for BA one has J<λ[B]=J<λ[A]P(B). The singleton {a} belongs to J<λ[A] exactly when a<λ. If λpcf(A), then J<λ[A] is proper.

Membership of E in J<λ[A] is equivalent to every ultrafilter D on A containing E having cf(A/D)<λ. With J={AE:EJ}, one has

J<λ[A]={D:D is an ultrafilter on A, cf(A/D)λ}.

The intersection of an empty family here is taken inside P(A), hence equals P(A); in that case the dual is an improper filter family. No assertion is made here that a fixed ultrafilter of cofinality below λ must meet J<λ[A]; that later cutoff theorem needs directedness.

Facts & Assumptions

Given: AC, a set A of infinite regular cardinals, a cardinal λ, and the displayed definitions.

[F1]

The PCF transfer lemma proves the empty and singleton values, monotonicity, and finite-union preservation (Progressive products and true cofinality transfers, Statement).

[F2]

An ultrafilter contains exactly one of each set and its complement (Characterisation of ultrafilters: every set or its complement).

[F3]

Restriction to a support in an ultrafilter and extension from that support preserve the ultraproduct order and cofinality (Progressive products and true cofinality transfers, Statement, support-restriction clause).

[A1]

AC is assumed, as in the PCF transfer lemma (The Axiom of Choice).

Proof

1.1

Since pcf()=, the empty set belongs to J<λ[A]. If E belongs and HE, monotonicity gives pcf(H)pcf(E)λ. If E,H both belong, finite-union preservation gives pcf(EH)=pcf(E)pcf(H)λ. Thus it is an ideal; the same argument with λ+ gives Jλ. Larger cutoffs enlarge the ideals because the corresponding ordinal intervals are nested. For EBA, the statement pcf(E)λ does not depend on the ambient set, proving the restriction identity in both directions.

F1A1given
1.2

By the singleton calculation, pcf({a})={a}, so its membership is exactly a<λ, including failure at the endpoint a=λ. If λpcf(A), then pcf(A)⊈λ, so AJ<λ[A]. If A is empty, its only ideal here is {}, improper on the empty support. For nonempty A and λ=0 or 1, the singleton calculation and monotonicity show that only the empty subset is null, since all coordinates are infinite. For a finite A, the same calculation gives exactly J<λ[A]=P({aA:a<λ}).

F1givenalgebra
2.1

Suppose first that EJ<λ[A] and D is an ultrafilter on A containing E. Restrict D to E; by the support isomorphism its product cofinality is unchanged and belongs to pcf(E), hence is below λ. Conversely, if every such D has cofinality below λ, any ultrafilter on E extends to one on A supported on E with the same cofinality. Thus every member of pcf(E) is below λ, proving membership. For E= both the universal ultrafilter assertions are vacuous and membership was proved in step 1.1.

F3step 1.1
3.1

A set HA belongs to every ultrafilter of cofinality at least λ exactly when none of those ultrafilters contains AH, by the complementary-pair law in F2. By step 2.1 this is exactly AHJ<λ[A], or HJ<λ[A]. This proves both inclusions in the dual identity. If there are no high-cofinality ultrafilters, step 2.1 with E=A puts A in the ideal, so the ideal and its dual are both P(A); the empty-intersection convention gives the same result. No witnesses are chosen in these computations beyond the AC-dependent facts already proved in F1. QED.

F2step 2.1

Depends on

Used by

Dependency tree · two levels

43 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