# Triangle: confirming in the coordinate model that three points determine a nondegenerate triangle

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-triangle/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-triangle-01 · production-20261019-adopted-96



## Goal and scope

In the coordinate-plane model ℝ², let A=(0,0), B=(4,0), C=(1,3). Confirm that A, B, C are pairwise distinct and noncollinear, so that by the MKO they determine the nondegenerate triangle ABC; write out its three sides and the side opposite each vertex, and show that the average of the vertices, G=(5/3,1), is not on triangle ABC. Then, with D=(2,1) and E=(6,3), show that the distinct points A, D, E are collinear and so do not determine a nondegenerate triangle.

Works only in the coordinate model of ℝ² (lines and segments defined parametrically) and treats what the MKO sets up: vertices, sides, opposite sides and the nondegeneracy condition. It does not treat classification by sides or angles, angle sums, area, congruence or similarity (the MKO says these need further data and theorems), does not derive the coordinate model from synthetic axioms, and does not change the canonical MKO or its English edition.





## Givens and symbols


- cartesian_product_def
- image_preimage_def
- set_operations_def
- eq_congruence
- numeric_evaluation


- G1 — Model: points are ordered pairs of reals in ℝ², with addition, subtraction and real multiples acting coordinatewise. For distinct points P≠Q, the line L(P,Q)={P+t(Q−P) ∣ t∈ℝ}; the lines of the model are exactly these sets. For any points P, Q, the segment [P,Q]={P+t(Q−P) ∣ 0≤t≤1}.
- G2 — Collinear: points are collinear if some line of the model contains all of them.
- G3 — A=(0,0), B=(4,0), C=(1,3), G=(5/3,1); D=(2,1), E=(6,3).


- A,B,C — the three vertices of the triangle
- L(P,Q) — the line through distinct points P and Q
- [P,Q] — the segment with endpoints P and Q
- \triangle ABC — the union of the three sides [A,B]∪[B,C]∪[C,A]
- t,s,u,r — real parameters
- G — the average of the three vertices, (5/3,1)





## Rules and sources


- cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
- image_preimage_def · prerequisite — Image and preimage: f(S)={f(a) ∣ a∈S}; f⁻¹(T)={a∈A ∣ f(a)∈T}. The preimage notation does not presuppose that f has an inverse.
- set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
- eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
- add_zero · prerequisite — Additive identity: u+0=u.
- contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a.
- eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
- contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
- add_comm · prerequisite — Commutativity of addition: u+v=v+u.
- mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
- set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
- subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
- mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
- exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
- imp_intro · prerequisite — →-introduction (discharging a hypothesis): if Q is derived inside a scope that temporarily assumes P, then P⇒Q follows, and P may no longer be used as known.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬Q.
- mko_triangle_def · cited — Given three distinct noncollinear points A, B, and C in the plane, the union of segments AB, BC, and CA determines the nondegenerate triangle ABC. · mko-triangle
- mko_model_dependence · cited — In a specified geometric model, a point represents a position. Lines and planes are geometric objects carrying points with their respective dimensions, and their precise properties are determined by the axioms and structure of that model. · mko-point-line-plane
- coord_ops · prerequisite — Coordinatewise operations: (a,b)+(c,d)=(a+c,b+d), (a,b)−(c,d)=(a−c,b−d), t(a,b)=(ta,tb).
- line_def · prerequisite — Lines of this model: for distinct points P≠Q, L(P,Q)={P+t(Q−P) ∣ t∈ℝ}; every line of the model is such an L(P,Q).
- segment_def · prerequisite — Segment: for points P, Q, [P,Q]={P+t(Q−P) ∣ 0≤t≤1}; P and Q are its endpoints.
- collinear_def · prerequisite — Collinear: points are collinear if some line contains all of them.
- L_line_unique · lemma — If P≠Q and X, Y are distinct points of L(P,Q), then L(X,Y)=L(P,Q).
- L_seg_reverse · lemma — For any points P, Q: [P,Q]=[Q,P].





## Main derivation

S01 · definitionBefore

\text{three points }A,B,C\text{ of the model}

After

\triangle ABC=[A,B]\cup[B,C]\cup[C,A]\ \text{when}\ A,B,C\ \text{are distinct and noncollinear}

Conditions: none

Rule: mko_triangle_def · Uses: G1, G2, mko_model_dependence

