Book X · Proposition 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.
Needs: nothing earlier.
Depth: 0 steps of argument above the first principles. Parallel postulate: not needed.
Nothing. It draws no intersections and reads nothing off the picture.
@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)