# Coordinate plane: deciding axis or quadrant membership and comparing ordered pairs

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-coordinate-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-coordinate-plane-01 · production-20261019-adopted-96



## Goal and scope

In a fixed Cartesian coordinate system, let A=(−3,2), B=(2,−3), B′=(6/3,−3), C=(0,−4), O=(0,0) and E=(−1/2,−5). First prove that the axes meet only at the origin and that every point either lies on an axis or lies in exactly one quadrant; then decide for each point its axis or quadrant, and decide whether A and B, and B and B′, are the same point.

Uses only the MKO's definitions: a fixed origin, perpendicular oriented axes and a unit on each, coordinates as ordered pairs of reals, the x-axis given by y=0 and the y-axis by x=0, and the quadrants off the axes given by the signs of the two coordinates. It infers no distance, angle or figure size (MKO assumption a2) and reads no coordinates from a sketch; the canonical MKO and its English edition are not changed.





## Givens and symbols


- cartesian_product_def
- order_basics
- set_extensionality
- set_operations_def
- numeric_evaluation


- G1 — An origin, perpendicular oriented x- and y-axes and a unit on each axis are fixed in the plane; in this coordinate system each point corresponds to an ordered pair of reals (x,y)∈ℝ², and all points are compared in the same system (MKO assumptions a1, a2).
- G2 — The x-axis is 𝒳={(x,y)∈ℝ² ∣ y=0} and the y-axis is 𝒴={(x,y)∈ℝ² ∣ x=0}; Q_I={(x,y) ∣ x>0 and y>0}, Q_II={(x,y) ∣ x<0 and y>0}, Q_III={(x,y) ∣ x<0 and y<0}, Q_IV={(x,y) ∣ x>0 and y<0}.
- G3 — A=(−3,2), B=(2,−3), B′=(6/3,−3), C=(0,−4), O=(0,0) and E=(−1/2,−5), all given in the coordinate system of G1.


- (x,y) — the ordered coordinates of a point, the first read along the x-axis and the second along the y-axis
- \mathcal{X},\ \mathcal{Y} — the x-axis {y=0} and the y-axis {x=0}
- Q_{\mathrm{I}},\ Q_{\mathrm{II}},\ Q_{\mathrm{III}},\ Q_{\mathrm{IV}} — the first, second, third and fourth quadrants
- O — the origin (0,0)





## 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.
- 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.
- set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
- 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.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
- set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
- 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.
- and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
- mko_coord_plane · cited — In a specified Cartesian coordinate system, a point has the ordered coordinates (x,y). The x-axis satisfies y=0 and the y-axis satisfies x=0, and they meet at (0,0). Away from the axes, the four quadrants are determined by the signs of x and y. · mko-coordinate-plane
- mko_quadrant_signs · cited — When x and y are both nonzero, the sign patterns (+,+), (−,+), (−,−) and (+,−) give the first, second, third and fourth quadrants; points on an axis belong to no quadrant. The origin lies on both axes. · mko-coordinate-plane
- L_classify · lemma — For every (x,y)∈ℝ²: if x=0 or y=0, it lies in no quadrant; if x≠0 and y≠0, it lies in exactly one quadrant.





## Main derivation

S01 · definitionBefore

\text{a point in the fixed coordinate system}

After

\text{point}\leftrightarrow(x,y)\in\mathbb{R}^2,\quad (x,y)=(x',y')\iff x=x'\land y=y'

Conditions: none

Rule: mko_coord_plane · Uses: G1

Leaf basis: mko_coord_plane + cartesian_product_def

First fix the coordinate system (G1); from then on a point is represented by an ordered pair of reals, the first coordinate read along the x-axis and the second along the y-axis. By the equality condition for ordered pairs, two points are the same exactly when both corresponding coordinates are equal; this is the comparison described in MKO para2, and it is meaningful only within one coordinate system.



S02 · definitionBefore

\text{axes and quadrants}

After

\mathcal{X}=\{y=0\},\ \mathcal{Y}=\{x=0\},\ Q_{\mathrm{I}}=\{x>0,y>0\},\ Q_{\mathrm{II}}=\{x<0,y>0\},\ Q_{\mathrm{III}}=\{x<0,y<0\},\ Q_{\mathrm{IV}}=\{x>0,y<0\}

Conditions: none

Rule: def_intro · Uses: G2, S01

Leaf basis: def_intro + mko_quadrant_signs + set_builder

Following the MKO, write the two axes and four quadrants as sets. Note that the quadrants use strict inequalities: Q_I needs x>0 and y>0, not x≥0 and y≥0; this is exactly why points on an axis are excluded from the quadrants.



S03 · impliesBefore

(x,y)\in\mathbb{R}^2

