Book X · Proposition 18

X.18

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 incommensurable, the square on the greater will be greater than the square on the less by the square on a straight line incommensurable with the greater.Heath, 1908

Every step, checked

• the lines are positive and unequalgiven
• the parts are incommensurable exactly when the excess is incommensurable with the greaterby X.18

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.18",
    THEOREM,
    sample=_greater_and_less,
)
def prop_X_18(greater, less) -> Out:
    """The other half of X.17, stated for the incommensurable case."""
    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)

    claim("the parts are incommensurable exactly when the excess is "
          "incommensurable with the greater", "X.18",
          (not commensurable(parts[0], parts[1]))
          == (not commensurable(excess, greater)))
    return Out(parts=parts, excess=excess)