Book VI · Proposition 10

VI.10

To cut a given uncut straight line similarly to a given cut straight line.Heath, 1908

Every step, checked

• A and B are distinctgiven
• the given line is cut in ordergiven
• the joining lines are parallel to CBby I.31
• so AB is cut in the same ratios as the given lineby VI.2

What it needs, and what needs it

Needs: I.31 VI.2

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

Depth: 15 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 meetcontinuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circlecontinuity

The proposition as code

@proposition(
    "VI.10",
    CONSTRUCTION,
    sample=lambda rng: samples.segment(rng)
    + (Fraction(rng.randint(1, 3), 8), Fraction(rng.randint(5, 7), 8)),
)
def prop_VI_10(a: Point, b: Point, first, second) -> Out:
    """Cut AB in the same ratios as a given cut line."""
    hypothesis("A and B are distinct", a != b)
    hypothesis("the given line is cut in order", sign(second - first) > 0
               and sign(first) > 0 and sign(1 - second) > 0)
    line(a, b, "the line to be cut")

    aside = posit(Point(a.x + (b.y - a.y), a.y - (b.x - a.x)), "C")
    line(a, aside, "the given cut line, laid alongside")
    given = [posit(_along(a, aside, part), name)
             for part, name in ((first, "D"), (second, "E"))]
    line(aside, b, "the join CB")
    cuts = [posit(_along(a, b, part), name)
            for part, name in ((first, "F"), (second, "G"))]
    for mark, cut in zip(given, cuts):
        line(mark, cut)

    because(prop_I_31, given[0], aside, b)
    because(prop_VI_2, a, aside, b, given[0], cuts[0])

    claim("the joining lines are parallel to CB", "I.31",
          all(parallel(Line.through(mark, cut), Line.through(aside, b))
              for mark, cut in zip(given, cuts)))
    claim("so AB is cut in the same ratios as the given line", "VI.2",
          length(a, cuts[0]) * length(a, aside) == length(a, given[0]) * length(a, b)
          and length(a, cuts[1]) * length(a, aside) == length(a, given[1]) * length(a, b))
    return Out(sections=tuple(cuts))