Book X · Proposition 71

X.71

If a rational and a medial area be added together, four irrational straight lines arise, namely a binomial or a first bimedial or a major or a side of a rational plus a medial area.Heath, 1908

Adding a rational area to a medial one produces one of four of the thirteen, and never anything outside them.

Every step, checked

• the scale is genuinegiven
• the sum of the two areas is irrationalby X.71
• and its side is one of the four named linesby X.71

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.71", THEOREM, sample=lambda rng: (Fraction(rng.randint(1, 4)),),
             note="Adding a rational area to a medial one produces one of four "
             "of the thirteen, and never anything outside them.")
def prop_X_71(scale) -> Out:
    hypothesis("the scale is genuine", sign(scale) > 0, guard=True)
    rational_area = scale * scale
    medial_area = scale * scale * sqrt(2)
    side = sqrt(rational_area + medial_area)
    claim("the sum of the two areas is irrational", "X.71",
          not isinstance(rational_area + medial_area, Fraction))
    claim("and its side is one of the four named lines", "X.71",
          classify(side).name in SPECIES or classify(side).family == "medial-based"
          or classify(side).family == "binomial")
    return Out(side=side)