LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

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.

The cut at an extremal element is closed under chain suprema

Statement

Let $(P, \le)$ be a chain-complete poset, $f : P \to P$ progressive, $M$ the smallest admissible set, and $x \in M$ extremal (Extremal element and its cut (Bourbaki–Witt)). Then $\sup C \in M_x$ for every chain $C \subseteq M_x$ .

Facts & Assumptions

Given: A chain-complete poset $(P, \le)$ , a progressive $f : P \to P$ , the smallest admissible set $M$ , an extremal $x \in M$ , and a chain $C \subseteq M_x$ .

[A1]

$M_x = \{z \in M : z \le x \text{ or } f(x) \le z\}$ (Extremal element and its cut (Bourbaki–Witt)).

[L1]

$M$ is admissible, so it is closed under $f$ and under suprema of its chains (A smallest admissible set exists).

[L2]

Every chain of $P$ has a least upper bound in $P$ (Chain-complete poset).

[L3]

A least upper bound of a set is itself an upper bound of that set and is below every other upper bound (Upper bound, least upper bound, and strict upper bound).

[L4]

$\le$ is a partial order, in particular transitive: $u \le v$ and $v \le w$ imply $u \le w$ (Partial order and partially ordered set).

Proof

technique · cases

1.1

Write $s = \sup C$ , which exists in $P$ because $C$ is a chain.

L2construct

1.2

Since $C \subseteq M_x \subseteq M$ and $M$ is closed under suprema of its chains, $s \in M$ .

A1L1

1.3

Suppose every $z \in C$ satisfies $z \le x$ .

assume-case under

1.4

Suppose some $z_0 \in C$ satisfies $z_0 \not\le x$ .

assume-case over

2.1

In the first case $x$ is an upper bound of $C$ , so $s \le x$ because $s$ is the least upper bound, hence $s \in M_x$ .

step 1.3step 1.1L3step 1.2A1

2.2

In the second case $z_0 \in M_x$ together with $z_0 \not\le x$ forces $f(x) \le z_0$ , and $z_0 \le s$ since $s$ is an upper bound of $C$ , so $f(x) \le s$ by transitivity, hence $s \in M_x$ .

step 1.4A1step 1.1step 1.2L3L4

3.1

Either every element of $C$ is below $x$ or some element is not, so the two cases are exhaustive and $\sup C \in M_x$ in both.

step 2.1step 2.2cases-exhaustive∎

Remarks

The empty chain is covered without a separate argument: it falls into the first case vacuously, and $\sup \emptyset = \bot \le x$ .
Note which property of the supremum each case uses. The first case uses leastness, that $s$ is below any upper bound; the second uses only that $s$ is an upper bound. Both halves of the definition of least upper bound are needed, which is why chain-completeness cannot be weakened here to the mere existence of some upper bound.
Together with The cut at an extremal element is closed under $f$ this makes $M_x$ admissible, which is what Everything in $M$ is comparable to an extremal element feeds to minimality.

Depends on

Used by

Everything in M is comparable to an extremal element Lemma

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 7 results over 6 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Mathlib, Order.BourbakiWitt (standard reference, not scraped)
Bourbaki-Witt Principle (Menemui Matematik 39(1), 2017) (standard reference, not scraped)
Bourbaki–Witt theorem (Wikipedia) (standard reference, not scraped)