Book X · Proposition 82

X.82

To a minor straight line only one straight line can be annexed which is incommensurable in square with the whole and which makes, with the whole, the sum of the squares on them rational but twice the rectangle contained by them medial.Heath, 1908

Every step, checked

• the greater term is the greatergiven
• the remainder is minorgiven
• the two terms are recovered from the line itselfby X.82
• and they give back the line, so the division is the only oneby X.82

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(ref, THEOREM, sample=_kind_sample(kind))
def _divided(a, b, _k=kind) -> Out:
    hypothesis("the greater term is the greater", sign(a - b) > 0)
    remainder = a - b
    named = classify(remainder)
    # An apotome is named with its species ("fourth apotome"), so the
    # family is what matches the bare name.
    hypothesis(f"the remainder is {SUBTRACTED_NAMES[_k]}",
               named.name == SUBTRACTED_NAMES[_k]
               or named.family == SUBTRACTED_NAMES[_k])
    claim("the two terms are recovered from the line itself", ref,
          len(named.terms) == 2)
    claim("and they give back the line, so the division is the only one",
          ref, is_zero(named.terms[0] + named.terms[1] - remainder))
    return Out(terms=tuple(named.terms))