Book XIII · Proposition 4

XIII.4

If a straight line be cut in extreme and mean ratio, the square on the whole and the square on the lesser segment together are triple of the square on the greater segment.Heath, 1908

A relation among the three lengths the cut already provides, so it needs no point beyond them.

Every step, checked

• A and B are distinctgiven
• AC is the greater segmentby Def.3
• the squares on the whole and on the lesser segment together are triple of the square on the greaterby II.7

What it needs, and what needs it

Needs: II.7 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.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 proposition as code

@proposition(
    "XIII.4",
    THEOREM,
    sample=samples.segment,
    note="A relation among the three lengths the cut already provides, so it "
    "needs no point beyond them.",
)
def prop_XIII_4(a: Point, b: Point) -> Out:
    hypothesis("A and B are distinct", a != b)
    section = prop_VI_30(a, b).section

    because(prop_II_7, a, section, b)

    claim("AC is the greater segment", "Def.3", len2(a, section) > len2(section, b))
    claim("the squares on the whole and on the lesser segment together are "
          "triple of the square on the greater", "II.7",
          len2(a, b) + len2(section, b) == 3 * len2(a, section))
    return Out(section=section)