After

(x=0\lor y=0\Rightarrow\text{no quadrant})\ \land\ (x\neq 0\land y\neq 0\Rightarrow\text{exactly one quadrant})

Conditions: none

Rule: L_classify · Uses: S02, order_basics

Leaf basis: L_classify + order_basics + case_analysis

By Lemma L_classify, every point of the plane is classified exactly once by the union of the two axes and the four quadrants: points on an axis are in no quadrant, and points off the axes are in exactly one quadrant. The proof is S03.1 (on an axis), S03.2 (off the axes, at least one) and S03.3 (at most one).



S04 · impliesBefore

\mathcal{X}\cap\mathcal{Y}

After

\{(0,0)\}

Conditions: none

Rule: set_extensionality · Uses: S02

Leaf basis: set_extensionality + set_operations_def

Prove the MKO's statement that the axes meet at (0,0), and only there. The two inclusions are S04.1 and S04.2.



S05 · impliesBefore

A=(-3,2)

After

A\in Q_{\mathrm{II}},\ A\notin\mathcal{X}\cup\mathcal{Y}

Conditions: -3<0; 2>0

Rule: mko_quadrant_signs · Uses: G3, S02, S03

Leaf basis: mko_quadrant_signs + order_basics + numeric_evaluation

The first coordinate of A is −3<0 and the second is 2>0, sign pattern (−,+), which is the definition of Q_II. Since −3≠0, A is not on the y-axis; since 2≠0, A is not on the x-axis. By L_classify, A is in no other quadrant.



S06 · impliesBefore

B=(2,-3)

After

B\in Q_{\mathrm{IV}},\ B\notin\mathcal{X}\cup\mathcal{Y}

Conditions: 2>0; -3<0

Rule: mko_quadrant_signs · Uses: G3, S02, S03

Leaf basis: mko_quadrant_signs + order_basics + numeric_evaluation

The first coordinate of B is 2>0 and the second is −3<0, sign pattern (+,−), so B∈Q_IV. Both coordinates are nonzero, so B is on neither axis.



S07 · impliesBefore

(-3,2)\ \text{and}\ (2,-3)

After

A\neq B,\quad\text{while}\quad\{-3,2\}=\{2,-3\}

Conditions: none

Rule: cartesian_product_def · Uses: S01, S05, S06

Leaf basis: cartesian_product_def + set_extensionality + numeric_evaluation

Equal ordered pairs need equal first coordinates, and −3≠2, so A≠B. By contrast the unordered sets {−3,2} and {2,−3} have the same elements and are equal by set_extensionality. Swapping the coordinates changed the point and even its quadrant (Q_II became Q_IV), so a point cannot be treated as an unordered set.



S08 · equivalentBefore

B'=\left(\tfrac{6}{3},-3\right)

After

B'=(2,-3)=B

Conditions: none

Rule: cartesian_product_def · Uses: G3, S01, S06

Leaf basis: cartesian_product_def + numeric_evaluation + eq_replace

6/3=2 and −3=−3, so both corresponding coordinates are equal and B′=B by the equality condition for ordered pairs; hence B′ is also in Q_IV. Whether points coincide is decided by the coordinate values, not by how they are written.



S09 · impliesBefore

C=(0,-4)

After

C\in\mathcal{Y},\ C\notin\mathcal{X},\ C\ \text{in no quadrant}

Conditions: 0=0; -4\neq 0

Rule: L_classify · Uses: G3, S02, S03

Leaf basis: L_classify + set_builder + numeric_evaluation

The first coordinate of C is 0, so C∈𝒴; the second coordinate is −4≠0, so C∉𝒳. By L_classify (the case x=0), C lies in no quadrant, even though its second coordinate is negative.



S10 · impliesBefore

O=(0,0)

After

O\in\mathcal{X}\cap\mathcal{Y},\ O\ \text{in no quadrant}

Conditions: none

Rule: L_classify · Uses: G3, S03, S04

Leaf basis: L_classify + set_operations_def

By S04, O lies on both axes; by L_classify (x=0), O lies in no quadrant. The origin is the only common point of the axes, not a corner of the first quadrant.



S11 · impliesBefore

E=\left(-\tfrac{1}{2},-5\right)

After

E\in Q_{\mathrm{III}},\ E\notin\mathcal{X}\cup\mathcal{Y}

Conditions: -\tfrac12<0; -5<0

Rule: mko_quadrant_signs · Uses: G3, S02, S03

Leaf basis: mko_quadrant_signs + order_basics + numeric_evaluation

The coordinates of E are −1/2<0 and −5<0, sign pattern (−,−), so E∈Q_III. The coordinates need not be integers; only their signs matter. Both are nonzero, so E is on no axis.



