Book II · Proposition 2

II.2

If a straight line be cut at random, the rectangle contained by the whole and both of the segments is equal to the square on the whole.Heath, 1908

Every step, checked

• B cuts ACgiven
• BF divides the square into the two rectanglesby C.N.2
• each is contained by the whole and one segmentby Def.22
• so the two rectangles together equal the square on the wholeby C.N.2

What it needs, and what needs it

Needs: nothing earlier.

Rests on: C.N.2, Def.22

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

What it takes on trust

• the argument reads a 'between' fact off the figureorder

The proposition as code

@proposition(
    "II.2",
    THEOREM,
    sample=_adjacent_segments,
)
def prop_II_2(a: Point, b: Point, c: Point) -> Out:
    """AC is cut at B. The square on AC is divided at B into the two rectangles."""
    hypothesis("B cuts AC", between(a, b, c))

    lift = _across(a, c)
    square = _rectangle(a, c, lift, "D", "E")
    cut = posit(Point(b.x + lift[0], b.y + lift[1]), "F")
    line(b, cut, "BF, dividing the square")

    first = (a, b, cut, square[3])
    second = (b, c, square[2], cut)
    claim("BF divides the square into the two rectangles", "C.N.2",
          _area(*first) + _area(*second) == _area(*square))
    claim("each is contained by the whole and one segment", "Def.22",
          _area(*first) == length(a, c) * length(a, b)
          and _area(*second) == length(a, c) * length(b, c))
    claim("so the two rectangles together equal the square on the whole", "C.N.2",
          _area(*first) + _area(*second) == length(a, c) * length(a, c))
    return Out(square=square)