Book X · Proposition 22

X.22

The square on a medial straight line, if applied to a rational straight line, produces as breadth a straight line rational and incommensurable in length with that to which it is applied.Heath, 1908

Every step, checked

• the first is medialgiven
• the second is rationalgiven
• the breadth produced is rational in squareby X.20
• but incommensurable in length with the line applied toby X.22

What it needs, and what needs it

Needs: X.20

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.22",
    THEOREM,
    sample=lambda rng: (_medial_line(rng), Fraction(rng.randint(1, 5), rng.randint(1, 3))),
)
def prop_X_22(medial, rational) -> Out:
    hypothesis("the first is medial", is_medial(medial))
    hypothesis("the second is rational", is_rational_line(rational) and sign(rational) > 0)
    breadth = (medial * medial) / rational
    because(prop_X_20, rational, rational) if is_rational_line(rational) else None

    claim("the breadth produced is rational in square", "X.20",
          is_rational_in_square(breadth))
    claim("but incommensurable in length with the line applied to", "X.22",
          not commensurable(breadth, rational))
    return Out(breadth=breadth)