S12 · impliesBefore

A,B,B',C,O,E

After

A\in Q_{\mathrm{II}},\ B=B'\in Q_{\mathrm{IV}},\ E\in Q_{\mathrm{III}},\ C\in\mathcal{Y}\setminus\mathcal{X},\ O\in\mathcal{X}\cap\mathcal{Y},\ A\neq B

Conditions: none

Rule: and_intro_elim · Uses: S05, S06, S07, S08, S09, S10, S11

Leaf basis: and_intro_elim

Collect the decisions: A is in the second quadrant, B and B′ are the same point in the fourth quadrant, E is in the third quadrant, C is on the y-axis but not the x-axis, and O is on both axes; C and O are in no quadrant; A≠B. Every conclusion follows from the coordinate values and the definitions of S02 alone.







## Substeps and lemmas

S03.1 · impliesBefore

x=0\ \lor\ y=0

After

(x,y)\notin Q_{\mathrm{I}}\cup Q_{\mathrm{II}}\cup Q_{\mathrm{III}}\cup Q_{\mathrm{IV}}

Conditions: none

Rule: order_basics · Uses: S02, order_basics

Leaf basis: order_basics + set_operations_def

Every quadrant requires x>0 or x<0, and also y>0 or y<0. By trichotomy, x=0 makes both x>0 and x<0 false, and y=0 makes both y>0 and y<0 false. So whenever x=0 or y=0, none of the four quadrant conditions holds and the point lies in no quadrant.



S03.2 · case_splitBefore

x\neq 0\ \land\ y\neq 0

After

(x,y)\in Q_{\mathrm{I}}\cup Q_{\mathrm{II}}\cup Q_{\mathrm{III}}\cup Q_{\mathrm{IV}}

Conditions: x\neq 0; y\neq 0

Rule: case_analysis · Uses: S02, order_basics

Leaf basis: case_analysis + order_basics

By trichotomy, x≠0 gives x>0 or x<0, and y≠0 gives y>0 or y<0. The four combinations (+,+), (−,+), (−,−) and (+,−) cover every possibility and are exactly the defining conditions of Q_I, Q_II, Q_III and Q_IV, so the point lies in at least one quadrant.



S03.3 · impliesBefore

(x,y)\in Q_i\cap Q_j,\ i\neq j

After

\bot

Conditions: none

Rule: contradiction · Uses: S02, order_basics

Leaf basis: contradiction + order_basics

Any two different quadrants demand opposite signs of x or of y: Q_I and Q_II, and Q_III and Q_IV, differ in x; Q_I and Q_IV, and Q_II and Q_III, differ in y; Q_I and Q_III, and Q_II and Q_IV, differ in both. A point in two different quadrants would need, for example, both x>0 and x<0, contradicting trichotomy. So a point lies in at most one quadrant, and with S03.2 in exactly one. S03.1 to S03.3 together prove Lemma L_classify.



S04.1 · impliesBefore

(x,y)\in\mathcal{X}\cap\mathcal{Y}

After

(x,y)=(0,0)

Conditions: none

Rule: set_operations_def · Uses: S02, set_operations_def

Leaf basis: set_operations_def + cartesian_product_def

(x,y)∈𝒳∩𝒴 means (x,y)∈𝒳 and (x,y)∈𝒴, that is y=0 and x=0; by the equality condition for ordered pairs, (x,y)=(0,0).



S04.2 · impliesBefore

(0,0)

After

(0,0)\in\mathcal{X}\cap\mathcal{Y}

Conditions: none

Rule: set_operations_def · Uses: S02, S04.1

Leaf basis: set_builder + set_operations_def + set_extensionality

The second coordinate of (0,0) is 0, so it lies in 𝒳; the first coordinate is 0, so it lies in 𝒴; hence it lies in the intersection. S04.1 and S04.2 together give 𝒳∩𝒴={(0,0)} by set_extensionality.







## Reverse audits


