Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (openai/gpt-5.4)audited 2026-07-25
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.

Order is preserved by adding a constant and by adding inequalities

Statement

Let F be an ordered field (Ordered field) with positive cone P, and let a,b,c,d∈F.

  1. Translation invariance. If a<b then a+c<b+c.
  2. Adding inequalities. If a<b and c<d then a+c<b+d.

Facts & Assumptions

Given: An ordered field F with positive cone P, and elements a,b,c,d∈F.

[L1]

For x,y∈F, the relation x<y means y−x∈P (Ordered field).

[L2]

P is closed under addition: if u,v∈P then u+v∈P (axiom O2 of Ordered field).

Proof

technique · direct
1.1

Assume a<b; by the definition of the order this means b−a∈P.

assume-hypL1
1.2

For every c∈F the field identities give (b+c)−(a+c)=b−a.

algebra
1.3

Assume moreover c<d; by the definition of the order this means d−c∈P.

assume-hypL1
1.4

The field identities give (b+d)−(a+c)=(b−a)+(d−c).

algebra
2.1

Hence (b+c)−(a+c)=b−a∈P, which is exactly a+c<b+c, proving claim 1.

step 1.1step 1.2L1
2.2

Since b−a∈P and d−c∈P, closure under addition gives (b−a)+(d−c)∈P.

step 1.1step 1.3L2
3.1

Therefore (b+d)−(a+c)=(b−a)+(d−c)∈P, which is exactly a+c<b+d, proving claim 2.

step 1.4step 2.2L1∎

Depends on

Used by

…and 131 more results.

Dependency tree · two levels

2 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