TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

DC detects non-well-orders by descending sequences

Statement

In ZF plus DC, a linear order $(X, <)$ is a well-order iff it has no sequence $(x_{n})_{n < ω}$ with $x_{n + 1} < x_{n}$ for every $n$ .

Facts & Assumptions

[F1]

Well-order and well-ordered set: Every nonempty subset of a well-order has a least member.

[F2]

The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain: A serial relation on a nonempty set admits an omega path from any initial point.

Proof

Given: The objects and hypotheses in the statement.

1.1

In a well-order, the nonempty range of a descending sequence would have a least element $x_{n}$ , contradicted by $x_{n + 1} < x_{n}$ . This direction needs no choice.

2.1

If the linear order is not a well-order, some nonempty $Y \subseteq X$ has no least point. Linearity implies that every $y \in Y$ has some $z \in Y$ with $z < y$ . Apply DC to $y R z$ iff $z < y$ , starting from any one point of $Y$ . It gives the forbidden descending sequence. The empty order is a well-order and has no such sequence.

F1F2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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

Jech, The Axiom of Choice, §2.4 final proposition, p.23 (standard reference, not scraped)