Book XIII · Proposition 8

XIII.8

If in an equilateral and equiangular pentagon straight lines subtend two angles taken in order, they cut one another in extreme and mean ratio, and their greater segments are equal to the side of the pentagon.Heath, 1908

Why the pentagon carries the golden section at all: its diagonals cut each other in extreme and mean ratio, and the greater piece is a side.

Every step, checked

• the circle has positive radiusgiven
• the diagonals meet within the pentagonby Post.1
• AC is cut at H in extreme and mean ratioby VI.30
• and its greater segment equals the side of the pentagonby Def.3

What it needs, and what needs it

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

The proposition as code

@proposition(
    "XIII.8",
    THEOREM,
    sample=samples.segment,
    note="Why the pentagon carries the golden section at all: its diagonals cut "
    "each other in extreme and mean ratio, and the greater piece is a side.",
)
def prop_XIII_8(o: Point, a: Point) -> Out:
    hypothesis("the circle has positive radius", o != a)
    corners = prop_IV_11(o, a).pentagon
    first, second = line(corners[0], corners[2]), line(corners[1], corners[3])
    cross = posit(meet(first, second)[0], "H")
    result(cross)

    whole = length(corners[0], corners[2])
    greater, lesser = length(corners[0], cross), length(cross, corners[2])
    because(prop_VI_30, corners[0], corners[2])

    claim("the diagonals meet within the pentagon", "Post.1",
          between(corners[0], cross, corners[2]))
    claim("AC is cut at H in extreme and mean ratio", "VI.30",
          whole * lesser == greater * greater)
    claim("and its greater segment equals the side of the pentagon", "Def.3",
          greater == length(corners[0], corners[1]) and greater > lesser)
    return Out(pentagon=corners, cross=cross)