Integers as differences¶

A pair of natural numbers (a, b) represents the difference a - b. Equality must compare represented differences, not fields.

What we already know

Natural numbers are immutable predecessor chains, and their equality and addition follow explicit zero/successor cases.

By the end, you can

explain why multiple pairs represent the same integer;
derive the cross-sum equality rule;
explain why eq=False is necessary;
separate a representative from its normalized form.

Read beside this chapter

Integer source and integer tests.

Definition

Equal differences form an equivalence class¶

If (a, b) means a - b, then (3, 1) and (4, 2) both mean 2. Avoiding subtraction gives a rule stated entirely with the natural-number addition we already constructed:

(a, b) ~ (c, d) exactly when a + d = b + c

This relation is reflexive, symmetric, and transitive, so each integer is an equivalence class of representatives. The library deliberately stores the chosen representative so that this construction remains visible.

Representation

@dataclass(frozen=True, slots=True, eq=False, repr=False)
class Integer:
    a: NaturalNumber
    b: NaturalNumber

    def __post_init__(self) -> None:
        if not isinstance(self.a, NaturalNumber) or not isinstance(
            self.b, NaturalNumber
        ):
            raise TypeError(
                "Integer.a and Integer.b must be NaturalNumber values"
            )

Generated field equality would make (3,1) != (4,2). eq=False prevents that incorrect rule and leaves equality to the hand-written method.

Implementation

@log(log_level=11)
def __eq__(self, other: object) -> tuple[bool, LogMessage]:
    converted = _coerce_integer(other)
    if converted is None:
        return cast(bool, NotImplemented), lambda: "NotImplemented"
    result = self.a + converted.b == self.b + converted.a
    return result, lambda: (
        f"{self!r} == {converted!r} ⇔ "
        f"{self.a!r} + {converted.b!r} == "
        f"{self.b!r} + {converted.a!r}"
    )

The line computing result is the defining equation with fields substituted directly. _coerce_integer lets a natural number participate by embedding n as (n, 0). An unrelated type returns NotImplemented and remains Python's dispatch problem.

Addition is componentwise:

(a, b) + (c, d) = (a + c, b + d)

Multiplication follows expansion of (a-b)(c-d):

(a, b) × (c, d) = (ac + bd, ad + bc)

Equality belongs to represented values

Frozen fields make a representative stable. The custom __eq__ decides whether two stable representatives belong to the same equivalence class.

Trace

Predict the two cross-sums

For (3,1) == (4,2), write the two natural-number sums that Integer.__eq__ compares.

⌘ / Ctrl + Enter

Output

Compare the logged cross-sums with the definition.

At level 11 the trace emphasizes integer equality. Lowering the threshold to 4 also exposes the natural-number additions used to build the cross-sums; it does not change the answer.

Test

Tests compare unequal representatives of the same value and check that operations respect equality. Those are executable checks of well-definedness for selected inputs. The general claim still requires showing that changing representatives cannot change an operation's equivalence class.

Boundary

normalize() chooses (n,0) for nonnegative values or (0,n) for negative values. Construction does not call it automatically. Keeping both (3,1) and (4,2) intact is an educational choice, not a mathematical requirement.

Next: construct rational numbers from pairs of integers →