Book X · Proposition 29

X.29

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

The pair that makes a *first* binomial: the excess of the squares is commensurable with the greater.

Every step, checked

• the parameters are genuinegiven
• both lines are rationalby X.Def.3
• they are commensurable in length here, being whole numbersby X.5
• and the excess is commensurable in length with the greaterby X.29

What it needs, and what needs it

Needs: X.5

Used by: X.31 X.32

Rests on: X.Def.3

Depth: 4 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.29",
    CONSTRUCTION,
    sample=lambda rng: (rng.randint(2, 8), rng.randint(1, 3)),
    note="The pair that makes a *first* binomial: the excess of the squares is "
    "commensurable with the greater.",
)
def prop_X_29(scale: int, offset: int) -> Out:
    """Rational lines in square only, the excess commensurable with the greater."""
    hypothesis("the parameters are genuine", scale > 1 and offset > 0, guard=True)
    # A Pythagorean-style pair: a = 5k, b = 4k gives excess 3k, commensurable.
    a = Fraction(5 * scale)
    b = Fraction(4 * scale)
    excess = sqrt(a * a - b * b)

    because(prop_X_5, Fraction(1), Fraction(2))

    claim("both lines are rational", "X.Def.3",
          is_rational_in_square(a) and is_rational_in_square(b))
    claim("they are commensurable in length here, being whole numbers", "X.5",
          commensurable(a, b))
    claim("and the excess is commensurable in length with the greater", "X.29",
          commensurable(excess, a))
    return Out(lines=(a, b), excess=excess)