Leaf basis: mko_triangle_def + mko_model_dependence

The MKO's definition has two hypotheses: the three points are distinct, and they are not collinear; under both, the union of the three segments is the nondegenerate triangle ABC. The precise meaning of lines, segments and collinearity depends on the chosen model, so the coordinate model of ℝ² (G1, G2) is fixed first. The rest of the work checks the two hypotheses one at a time and then writes out the union.



S02 · impliesBefore

A=(0,0),\ B=(4,0),\ C=(1,3)

After

A\neq B,\ B\neq C,\ C\neq A

Conditions: none

Rule: cartesian_product_def · Uses: G3, cartesian_product_def

Leaf basis: cartesian_product_def + numeric_evaluation

Ordered pairs are equal only if both coordinates agree. The first coordinates of A and B are 0≠4, of B and C are 4≠1, and of C and A are 1≠0, so the three points are pairwise distinct. This is the MKO's first hypothesis, and it also supplies A≠B, which G1 needs for L(A,B) to be defined.



S03 · equivalentBefore

L(A,B)=\{A+t(B-A)\mid t\in\mathbb{R}\}

After

L(A,B)=\{(4t,\,0)\mid t\in\mathbb{R}\}

Conditions: A\neq B

Rule: coord_ops · Uses: G1, G3, S02

Leaf basis: coord_ops + mul_zero + add_zero

Compute coordinatewise: B−A=(4−0, 0−0)=(4,0), so A+t(B−A)=(0+4t, 0+0·t)=(4t,0). For every t the two expressions are the same point, so the two sets are equal. The condition A≠B was checked in S02.



S04 · equivalentBefore

C\in L(A,B)

After

\exists t\in\mathbb{R}:\ 1=4t\ \land\ 3=0

Conditions: none

Rule: image_preimage_def · Uses: S03, G3

Leaf basis: image_preimage_def + cartesian_product_def

L(A,B) is the image of t↦(4t,0), so C∈L(A,B) means exactly that some real t gives (1,3)=(4t,0); equality of ordered pairs splits this into the coordinate equations 1=4t and 3=0, both with the same t.



S05 · impliesBefore

\exists t\in\mathbb{R}:\ 1=4t\ \land\ 3=0

After

C\notin L(A,B)

Conditions: none

Rule: contradiction · Uses: S04

Leaf basis: contradiction + quantifier_negation + numeric_evaluation

The second equation 3=0 does not involve t and fails for every t, so the conjunction fails for every t and no such t exists; by the equivalence S04, C∉L(A,B). Note that the first equation alone has the solution t=1/4, so looking at the first coordinate alone would mislead.



S06 · equivalentBefore

A,B,C\ \text{collinear}

After

\exists P,Q,\ P\neq Q:\ A,B,C\in L(P,Q)

Conditions: none

Rule: collinear_def · Uses: G1, G2

Leaf basis: collinear_def + line_def + def_unfold

By G2, the three points are collinear when one line contains all three; by G1, the lines of the model are exactly the sets L(P,Q) for distinct P, Q. Together the two definitions give the right-hand side. The next step temporarily assumes the points are collinear and sees what follows.



S07 · impliesBefore

A,B,C\in L(P,Q),\ P\neq Q,\ A\neq B

After

L(P,Q)=L(A,B),\ C\in L(A,B)

Conditions: P\neq Q; A\neq B

Rule: L_line_unique · Uses: S02, S06, L_line_unique

Leaf basis: L_line_unique + exists_elim + eq_replace

Assume A, B, C are collinear; by S06 take P≠Q with A, B, C∈L(P,Q) (∃-elimination; P and Q are fresh names). A and B are two points of L(P,Q) and A≠B (S02), so Lemma L_line_unique (X=A, Y=B) gives L(P,Q)=L(A,B). Then C∈L(P,Q) gives C∈L(A,B). The lemma is proved in S07.1 to S07.3.



S08 · impliesBefore

C\in L(A,B)\ \text{(under the assumption)},\ C\notin L(A,B)

After

A,B,C\ \text{noncollinear}

Conditions: none

Rule: contradiction · Uses: S05, S07

Leaf basis: contradiction + imp_intro

