Book X · Proposition 80

X.80

To a first apotome of a medial straight line only one medial straight line can be annexed which is commensurable with the whole in square only and which contains with the whole a rational rectangle.Heath, 1908

Every step, checked

• the greater term is the greatergiven
• the remainder is first apotome of a medial linegiven
• the two terms are recovered from the line itselfby X.80
• and they give back the line, so the division is the only oneby X.80

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