Book X · Proposition 72

X.72

If two medial areas incommensurable with one another be added together, the remaining two irrational straight lines arise, namely either a second bimedial or a side of the sum of two medial areas.Heath, 1908

Every step, checked

• the radicand is not a squaregiven
• both areas are medialgiven
• they are incommensurablegiven
• the sum is irrationalby X.72
• and its side is one of the named linesby X.72

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.72", THEOREM, sample=lambda rng: (rng.choice([2, 3, 5]),))
def prop_X_72(radicand: int) -> Out:
    """Two medial areas added, incommensurable with one another."""
    hypothesis("the radicand is not a square", not _is_square_int(radicand))
    first, second = sqrt(radicand), sqrt(radicand + 1) if not _is_square_int(radicand + 1) \
        else sqrt(radicand + 2)
    hypothesis("both areas are medial", is_medial_area(first) and is_medial_area(second))
    hypothesis("they are incommensurable", not commensurable(first, second))
    side = sqrt(first + second)
    claim("the sum is irrational", "X.72", not isinstance(first + second, Fraction))
    claim("and its side is one of the named lines", "X.72",
          classify(side).name in SPECIES or classify(side).family in
          ("binomial", "medial-based"))
    return Out(side=side)