Book I · Proposition 12

I.12

To a given infinite straight line, from a given point which is not on it, to draw a perpendicular straight line.Heath, 1908

Every step, checked

• C does not lie on ABgiven
• CG = CH, radii of the circle centre Cby Def.15
• GE = EH, since E bisects GHby I.10
• triangles CGE and CHE have three sides equalby I.8
• hence the adjacent angles at E are equal, so CE is perpendicular to ABby Def.10

What it needs, and what needs it

Needs: I.8 I.10

Used by: II.12 II.13 IV.4 IV.8 IV.13 VI.8

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

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

The proposition as code

@proposition(
    "I.12",
    CONSTRUCTION,
    sample=samples.line_and_external_point,
)
def prop_I_12(a: Point, b: Point, c: Point) -> Out:
    base = Line.through(a, b)
    hypothesis("C does not lie on AB", not on_line(c, base))

    # A circle centred at C large enough to cut AB twice: the distance from C
    # to the line is at most |CA|, so this radius strictly exceeds it.
    reach = len2(c, a) + len2(c, b)
    sweep = circle_with_radius2(c, reach, "circle centre C cutting AB")
    g, h = meet(line(a, b), sweep, "GH")
    g, h = posit(g, "G"), posit(h, "H")

    middle = posit(prop_I_10(g, h).midpoint, "E")
    dropped = line(c, middle, "the perpendicular CE")

    claim("CG = CH, radii of the circle centre C", "Def.15", eq_len(c, g, c, h))
    claim("GE = EH, since E bisects GH", "I.10", eq_len(g, middle, middle, h))
    because(prop_I_8, c, g, middle, c, h, middle)
    claim("triangles CGE and CHE have three sides equal", "I.8",
          congruent_sss((c, g, middle), (c, h, middle)))
    claim("hence the adjacent angles at E are equal, so CE is perpendicular to AB", "Def.10",
          perpendicular(dropped, base))
    return Out(perpendicular=dropped, foot=middle)