How big is a signed number?

The absolute value |c| keeps only the size: how far the number sits from zero.

Start with a concrete example

On a number line, −7 and 7 are both seven steps from 0. Absolute value records this distance, so |−7|=7.

A small check: try the idea

Think with the concrete example above. You can try again.

What is |−7|?

Read the answer and reasoning

7. Measure the distance from 0 on a number line. −7 is seven steps away, and a distance is not negative.

Build the idea in three steps

Signed numbers need a size: Int.natAbs reads |c|, the distance from zero — −11 and 11 both measure 11, and the sign is forgotten on purpose.
The record natAbsHom stores the machine and its promises side by side: map_mul' fixes |a × b| = |a| × |b|, map_one' fixes |1| = 1, and map_zero' fixes |0| = 0.
Sizes multiply — that is the field map_mul' — and it is the reason a descent can rank suspects by size: replace each solution's c by |c|, a natural number, and "smaller suspect" becomes a smallest number that you can always find.

A small example

Measure, then multiply: |−7| = 7 and |3| = 3, and indeed |−7 × 3| = |−21| = 21 = 7 × 3. Sizes never care about the sign, only how far from zero.

Lean definition · original excerpt

Mathlib · db584cd · NatAbs.lean

27/-- `Int.natAbs` as a bundled `MonoidWithZeroHom`. -/28@[simps]29def natAbsHom : ℤ →*₀ ℕ where30  toFun := Int.natAbs31  map_mul' := Int.natAbs_mul32  map_one' := Int.natAbs_one33  map_zero' := Int.natAbs_zero

How to read this Lean

natAbsHom is a tiny machine-listing: it eats a signed integer and returns a natural number, and each field certifies one promise of the bundling — mul, one, zero. In the descent pages, solutions are ranked exactly by this machine (the Minimal definition compares Int.natAbs of c), so "the smallest suspect" literally becomes "the smallest natural number" — a ranking that cannot go on forever.

Original source ↗ · L27–33 Open the complete saved source

Where this idea is used

2. The case of three 7. The veterans’ cabinet

How big is a signed number?

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Lean definition · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue