Book VI · Proposition 13

VI.13

To two given straight lines to find a mean proportional.Heath, 1908

The geometric mean, raised as the height of a semicircle. This is the construction that makes every rational length's square root constructible.

Every step, checked

• B lies between A and Cgiven
• the angle in the semicircle is rightby III.31
• BD is the mean proportional: AB is to BD as BD is to BCby VI.8

What it needs, and what needs it

Needs: I.10 I.11 III.31 VI.8

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

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

The proposition as code

@proposition(
    "VI.13",
    CONSTRUCTION,
    sample=_mean_proportional_setup,
    note="The geometric mean, raised as the height of a semicircle. This is the "
    "construction that makes every rational length's square root constructible.",
)
def prop_VI_13(a: Point, b: Point, c: Point) -> Out:
    hypothesis("B lies between A and C", on_line(b, Line.through(a, c)) and b != a and b != c)
    middle = posit(prop_I_10(a, c).midpoint, "M")
    semicircle = circle_with_radius2(middle, len2(middle, a), "the semicircle on AC")
    upright = prop_I_11(a, c, b).perpendicular
    d = posit(meet(upright, semicircle)[1], "D")

    because(prop_III_31, middle, a, c, d)
    because(prop_VI_8, a, d, c)

    claim("the angle in the semicircle is right", "III.31", right_angle(a, d, c))
    claim("BD is the mean proportional: AB is to BD as BD is to BC", "VI.8",
          length(a, b) * length(b, c) == length(b, d) * length(b, d))
    return Out(mean=d)