Book I · Proposition 3

I.3

Given two unequal straight lines, to cut off from the greater a straight line equal to the less.Heath, 1908

Every step, checked

• AB is greater than CDgiven
• AE = AL = CDby I.2
• E falls between A and B, since AB is the greaterby C.N.5

What it needs, and what needs it

Needs: I.2

Used by: I.5 I.6 I.9 I.11 I.18 I.44 I.46 II.8 IV.10 VI.9

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

Depth: 2 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 (×3)continuity
• the argument reads a 'between' fact off the figureorder

The proposition as code

@proposition(
    "I.3",
    CONSTRUCTION,
    sample=samples.unequal_segments,
)
def prop_I_3(a: Point, b: Point, c: Point, d: Point) -> Out:
    hypothesis("AB is greater than CD", len2(a, b) > len2(c, d))
    line(c, d, "the given lesser line CD")

    # I.2 exists because the compass collapses: it carries a length to a point
    # that is not on it. A lesser line already beginning at A needs no carrying,
    # and asking I.2 for it makes Postulate 1 draw a line from A to itself.
    # I.5, I.9, I.11, I.18, IV.10 and VI.9 all cut off a length from a line they
    # share an end with, and every one of them met that.
    placed = d if a == c else prop_I_2(a, c, d).placed
    reach = circle_with_radius2(a, len2(a, placed), "circle centre A with radius CD")
    cut = posit(meet(line(a, b), reach)[1], "E")

    claim("AE = AL = CD", "I.2", eq_len(a, cut, c, d))
    claim("E falls between A and B, since AB is the greater", "C.N.5", between(a, cut, b))
    return Out(cut=cut)