Book I · Proposition 2

I.2

To place at a given point (as an extremity) a straight line equal to a given straight line.Heath, 1908

Every step, checked

• A and B are distinctgiven
• BC is a genuine magnitudegiven
• DA = DB, sides of the equilateral triangleby I.1
• BG = BC, radii of the circle centre Bby Def.15
• DL = DG, radii of the circle centre Dby Def.15
• so AL = BG, the remaindersby C.N.3
• therefore AL = BCby C.N.1

What it needs, and what needs it

Needs: I.1

Used by: I.3

Rests on: C.N.1, C.N.3, Def.15

Depth: 1 steps of argument above the first principles. Parallel postulate: not 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 circle (×2)continuity

The proposition as code

@proposition(
    "I.2",
    CONSTRUCTION,
    sample=samples.point_and_segment,
)
def prop_I_2(a: Point, b: Point, c: Point) -> Out:
    """Euclid cannot simply carry a length across the plane -- his compass
    collapses -- so he transports it through an equilateral triangle."""
    hypothesis("A and B are distinct", a != b)
    hypothesis("BC is a genuine magnitude", b != c, guard=True)
    line(b, c, "the given line BC")

    apex = posit(prop_I_1(a, b).apex, "D")
    through_b = line(apex, b, "DB produced")
    through_a = line(apex, a, "DA produced")

    radius_bc = circle(b, c, "circle centre B through C")
    g = posit(meet(through_b, radius_bc)[1], "G")

    radius_dg = circle_with_radius2(apex, len2(apex, g), "circle centre D through G")
    placed = posit(meet(through_a, radius_dg)[1], "L")

    claim("DA = DB, sides of the equilateral triangle", "I.1", eq_len(apex, a, apex, b))
    claim("BG = BC, radii of the circle centre B", "Def.15", eq_len(b, g, b, c))
    claim("DL = DG, radii of the circle centre D", "Def.15", eq_len(apex, placed, apex, g))
    claim("so AL = BG, the remainders", "C.N.3", eq_len(a, placed, b, g))
    claim("therefore AL = BC", "C.N.1", eq_len(a, placed, b, c))
    return Out(placed=placed, equal_to=(b, c))