Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)
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 shift x↦x+1 is a nonidentity order automorphism of (Z,<)

Statement refuted

Refuted claim: claims (a) and (c) of Rigidity of well-orders hold for every total order, that is, totality in place of well-ordering suffices for both: (a) every strictly increasing f:W→W satisfies a≤f(a) for all a∈W, and (c) the identity is the only order isomorphism W→W.

The witness is Z with its usual order (Order on the integers), a total order that is not a well-order. The shift σ(x)=x+1 is an order isomorphism Z→Z (Order embedding and order isomorphism) with σ(x)≠x for every x, so the identity is not the only order automorphism and claim (c) fails. The shift τ(x)=x−1 in the other direction is strictly increasing and satisfies τ(x)<x for every x, so claim (a) fails as well. In the proof of claim (a) the least-element property is applied once, to the set of points moved down; here that set is all of Z, which has no least element, and this is exactly where the well-ordering hypothesis is spent. No choice principle is used.

Facts & Assumptions

Given: The integers Z with their order and ring operations, and the maps σ(x)=x+1, τ(x)=x−1 on Z.

[F1]

Rigidity of well-orders, claims (a) and (c): if (W,<) is a well-order and f:W→W is strictly increasing then a≤f(a) for every a∈W; and the identity is the only order isomorphism W→W (Rigidity of well-orders).

[F2]

Let (P,≤P) and (Q,≤Q) be posets; f:P→Q is an order embedding when x≤Py  ⟺  f(x)≤Qf(y), an order embedding is injective, and an order isomorphism is a surjective order embedding, equivalently a bijection with x≤Py  ⟺  f(x)≤Qf(y) (Order embedding and order isomorphism).

[F3]

A well-order is a total order in which every nonempty subset has a least element, and its strict part is irreflexive, transitive and trichotomous (Well-order and well-ordered set).

[F4]

On representatives, x≤y means a+d≤b+c in N, x<y means x≤y and x≠y, and 0<[(a,b)] holds exactly when b<a (Order on the integers).

[F5]

The relation of Order on the integers is a total order on Z, compatible with addition: x≤y implies x+z≤y+z for all integers x,y,z; its strict part is irreflexive and transitive (The integers form a totally ordered ring).

[F6]

(Z,+,⋅,0,1) with the operations of Arithmetic on the integers is a commutative ring with multiplicative identity, where 0=[(0,0)], 1=[(1,0)], and every element has the additive inverse −[(a,b)]=[(b,a)]; thus x+0=x, x+(−x)=0, and addition is associative and commutative (The integers form a commutative ring, Arithmetic on the integers).

[F7]

The canonical embedding n↦[(n,0)] of N in Z is injective and preserves order; its image is exactly the set of nonnegative integers, so the image of 1 is nonnegative and differs from the image of 0, which is 0 (The naturals embed in the integers).

[F8]

1=σ(0)≠0 in N (The von Neumann naturals form a Peano system).

[F9]

f:A→B is injective when f(x)=f(y) implies x=y, surjective when every b∈B is f(x) for some x∈A, and bijective when both (Injection, surjection, bijection).

Counterexample

technique · direct
1.1F5F6

The shift σ preserves and reflects the strict order: for integers x,y one has x<y if and only if x+1<y+1. Adding −1 to x+1<y+1 gives x<y, and adding 1 to x<y gives x+1<y+1.

1.2F5F6F9

The shift σ is bijective: it is injective, since x+1=y+1 gives x=(x+1)+(−1)=(y+1)+(−1)=y; and it is surjective, since an arbitrary integer y is σ(y+(−1))=y+(−1)+1=y.

1.3F4F5F6F7F8

1≠0 and −1<0 in Z: the integer 1 is [(1,0)] and lies in the image of the canonical embedding n↦[(n,0)], which consists of the nonnegative integers, so 0≤1; and 1≠0 because that embedding is injective while 1≠0 in N; hence 0<1, and adding −1 to both sides gives −1<0.

1.4F5F6

The backward shift τ(x)=x−1 is strictly increasing: for integers x,y one has x<y if and only if x+(−1)<y+(−1), that is τ(x)<τ(y), by adding 1 or −1 to an inequality.

2.1step 1.1step 1.2step 1.3F2F4F6

The shift σ is an order isomorphism of Z onto itself: it is a bijection by step 1.2 and satisfies x<y  ⟺  σ(x)<σ(y) by step 1.1, so also x≤y  ⟺  σ(x)≤σ(y), since x≤y means x<y or x=y and σ is injective. Moreover σ(x)=x+1≠x for every x: equality would give 1=0 by adding −x to both sides, contradicting step 1.3.

2.2step 1.3step 1.4F5F6

The backward shift τ is strictly increasing by step 1.4 and moves every point down: τ(x)=x+(−1)<x+0=x for every integer x, by adding x to −1<0 from step 1.3.

3.1step 1.3step 2.1step 2.2F1F3F4F5∎

Both claims fail at the total order (Z,<). Claim (c) of [F1] asserts that the identity is the only order isomorphism Z→Z, but σ is a nonidentity order isomorphism by step 2.1. Claim (a) asserts that every strictly increasing f:Z→Z satisfies x≤f(x) for all x, but τ is strictly increasing by step 2.2 with τ(x)<x, so x≤τ(x) fails for every x. In the proof of claim (a) the least element of {x:τ(x)<x} is used once; here {x:τ(x)<x}=Z, a total order with no least element, which is precisely why the well-ordering hypothesis cannot be dropped. The refuted claim that totality suffices for claims (a) and (c) is therefore false.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 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