- S12 · sufficient_goal_reduction · S05, S06, S07, S08, S09, S10, S11, and_intro_elim — Goal G: the classification of every point and the two comparisons. Sufficient condition H: the separate conclusions of S05 to S11; H⇒G is just conjunction. H is proved forwards from the coordinates and the definitions; G is never used as a premise.
- S11 · premise_audit · G3, S02, S03, mko_quadrant_signs — Uses only the signs of the coordinates (N8, N9).
- S10 · premise_audit · S03, S04, L_classify — Directly cites S04 and the lemma; no further computation is needed.
- S09 · premise_audit · S02, S03, L_classify — It needs the strict inequalities in the quadrant definitions; C may not be placed in the third or fourth quadrant (N7).
- S08 · inverse_equivalence · cartesian_product_def, numeric_evaluation — 6/3 and 2 are the same rational number (N6), so the two forms may replace each other in either direction.
- S07 · premise_audit · S01, cartesian_product_def, set_extensionality — One differing coordinate is enough for the points to differ (N5); the converse, that distinct points differ in a particular coordinate, is not claimed.
- S06 · premise_audit · G3, S02, S03, mko_quadrant_signs — As in S05, only the signs of the coordinates are used (N3, N4).
- S05 · premise_audit · G3, S02, S03, mko_quadrant_signs — Only the signs of the two coordinates are needed (N1, N2); the decision does not depend on any drawing.
- S04.2 · premise_audit · S04.1, set_extensionality, set_builder — Both directions are now proved, so the sets are equal.
- S04.1 · premise_audit · set_operations_def, cartesian_product_def — Uses only the definitions of intersection and of ordered pairs; the reverse inclusion is S04.2.
- S04 · premise_audit · S02, set_extensionality — Set equality needs both directions, proved separately in the sub-steps.
- S03.3 · premise_audit · S02, order_basics, contradiction — All six pairs of quadrants are checked; each pair has one coordinate with opposite signs, and the contradiction comes from trichotomy.
- S03.2 · premise_audit · S02, order_basics, case_analysis — The cases must cover every possibility: two signs for x and two for y give four cases, and none may be left out.
- S03.1 · premise_audit · S02, order_basics, set_operations_def — It relies on the strict inequalities in the quadrant definitions; with ≥ instead, the origin would fall into all four 'quadrants'.
- S03 · premise_audit · L_classify, order_basics, S02 — Relies only on the definitions of S02 and trichotomy of the reals; no particular point is involved.
- S02 · premise_audit · G2, def_intro, mko_quadrant_signs, set_builder — This step only names the sets; the strict inequalities are part of the definition and may not be relaxed to ≥ or ≤.
- S01 · premise_audit · G1, mko_coord_plane, cartesian_product_def — This step only fixes the representation and derives no new fact; in a different coordinate system the same point could have other coordinates, so every later decision is confined to the system of G1.





## Error controls and negative controls

Points on an axis are in no quadrantThe first error named in the MKO is to put points on an axis, or the origin, into a quadrant. The quadrants are defined with strict inequalities (S02), so C=(0,−4), although its second coordinate is negative, is in neither the third nor the fourth quadrant, and the origin is not a point of the first quadrant (S03.1, S09, S10).

Ordered pairs do not commuteThe second error named in the MKO is to treat an ordered pair as an unordered set. {−3,2}={2,−3}, but (−3,2)≠(2,−3): the first is in the second quadrant and the second in the fourth (S07). Whether two points coincide is decided by comparing corresponding coordinates one by one.

Coordinates are data, not read from a sketchB′=(6/3,−3) is written differently from B but is the same point (S08), and E with first coordinate −1/2 might look close to the y-axis in a rough sketch. Decisions rest only on the stated coordinate values and the definitions; this guide also infers no distance between points and no figure size (MKO assumption a2).


- The origin (0,0) is in the first quadrant because both its coordinates are ≥0 → reject — Q_I requires x>0 and y>0; 0>0 is false, so the origin is in no quadrant.
- (−3,2)=(2,−3) because both use the same two numbers → reject — Equal ordered pairs need equal first coordinates, and −3≠2; the two points are even in different quadrants.
- C=(0,−4) has a negative second coordinate, so C is in the third or fourth quadrant → reject — The third and fourth quadrants both require x≠0 (x<0 or x>0), while C has x=0, so C is on the y-axis.
- B′=(6/3,−3) and B=(2,−3) are written differently, so they are different points → reject — 6/3=2, so both corresponding coordinates agree and B′=B.





## Result and limitations

The axes meet only at the origin, and every point either lies on an axis (and then in no quadrant) or lies in exactly one quadrant. A=(−3,2)∈Q_II, B=(2,−3)=B′∈Q_IV, E=(−1/2,−5)∈Q_III, C=(0,−4) is on the y-axis and in no quadrant, and O is on both axes and in no quadrant; A≠B although {−3,2}={2,−3}.


- The correspondence between points and ordered pairs of reals (G1) is a premise of the coordinate system; this guide does not derive it from geometric axioms.
- This guide does not deal with distance, angle or figure size; those need a separate semantic bridge (MKO formal next).





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: fd4a7cac8ca8a31eb2c39927c5e170926c77882e66ef91e074b8612e9fe3626b
- original source SHA-256: fd4a7cac8ca8a31eb2c39927c5e170926c77882e66ef91e074b8612e9fe3626b
- 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-coordinate-plane-01.json)