Book XIII · Proposition 12

XIII.12

If an equilateral triangle be inscribed in a circle, the square on the side of the triangle is triple of the square on the radius of the circle.Heath, 1908

Stepping the radius round the circle gives the hexagon; every other vertex of it gives the equilateral triangle.

Every step, checked

• the circle has positive radiusgiven
• the alternate vertices of the hexagon form an equilateral triangleby IV.15
• the square on its side is triple of the square on the radiusby I.47

What it needs, and what needs it

Needs: I.47 IV.15

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.3, Post.5

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

The proposition as code

@proposition(
    "XIII.12",
    THEOREM,
    sample=samples.segment,
    note="Stepping the radius round the circle gives the hexagon; every other "
    "vertex of it gives the equilateral triangle.",
)
def prop_XIII_12(o: Point, a: Point) -> Out:
    hypothesis("the circle has positive radius", o != a)
    corners = prop_IV_15(o, a).hexagon
    triangle = (corners[0], corners[2], corners[4])
    outline(*triangle)
    result(*triangle)

    because(prop_I_47, o, midpoint_of(triangle[0], triangle[1]), triangle[0])

    claim("the alternate vertices of the hexagon form an equilateral triangle",
          "IV.15",
          eq_len(triangle[0], triangle[1], triangle[1], triangle[2])
          and eq_len(triangle[1], triangle[2], triangle[2], triangle[0]))
    claim("the square on its side is triple of the square on the radius",
          "I.47", len2(triangle[0], triangle[1]) == 3 * len2(o, a))
    return Out(triangle=triangle)