# Quotient by the diagonal line

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

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-quotient-vector-space-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

R2/span{(1,1)} has basis [(0,1)] and dimension 1; its zero coset is the whole diagonal.

Full equivalence and representative-independent operations for a finite-dimensional real quotient vector space; no topological quotient is considered.





## Givens and symbols


- calc


- G1 — V=R2, W={t(1,1):t in R}; [v]=v+W and q(x,y)=y-x.


- [v] — whole coset
- q — coset label y-x
- b — basis representative (0,1)





## Rules and sources


- calc · prerequisite — Assume the real field, usual coordinate-vector arithmetic, matrix multiplication, and definitions of independence and span; elimination uses invertible elementary row operations.
- mko_definition · cited — Vectors v,u name the same coset exactly when v−u lies in W. Quotient elements are cosets, not unique representatives. Check representative independence of [v]+[u]=[v+u] and scalar*[v]=[scalar*v]. In finite dimension dim(V/W)=dim(V)−dim(W), and the zero coset is W. · mko-quotient-vector-space





## Main derivation

S01 · impliesBefore

W=\{(t,t):t\in\mathbb R\}

After

0\in W,\quad(s,s)+(t,t)=(s+t,s+t),\quad\lambda(t,t)=(\lambda t,\lambda t)

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

Universal closure qualifies W as a subspace, with complete one-vector basis (1,1).



S02 · equivalentBefore

v=(x,y),\quad u=(a,b)

After

v-u\in W\iff y-b=x-a\iff q(v)=q(u)

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Two vectors represent the same coset exactly when their q-values agree; cosets are whole lines with a fixed value of y-x.



S03 · impliesBefore

v'=v+w_1,\quad u'=u+w_2,\quad w_1,w_2\in W

After

(v'+u')-(v+u)=w_1+w_2\in W

Conditions: none

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

Any representative replacement changes the sum by W, proving quotient addition well-defined.



S04 · impliesBefore

v'=v+w,\quad w\in W,\quad\lambda\in\mathbb R

After

\lambda v'-\lambda v=\lambda w\in W

Conditions: none

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

Every real scalar preserves the class, making scalar multiplication well-defined.



S05 · impliesBefore

[0]=0+W

After

[0]=W,\quad[(1,1)]=[(0,0)]

Conditions: none

Rule: mko_definition · Uses: G1, S01, S02

Leaf basis: mko_definition

The quotient zero is all of W, not a singleton.



S06 · impliesBefore

v=(x,y),\quad b=(0,1)

After

v-(y-x)b=(x,x)\in W\Rightarrow[v]=(y-x)[b]

Conditions: none

Rule: calc · Uses: G1, S02, S04

Leaf basis: calc

Every coset is a real multiple of [b], giving full spanning.



S07 · impliesBefore

\lambda[b]=[0]

After

(0,\lambda)\in W\iff\lambda=0

Conditions: none

Rule: calc · Uses: G1, S01, S04, S05

Leaf basis: calc

A diagonal vector with first coordinate zero has second coordinate zero, proving [b] independent and nonzero.



S08 · impliesBefore

\{[b]\}\text{ independent and spanning}

After

\dim(V/W)=1=2-1=\dim V-\dim W

Conditions: none

Rule: mko_definition · Uses: G1, S01, S06, S07

Leaf basis: mko_definition

Three complete bases verify the dimension difference here: two for V, one for W, one for the quotient.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S01, S06, S07 — This is an instance certificate, not a general abstract proof.
- S07 · premise_audit · G1, S01, S04, S05 — A nonzero vector need not have a nonzero coset; b outside W is checked here.
- S06 · premise_audit · G1, S02, S04 — This uses the well-defined quotient scalar operation, not numerical division.
- S05 · premise_audit · G1, S01, S02 — The representative vectors differ, but their difference is in W, so their cosets agree.
- S04 · premise_audit · G1, S01, S02 — Zero and negative scalars are included without extra restrictions.
- S03 · premise_audit · G1, S01, S02 — This uses additive closure of W, not preferred-representative tests.
- S02 · inverse_equivalence · G1, S01 — The equivalence covers all real coordinates, not finite membership tests.
- S01 · premise_audit · G1 — Subspace qualification precedes the vector quotient.





## Error controls and negative controls

Zero typeThe quotient zero is W itself, not a unique representative.

Both well-defined operationsAddition and scalar multiplication each require universal closure of W.


- The zero coset contains only (0,0). → reject — It is W, containing all (t,t).
- [(1,0)] differs from [(2,1)]. → reject — Their difference (1,1) is in W.
- Every nonzero vector represents a nonzero coset. → reject — (1,1) is nonzero but lies in W.





## Result and limitations

R2/span{(1,1)} has basis [(0,1)] and dimension 1; its zero coset is the whole diagonal.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 771c4e584bb1897c89adcfcd5b4e225c158db4a9c6492ad3ea24f5772b21d017
- original source SHA-256: f3cefaafea5ecc2a3034c11fb42fd17ee54ad688f67e38f2f43a3a14ed5f3351
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-quotient-vector-space-01.json)