Book IV · Proposition 4

IV.4

In a given triangle to inscribe a circle.Heath, 1908

The incircle. Its centre is where the angle bisectors meet, and unlike the circumcentre it is irrational in general -- the kernel carries it exactly.

Every step, checked

• ABC is a genuine trianglegiven
• the centre lies on the bisector of each angleby I.9
• the perpendiculars from it to the three sides are equalby I.26
• each perpendicular meets its side at right anglesby I.12
• so the circle on that radius touches all three sidesby III.16

What it needs, and what needs it

Needs: I.9 I.12 I.26 III.16

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

Depth: 12 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 meet (×6)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×9)continuity

The proposition as code

@proposition(
    "IV.4",
    CONSTRUCTION,
    sample=samples.triangle,
    note="The incircle. Its centre is where the angle bisectors meet, and unlike "
    "the circumcentre it is irrational in general -- the kernel carries it exactly.",
)
def prop_IV_4(a: Point, b: Point, c: Point) -> Out:
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    outline(a, b, c)

    # Where two angle bisectors cross. Weighting each vertex by the opposite
    # side is the same point Euclid reaches with I.9, and reaches it without
    # intersecting two constructed rays.
    opposite = (length(b, c), length(c, a), length(a, b))
    total = opposite[0] + opposite[1] + opposite[2]
    centre = posit(
        Point(
            (opposite[0] * a.x + opposite[1] * b.x + opposite[2] * c.x) / total,
            (opposite[0] * a.y + opposite[1] * b.y + opposite[2] * c.y) / total,
        ),
        "O",
    )
    feet = [
        posit(_foot_of_the_perpendicular(centre, *side), "DEF"[index])
        for index, side in enumerate(((b, c), (c, a), (a, b)))
    ]
    for foot in feet:
        line(centre, foot)
    inscribed = circle(centre, feet[0], "the inscribed circle")

    because(prop_I_9, b, a, c)
    because(prop_I_12, b, c, centre)
    because(prop_I_26, centre, feet[0], b, centre, feet[2], b)
    because(prop_III_16, centre, feet[0])

    claim("the centre lies on the bisector of each angle", "I.9",
          all(eq_angle(*pair) for pair in (
              (b, a, centre, centre, a, c),
              (a, b, centre, centre, b, c),
              (a, c, centre, centre, c, b))))
    claim("the perpendiculars from it to the three sides are equal", "I.26",
          eq_len(centre, feet[0], centre, feet[1])
          and eq_len(centre, feet[0], centre, feet[2]))
    claim("each perpendicular meets its side at right angles", "I.12",
          all(right_angle(centre, feet[index], vertex)
              for index, vertex in enumerate((b, c, a))))
    claim("so the circle on that radius touches all three sides", "III.16",
          all(on_circle(foot, inscribed) for foot in feet))
    return Out(centre=centre, circle=inscribed)