Book X · Proposition 110

X.110

If from a medial area there be subtracted a medial area incommensurable with the whole, the two remaining irrational straight lines arise, either a second apotome of a medial straight line or a straight line which produces with a medial area a medial whole.Heath, 1908

Every step, checked

• the radicand is not a squaregiven
• both are medial areasgiven
• they are incommensurable and the second the lessgiven
• the remainder is irrationalby X.110
• and its side is one of the named linesby X.110

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("X.110", THEOREM, sample=lambda rng: (rng.choice([2, 3, 5]),))
def prop_X_110(radicand: int) -> Out:
    """A medial area subtracted from a medial area incommensurable with it."""
    hypothesis("the radicand is not a square", not _is_square_int(radicand))
    greater = 4 * sqrt(radicand)
    lesser = sqrt(3) if radicand != 3 else sqrt(2)
    hypothesis("both are medial areas",
               is_medial_area(greater) and is_medial_area(lesser))
    hypothesis("they are incommensurable and the second the less",
               not commensurable(greater, lesser) and sign(greater - lesser) > 0)
    side = sqrt(greater - lesser)
    claim("the remainder is irrational", "X.110",
          not isinstance(greater - lesser, Fraction))
    claim("and its side is one of the named lines", "X.110",
          classify(side).family in ("apotome", "medial-based")
          or classify(side).name in SPECIES)
    return Out(side=side)