Book X · Proposition 33

X.33

To find two straight lines incommensurable in square which make the sum of the squares on them rational but the rectangle contained by them medial.Heath, 1908

The pair behind the *major* line: squares rational, rectangle medial.

Every step, checked

• the scale is genuinegiven
• the two are incommensurable in squareby X.33
• the sum of the squares on them is rationalby X.33
• and the rectangle they contain is medialby X.33

What it needs, and what needs it

Needs: nothing earlier.

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.33",
    CONSTRUCTION,
    sample=lambda rng: (Fraction(rng.randint(1, 3), rng.randint(1, 2)),),
    note="The pair behind the *major* line: squares rational, rectangle medial.",
)
def prop_X_33(scale) -> Out:
    hypothesis("the scale is genuine", sign(scale) > 0, guard=True)
    squares = scale * scale
    rectangle = squares * sqrt(2) / 4
    a, b = _pair_from(squares, rectangle)

    claim("the two are incommensurable in square", "X.33",
          not commensurable_in_square(a, b))
    claim("the sum of the squares on them is rational", "X.33",
          is_rational_area(a * a + b * b))
    claim("and the rectangle they contain is medial", "X.33",
          is_medial_area(a * b))
    return Out(lines=(a, b))