Book X · Proposition 78

X.78

If from a straight line there be subtracted a straight line which is incommensurable in square with the whole and which with the whole makes the sum of the squares on them medial, twice the rectangle contained by them medial, and further the squares on them incommensurable with twice the rectangle contained by them, the remainder is irrational; and let it be called that which produces with a medial area a medial whole.Heath, 1908

Every step, checked

• the greater term is the greatergiven
• the remainder is irrationalby X.78
• and it is that which produces with a medial area a medial wholeby X.78

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 _difference(a, b, _k=kind) -> Out:
    hypothesis("the greater term is the greater", sign(a - b) > 0)
    remainder = a - b
    claim("the remainder is irrational", ref,
          not isinstance(remainder, Fraction))
    claim(f"and it is {SUBTRACTED_NAMES[_k]}", ref,
          classify(remainder).name == SUBTRACTED_NAMES[_k])
    return Out(remainder=remainder)