Points, lines and planes: deciding incidence in the coordinate model

Goal and scope

In the coordinate-plane model ℝ², let P=(1,2) and Q=(3,6). Decide whether R=(4,8) and S=(2,5) lie on the line L through P and Q, and hence whether P, Q, R are collinear.

Decides incidence only in one stated model (the coordinate model of ℝ², with lines defined parametrically), illustrating the MKO's point that the precise properties of lines and planes are fixed by the chosen model. It does not treat axiomatic geometry in general, planes or higher dimensions, and does not change the canonical MKO or its English edition.

Givens and symbols

• cartesian_product_def
• image_preimage_def
• eq_congruence
• mul_inverse_nonzero
• numeric_evaluation

• G1 — Model: points are ordered pairs of reals in ℝ²; addition, subtraction and real multiples act coordinatewise.
• G2 — Lines in this model: for distinct points P≠Q, the line through P and Q is L(P,Q)={P+t(Q−P) ∣ t∈ℝ}.
• G3 — P=(1,2), Q=(3,6), R=(4,8), S=(2,5).

• \mathbb{R}^2 — the set of ordered pairs of reals; the points here
• P,Q,R,S — the four given points
• L(P,Q) — the line through distinct points P and Q
• t — the real parameter of the line
• Q-P — direction vector, coordinatewise difference

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.
• 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.
• 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.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• 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.
• 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.
• two_nonzero · prerequisite — In the reals 0<1, hence 0<1+1=2, so 2≠0.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• add_zero · prerequisite — Additive identity: u+0=u.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• 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).
• collinear_def · prerequisite — Collinear: points are collinear if some line contains all of them.
• L_solve_linear · lemma — For reals a, c and b≠0: c=a+bt ⇔ t=(c−a)/b.

Main derivation

\text{points and lines of the chosen model}

\text{point}\in\mathbb{R}^2,\ L(P,Q)=\{P+t(Q-P)\mid t\in\mathbb{R}\}\ (P\neq Q)

P=(1,2),\ Q=(3,6)

P\neq Q

Q-P

(2,4)

L(P,Q)=\{P+t(Q-P)\mid t\in\mathbb{R}\}

L=\{(1+2t,\,2+4t)\mid t\in\mathbb{R}\}

R\in L

\exists t\in\mathbb{R}:\ (4,8)=(1+2t,\,2+4t)

(4,8)=(1+2t,\,2+4t)

4=1+2t\ \land\ 8=2+4t

4=1+2t

t=\tfrac{3}{2}

8=2+4t

t=\tfrac{3}{2}

4=1+2t\ \land\ 8=2+4t

R\in L

S\in L

\exists t\in\mathbb{R}:\ 2=1+2t\ \land\ 5=2+4t

2=1+2t\ \land\ 5=2+4t

t=\tfrac{1}{2}\ \land\ t=\tfrac{3}{4}

\exists t:\ t=\tfrac{1}{2}\ \land\ t=\tfrac{3}{4}

S\notin L

t=0,\ t=1

P\in L,\ Q\in L

P,Q,R\in L,\ S\notin L

P,Q,R\ \text{collinear};\ S\notin L(P,Q)

Substeps and lemmas

c=a+bt

c-a=bt

c-a=bt

t=\frac{c-a}{b}

Reverse audits

