Book X · Proposition 83

X.83

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

Every step, checked

• the greater term is the greatergiven
• the remainder is that which produces with a rational area a medial wholegiven
• the two terms are recovered from the line itselfby X.83
• and they give back the line, so the division is the only oneby X.83

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))