Book VI · Proposition 12

VI.12

To three given straight lines to find a fourth proportional.Heath, 1908

Every step, checked

• A and B are distinctgiven
• the given lines are genuine magnitudesgiven
• CF is parallel to BEby I.31
• so AB is to AC as AE is to AFby 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.12",
    CONSTRUCTION,
    sample=lambda rng: samples.segment(rng)
    + (Fraction(rng.randint(2, 7), 4), Fraction(rng.randint(2, 7), 4)),
)
def prop_VI_12(a: Point, b: Point, second, third) -> Out:
    """To three given lines, find the fourth proportional."""
    hypothesis("A and B are distinct", a != b)
    hypothesis("the given lines are genuine magnitudes",
               sign(second) > 0 and sign(third) > 0, guard=True)
    line(a, b, "the first given line AB")
    c = posit(_along(a, b, second), "C")

    aside = posit(Point(a.x + (b.y - a.y), a.y - (b.x - a.x)), "D")
    line(a, aside, "a line through A")
    e = posit(_along(a, aside, third), "E")
    line(b, e, "the join BE")
    fourth = posit(_along(a, aside, third * second), "F")
    line(c, fourth, "the parallel through C")

    because(prop_I_31, c, b, e)
    because(prop_VI_2, a, b, e, c, fourth)

    claim("CF is parallel to BE", "I.31",
          parallel(Line.through(c, fourth), Line.through(b, e)))
    claim("so AB is to AC as AE is to AF", "VI.2",
          length(a, b) * length(a, fourth) == length(a, c) * length(a, e))
    return Out(fourth=fourth)