Book X · Proposition 30

X.30

To find two rational straight lines commensurable in square only and such that the square on the greater is greater is greater than the square on the less by the square on a straight line incommensurable in length with the greater.Heath, 1908

Every step, checked

• the parameter is genuinegiven
• both lines are rationalby X.Def.3
• and the excess is incommensurable in length with the greaterby X.30

What it needs, and what needs it

Needs: nothing earlier.

Rests on: X.Def.3

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.30",
    CONSTRUCTION,
    sample=lambda rng: (rng.randint(2, 8),),
)
def prop_X_30(scale: int) -> Out:
    """The same, but with the excess incommensurable with the greater."""
    hypothesis("the parameter is genuine", scale > 1, guard=True)
    a = Fraction(2 * scale)
    b = Fraction(scale)
    excess = sqrt(a * a - b * b)  # sqrt(3) * scale

    claim("both lines are rational", "X.Def.3",
          is_rational_in_square(a) and is_rational_in_square(b))
    claim("and the excess is incommensurable in length with the greater", "X.30",
          not commensurable(excess, a))
    return Out(lines=(a, b), excess=excess)