Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-28
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 absolute value ∣a∣ of an integer

Definition

Let a∈Z (The integers as equivalence classes of pairs of naturals). The absolute value of a is

∣a∣  :=  {aif a≥0,−aif a<0,

where ≤ is the order of Order on the integers and −a is the additive inverse supplied by The integers form a commutative ring for the operations of Arithmetic on the integers.

Why the two clauses define a function. The order on Z is total and antisymmetric (The integers form a totally ordered ring), so for each a exactly one of a≥0 and a<0 holds: totality gives at least one of 0≤a and a≤0, and if both hold then a=0 by antisymmetry, in which case a≥0 and a<0 fails, since a<0 means a≤0 together with a≠0. The two clauses therefore never both apply and never both fail, and −a is a single element of Z because additive inverses are unique in a commutative ring: if a+u=0 and a+v=0 then u=u+0=u+(a+v)=(u+a)+v=0+v=v.

At the boundary, ∣0∣=0 by the first clause, and the second clause also gives −a whenever a≤0: for a<0 that is the definition, and for a=0 both readings give 0.

Remarks

Depends on

Used by

Dependency tree · two levels

21 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