Book X · Proposition 17

X.17

If there be two unequal straight lines, and to the greater there be applied a parallelogram equal to the fourth part of the square on the less and deficient by a square figure, and if it divide it into parts which are commensurable in length, then the square on the greater will be greater than the square on the less by the square on a straight line commensurable with the greater.Heath, 1908

Applying an area to a line and asking whether the parts come out commensurable is exactly asking whether a quadratic has a nice root. X.17 and X.18 are the two answers.

Every step, checked

• the lines are positive and unequalgiven
• the two parts make up the greaterby II.5
• and the rectangle they contain is a quarter the square on the lessby II.5
• the parts are commensurable exactly when the excess is commensurable with the greaterby X.17

What it needs, and what needs it

Needs: II.5

Rests on: C.N.1, C.N.2, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.22, Def.4, Post.5

Depth: 13 steps of argument above the first principles. Parallel postulate: needed.

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×4)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×4)continuity

The proposition as code

@proposition(
    "X.17",
    THEOREM,
    sample=_greater_and_less,
    note="Applying an area to a line and asking whether the parts come out "
    "commensurable is exactly asking whether a quadratic has a nice root. "
    "X.17 and X.18 are the two answers.",
)
def prop_X_17(greater, less) -> Out:
    """The parallelogram equal to a quarter the square on the less, deficient
    by a square, divides the greater at these two points."""
    hypothesis("the lines are positive and unequal",
               sign(greater) > 0 and sign(less) > 0 and sign(greater - less) > 0, guard=True)
    excess = sqrt(greater * greater - less * less)
    parts = ((greater - excess) / 2, (greater + excess) / 2)
    # II.5 is about a line bisected and also cut unequally, so the greater line
    # is laid down and cut at the first of the two parts. Book X argues about
    # magnitudes and draws nothing; the appeal needs a figure, and this is the
    # one Euclid's own statement describes.
    because(prop_II_5, Point(0, 0), Point(parts[0], 0), Point(greater, 0))

    claim("the two parts make up the greater", "II.5", parts[0] + parts[1] == greater)
    claim("and the rectangle they contain is a quarter the square on the less",
          "II.5", parts[0] * parts[1] == less * less / 4)
    claim("the parts are commensurable exactly when the excess is commensurable "
          "with the greater", "X.17",
          commensurable(parts[0], parts[1]) == commensurable(excess, greater))
    return Out(parts=parts, excess=excess)