The collinearity assumption leads to C∈L(A,B) (S07), but S05 proved C∉L(A,B): a contradiction. By proof by contradiction the assumption fails: no line contains A, B and C, that is, the three points are noncollinear. This is the MKO's second hypothesis.



S09 · theorem_applicationBefore

A,B,C\ \text{distinct and noncollinear}

After

\triangle ABC=[A,B]\cup[B,C]\cup[C,A]\ \text{nondegenerate}

Conditions: A\neq B,\ B\neq C,\ C\neq A; A,B,C\ \text{noncollinear}

Rule: mko_triangle_def · Uses: S02, S08, mko_triangle_def

Leaf basis: mko_triangle_def + and_intro_elim

Both hypotheses hold (S02, S08), so by the MKO the union of the three segments determines the nondegenerate triangle ABC. Its vertices are the three points A, B, C; its sides are the three segments [A,B], [B,C], [C,A]. The side opposite a vertex is the side that does not have it as an endpoint: BC is opposite A, CA is opposite B, and AB is opposite C.



S10 · equivalentBefore

[A,B],\ [B,C],\ [C,A]

After

\{(4t,0)\},\ \{(4-3t,\,3t)\},\ \{(1-t,\,3-3t)\}\quad(0\le t\le 1)

Conditions: none

Rule: segment_def · Uses: S09, G1, G3

Leaf basis: segment_def + coord_ops + numeric_evaluation

By the segment definition and coordinatewise operations: B−A=(4,0), so [A,B]={(4t,0)}; C−B=(1−4, 3−0)=(−3,3), so [B,C]={(4−3t, 3t)}; A−C=(0−1, 0−3)=(−1,−3), so [C,A]={(1−t, 3−3t)}; all with 0≤t≤1.



S11 · equivalentBefore

\triangle ACB=[A,C]\cup[C,B]\cup[B,A]

After

[C,A]\cup[B,C]\cup[A,B]=\triangle ABC

Conditions: none

Rule: L_seg_reverse · Uses: S09, L_seg_reverse

Leaf basis: L_seg_reverse + set_operations_def + set_extensionality

Changing the order of the vertices only changes the name: by Lemma L_seg_reverse, [A,C]=[C,A], [C,B]=[B,C] and [B,A]=[A,B]; a union does not depend on order, so ACB and ABC are the same set. The lemma is proved in S11.1 and S11.2.



S12 · impliesBefore

A=(4-3t,\,3t),\ 0\le t\le 1

After

A\notin[B,C]

Conditions: none

Rule: contradiction · Uses: S10, G3

Leaf basis: contradiction + cartesian_product_def + numeric_evaluation

If A∈[B,C], some t gives (0,0)=(4−3t, 3t). The second coordinate 0=3t gives t=0, and then the first coordinate is 4−3·0=4≠0, a contradiction. So the vertex A is not on its opposite side BC. The general reason: [B,C]⊆L(B,C), and A∈L(B,C) would make the three points collinear, contradicting S08.



S13 · equivalentBefore

G\in\triangle ABC

After

G\in[A,B]\ \lor\ G\in[B,C]\ \lor\ G\in[C,A]

Conditions: none

Rule: set_operations_def · Uses: S09, G3

Leaf basis: set_operations_def + def_unfold

G=((0+4+1)/3, (0+0+3)/3)=(5/3,1) is the average of the three vertices. By the MKO, triangle ABC is the union of its three sides, so G is on the triangle exactly when it is on at least one side. The three sub-steps check each side.



S14 · impliesBefore

G\notin[A,B],\ G\notin[B,C],\ G\notin[C,A]

After

G\notin\triangle ABC

Conditions: none

Rule: de_morgan_logic · Uses: S13, S13.1, S13.2, S13.3

Leaf basis: de_morgan_logic + set_operations_def

All three disjuncts fail, so by De Morgan's law the disjunction is false, and by the equivalence S13, G∉△ABC. In a sketch G lies in the region the triangle encloses, but the triangle in the MKO is the union of the three sides and contains no interior point. By contrast M=(2,0)=(4·(1/2),0) is on [A,B], so M∈△ABC.



S15 · impliesBefore

A=(0,0),\ D=(2,1),\ E=(6,3)

After

A,D,E\in L(A,D)

Conditions: A\neq D

Rule: collinear_def · Uses: G1, G2, G3

Leaf basis: collinear_def + exists_intro + coord_ops + numeric_evaluation

