Book X · Proposition 27

X.27

To find medial straight lines commensurable in square only which contain a rational 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 rationalby X.19

What it needs, and what needs it

Needs: X.19 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.27",
    CONSTRUCTION,
    sample=lambda rng: (rng.choice([2, 3, 5, 7]),),
)
def prop_X_27(radicand: int) -> Out:
    """Medials commensurable in square only, containing a rational rectangle."""
    hypothesis("the radicand is not a square", not _is_square_int(radicand))
    a, b = _medials_in_square_only(radicand, rational_rectangle=True)
    # Each line is the side of a rectangle contained by two rationals
    # commensurable in square only, which is what X.21 makes medial: the first
    # by 1 and sqrt(d), the second by d and sqrt(d).
    because(prop_X_21, Fraction(1), sqrt(radicand))
    because(prop_X_21, Fraction(radicand), sqrt(radicand))
    # X.19 speaks of a rectangle contained by rational lines commensurable in
    # length, and these two are medial. The rectangle here is rational because
    # the medials were chosen to make it so, and the appeal has no pair of
    # rationals in the figure to be about.

    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 rational", "X.19",
          is_rational_area(a * b))
    return Out(lines=(a, b))