Book I · Proposition 1

I.1

On a given finite straight line to construct an equilateral triangle.Heath, 1908

Every step, checked

• CA = AB, both radii of the circle centre Aby Def.15
• CB = BA, both radii of the circle centre Bby Def.15
• therefore CA = CBby C.N.1

What it needs, and what needs it

Needs: nothing earlier.

Used by: I.2 I.9 I.10 I.11

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

Depth: 0 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

The proposition as code

@proposition(
    "I.1",
    CONSTRUCTION,
    sample=samples.segment,
)
def prop_I_1(a: Point, b: Point) -> Out:
    """The first construction in the *Elements*, and the first thing it takes
    on faith: that the two circles meet at all."""
    line(a, b, "the given line AB")
    around_a = circle(a, b, "circle centre A through B")
    around_b = circle(b, a, "circle centre B through A")
    apex = posit(meet(around_a, around_b)[0], "C")
    line(a, apex)
    line(b, apex)

    claim("CA = AB, both radii of the circle centre A", "Def.15", eq_len(apex, a, a, b))
    claim("CB = BA, both radii of the circle centre B", "Def.15", eq_len(apex, b, b, a))
    claim("therefore CA = CB", "C.N.1", eq_len(apex, a, apex, b))
    return Out(apex=apex, triangle=(a, b, apex))