Book X · Proposition 9

X.9

The squares on straight lines commensurable in length have to one another the ratio which a square number has to a square number; and squares which have to one another the ratio which a square number has to a square number will also have their sides commensurable in length. But the squares on straight lines incommensurable in length have not to one another the ratio which a square number has to a square number; and squares which have not to one another the ratio which a square number has to a square number will not have their sides commensurable in length either.Heath, 1908

The bridge between Book X and Book VII: commensurability in length is the squares standing in the ratio of two square numbers.

Every step, checked

• the magnitudes are positivegiven
• lines commensurable in length have squares in the ratio of two square numbersby X.9
• and lines incommensurable in length have notby X.9

What it needs, and what needs it

Needs: nothing earlier.

Used by: X.10

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.9",
    THEOREM,
    sample=_either_pair,
    note="The bridge between Book X and Book VII: commensurability in length is "
    "the squares standing in the ratio of two square numbers.",
)
def prop_X_9(a, b) -> Out:
    hypothesis("the magnitudes are positive", sign(a) > 0 and sign(b) > 0, guard=True)
    ratio_of_squares = (a * a) / (b * b)
    square_ratio = (
        isinstance(ratio_of_squares, Fraction)
        and _is_square_int(ratio_of_squares.numerator)
        and _is_square_int(ratio_of_squares.denominator)
    )
    claim("lines commensurable in length have squares in the ratio of two square "
          "numbers", "X.9", commensurable(a, b) == square_ratio)
    claim("and lines incommensurable in length have not", "X.9",
          (not commensurable(a, b)) == (not square_ratio))
    return Out(square_ratio=square_ratio)