Book XIII · Proposition 9

XIII.9

If the side of the hexagon and that of the decagon inscribed in the same circle be added together, the whole straight line has been cut in extreme and mean ratio, and its greater segment is the side of the hexagon.Heath, 1908

The decagon side is cut from the circle: bisecting the arc the pentagon subtends halves it into two decagon arcs. That the hexagon side is the radius is IV.15's, and is cited here as Euclid cites it.

Every step, checked

• the circle has positive radiusgiven
• K bisects the arc the pentagon side subtends, so AK is the side of the decagonby III.30
• OL is the side of the hexagon with the side of the decagon added to itby IV.15, Post.2
• OL is cut at A in extreme and mean ratioby VI.30
• and its greater segment is the side of the hexagonby Def.3

What it needs, and what needs it

Needs: III.30 IV.11 IV.15 VI.30

Rests on: C.N.1, C.N.2, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.19, Def.22, Def.3, Def.4, Post.1, Post.2, Post.3, Post.5, V.Def.5

Depth: 19 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 (×20)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×20)continuity
• the argument reads a 'between' fact off the figureorder

The proposition as code

@proposition(
    "XIII.9",
    THEOREM,
    sample=samples.segment,
    note="The decagon side is cut from the circle: bisecting the arc the "
    "pentagon subtends halves it into two decagon arcs. That the hexagon side "
    "is the radius is IV.15's, and is cited here as Euclid cites it.",
)
def prop_XIII_9(o: Point, a: Point) -> Out:
    hypothesis("the circle has positive radius", o != a)
    around = circle(o, a, "the given circle")
    corners = prop_IV_11(o, a).pentagon
    tenth = posit(_arc_midpoint(o, corners[0], corners[1], around), "K")
    decagon = length(corners[0], tenth)
    hexagon = length(o, a)  # IV.15: the side of the hexagon is the radius
    end = posit(_along(a, o, -decagon / hexagon), "L")
    line(o, end, "the hexagon side with the decagon side added to it")
    result(tenth, end)

    because(prop_III_30, o, corners[0], corners[1])
    because(prop_IV_15, o, a)
    because(prop_VI_30, o, end)

    claim("K bisects the arc the pentagon side subtends, so AK is the side of "
          "the decagon", "III.30",
          on_circle(tenth, around) and eq_len(tenth, corners[0], tenth, corners[1]))
    claim("OL is the side of the hexagon with the side of the decagon added "
          "to it", ["IV.15", "Post.2"],
          on_line(end, line(o, a)) and length(o, end) == hexagon + decagon
          and between(o, a, end))
    claim("OL is cut at A in extreme and mean ratio", "VI.30",
          length(o, end) * length(a, end) == hexagon * hexagon)
    claim("and its greater segment is the side of the hexagon", "Def.3",
          hexagon > decagon)
    return Out(decagon=decagon, hexagon=hexagon, whole=end)