Book X · Proposition 10

X.10

To find two straight lines incommensurable, the one in length only, and the other in square also, with an assigned straight line.Heath, 1908

The existence of the incommensurable, constructed rather than argued: one line irrational in length only, another irrational in square as well.

Every step, checked

• the assigned line is positivegiven
• the first is incommensurable in length with the assigned lineby X.9
• but commensurable with it in squareby X.9
• the second is incommensurable with it in square as wellby X.9

What it needs, and what needs it

Needs: X.9

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.10",
    CONSTRUCTION,
    sample=lambda rng: (Fraction(rng.randint(1, 6), rng.randint(1, 4)),),
    note="The existence of the incommensurable, constructed rather than argued: "
    "one line irrational in length only, another irrational in square as well.",
)
def prop_X_10(assigned) -> Out:
    hypothesis("the assigned line is positive", sign(assigned) > 0)
    in_length_only = assigned * sqrt(2)
    in_square_also = assigned * sqrt(sqrt(2))

    because(prop_X_9, assigned, assigned * 2)

    claim("the first is incommensurable in length with the assigned line", "X.9",
          not commensurable(in_length_only, assigned))
    claim("but commensurable with it in square", "X.9",
          commensurable_in_square(in_length_only, assigned))
    claim("the second is incommensurable with it in square as well", "X.9",
          not commensurable_in_square(in_square_also, assigned))
    return Out(in_length_only=in_length_only, in_square_also=in_square_also)