Book X · Proposition 35

X.35

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

The pair behind *the side of the sum of two medial areas* -- the hardest of the six, needing both areas medial and incommensurable.

Every step, checked

• the radicand is not a squaregiven
• the two are incommensurable in squareby X.35
• the sum of the squares is medialby X.35
• the rectangle is medialby X.35
• and the two areas are incommensurable with one anotherby X.35

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.35",
    CONSTRUCTION,
    sample=lambda rng: (rng.choice([5, 7]),),
    note="The pair behind *the side of the sum of two medial areas* -- the "
    "hardest of the six, needing both areas medial and incommensurable.",
)
def prop_X_35(radicand: int) -> Out:
    hypothesis("the radicand is not a square", not _is_square_int(radicand))
    squares = sqrt(radicand)
    rectangle = sqrt(3) / 2
    a, b = _pair_from(squares, rectangle)

    claim("the two are incommensurable in square", "X.35",
          not commensurable_in_square(a, b))
    claim("the sum of the squares is medial", "X.35",
          is_medial_area(a * a + b * b))
    claim("the rectangle is medial", "X.35", is_medial_area(a * b))
    claim("and the two areas are incommensurable with one another", "X.35",
          not commensurable(a * a + b * b, a * b))
    return Out(lines=(a, b))