# Universal closure of a line through zero

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

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



## Goal and scope

U={(x,2x):x in R} is a subspace of R2, whereas U+(0,1) is not.

A homogeneous line, zero space, whole R2 and explicit counterexamples; no sampled positive proof.





## Givens and symbols


- calc
- subspace_def


- G1 — V=R2, U={(x,y):y-2x=0}, with usual vector addition and all real scalars.


- U — homogeneous line
- \lambda — arbitrary real scalar





## 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 — This slice handles the zero space, the whole space, lines through the origin and explicit finite counterexamples in R². Positive cases use universal algebraic certificates from homogeneous linear equations or spans. Finitely many successful samples do not prove a subspace. · mko-vector-subspace
- subspace_def · prerequisite — A subset U of a real vector space V is a subspace under restricted operations if it contains zero and is closed under addition and every real scalar; the remaining vector laws are inherited from V.





## Main derivation

S01 · equivalentBefore

(x,y)\in U

After

y=2x\iff(x,y)=x(1,2)

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

Solving the homogeneous equation gives a complete parameterization, not just several points.



S02 · impliesBefore

0\in\mathbb R

After

(0,0)=0(1,2)\in U

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Parameter zero gives the zero vector, proving nonemptiness.



S03 · impliesBefore

u=a(1,2),\ v=b(1,2),\quad a,b\in\mathbb R

After

u+v=(a+b)(1,2)\in U

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

The sum of any two elements remains a real multiple of the same generator.



S04 · impliesBefore

u=a(1,2),\quad\lambda\in\mathbb R

After

\lambda u=(\lambda a)(1,2)\in U

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Every real scalar preserves the parameterization, including negative and noninteger scalars.



S05 · impliesBefore

0\in U,\quad U+U\subseteq U,\quad\mathbb R U\subseteq U

After

U\le\mathbb R^2

Conditions: none

Rule: subspace_def · Uses: G1, S02, S03, S04

Leaf basis: subspace_def

All three obligations have universal algebraic proofs, so U is a subspace; other vector laws restrict from R2.



S06 · impliesBefore

Z=\{(0,0)\},\quad V=\mathbb R^2

After

Z+Z=Z,\ \lambda Z\subseteq Z;\quad V+V\subseteq V,\ \lambda V\subseteq V

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

The zero space is closed directly; the whole space is closed because sums and products of reals are real.



S07 · impliesBefore

A=\{(x,y):y=2x+1\}

After

(0,0)\notin A

Conditions: none

Rule: calc · Uses: G1, S02

Leaf basis: calc

The translated affine line omits zero, immediately refuting subspace status.



S08 · impliesBefore

B=\{(x,0):x\in\mathbb R\}\cup\{(0,y):y\in\mathbb R\}

After

(1,0),(0,1)\in B,\quad(1,1)\notin B

Conditions: none

Rule: calc · Uses: G1, S03

Leaf basis: calc

The union of coordinate axes contains zero and each axis is closed, but their union fails additive closure.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S03 — One explicit counterexample refutes universal closure; finitely many positive samples cannot prove it.
- S07 · premise_audit · G1, S02 — (0,1) lies in A but zero times it does not, also directly refuting scalar closure.
- S06 · premise_audit · G1 — Both contain zero, and addition and all scalars are checked separately.
- S05 · premise_audit · G1, S02, S03, S04 — The certificate uses the usual operations and cannot be reused unchanged for different ones.
- S04 · premise_audit · G1, S01 — Lambda is neither bounded nor restricted to integers; checking only 2 is insufficient.
- S03 · premise_audit · G1, S01 — a and b are arbitrary; two numerical examples would not replace the proof.
- S02 · premise_audit · G1, S01 — Containing zero is necessary but does not yet prove closure.
- S01 · inverse_equivalence · G1 — Substitution gives 2x-2x=0, verifying both directions.





## Error controls and negative controls

All real scalarsClosure must hold for every real lambda, not merely integers.

Homogeneityy-2x=0 contains zero; replacing zero by 1 gives a different affine set.


- The line y=2x+1 is a subspace. → reject — It omits (0,0).
- Containing zero and closure under integer multiples suffice. → reject — Z2 is closed under addition and integer multiples, but (1/2)(1,0) is outside it.
- A union of two subspaces is a subspace. → reject — The union of axes omits (1,0)+(0,1)=(1,1).





## Result and limitations

U={(x,2x):x in R} is a subspace of R2, whereas U+(0,1) is not.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 866398e5461531188f4557b3cabd302424ab3b6911d677de331ab220569bbdb6
- original source SHA-256: 866398e5461531188f4557b3cabd302424ab3b6911d677de331ab220569bbdb6
- 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-vector-subspace-01.json)