Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck 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.

Inverses of positives are positive, and reciprocation reverses order

Statement

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

  1. If a>0 then a−1>0.
  2. If 0<a<b then 0<b−1<a−1.

Facts & Assumptions

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

[L1]

x>0  ⟺  x∈P; x<0  ⟺  −x∈P; and for x≠0 exactly one of x∈P, −x∈P holds (Ordered field).

[L2]

Sign rules: a product of a positive and a negative is negative, a product of two positives is positive, and for c>0 one has a<b  ⟺  ac<bc (Sign rules for products and monotonicity of multiplication).

[L3]

0<1; in particular 1≠0 (The multiplicative identity is positive).

[L4]

P is closed under addition, so < is transitive (Ordered field).

Proof

technique · direct
1.1

Assume a>0, so a≠0 and its inverse a−1 exists with a⋅a−1=1; moreover a−1≠0, since a−1 has a as its inverse while 0 is non-invertible (1≠0 by L3).

assume-hypL1L3
2.1

By trichotomy a−1∈P or −a−1∈P; if −a−1∈P, then a>0 and a−1<0 give a⋅a−1<0 by the sign rules, i.e. 1<0, contradicting 0<1; hence a−1∈P, i.e. a−1>0, proving claim 1.

step 1.1L2L3L1
3.1

Assume 0<a<b; then 0<b by transitivity, so by claim 1 both a−1>0 and b−1>0, and the sign rules give a−1b−1>0.

assume-hypstep 2.1L4L2L1
4.1

Multiplying a<b by the positive a−1b−1 via the sign rules gives a(a−1b−1)<b(a−1b−1); since aa−1=1 and bb−1=1, this simplifies to b−1<a−1.

step 3.1L2algebra
5.1

Together with b−1>0 from step 3.1, we conclude 0<b−1<a−1, proving claim 2.

step 3.1step 4.1∎

Depends on

Used by

…and 176 more results.

Dependency tree · two levels

7 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