Book X · Proposition 84

X.84

To a straight line which produces with a medial 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 and twice the rectangle contained by them both medial and also incommensurable with the sum of the squares on them.Heath, 1908

Every step, checked

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

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