LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

Ladder separation from HYP

Statement

Let $κ, (κ_{n})_{n \in ω}, E$ satisfy HYP and fix ladders $(δ_{i})_{i \in ω}$ for $δ \in E$ (Fleissner's HYP covering interface). Then for every $β < κ^{+}$ there is a function $m_{β} : E \cap β \to ω$ such that for all distinct $δ, η \in E \cap β$ , writing $m : = \max (m_{β} (δ), m_{β} (η))$ , one has $δ_{m} \neq η_{m}$ ; and in fact $δ_{i} \neq η_{i} for every i \geq \max (m_{β} (δ), m_{β} (η)) .$

Facts & Assumptions

Given: Witnesses $κ, (κ_{n}), E$ for HYP and ladders $(δ_{i})$ for $δ \in E$ ; the induction is on $β < κ^{+}$ .

[F1]

For every limit $β < κ^{+}$ there is a club $C \subseteq β$ disjoint from $E$ . If $cf (β) > ω$ , this is exactly HYP clause (3b). If $cf (β) = ω$ , fix a strictly increasing cofinal sequence $(b_{n})$ in $β$ and take $C = {0} \cup {b_{n} + 1 : n \in ω}$ . This set is unbounded; it has no limit point below $β$ (every proper initial segment of an increasing $ω$ -sequence is finite), hence is closed; and its nonzero members are successors, while every member of $E$ has cofinality $ω$ by clause (3a). These are all possible cofinalities of a nonzero limit ordinal in ZFC (Fleissner's HYP covering interface, Cardinal (initial ordinal) and cardinality).

[F2]

Every element of $E$ has cofinality $ω$ , so successor ordinals are not in $E$ . If $C \subseteq β$ is club, $0 \in C$ , and $δ < β$ is not in $C$ , then $γ = \sup (C \cap δ)$ belongs to $C$ and is below $δ$ , while $\min (C ∖ δ)$ exists and is strictly between $δ$ and $β$ (Cardinal (initial ordinal) and cardinality).

[L1]

Each ladder $(δ_{i})$ is increasing and cofinal in $δ$ , so for every $γ < δ$ there is a least $i$ with $δ_{i} > γ$ , and $δ_{i} > γ$ for all larger $i$ (Fleissner's HYP covering interface, The natural numbers $N$ (von Neumann)).

[L2]

Induction: if a statement about $m_{β}$ is proved for $β = 0$ , for $β = α + 1$ from $m_{α}$ , and for limit $β$ from all $m_{γ}$ with $γ < β$ , then it holds for every $β < κ^{+}$ (Cardinal (initial ordinal) and cardinality).

Proof

technique · induction

1.1

We build $m_{β}$ for all $β < κ^{+}$ by induction, maintaining the strengthened property that for distinct $δ, η \in E \cap β$ one has $δ_{i} \neq η_{i}$ for every $i \geq \max (m_{β} (δ), m_{β} (η))$ .

givenL2

2.1

For $β = 0$ take $m_{0} : = \emptyset$ ; the domain is empty and both properties are vacuous.

basestep 1.1

2.2

Successor case. Let $β = α + 1$ . If $α \notin E$ put $m_{β} : = m_{α}$ ; this keeps the domain and the strengthened property. If $α \in E$ , define, for $δ \in E \cap α$ , $m_{β} (δ) : = \max (m_{α} (δ), j (δ, α))$ where $j (δ, α)$ is the least $i$ with $α_{i} > δ$ , and put $m_{β} (α) : = 0$ .

step 1.1F2L1

2.3

Limit case. Let $β$ be a limit ordinal. By [F1] choose a club $C \subseteq β$ disjoint from $E$ and containing $0$ . For $δ \in E \cap β$ , [F2] gives $γ (δ) : = \sup (C \cap δ) \in C$ with $γ (δ) < δ$ and $\overset{ˉ}{γ} (δ) : = \min (C ∖ δ) \in C$ with $δ < \overset{ˉ}{γ} (δ) < β$ . Thus $m_{\overset{ˉ}{γ} (δ)}$ is defined by induction and contains $δ$ in its domain. Define $m_{β} (δ) : = \max (m_{\overset{ˉ}{γ} (δ)} (δ), i (δ))$ , where $i (δ)$ is the least $i$ with $δ_{i} > γ (δ)$ .

step 1.1F1F2L1

3.1

In the successor case, pairs inside $E \cap α$ keep the strengthened property because $m_{β} \geq m_{α}$ pointwise, so their separating level is not decreased. For $δ \in E \cap α$ and the new point $α$ : for $i \geq \max (m_{β} (δ), m_{β} (α)) = m_{β} (δ) \geq j (δ, α)$ we have $α_{i} \geq α_{j (δ, α)} > δ > δ_{i}$ , so $α_{i} \neq δ_{i}$ . Hence $m_{β}$ works.

step 2.2F2L1

3.2

In the limit case let $δ < η$ in $E \cap β$ . If $γ (δ) = γ (η)$ then also $\overset{ˉ}{γ} (δ) = \overset{ˉ}{γ} (η) = : \overset{ˉ}{γ}$ , and $m_{β} \geq m_{\overset{ˉ}{γ}}$ pointwise on ${δ, η}$ , so the strengthened property for $m_{\overset{ˉ}{γ}}$ , which is available by induction and holds at levels $\geq \max (m_{\overset{ˉ}{γ}} (δ), m_{\overset{ˉ}{γ}} (η))$ , transfers to $m_{β}$ .

step 2.3

3.3

In the limit case, if $γ (δ) < γ (η)$ then $\overset{ˉ}{γ} (δ) \leq γ (η)$ : otherwise $γ (η) < \overset{ˉ}{γ} (δ)$ would put both $δ$ and $η$ in the same gap of $C$ , forcing $γ (δ) = γ (η)$ . Then for $i \geq \max (m_{β} (δ), m_{β} (η)) \geq \max (i (δ), i (η))$ we have $δ_{i} < δ < \overset{ˉ}{γ} (δ) \leq γ (η) < η_{i}$ , so $δ_{i} \neq η_{i}$ .

step 2.3F2L1

4.1

Steps 2.1, 3.1, 3.2 and 3.3 establish the strengthened property for $m_{β}$ in all three cases of the induction, so by [L2] the functions $m_{β}$ exist for every $β < κ^{+}$ with the strengthened property. Since $δ_{m} \neq η_{m}$ for the single level $m = \max (m_{β} (δ), m_{β} (η))$ is the special case $i = m$ , the asserted functions exist.

step 2.1step 3.1step 3.2step 3.3L2discharge-induction∎

Remarks

Where (3b) is needed. At limit stages of uncountable cofinality it supplies a club disjoint from $E$ . At countable-cofinality stages such a club is automatic from clause (3a), by using a cofinal $ω$ -sequence of successors. In either case the club gaps put each $δ \in E$ below a smaller ordinal $\overset{ˉ}{γ} (δ)$ where the induction hypothesis separates ladders.
The strengthened form is not needed elsewhere, but it is what makes both the same-gap and the different-gap cases work at once; the paper's Lemma 1 is the special case of the single level $m$ .

Depends on

Used by

HYP produces a normal nonmetrizable Moore space Theorem

Dependency tree · two levels

31 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

William G. Fleissner, If all normal Moore spaces are metrizable, then there is an inner model with a measurable cardinal (standard reference, not scraped)