Book X · Proposition 2

X.2

If, when the less of two unequal magnitudes is continually subtracted in turn from the greater, that which is left never measures the one before it, the magnitudes will be incommensurable.Heath, 1908

Euclid's test for incommensurability: the alternating subtraction never ends. The kernel settles the same question by looking at the ratio, and the two are checked against each other here.

Every step, checked

• the magnitudes are positive and unequalgiven
• the subtraction ends exactly when a common measure existsby X.2
• so if it never measures the one before it, they are incommensurableby X.2

What it needs, and what needs it

Needs: nothing earlier.

Depth: 0 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "X.2",
    THEOREM,
    sample=_either_pair,
    note="Euclid's test for incommensurability: the alternating subtraction "
    "never ends. The kernel settles the same question by looking at the ratio, "
    "and the two are checked against each other here.",
)
def prop_X_2(a, b) -> Out:
    hypothesis("the magnitudes are positive and unequal",
               sign(a) > 0 and sign(b) > 0 and a != b, guard=True)
    greater, lesser = (a, b) if sign(a - b) > 0 else (b, a)
    quotients, ended = anthyphairesis(greater, lesser, steps=40)

    claim("the subtraction ends exactly when a common measure exists", "X.2",
          ended == commensurable(a, b))
    claim("so if it never measures the one before it, they are incommensurable",
          "X.2", ended or not commensurable(a, b))
    return Out(quotients=quotients, terminated=ended)