Book IV · Proposition 1

IV.1

Into a given circle to fit a straight line equal to a given straight line which is not greater than the diameter of the circle.Heath, 1908

The proviso matters: a chord cannot be longer than a diameter, and Euclid states the limit rather than letting the construction fail.

4 lines and circles drawn

Every step, checked

the circle has positive radiusgiven
CD is a genuine magnitudegiven
CD is not greater than the diametergiven
B lies on the given circleby Def.15
AB equals the given line, both radii of the circle about Aby Def.15

What it needs, and what needs it

Needs: nothing earlier.

Rests on: 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(
    "IV.1",
    CONSTRUCTION,
    sample=samples.circle_and_chord,
    note="The proviso matters: a chord cannot be longer than a diameter, and "
    "Euclid states the limit rather than letting the construction fail.",
)
def prop_IV_1(o: Point, a: Point, c: Point, d: Point) -> Out:
    """Fit into the circle about O a chord equal to the given line CD."""
    hypothesis("the circle has positive radius", o != a)
    hypothesis("CD is a genuine magnitude", c != d, guard=True)
    hypothesis("CD is not greater than the diameter", len2(c, d) <= 4 * len2(o, a))
    given = circle(o, a, "the given circle")
    line(c, d, "the given line CD")

    reach = circle_with_radius2(a, len2(c, d), "circle centre A with radius CD")
    b = posit(meet(reach, given)[0], "B")
    fitted = line(a, b, "the chord AB")

    claim("B lies on the given circle", "Def.15", on_circle(b, given))
    claim("AB equals the given line, both radii of the circle about A", "Def.15",
          eq_len(a, b, c, d))
    return Out(chord=fitted, at=b)