Book X · Proposition 28

X.28

To find medial straight lines commensurable in square only which contain a medial rectangle.Heath, 1908

Every step, checked

• the radicand is not a squaregiven
• both lines are medialby X.21
• they are commensurable in square onlyby X.Def.2
• and the rectangle they contain is medialby X.21

What it needs, and what needs it

Needs: X.21

Rests on: X.Def.2, X.Def.4

Depth: 1 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.28",
    CONSTRUCTION,
    sample=lambda rng: (rng.choice([2, 3, 5, 7]),),
)
def prop_X_28(radicand: int) -> Out:
    """Medials commensurable in square only, containing a medial rectangle."""
    hypothesis("the radicand is not a square", not _is_square_int(radicand))
    a, b = _medials_in_square_only(radicand, rational_rectangle=False)

    # X.21 makes a medial out of two rational lines commensurable in square
    # only, which is where these medials come from; it does not apply to the
    # medials themselves.
    because(prop_X_21, Fraction(1), sqrt(radicand))

    claim("both lines are medial", "X.21", is_medial(a) and is_medial(b))
    claim("they are commensurable in square only", "X.Def.2",
          commensurable_in_square(a, b) and not commensurable(a, b))
    claim("and the rectangle they contain is medial", "X.21",
          is_medial_area(a * b))
    return Out(lines=(a, b))