Book X · Proposition 25

X.25

The rectangle contained by medial straight lines commensurable in square only is either rational or medial.Heath, 1908

Every step, checked

• both are medialgiven
• they are commensurable in square onlygiven
• the rectangle they contain is either rational or medialby X.25

What it needs, and what needs it

Needs: nothing earlier.

Used by: X.31

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.25",
    THEOREM,
    sample=lambda rng: _medials_in_square_only(
        rng.choice([2, 3, 5, 7]), rng.random() < 0.5),
)
def prop_X_25(a, b) -> Out:
    hypothesis("both 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))
    rectangle = a * b
    claim("the rectangle they contain is either rational or medial", "X.25",
          is_rational_area(rectangle) or is_medial_area(rectangle))
    return Out(rectangle=rectangle)