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 $f$

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 the cut $M_x$ satisfies $f(y) \in M_x$ for every $y \in 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 an element $y \in M_x$ .

[A1]

$x$ is extremal: for every $z \in M$ with $z < x$ , $f(z) \le x$ (Extremal element and its cut (Bourbaki–Witt)).

[A2]

$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, Admissible subset (Bourbaki–Witt)).

[L2]

$f$ is progressive: $z \le f(z)$ for every $z \in P$ (Chain-complete poset).

[L3]

$\le$ is a partial order: it is reflexive ( $u \le u$ ) and transitive ( $u \le v$ and $v \le w$ imply $u \le w$ ), and its strict form $u < v$ means $u \le v$ together with $u \ne v$ (Partial order and partially ordered set).

Proof

technique · cases

1.1

Since $y \in M_x$ we have $y \in M$ , and $M$ is closed under $f$ , so $f(y) \in M$ .

A2L1

1.2

Membership of $M_x$ gives $y \le x$ or $f(x) \le y$ , and the relation $y \le x$ holds exactly when $y < x$ or $y = x$ , by the definition of the strict order.

A2L3

1.3

Suppose $y < x$ .

assume-case below

1.4

Suppose $y = x$ .

assume-case equal

1.5

Suppose $f(x) \le y$ .

assume-case above

2.1

In the case $y < x$ , extremality of $x$ gives $f(y) \le x$ , so $f(y)$ lies in $M$ and satisfies $f(y) \le x$ , hence $f(y) \in M_x$ .

step 1.3A1step 1.1A2

2.2

In the case $y = x$ , we get $f(y) = f(x)$ , and $f(x) \le f(x)$ by reflexivity, so $f(y) \in M$ satisfies the second alternative, hence $f(y) \in M_x$ .

step 1.4step 1.1A2L3

2.3

In the case $f(x) \le y$ , progressivity gives $y \le f(y)$ , so $f(x) \le f(y)$ by transitivity, hence $f(y) \in M_x$ .

step 1.5L2step 1.1A2L3

3.1

The three cases cover every $y \in M_x$ , and each yields $f(y) \in M_x$ .

step 1.2step 2.1step 2.2step 2.3cases-exhaustive∎

Remarks

The case $y = x$ is the one that explains the shape of the cut. It is precisely why $M_x$ is defined with $f(x) \le z$ rather than $x < z$ : the image $f(x)$ must itself land inside $M_x$ , and it does so on the upper side.
Extremality of $x$ is used only in the first case, and it is exactly what stops $f$ from carrying an element from strictly below $x$ into the forbidden zone strictly between $x$ and $f(x)$ . That zone is what the cut omits, and keeping it empty of elements of $M$ is what eventually makes $M$ a chain (The smallest admissible set is a chain).

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)

The cut at an extremal element is closed under fff