• S14 · sufficient_goal_reduction · S09, S12, S13, collinear_def — Goal G: P, Q, R are collinear and S∉L(P,Q). The sufficient condition H is the conjunction that L contains P, Q and R and that S∉L. S09 and S13 establish the first conjunct; S12 establishes the second. The collinearity definition and conjunction introduction give H⇒G, without using G as a premise.
• S13 · premise_audit · S04, image_preimage_def — Each point needs only one parameter value; the step does not claim the value is unique.
• S12 · premise_audit · S10, S11, contradiction — The contradiction comes from one t having to satisfy both equations; each equation alone has a solution, so one coordinate alone cannot decide membership.
• S11 · inverse_equivalence · L_solve_linear — Substituting back, 1+2·(1/2)=2 and 2+4·(3/4)=5; each equivalence is two-way.
• S10 · inverse_equivalence · image_preimage_def, cartesian_product_def — As in S05 and S06, both unfoldings are two-way.
• S09 · premise_audit · S05, S07, S08, exists_intro — What is needed is one common t: S07 and S08 give the same value, which is what makes the existence claim true. A solution of one equation alone is not enough.
• S08 · inverse_equivalence · L_solve_linear — Substituting back, 2+4·(3/2)=8; both directions are given by the lemma.
• S07.2 · inverse_equivalence · mul_inverse_nonzero, eq_congruence — Multiplying by 1/b and by b undo each other, given b≠0; that is exactly the lemma's hypothesis.
• S07.1 · inverse_equivalence · eq_congruence, add_inverse — Subtracting a and adding a undo each other and are possible for every real a, with no side condition.
• S07 · inverse_equivalence · L_solve_linear — Substituting back, 1+2·(3/2)=4; both directions are given by the lemma.
• S06 · inverse_equivalence · cartesian_product_def — The equality condition for ordered pairs is itself two-way; after splitting, the two equations may not use different values of t.
• S05 · inverse_equivalence · image_preimage_def — This unfolds membership in an image: such a t gives R∈L, and R∈L supplies such a t, so it holds both ways.
• S04 · inverse_equivalence · S02, S03, coord_ops — Each t gives the same point in both forms, so the sets agree element by element and the step holds both ways.
• S03 · inverse_equivalence · coord_ops, numeric_evaluation — Backward: P+(2,4)=(1+2, 2+4)=(3,6)=Q, which restores Q−P=(2,4); both expressions name the same point.
• S02 · premise_audit · G3, cartesian_product_def — One differing coordinate suffices for the points to differ; the converse (distinct points differ in a particular coordinate) is not claimed.
• S01 · premise_audit · G1, G2, mko_model_dependence — This step only chooses and states the model and derives no new fact; every later conclusion holds in this model only.

Error controls and negative controls

Appearing to lie on a line is not the same as lying on it

In a sketch S=(2,5) is close to L: at x=2 the point of L is (2,4), only 1 away. The MKO warns against taking a drawing's appearance as a definition. Here membership is decided entirely by the model's equations: the two coordinate equations of S have no common solution, so S∉L however close it looks.

One coordinate is not enough

The first coordinate equation of S, 2=1+2t, has the solution t=1/2, and on its own suggests S is on the line. But t=1/2 in the second coordinate gives 2+4·(1/2)=4≠5. Incidence needs one t that satisfies both coordinate equations (S06 and S12).

Why P≠Q is checked first

If P=Q then Q−P=(0,0) and {P+t·(0,0) ∣ t∈ℝ} is the single point P, not a line. The definition in G2 gives a line only for two distinct points, so S02 must establish P≠Q before S04 can treat L as a line.

• S looks very close to the line in a sketch, so S is on L → reject — Incidence is decided by equations; the coordinate equations of S demand t=1/2 and t=3/4, with no common solution.
• From 2=1+2t we get t=1/2, so S∈L → reject — The second coordinate fails: 2+4·(1/2)=4≠5.
• Any two points P, Q (including P=Q) determine a line {P+t(Q−P)} → reject — When P=Q this set is the single point P.
• In every geometric model, collinearity of three points can be decided by these coordinate equations → reject — These equations belong to the coordinate model of ℝ²; the MKO says the properties of lines depend on the chosen model, and in another model (for example spherical geometry) lines are defined differently.

Result and limitations

In the coordinate model of ℝ², R=(4,8) lies on the line through P and Q (at t=3/2), so P, Q, R are collinear; S=(2,5) does not lie on this line, because its two coordinate equations demand t=1/2 and t=3/4, which contradict each other.

• This guide does not prove that the line through two distinct points is unique, so it claims only S∉L(P,Q), not that P, Q, S lie on no common line.
• N8 and N9 are independent cross-checks in determinant form, valid for these numbers only; the argument does not depend on them.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: acf8e1534a6a5a0b508ab339ff6a480eccfed9de9c617ae4b40a60230ec65bfc
• original source SHA-256: fe3365f185ad4359da5ff93616296d2ba284d6ea11f6bb9927b953ceefeb6905
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)