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.
Tail suprema land in the scale subspace
Statement
Assume AC. Let and let be points of the scale subspace such that for every and with . Put on . There is with at every in , hence . On that tail and . No condition on the cofinalities of the finitely many initial values of is needed.
Facts & Assumptions
Given: The normalized scale defining , with , and the sequence in the statement.
Points of are Rudin points eventually equal to scale terms; the scale is strictly increasing in , and admissible finite modifications preserve (Kojman-Shelah scale subspace).
For strictly increasing scale indices indexed by and pointwise strictly increasing representatives in the actual product on , their tail supremum is below each factor, has coordinate cofinality , and is eventually equal to for the index supremum of cofinality (Tail suprema and normalized scales).
Under AC the finite positive alephs are regular ( is regular in ZF; assuming the Axiom of Choice every successor aleph is regular; , so is singular, and under choice it is the least singular infinite cardinal).
Uncountable cofinality excludes zero and successor ordinal values (; and ; for a limit ordinal the value is an infinite cardinal with , so it is regular; and every cofinal subset of has cardinality at least , a value that is attained).
AC is assumed for the scale and cardinal-regularity suppliers (The Axiom of Choice).
Proof
Each has exactly one scale index with . Existence is F1. If two distinct indices worked, put the smaller first; scale strictness outside a finite set would give at all but finitely many coordinates. The infinite has a coordinate outside their finite union, a contradiction. For , the supplied strict inequality on the cofinite tail excludes : equality would imply eventual equality of the two points, while a strict reverse index inequality would imply . Either conflicts with the strict tail inequalities outside finitely many coordinates. Thus is strictly increasing.
Set . For every there is a successor , since the infinite cardinal is a limit ordinal (also its cofinality exceeds one by F3–F4). For , , so . Hence the restrictions are members of the actual strict product, not just the inclusive-top product. They are pointwise increasing by hypothesis and eventually equal to by step 1.1. Thus all hypotheses of F2, including , hold. F2 and A1 give , , and with and on .
Define for with , and for . On the finite prefix, F3 gives uncountable cofinalities ; on the tail, step 2.1 gives cofinality . Thus every coordinate cofinality lies strictly between and , and . Step 2.1 and the finite prefix imply , so F1 gives . It agrees with on every required tail coordinate and differs, if at all, only on the finite prefix. QED.
Depends on
- Kojman-Shelah scale subspace
- Tail suprema and normalized scales
- The Axiom of Choice
- $\aleph_0$ is regular in ZF; assuming the Axiom of Choice every successor aleph $\aleph_{\alpha+1}$ is regular; $\operatorname{cf}(\aleph_\omega) = \aleph_0$, so $\aleph_\omega$ is singular, and under choice it is the least singular infinite cardinal
- $\operatorname{cf}(\alpha) \le \alpha$; $\operatorname{cf}(0) = 0$ and $\operatorname{cf}(\alpha + 1) = 1$; for a limit ordinal $\lambda$ the value $\operatorname{cf}(\lambda)$ is an infinite cardinal with $\operatorname{cf}(\operatorname{cf}(\lambda)) = \operatorname{cf}(\lambda)$, so it is regular; and every cofinal subset of $\lambda$ has cardinality at least $\operatorname{cf}(\lambda)$, a value that is attained
Used by
Dependency tree · two levels
33 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.