Book VI · Proposition 30

VI.30

To cut a given finite straight line in extreme and mean ratio.Heath, 1908

The golden section again, reached through ratios rather than through II.11's rectangles -- and giving the same point.

Every step, checked

• A and B are distinctgiven
• the drawn figures are the square on AC and the rectangle AB by CBby Def.22
• they are equal, which is what cutting in extreme and mean ratio meansby VI.17
• so the whole is to the greater as the greater is to the lessby VI.17
• and the point is the same one II.11 findsby II.11

What it needs, and what needs it

Needs: II.11 VI.17

Used by: XIII.1 XIII.2 XIII.3 XIII.4 XIII.5 XIII.6 XIII.8 XIII.9

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

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

The proposition as code

@proposition(
    "VI.30",
    CONSTRUCTION,
    sample=samples.segment,
    note="The golden section again, reached through ratios rather than through "
    "II.11's rectangles -- and giving the same point.",
)
def prop_VI_30(a: Point, b: Point) -> Out:
    hypothesis("A and B are distinct", a != b)
    line(a, b, "the given line AB")

    golden = (sqrt(5) - 1) / 2
    section = posit(_along(a, b, golden), "C")
    whole, greater, lesser = length(a, b), length(a, section), length(section, b)

    # The section is defined by an equality of figures, so the figures are built:
    # the square on the greater segment against the rectangle contained by the
    # whole and the lesser.
    square = _standing_on(a, section, greater)
    rectangle = _standing_on(a, b, lesser)
    outline(*square)
    outline(*rectangle)

    because(prop_VI_17, a, b, a, section, section, b)

    claim("the drawn figures are the square on AC and the rectangle AB by CB",
          "Def.22",
          _area(*square) == greater * greater and _area(*rectangle) == whole * lesser)
    claim("they are equal, which is what cutting in extreme and mean ratio means",
          "VI.17", _area(*square) == _area(*rectangle))
    claim("so the whole is to the greater as the greater is to the less", "VI.17",
          whole * lesser == greater * greater)
    because(prop_II_11, a, b)

    claim("and the point is the same one II.11 finds", "II.11",
          length(a, section) == whole * golden)
    return Out(section=section, square=square, rectangle=rectangle)