∠-bisector unique — Angle bisector exists and is unique · Principia

Dependencies: Protractor axiom.

Statement

Let $\angle AOB$ satisfy $0^\circ < \theta < 180^\circ$ , where $\theta = \angle AOB$ . Then inside $\angle AOB$ there exists a unique ray $OC$ emanating from $O$ such that

\angle AOC = \angle COB = \tfrac{\theta}{2}.

This ray $OC$ is called the bisector of $\angle AOB$ .

$Angle-bisector uniqueness: inside \angle AOB there is a unique ray OC that cuts \angle AOB into two equal halves \theta/2$

Proof

Use only Protractor axiom: inside $\angle AOB$ , sweeping counterclockwise around $O$ from $OA$ to $OB$ , each $\varphi\in(0,\theta)$ corresponds uniquely to an interior ray $OC_\varphi$ with $\angle AOC_\varphi = \varphi$ (the protractor gives a bijection between $(0,\theta)$ and the interior rays of $\angle AOB$ ).

Existence: take $\varphi = \theta/2 \in (0,\theta)$ and call the corresponding ray $OC$ . Then $\angle AOC = \theta/2$ , so $\angle COB = \theta - \theta/2 = \theta/2 = \angle AOC$ .

Uniqueness: if some other ray $OC'$ also bisects $\angle AOB$ , i.e. $\angle AOC' = \angle C'OB$ , then $2\angle AOC' = \theta$ , so $\angle AOC' = \theta/2 = \angle AOC$ . By the injectivity of the protractor, the same angle value corresponds to the same interior ray, so $OC' = OC$ . $\qquad\blacksquare$

$Step 1: the protractor pins down OC at \varphi = \theta/2 (existence); any alternative OC' is squeezed back to the same OC via "2\angle AOC' = \theta" (uniqueness)$

Immediate consequences

Isoceles: median, altitude, bisector coincide reduces the "apex-angle bisector" to this unique ray, and then by symmetry shows it is simultaneously the median and altitude to the base.
In the argument that the three angle bisectors of a triangle meet at a point (triangle Three angle bisectors meet (incenter)), "the bisector" of each interior angle is the unique object provided by this theorem — without it, "three lines concurrent" cannot even be stated cleanly.

Remarks

The proof contains no figure manipulation: no folding, no rotation to overlay $\angle AOC$ onto $\angle COB$ . We simply translate the geometric condition "bisection" into the numerical condition "angle measure equals $\theta/2$ ", and then invoke the bijectivity of the protractor. This is the immediate dividend of Protractor axiom having algebraised "angle" — many arguments that appear to require "moving" pieces around are in fact just a single substitution.