TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 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.

Fixed points of a normal function form a club

Statement

In ZFC, if $f : κ \to κ$ is normal and $κ$ is regular uncountable, then ${α < κ : f (α) = α}$ is club.

Facts & Assumptions

[F1]

Normal ordinal functions: Normal functions are strictly increasing and continuous at nonzero limits.

[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: Countable sets of ordinals are bounded below regular uncountable kappa.

[F3]

The recursion theorem: A specified self-map can be iterated on omega.

Proof

Given: The objects and hypotheses in the statement.

1.1

Transfinite induction gives $f (α) \geq α$ : zero is automatic, successors use strict increase, and limits use continuity. Given $β < κ$ , iterate $a_{0} = β + 1$ , $a_{n + 1} = f (a_{n})$ . If some adjacent terms agree, that term is a fixed point above $β$ . Otherwise the sequence is strictly increasing and its supremum $a < κ$ is a nonzero limit.

F1F2F3

2.1

In the latter case continuity and cofinality of the $a_{n}$ in $a$ give $f (a) = \sup_{n} f (a_{n}) = \sup_{n} a_{n + 1} = a$ . This proves unboundedness in both cases.

F1step 1.1

3.1

If fixed points are unbounded in a nonzero limit $δ < κ$ , monotonicity and continuity give $f (δ) = \sup {f (γ) : γ < δ, f (γ) = γ} = δ$ . Thus the fixed-point set is closed. Zero may or may not be fixed; no claim depends on it.

F1step 2.1∎

Depends on

Used by

Normal functions and fixed points at omega-one Example

Dependency tree · two levels

25 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

Welch, Lemma 2.13, p.21; live original reread (standard reference, not scraped)