Book X · Proposition 31

X.31

To find two medial straight lines commensurable in square only, containing a rational rectangle, and such that the square on the greater is greater than the square on the less by the square on a straight line commensurable in length with the greater.Heath, 1908

Every step, checked

• the radicand is not a squaregiven
• the two are medialgiven
• the rectangle they contain is medial or rationalby X.25
• and the excess is commensurable with the greaterby X.29

What it needs, and what needs it

Needs: X.25 X.29

Rests on: X.Def.3

Depth: 5 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.31",
    CONSTRUCTION,
    sample=lambda rng: (rng.choice([2, 3, 5, 7]),),
)
def prop_X_31(radicand: int) -> Out:
    """Medials in square only, rational rectangle, excess commensurable."""
    hypothesis("the radicand is not a square", not _is_square_int(radicand))
    quarter = sqrt(sqrt(radicand))
    a, b = 5 * quarter, 4 * quarter
    hypothesis("the two are medial", is_medial(a) and is_medial(b))
    excess = sqrt(a * a - b * b)

    because(prop_X_29, 2, 1)

    # X.25 wants two medials commensurable in square only; these two stand in
    # the ratio 5 to 4 and so are commensurable in length.

    claim("the rectangle they contain is medial or rational", "X.25",
          is_medial_area(a * b) or is_rational_area(a * b))
    claim("and the excess is commensurable with the greater", "X.29",
          commensurable(excess, a))
    return Out(lines=(a, b), excess=excess)