LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Closure points form a club

Statement

Work in ZFC. If $f : κ \to κ$ and $κ$ is regular uncountable, then $C_{f} = {α < κ : f [α] \subseteq α}$ is club. The same conclusion holds for a nondecreasing $f : θ \to θ$ whenever $cf (θ) > ω$ .

Facts & Assumptions

[F1]

Closed unbounded subsets of ordinals: Closure is tested at nonzero limit points below the ambient ordinal.

[F2]

$cf (α) \leq α$ ; $cf (0) = 0$ and $cf (α + 1) = 1$ ; for a limit ordinal $λ$ the value $cf (λ)$ is an infinite cardinal with $cf (cf (λ)) = cf (λ)$ , so it is regular; and every cofinal subset of $λ$ has cardinality at least $cf (λ)$ , a value that is attained: A set of fewer than the cofinality many ordinals is bounded below a limit ordinal.

[F3]

The recursion theorem: A specified self-map admits omega iteration.

Proof

Given: The objects and hypotheses in the statement.

1.1

In the regular case, given $β < κ$ , set $a_{0} = β + 1$ and $a_{n + 1} = \max (a_{n}, \sup f [a_{n}]) + 1$ . Regularity bounds $f [a_{n}]$ below $κ$ ; recursion defines the increasing sequence, and $a = \sup_{n} a_{n} < κ$ because $ω < cf (κ)$ . For $x < a$ take $n$ with $x < a_{n}$ ; then $f (x) < a_{n + 1} < a$ . Thus $a \in C_{f}$ and $a > β$ .

F2F3

1.2

In the nondecreasing case use $a_{n + 1} = \max (a_{n}, f (a_{n})) + 1$ instead. Each term stays below the limit $θ$ , and the omega supremum stays below $θ$ . If $x < a_{n}$ , monotonicity gives $f (x) \leq f (a_{n}) < a_{n + 1} < a$ . Again this proves unboundedness.

F2F3

2.1

In either case, if a nonzero limit $δ$ is a limit point of $C_{f}$ , then for every $x < δ$ some $γ \in C_{f} \cap δ$ exceeds $x$ . Hence $f (x) < γ < δ$ . This proves closure. Zero itself belongs to $C_{f}$ vacuously, but is not a required closure limit.

F1step 1.1step 1.2∎

Depends on

Used by

Dependency tree · two levels

24 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

Lietz, Lemma 5.2, Claim 5.3 and Lemma 5.4, pp.39–40 (standard reference, not scraped)