Book II · Proposition 14

II.14

To construct a square equal to a given rectilineal figure.Heath, 1908

Quadrature of the rectangle. The side of the equal square is the mean proportional between the sides, raised as the height of a semicircle.

ABCMD
88 lines and circles drawn, of which 68 helper constructions drew the fainter ones

Every step, checked

What it needs, and what needs it

Needs: I.10 I.11 I.46 I.47 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: 15 steps of argument above the first principles. Parallel postulate: needed.

What it takes on trust

The proposition as code

@proposition(
    "II.14",
    CONSTRUCTION,
    sample=_adjacent_segments,
    note="Quadrature of the rectangle. The side of the equal square is the mean "
    "proportional between the sides, raised as the height of a semicircle.",
)
def prop_II_14(a: Point, b: Point, c: Point) -> Out:
    """The rectangle has sides AB and BC, laid end to end along AC."""
    hypothesis("B lies between A and C", on_line(b, Line.through(a, c)) and b != a and b != c)
    middle = posit(prop_I_10(a, c).midpoint, "M")
    semicircle = circle_with_radius2(middle, len2(middle, a), "the semicircle on AC")
    upright = prop_I_11(a, c, b).perpendicular
    d = posit(meet(upright, semicircle)[1], "D")
    square = prop_I_46(b, d).square

    # Euclid has no Book III here, and does not need it: the right angle is the
    # one he constructed at B, not the one in the semicircle. II.5 and I.47 do
    # the rest between them.
    because(prop_I_47, middle, b, d)
    because(prop_II_5, a, b, c)

    claim("BD stands at right angles to AC, being so constructed", "I.11",
          right_angle(d, b, a))
    claim("MD and MA are equal, both radii of the semicircle", "Def.15",
          eq_len(middle, d, middle, a))
    claim("the square on MD equals the squares on MB and BD", "I.47",
          len2(middle, d) == len2(middle, b) + len2(b, d))
    claim("the rectangle AB by BC, with the square on MB, equals the square on MA",
          "II.5", length(a, b) * length(b, c) + len2(middle, b) == len2(middle, a))
    claim("so the square on BD equals the given rectangle", "C.N.3",
          len2(b, d) == length(a, b) * length(b, c))
    return Out(square=square, side=(b, d))