Book XIII · Proposition 6

XIII.6

If a rational straight line be cut in extreme and mean ratio, each of the segments is the irrational straight line called apotome.Heath, 1908

Book X is asked to name the two segments, and finds both to be apotomes. Euclid stops there; the species is what the classifier adds, and it turns on the given line. Commensurable in length, the segments are of the fifth and first species; commensurable in square only, the sixth and third; commensurable with the square root of five, the fourth and second, because there the greater segment has a rational term.

Every step, checked

• A and B are distinctgiven
• the given line is rationalgiven
• the greater segment is the irrational line called apotomeby X.73
• and so is the lesserby X.73
• the two are of different speciesby X.85, X.89

What it needs, and what needs it

Needs: VI.30 X.73 X.85 X.89

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, X.85-90

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.6",
    THEOREM,
    sample=_rational_line,
    note="Book X is asked to name the two segments, and finds both to be "
    "apotomes. Euclid stops there; the species is what the classifier adds, "
    "and it turns on the given line. Commensurable in length, the segments are "
    "of the fifth and first species; commensurable in square only, the sixth "
    "and third; commensurable with the square root of five, the fourth and "
    "second, because there the greater segment has a rational term.",
)
def prop_XIII_6(a: Point, b: Point) -> Out:
    hypothesis("A and B are distinct", a != b)
    # Book X Def. 3: a rational straight line is one commensurable with the
    # assigned line in length or in square only. Asking for commensurability in
    # length is a narrower condition than Euclid's, and the conclusion does not
    # need it -- the necessity analysis reported this hypothesis as surviving
    # being broken, which is what a condition doing no work looks like.
    hypothesis("the given line is rational", is_rational_in_square(length(a, b)))
    section = prop_VI_30(a, b).section
    greater, lesser = length(a, section), length(section, b)
    named, other = classify(greater), classify(lesser)

    # X.73 makes the apotome out of two rational lines commensurable in square
    # only; those are the terms of the greater segment, not the segment itself.
    because(prop_X_73, length(a, b) * sqrt(5) / 2, length(a, b) / 2)
    # Which species an apotome belongs to is settled against the assigned
    # rational line, not against the figure it came from, so the segments of a
    # line of arbitrary length are apotomes of a species that moves with that
    # length: on the unit line the greater is the fifth and the lesser the
    # first, and on others neither. There is no one species proposition the
    # step answers to, and X.85 and X.89 are named here for the pair of species
    # this cut produces rather than for a construction to be carried out.

    claim("the greater segment is the irrational line called apotome", "X.73",
          named.family == "apotome")
    claim("and so is the lesser", "X.73", other.family == "apotome")
    claim("the two are of different species", ["X.85", "X.89"],
          named.species != other.species)
    return Out(greater=greater, lesser=lesser,
               species=(named.species, other.species))