Book XIII · Proposition 2

XIII.2

If the square on a straight line be five times the square on a segment of it, then, when the double of the said segment is cut in extreme and mean ratio, the greater segment is the remaining part of the original straight line.Heath, 1908

The converse of XIII.1. Alone among the five, its given configuration needs sqrt 5 before any construction begins: C stands at a fifth part of the square, so the sampler leaves the rationals to lay the figure out.

Every step, checked

• C lies on ABgiven
• the square on AB is five times the square on ACgiven
• CD is double of ACby Post.2
• the greater segment of CD equals the remainder CBby VI.30
• and it is the greater of the twoby Def.3

What it needs, and what needs it

Needs: VI.30

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.2, 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 (×7)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.2",
    THEOREM,
    sample=_five_times,
    note="The converse of XIII.1. Alone among the five, its given configuration "
    "needs sqrt 5 before any construction begins: C stands at a fifth part of "
    "the square, so the sampler leaves the rationals to lay the figure out.",
)
def prop_XIII_2(a: Point, b: Point, c: Point) -> Out:
    hypothesis("C lies on AB", collinear(a, b, c) and between(a, c, b))
    hypothesis("the square on AB is five times the square on AC",
               len2(a, b) == 5 * len2(a, c))
    line(a, b, "the given line AB")
    doubled = posit(_along(a, c, -1), "D")
    section = prop_VI_30(c, doubled).section
    result(doubled)

    claim("CD is double of AC", "Post.2",
          collinear(c, doubled, a) and len2(c, doubled) == 4 * len2(a, c))
    claim("the greater segment of CD equals the remainder CB", "VI.30",
          len2(c, section) == len2(c, b))
    claim("and it is the greater of the two", "Def.3",
          len2(c, section) > len2(section, doubled))
    return Out(doubled=doubled, section=section)