ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

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.

A concrete Rudin slice

Example

Assume AC. Take $B = {2, 3, 4, \dots}$ and a natural number $k$ . Define

$h_{k} (n) = {\begin{cases} ℵ_{n} & 2 \leq n \leq k, \\ ω_{1} & n > k . \end{cases}$

Then $h_{k} \in X_{R} (B)$ and lies in the initial-top slice $F_{k}$ . For every $l > k$ with $l \geq 2$ , it does not lie in $F_{l}$ . For instance $h_{3} = (ω_{2}, ω_{3}, ω_{1}, ω_{1}, \dots)$ belongs to $F_{3} ∖ F_{4}$ .

Facts & Assumptions

Given: The displayed function and $k < ω$ .

[F1]

Rudin points require uncountable coordinate cofinalities bounded strictly by some finite aleph (Rudin ordinal box spaces on infinite index sets).

[F2]

Under AC $cf (ℵ_{n}) = ℵ_{n}$ for positive finite $n$ ( $ℵ_{0}$ is regular in ZF; assuming the Axiom of Choice every successor aleph $ℵ_{α + 1}$ is regular; $cf (ℵ_{ω}) = ℵ_{0}$ , so $ℵ_{ω}$ is singular, and under choice it is the least singular infinite cardinal).

[F3]

$F_{j}$ imposes $h (n) = ℵ_{n}$ on coordinates $n \leq j$ (Neighborhoods of Rudin initial-top slices contain tails).

[A1]

AC is assumed for F2 and the Rudin setting (The Axiom of Choice).

Verification

1.1

All coordinates of $h_{k}$ are in $[0, ℵ_{n}]$ : the prefix equals its tops and the tail has $ω_{1} < ℵ_{n}$ since $n \geq 2$ . By F2 and A1 their cofinalities are respectively $ℵ_{n}$ and $ℵ_{1}$ . Set $m = \max (k, 1) + 1$ . These cofinalities are above $ω$ and strictly below $ℵ_{m}$ , including for $k = 0, 1$ when the prefix is empty and $m = 2$ . F1 therefore gives $h_{k} \in X_{R} (B)$ .

F1F2A1

2.1

For every $n \leq k$ in $B$ the defining value is $ℵ_{n}$ , so F3 gives $h_{k} \in F_{k}$ . If $l > k$ and $l \in B$ , its $l$ -th coordinate is $ω_{1} < ℵ_{l}$ , violating the equality required for $F_{l}$ . At $k = 3$ , the first two coordinates are $ω_{2}, ω_{3}$ , and the next is $ω_{1} < ω_{4}$ , giving the asserted concrete instance. QED.

step 1.1F3

Depends on

Used by

Nothing in the library uses this result yet.

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

Hart, Set-Theoretic Methods in General Topology, Chapter 6 section 3, initial-top slices, printed p. 37; explicit point calculated here (standard reference, not scraped)