Book X · Proposition 38

X.38

If two medial straight lines commensurable in square only and containing a medial rectangle be added together, the whole is irrational; and let it be called a second bimedial straight line.Heath, 1908

The second of the two bimedials: the rectangle is a medial area rather than a rational one.

Every step, checked

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.38", THEOREM, sample=_kind_sample("second bimedial"),
             note="The second of the two bimedials: the rectangle is a medial "
             "area rather than a rational one.")
def prop_X_38(a, b) -> Out:
    hypothesis("both lines are medial", is_medial(a) and is_medial(b))
    hypothesis("they are commensurable in square only",
               commensurable_in_square(a, b) and not commensurable(a, b))
    hypothesis("the rectangle they contain is medial", is_medial_area(a * b))
    whole = a + b
    claim("the whole is irrational", "X.38", not isinstance(whole, Fraction))
    claim("and it is a second bimedial", "X.38", classify(whole).name == "second bimedial")
    return Out(bimedial=whole)