# Points, lines and planes: deciding incidence in the coordinate model [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-point-line-plane/) 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-point-line-plane-01 · production-20261019-adopted-96 ## 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 S01 · definitionBefore \text{points and lines of the chosen model} After \text{point}\in\mathbb{R}^2,\ L(P,Q)=\{P+t(Q-P)\mid t\in\mathbb{R}\}\ (P\neq Q) Conditions: none Rule: mko_model_dependence · Uses: G1, G2 Leaf basis: mko_model_dependence The MKO says the precise properties of lines are fixed by the chosen model, so the model is fixed first: points are ordered pairs in ℝ², and lines are given by the parametric form of G2. From here on, 'on the line' means membership in a set of this model, not how a sketch looks. S02 · impliesBefore P=(1,2),\ Q=(3,6) After P\neq Q Conditions: none Rule: cartesian_product_def · Uses: G3, cartesian_product_def Leaf basis: cartesian_product_def + numeric_evaluation Two ordered pairs are equal only if both coordinates agree; the first coordinates of P and Q are 1≠3, so P≠Q. This is the hypothesis the line definition in G2 requires, so L(P,Q) really is a line. S03 · equivalentBefore Q-P After (2,4) Conditions: none Rule: coord_ops · Uses: G1, G3 Leaf basis: coord_ops + numeric_evaluation Subtract coordinatewise: Q−P=(3−1, 6−2)=(2,4). Both sides name the same ordered pair, so this is a replacement of equals. S04 · equivalentBefore L(P,Q)=\{P+t(Q-P)\mid t\in\mathbb{R}\} After L=\{(1+2t,\,2+4t)\mid t\in\mathbb{R}\} Conditions: P\neq Q Rule: coord_ops · Uses: S01, S02, S03, G3 Leaf basis: coord_ops + eq_replace Substitute P=(1,2) and Q−P=(2,4): P+t(Q−P)=(1,2)+(2t,4t)=(1+2t, 2+4t). For every t the two expressions are the same point, so the two sets are equal. The condition P≠Q was checked in S02. S05 · equivalentBefore R\in L After \exists t\in\mathbb{R}:\ (4,8)=(1+2t,\,2+4t) Conditions: none Rule: image_preimage_def · Uses: S04, G3 Leaf basis: image_preimage_def + def_unfold L is the set of points obtained as t runs through ℝ (the image of t↦(1+2t,2+4t)). So R belongs to L exactly when some real t makes R equal to (1+2t, 2+4t). S06 · equivalentBefore (4,8)=(1+2t,\,2+4t) After 4=1+2t\ \land\ 8=2+4t Conditions: none Rule: cartesian_product_def · Uses: S05, cartesian_product_def Leaf basis: cartesian_product_def Ordered pairs are equal exactly when both coordinates agree, so the point equation splits into two real equations, and both use the same t. S07 · equivalentBefore 4=1+2t After t=\tfrac{3}{2} Conditions: 2\neq 0 Rule: L_solve_linear · Uses: S06 Leaf basis: eq_congruence + mul_inverse_nonzero + two_nonzero By Lemma L_solve_linear (a=1, b=2, c=4): 4=1+2t ⇔ t=(4−1)/2=3/2. Dividing by 2 needs 2≠0. S08 · equivalentBefore 8=2+4t After t=\tfrac{3}{2} Conditions: 4\neq 0 Rule: L_solve_linear · Uses: S06 Leaf basis: eq_congruence + mul_inverse_nonzero + numeric_evaluation The same lemma (a=2, b=4, c=8): 8=2+4t ⇔ t=(8−2)/4=6/4=3/2; here 4≠0. S09 · impliesBefore 4=1+2t\ \land\ 8=2+4t After R\in L Conditions: none Rule: exists_intro · Uses: S05, S06, S07, S08 Leaf basis: exists_intro + and_intro_elim + logic_chain Each equation is satisfied exactly by t=3/2, so the single value t=3/2 satisfies both. By the equivalences S05 and S06, R∈L, and indeed R=P+(3/2)(Q−P). S10 · equivalentBefore S\in L After \exists t\in\mathbb{R}:\ 2=1+2t\ \land\ 5=2+4t Conditions: none Rule: image_preimage_def · Uses: S04, G3 Leaf basis: image_preimage_def + cartesian_product_def Repeat the two unfoldings of S05 and S06 for S: S∈L exactly when some t satisfies both coordinate equations 2=1+2t and 5=2+4t. S11 · equivalentBefore 2=1+2t\ \land\ 5=2+4t After t=\tfrac{1}{2}\ \land\ t=\tfrac{3}{4} Conditions: 2\neq 0; 4\neq 0 Rule: L_solve_linear · Uses: S10 Leaf basis: eq_congruence + mul_inverse_nonzero + two_nonzero + numeric_evaluation Solve each equation: 2=1+2t ⇔ t=1/2 and 5=2+4t ⇔ t=3/4. Each equation is transformed by an equivalence, so the conjunction before and after is true or false together. S12 · impliesBefore \exists t:\ t=\tfrac{1}{2}\ \land\ t=\tfrac{3}{4} After S\notin L Conditions: none Rule: contradiction · Uses: S10, S11 Leaf basis: contradiction + eq_refl_symm_trans + numeric_evaluation If some t equalled both 1/2 and 3/4, symmetry and transitivity of equality would give 1/2=3/4, but 1/2≠3/4. So no such t exists, and by the equivalence S10, S∉L. S13 · impliesBefore t=0,\ t=1 After P\in L,\ Q\in L Conditions: none Rule: image_preimage_def · Uses: S04, G3 Leaf basis: image_preimage_def + coord_ops + numeric_evaluation Taking t=0 gives (1+0, 2+0)=(1,2)=P, and t=1 gives (1+2, 2+4)=(3,6)=Q. So L does pass through the two given points. S14 · impliesBefore P,Q,R\in L,\ S\notin L After P,Q,R\ \text{collinear};\ S\notin L(P,Q) Conditions: none Rule: collinear_def · Uses: S09, S12, S13 Leaf basis: collinear_def + and_intro_elim L contains P, Q and R, so by the definition the three points are collinear; S is not on L. Both conclusions hold in this model. ## Substeps and lemmas S07.1 · equivalentBefore c=a+bt After c-a=bt Conditions: none Rule: eq_congruence · Uses: eq_congruence Leaf basis: eq_congruence + add_assoc + add_comm + add_inverse + add_zero Subtract a from both sides: (a+bt)−a=bt (associativity, commutativity and inverses for addition). The backward move is to add a to both sides. S07.2 · equivalentBefore c-a=bt After t=\frac{c-a}{b} Conditions: b\neq 0 Rule: mul_inverse_nonzero · Uses: S07.1, mul_inverse_nonzero Leaf basis: eq_congruence + mul_inverse_nonzero + mul_assoc + mul_comm + mul_one Since b≠0, 1/b exists; multiplying both sides by 1/b gives (c−a)/b=t. The backward move is to multiply both sides by b. If b=0 there is no 1/b and the step cannot be taken. S07.1 and S07.2 together prove Lemma L_solve_linear. ## 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 itIn 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 enoughThe 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 firstIf 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-point-line-plane-01.json)