A≠D (first coordinates 0≠2), so L(A,D) is defined, and D−A=(2,1). t=0 gives A, t=1 gives D, and t=3 gives A+3(D−A)=(6,3)=E. All three points lie on the one line L(A,D), so by G2 they are collinear. They are also pairwise distinct (the first coordinate 6 of E differs from 0 and from 2).



S16 · impliesBefore

\text{S09, S10, S14, S15}

After

\triangle ABC\ \text{nondegenerate};\ A,D,E\ \text{give no nondegenerate triangle}

Conditions: none

Rule: mko_triangle_def · Uses: S09, S10, S12, S14, S15

Leaf basis: mko_triangle_def + and_intro_elim

A, B, C are distinct and noncollinear and determine the nondegenerate triangle ABC, with sides as in S10 and opposite sides as in S09, and G is not on the triangle. A, D, E are distinct but collinear, violating the MKO's second hypothesis, so they do not determine a nondegenerate triangle in this entry's sense.







## Substeps and lemmas

S07.1 · impliesBefore

X,Y\in L(P,Q),\ X\neq Y,\ D=Q-P

After

X=P+sD,\ Y=P+uD,\ s\neq u

Conditions: none

Rule: exists_elim · Uses: G1

Leaf basis: exists_elim + contrapositive + eq_replace

X∈L(P,Q) gives some real s with X=P+sD, and Y∈L(P,Q) gives some real u with Y=P+uD (∃-elimination; s and u are fresh names). If s=u, then X=P+sD=P+uD=Y, contradicting X≠Y; so s≠u.



S07.2 · equivalentBefore

X+t(Y-X)

After

P+\bigl(s+t(u-s)\bigr)D

Conditions: none

Rule: distributive · Uses: S07.1

Leaf basis: distributive + add_assoc + add_comm + mul_comm + coord_ops

First Y−X=(P+uD)−(P+sD)=(u−s)D; then X+t(Y−X)=P+sD+t(u−s)D=P+(s+t(u−s))D. In each coordinate only associativity, commutativity and distributivity are used, so it holds for every real t (N14 checks it as a polynomial identity).



S07.3 · impliesBefore

L(X,Y)=\{P+(s+t(u-s))D\mid t\in\mathbb{R}\}

After

L(X,Y)=\{P+rD\mid r\in\mathbb{R}\}=L(P,Q)

Conditions: u-s\neq 0

Rule: set_extensionality · Uses: S07.1, S07.2

Leaf basis: set_extensionality + subset_def + mul_inverse_nonzero + exists_intro

⊆: each s+t(u−s) is a real number r, so every point of L(X,Y) is in L(P,Q). ⊇: given a real r, take t=(r−s)/(u−s), which is defined because u−s≠0, and then s+t(u−s)=r, so P+rD∈L(X,Y). The two inclusions give equality of the sets. S07.1 to S07.3 together prove Lemma L_line_unique.



S11.1 · equivalentBefore

P+t(Q-P)

After

Q+(1-t)(P-Q)

Conditions: none

Rule: distributive · Uses: G1

Leaf basis: distributive + add_inverse + add_comm + add_assoc + coord_ops

Expand the right side: Q+(1−t)(P−Q)=Q+P−Q−tP+tQ=P+t(Q−P). In each coordinate this is a polynomial identity of reals, valid for every t, P and Q (N15).



S11.2 · impliesBefore

0\le t\le 1

After

[P,Q]=[Q,P]

Conditions: none

Rule: set_extensionality · Uses: S11.1

Leaf basis: order_basics + set_extensionality + subset_def

0≤t≤1 ⇔ 0≤1−t≤1 (multiplying by −1 reverses the inequalities, then add 1). So as t runs over [0,1], 1−t also runs over exactly [0,1]; with S11.1, every point of [P,Q] is a point of [Q,P] and conversely. S11.1 and S11.2 together prove Lemma L_seg_reverse.



S13.1 · impliesBefore

(5/3,\,1)=(4t,\,0)

After

G\notin[A,B]

Conditions: none

Rule: contradiction · Uses: S10

Leaf basis: cartesian_product_def + contradiction

Every point of [A,B] has second coordinate 0, while G has second coordinate 1, and 1≠0, so G∉[A,B].



S13.2 · impliesBefore

(5/3,\,1)=(4-3t,\,3t)

