Try
Extend side BC of a triangle beyond C to D. The exterior angle ACD is larger than either remote interior angle A or B in neutral geometry. This statement is weaker than saying the exterior angle equals their sum, which is Euclidean.
A linear pair still sums to π radians: if the interior angle at C is 70°, its supplementary exterior angle is 110°. The exterior-angle theorem bounds each remote angle by 110° separately. It does not yet give their sum. Here neutral geometry means incidence, order and congruence assumptions of an ordered plane, without a parallel axiom; midpoint and angle-transport lemmas are understood as previously available neutral results.
Predict
Predict what happens if two distinct lines perpendicular to the same line meet above it. Their intersection would form a triangle with two right angles. The exterior angle supplementary to one right angle is right as well, contradicting its required strict excess over the other remote right angle.
This proves a useful parallel existence mechanism. It does not prove uniqueness of a line disjoint from another through a prescribed point.
Experiment
Keep the dependency distinction visible.
| Claim | Neutral status in this development | Extra issue |
|---|
| Exterior angle exceeds each remote angle | Neutral theorem | Order placement and SAS |
| Double perpendiculars are disjoint | Neutral consequence | Exterior-angle contradiction |
| Triangle angle sum equals π | Not neutral | Euclidean parallel assumption |
| Triangle angle sum at most π | Archimedean neutral theorem | Saccheri–Legendre proof needed |
Try writing a proof of the second row without a coordinate slope. Then find the step in your usual school proof of the third row that transfers angles across a parallel line. That is the dependency to investigate.
Understand
The exterior-angle construction contains a genuine congruence argument. Let M be the midpoint of AC. Extend BM through M to E so ME=MB. Triangles AMB and CME have AM=CM, BM=EM and equal vertical included angles. SAS gives ∠MCE=∠MAB, the original angle at A. The order/Pasch placement lemma puts ray CE strictly inside angle ACD. Consequently ∠ACD>∠A.
For the remote angle B, apply the same construction with the relevant sides exchanged, and use equality of vertical exterior angles. The strict comparison relies on interior placement; SAS alone gives equality to a subangle but does not establish containment.
The midpoint existence and placement lemmas are dependencies from neutral order/congruence theory. This page supplies the central argument and identifies those dependencies instead of pretending that an unlabelled sketch proves them. A fully formal Hilbert development would prove the lemmas before invoking them.
Apply
A tempting invalid proof of triangle sum π draws a line through A parallel to BC and transfers both base angles. In a neutral theory, constructing a nonintersecting line does not automatically supply the Euclidean parallel-angle identities. The transfer is the hidden assumption.
For optional depth, Saccheri–Legendre proves angle sum at most π in an Archimedean neutral plane. Its full subdivision/Archimedean argument is not supplied here and is not used to establish parallel independence. The coming hyperbolic model will calculate its own triangles, while the real Euclidean model supplies equality. Do not treat finite numerical triangles as a proof of the general synthetic bound.
Prove a midpoint lemma, then audit its model dependence
A synthetic neutral lemma with explicit dependencies. Let A and C be distinct. Assume segment AC has a midpoint M, and let ℓ be the perpendicular to AC at M. Use only segment addition/order, SAS, SSS, uniqueness of the perpendicular at a point and the linear-pair/right-angle conventions. Then the points equidistant from A and C are exactly the points on ℓ. Midpoint existence and perpendicular construction are assumptions of this lemma, not consequences secretly borrowed from coordinates.
For P on ℓ with P≠M, triangles AMP and CMP have AM=CM, shared side MP and equal included right angles. SAS gives AP=CP. The point M itself is equidistant by definition. Conversely, suppose AP=CP and P does not lie on line AC. SSS gives congruent triangles AMP and CMP; hence angles AMP and PMC are equal. They form a linear pair, so each is a right angle and PM is ℓ (using uniqueness of the perpendicular at M). If P lies on AC, order gives three possibilities: outside segment AC its two endpoint distances differ by AC>0; inside, segment addition and AP=PC force P to be its unique midpoint; at an endpoint equality fails. Thus P=M in that case. This proves both directions without slopes, affine averages or a parallel axiom.
Synthetic changed case. A point P lies strictly on A’s side of the perpendicular bisector. Can AP=CP? Explain using the locus theorem, without a diagram-based comparison of which length is shorter. Feedback: equality would force P onto ℓ, contradicting strict sidedness. The lemma excludes equality but, by itself, has not proved the stronger inequality AP<CP. A separate order/congruence argument is needed for that inequality. This is the exact logical strength of a locus theorem.
The following coordinate calculation is a separate model-level verification, not the synthetic proof above.
In the Euclidean coordinate plane, a nondegenerate segment from A to C has exactly one point M lying strictly between its endpoints and equidistant from them. This is a model-specific lemma we can prove completely. It must not be relabeled as a derivation from neutral incidence/order/congruence axioms.
Write a point on the segment as X=A+t(C−A), with 0≤t≤1. Positive homogeneity of the Euclidean norm gives |AX|=t|AC| and |XC|=(1−t)|AC|. Since A≠C, |AC|>0. Equality forces t=1/2, and conversely that value gives equal lengths and lies strictly between 0 and 1. Thus M=(A+C)/2 exists, is unique and satisfies the required order statement. This proof names its affine parametrization, real-number order and norm assumptions rather than hiding them in a picture.
Worked affine transfer. For A=(−2,0), C=(4,0), M=(1,0). Under the invertible affine map T(x,y)=(2x+y+3,y−1), these become (−1,−1), (11,−1) and (5,−1). Affine maps preserve midpoint equations: T((A+C)/2)=(T(A)+T(C))/2. They do not generally preserve arbitrary lengths or angles; midpoint preservation here follows from the algebraic average and collinearity, not from calling T a rigid motion.
Changed written task. Replace T by the noninvertible projection P(x,y)=(x,0), and start with A=(0,−1), C=(0,1). Which conclusion survives? Feedback: P still preserves the midpoint equation but sends both endpoints and midpoint to (0,0). Strict betweenness of distinct images fails. Invertibility or at least noncollapse on the chosen segment is needed for that order conclusion.
Return to the exterior-angle construction above and label every invocation of midpoint existence. The coordinate argument verifies it in this particular Euclidean model. A fully synthetic neutral development must independently establish midpoint existence from its chosen axioms; neither this calculation nor a plotted hyperbolic example supplies that missing general derivation.
Continue
Write one neutral proof and one Euclidean proof side by side, annotating every added assumption. Continue to parallel postulates to distinguish nonintersection existence, uniqueness and the consequences that textbooks often combine under one word.
