Book I · Proposition 46

I.46

On a given straight line to describe a square.Heath, 1908

Every step, checked

• A and B are distinctgiven
• AD = AB by constructionby I.3
• ADEB is a parallelogram, so the opposite sides are equalby I.34
• the angle at A is rightby I.11
• and therefore all four angles are rightby I.34
• the figure is equilateral and right-angled: a squareby Def.22

What it needs, and what needs it

Needs: I.3 I.11 I.34

Used by: I.47 II.4 II.5 II.6 II.7 II.11 II.14

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: 11 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 (×3)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×8)continuity

The proposition as code

@proposition(
    "I.46",
    CONSTRUCTION,
    sample=samples.segment,
)
def prop_I_46(a: Point, b: Point) -> Out:
    hypothesis("A and B are distinct", a != b)
    beyond = posit(Point(a.x + (a.x - b.x), a.y + (a.y - b.y)), "A'")
    upright = prop_I_11(beyond, b, a).perpendicular
    # AD is cut off from the upright equal to AB, which is I.3's business. The
    # lesser line is named BA: I.3 places it at A through I.2, and I.2 joins the
    # point to an end of the line.
    span = circle_with_radius2(a, len2(a, b) * 4, "circle centre A, twice AB")
    far = meet(upright, span)[1]
    d = posit(prop_I_3(a, far, b, a).cut, "D")
    e = posit(_fourth_vertex(a, b, d), "E")
    line(b, e)
    line(d, e)
    because(prop_I_34, a, b, e, d)

    claim("AD = AB by construction", "I.3", eq_len(a, d, a, b))
    claim("ADEB is a parallelogram, so the opposite sides are equal", "I.34",
          eq_len(a, d, b, e) and eq_len(a, b, d, e))
    claim("the angle at A is right", "I.11", right_angle(d, a, b))
    claim("and therefore all four angles are right", "I.34",
          right_angle(a, b, e) and right_angle(b, e, d) and right_angle(e, d, a))
    claim("the figure is equilateral and right-angled: a square", "Def.22",
          eq_len(a, b, b, e) and eq_len(b, e, e, d) and eq_len(e, d, d, a))
    return Out(square=(a, b, e, d))