Book XIII · Proposition 1

XIII.1

If a straight line be cut in extreme and mean ratio, the square on the greater segment added to the half of the whole is five times the square on the half.Heath, 1908

The first of five metrical readings of the same cut. Each is an identity in Q(sqrt 5), and each is checked against the point VI.30 produces.

Every step, checked

• A and B are distinctgiven
• D lies on BA produced, with AD half of ABby Post.2, I.10
• the square on CD is five times the square on ADby II.6

What it needs, and what needs it

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

The proposition as code

@proposition(
    "XIII.1",
    THEOREM,
    sample=samples.segment,
    note="The first of five metrical readings of the same cut. Each is an "
    "identity in Q(sqrt 5), and each is checked against the point VI.30 "
    "produces.",
)
def prop_XIII_1(a: Point, b: Point) -> Out:
    hypothesis("A and B are distinct", a != b)
    section = prop_VI_30(a, b).section
    half = posit(_along(a, b, Fraction(-1, 2)), "D")
    line(half, b, "DB, the whole with its half set out beyond A")
    result(half)

    because(prop_I_10, a, b)
    because(prop_II_6, half, a, b)

    claim("D lies on BA produced, with AD half of AB", ["Post.2", "I.10"],
          collinear(half, a, b) and between(half, a, b)
          and 4 * len2(a, half) == len2(a, b))
    claim("the square on CD is five times the square on AD", "II.6",
          len2(section, half) == 5 * len2(a, half))
    return Out(section=section, half=half)