After

G\notin[B,C]

Conditions: none

Rule: contradiction · Uses: S10

Leaf basis: eq_congruence + mul_inverse_nonzero + contradiction + numeric_evaluation

The second coordinate gives 1=3t ⇔ t=1/3 (3≠0); in the first coordinate this gives 4−3·(1/3)=3, and 3≠5/3, so no t satisfies both, and G∉[B,C].



S13.3 · impliesBefore

(5/3,\,1)=(1-t,\,3-3t)

After

G\notin[C,A]

Conditions: none

Rule: contradiction · Uses: S10

Leaf basis: eq_congruence + mul_inverse_nonzero + contradiction + numeric_evaluation

The second coordinate gives 1=3−3t ⇔ t=(3−1)/3=2/3; in the first coordinate this gives 1−2/3=1/3, and 1/3≠5/3, so G∉[C,A].







## Reverse audits


- S16 · sufficient_goal_reduction · S02, S08, S09, S14, S15, mko_triangle_def — Goal: ABC is a nondegenerate triangle, while A, D, E determine none. Sufficient condition H: A, B, C are distinct (S02) and noncollinear (S08), and A, D, E are collinear (S15); H gives the goal by the MKO's definition. H is proved forwards from the givens in S02 to S15; the goal is never used as a premise.
- S15 · premise_audit · G2, collinear_def, exists_intro — Collinearity needs only one line containing the three points, with one parameter value for each point; no uniqueness is needed.
- S14 · premise_audit · S13, S13.1, S13.2, S13.3, de_morgan_logic — To show a point is not in the union, all three sides must be excluded; excluding one is not enough.
- S13.3 · premise_audit · S10, contradiction, mul_inverse_nonzero — As in S13.2: the second coordinate determines t, then the first coordinate is checked against it.
- S13.2 · premise_audit · S10, contradiction, mul_inverse_nonzero — The second coordinate determines t uniquely; both coordinates must use the same t.
- S13.1 · premise_audit · S10, cartesian_product_def — One unequal coordinate is enough to exclude it; the first coordinate need not be solved.
- S13 · inverse_equivalence · set_operations_def, S09 — The membership condition for a union is two-way.
- S12 · premise_audit · S10, contradiction — The second coordinate forces t=0; it remains only to check whether this t also satisfies the first coordinate.
- S11.2 · premise_audit · S11.1, order_basics, set_extensionality — This proof needs the chosen parameter range to be invariant under t↦1−t, as [0,1] is. The range [0,2] is not invariant, but being different from [0,1] does not by itself cause failure: [1/4,3/4] is invariant too. The guide still defines segments using [0,1].
- S11.1 · inverse_equivalence · distributive, add_inverse — It is an identity and holds both ways.
- S11 · inverse_equivalence · L_seg_reverse, set_operations_def — Each replacement is an equality of sets and reordering a union is an equality, so the step holds both ways.
- S10 · inverse_equivalence · segment_def, coord_ops — Backward, check the endpoints: t=0 and t=1 give A and B; then B and C=(4−3,3)=(1,3); then C and A=(1−1,3−3)=(0,0). For each t both forms give the same point.
- S09 · premise_audit · S02, S08, mko_triangle_def — Neither of the MKO's two hypotheses can be dropped; no property of lengths, angles or area of the triangle is claimed here.
- S08 · premise_audit · S05, S07, contradiction — Proof by contradiction needs a statement and its negation together: C∈L(A,B) and C∉L(A,B). C∉L(A,B) alone is not enough; the uniqueness used in S07 is what rules out every other line.
- S07.3 · premise_audit · S07.1, set_extensionality, mul_inverse_nonzero — The ⊇ direction divides by u−s, which needs s≠u from S07.1. If s=u the set would be the single point P+sD, not a line.
- S07.2 · inverse_equivalence · distributive, coord_ops — Both expressions give the same point for every t; it is an identity and holds both ways.
- S07.1 · premise_audit · exists_elim, contrapositive — s≠u comes from X≠Y by contraposition; the converse (s≠u implies X≠Y) would need D≠0, and is neither needed nor claimed here.
- S07 · premise_audit · S02, S06, L_line_unique, exists_elim — The lemma needs A≠B; if A=B, many lines pass through A and L(P,Q)=L(A,B) would not follow. This step is under the collinearity assumption, so its conclusion is conditional; it does not claim that C∈L(A,B) is actually true.
- S06 · inverse_equivalence · collinear_def, line_def — This only unfolds two definitions, so it holds both ways.
- S05 · premise_audit · S04, contradiction, quantifier_negation — The conclusion needs only that no t satisfies both equations; 3≠0 holds whatever t is, so the existential statement is false.
- S04 · inverse_equivalence · image_preimage_def, cartesian_product_def — Unfolding membership in an image and the equality condition for ordered pairs are both two-way.
- S03 · inverse_equivalence · coord_ops, S02 — Backward: t=1 gives (4,0)=B and t=0 gives (0,0)=A; each t gives the same point in both forms, so the step holds both ways.
- S02 · premise_audit · G3, cartesian_product_def — Each pair needs just one differing coordinate; checking only two of the three pairs would not be enough, so all three are checked. The converse (distinct points differ in a particular coordinate) is not claimed.
- S01 · premise_audit · G1, G2, mko_triangle_def, mko_model_dependence — This step only states the definition and the model and derives no new fact; the two hypotheses are not yet checked, so 'ABC is a triangle' may not be written yet.





## Error controls and negative controls

Three points need not form a triangleThe MKO notes the common mistake of thinking that any three points form a nondegenerate triangle. A, D, E are pairwise distinct and in a rough sketch may look like a very flat triangle, but E=A+3(D−A), so the three points lie on one line (S15). If two of the points coincide, as in A, A, B, even distinctness fails. So both hypotheses, S02 and S08, must be checked explicitly; saying 'there are three points' is not enough.

Vertices, sides and the triangle itselfA vertex is a point (for example A), a side is a segment (AB means [A,B]), and the two may not be swapped: 'the vertex AB' uses a side's name as if it were a vertex. By the MKO, triangle ABC is the union of the three sides: G=(5/3,1) looks 'inside the triangle' in a picture, yet lies on none of the sides (S13 to S14), so G∉△ABC.

Do not read lengths or angles off the sketchThe MKO warns against guessing properties from the proportions of a drawing. In a sketch AC and BC may look about equally long, but computing squared lengths separately gives |AC|²=(−1)²+(−3)²=10 and |BC|²=(−3)²+3²=18 (N20, N21), which differ. Such length and angle conclusions belong to other MKOs with their own definitions and theorems; this guide establishes only vertices, sides and opposite sides.


- A, D, E are pairwise distinct, so they determine a nondegenerate triangle → reject — E=A+3(D−A), so the three points are collinear (S15), violating the noncollinearity hypothesis.
- G=(5/3,1) is on triangle ABC because it lies in the region the triangle encloses → reject — By the MKO the triangle is the union of its three sides; G lies on none of them (S13.1 to S13.3).
- AB is a vertex of triangle ABC → reject — AB is a side, the segment [A,B]; the vertices are the three points A, B, C.
- 1=4t has the solution t=1/4, so C is on line AB → reject — The same t must also satisfy the second coordinate equation 3=0, which fails for every t (S05).





## Result and limitations

A=(0,0), B=(4,0), C=(1,3) are pairwise distinct and noncollinear, so by the MKO they determine the nondegenerate triangle ABC=[A,B]∪[B,C]∪[C,A]; its sides are {(4t,0)}, {(4−3t,3t)}, {(1−t,3−3t)} (0≤t≤1), and the sides opposite A, B, C are BC, CA, AB. The average of the vertices, G=(5/3,1), lies on none of the sides and so is not on the triangle. A, D=(2,1), E=(6,3) are distinct but collinear (E=A+3(D−A)), so they determine no nondegenerate triangle.


- N18 and N19 are independent cross-checks in determinant form, valid for these numbers only; the argument does not depend on them.
- This guide works only in the coordinate model of ℝ²; the correspondence between the coordinate model and a synthetic axiom system is not treated here.
- The squared lengths in N20 and N21 serve only an error control; they belong to the Euclidean length MKO and are not part of this argument.





## Verification and source binding

22 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 579b72812beece3e12baad63e611a795eb814972eceec9d3b1dd1abbe85ae559
- original source SHA-256: c4b2a9675620225c60a7ccfcc9072afda7b8e81861a9cd1a613e7b2b997c9dcc
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-triangle-01.json)