# Real vector space: auditing axiom instances in ℝ³ and proving one distributive law

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



## Goal and scope

In ℝ³ take u=(1,−2,3), v=(4,0,−1), a=2, b=−3. (1) Confirm the dimensions agree; (2) check exactly the five axiom instances a(u+v)=au+av, (a+b)u=au+bu, (ab)u=a(bu), 1u=u and u+(−u)=0; (3) prove a(u+v)=au+av for every real a and all u, v∈ℝ³; (4) use a modified scalar multiplication on ℝ² to show that successful instances do not establish an axiom.

Treats only the fixed-dimensional real coordinate space ℝ³ (and an ℝ² structure as a counterexample), with integer-coordinate vectors and integer scalars regarded as real vectors and real scalars, respectively (MKO assumption a1). The general proof covers only the distributive law a(u+v)=au+av; the other axioms are checked here as instances only, and no complete proof for ℝ³ is claimed (MKO assumption a2). The canonical MKO and its English edition are not changed.





## Givens and symbols


- distributive
- mul_assoc
- mul_one
- add_inverse
- numeric_evaluation


- G1 — ℝ³ is the set of ordered triples of reals; addition is componentwise: (x₁,x₂,x₃)+(y₁,y₂,y₃)=(x₁+y₁,x₂+y₂,x₃+y₃); scalar multiplication is componentwise: a(x₁,x₂,x₃)=(ax₁,ax₂,ax₃); the zero vector is (0,0,0); −(x₁,x₂,x₃)=(−x₁,−x₂,−x₃). Addition is defined only between vectors of the same dimension.
- G2 — u=(1,−2,3), v=(4,0,−1), a=2, b=−3.
- G3 — Comparison structure: ℝ² with the usual componentwise addition, but with scalar multiplication changed to a⊙(x,y)=(ax,y), which scales only the first component.


- \mathbb{R}^3 — the set of ordered triples of reals
- u,\ v — the given vectors
- a,\ b — the given real scalars
- 0=(0,0,0) — the zero vector of ℝ³
- u_k — the k-th component of u, k=1,2,3
- a\odot(x,y) — the modified scalar multiplication (ax,y) of the comparison structure





## Rules and sources


- distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
- mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
- mul_one · prerequisite — Multiplicative identity: 1·u=u.
- add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- vector_space_axioms · prerequisite — Vector space axioms (over ℝ or another field F): vectors form a commutative group under addition; scalar multiplication satisfies a(u+v)=au+av, (a+b)u=au+bu, (ab)u=a(bu) and 1u=u.
- 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.
- two_nonzero · prerequisite — In the reals 0<1, hence 0<1+1=2, so 2≠0.
- 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.
- forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
- 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.
- neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- mko_rvs_def · cited — A real vector space V has vector addition, a zero vector, additive inverses and real scalar multiplication, satisfying associativity, commutativity, distributivity, the unit-scalar law and scalar-multiplication compatibility. Exercises here check only exact axiom instances in fixed-dimensional real coordinate spaces. · mko-real-vector-space
- coord_ops · prerequisite — In the real coordinate space ℝⁿ of fixed dimension n, vector addition and scalar multiplication act componentwise; the sum of vectors of different dimensions is undefined.
- tuple_eq · prerequisite — Two ordered tuples of the same length are equal if and only if all corresponding components are equal.
- L_coord_distrib · lemma — For every real a and all u, v∈ℝ³: a(u+v)=au+av.





## Main derivation

S01 · definitionBefore

(\mathbb{R}^3,+,\cdot)

After

\text{audit: } a(u+v)=au+av,\ (a+b)u=au+bu,\ (ab)u=a(bu),\ 1u=u,\ u+(-u)=0

Conditions: none

Rule: vector_space_axioms · Uses: G1, mko_rvs_def

Leaf basis: vector_space_axioms + mko_rvs_def

By the MKO, a real vector space needs vector addition, a zero vector, additive inverses and real scalar multiplication satisfying, for all vectors and all scalars, the associative, commutative, distributive, unit-scalar and compatibility axioms. This guide picks five of them and first checks instances on the given data.



S02 · impliesBefore

u=(1,-2,3),\ v=(4,0,-1)

After

u,v\in\mathbb{R}^3,\ u+v\ \text{defined}

Conditions: \dim u=\dim v=3

Rule: coord_ops · Uses: G1, G2

Leaf basis: coord_ops

u and v both have three components and lie in the same ℝ³, so u+v is defined. If one vector were in ℝ² and the other in ℝ³, as in (1,2)+(1,2,3), the model has no such operation.



S03 · equivalentBefore

u+v

After

(1+4,\,-2+0,\,3+(-1))=(5,-2,2)

Conditions: none

Rule: coord_ops · Uses: S02

Leaf basis: coord_ops + numeric_evaluation

Add componentwise: 1+4=5, −2+0=−2, 3+(−1)=2.



S04 · equivalentBefore

a(u+v)=2(5,-2,2)

After

(10,-4,4)

Conditions: none

Rule: coord_ops · Uses: S03, G2

Leaf basis: coord_ops + numeric_evaluation

The scalar 2 multiplies every component: 2·5=10, 2·(−2)=−4, 2·2=4. Scaling only the first component is a common mistake.



S05 · equivalentBefore

au,\ av

After

au=(2,-4,6),\ av=(8,0,-2)

Conditions: none

Rule: coord_ops · Uses: G2

Leaf basis: coord_ops + numeric_evaluation

Scale each vector: 2·(1,−2,3)=(2,−4,6) and 2·(4,0,−1)=(8,0,−2).



S06 · equivalentBefore

au+av

After

(2+8,\,-4+0,\,6+(-2))=(10,-4,4)

Conditions: none

Rule: coord_ops · Uses: S05

Leaf basis: coord_ops + numeric_evaluation

Add componentwise: 2+8=10, −4+0=−4, 6+(−2)=4.



S07 · impliesBefore

a(u+v)=(10,-4,4),\ au+av=(10,-4,4)

After

a(u+v)=au+av\ \text{for these } a,u,v

Conditions: none

Rule: eq_refl_symm_trans · Uses: S04, S06

Leaf basis: eq_refl_symm_trans + tuple_eq

Both sides equal (10,−4,4), so by symmetry and transitivity of equality the instance holds for these data. It is only an instance: MKO assumption a2 warns that a passing instance does not establish the axiom.



S08 · impliesBefore

a\in\mathbb{R},\ u,v\in\mathbb{R}^3\ \text{arbitrary}

After

\forall a\in\mathbb{R}\ \forall u,v\in\mathbb{R}^3:\ a(u+v)=au+av

Conditions: none

Rule: L_coord_distrib · Uses: G1, distributive

Leaf basis: coord_ops + distributive + tuple_eq + forall_intro

To raise the instance of S07 to the axiom, the law must be proved for an arbitrary real a and arbitrary u=(u₁,u₂,u₃), v=(v₁,v₂,v₃). The proof is in sub-steps S08.1 to S08.3 (Lemma L_coord_distrib): the vector equation reduces to three real distributive laws.



S09 · equivalentBefore

(a+b)u

After

(-1)(1,-2,3)=(-1,2,-3)

Conditions: none

Rule: coord_ops · Uses: G2

Leaf basis: coord_ops + numeric_evaluation

First compute a+b=2+(−3)=−1 in the reals (this + is real addition), then scale: (−1)·(1,−2,3)=(−1,2,−3).



S10 · impliesBefore

au+bu

After

(2,-4,6)+(-3,6,-9)=(-1,2,-3)=(a+b)u

Conditions: none

Rule: coord_ops · Uses: S05, S09

Leaf basis: coord_ops + tuple_eq + numeric_evaluation

bu=(−3)·(1,−2,3)=(−3,6,−9). Here + is vector addition, componentwise: (2−3, −4+6, 6−9)=(−1,2,−3), the same as S09, so the instance (a+b)u=au+bu holds.



S11 · impliesBefore

(ab)u\ \text{and}\ a(bu)

After

(-6)(1,-2,3)=(-6,12,-18)=2(-3,6,-9)

Conditions: none

Rule: coord_ops · Uses: G2

Leaf basis: coord_ops + mul_assoc + numeric_evaluation

ab=2·(−3)=−6, so (ab)u=(−6,12,−18); bu=(−3,6,−9) and a(bu)=2·(−3,6,−9)=(−6,12,−18). They agree, so the instance of the compatibility law holds.



S12 · impliesBefore

1u,\ u+(-u)

After

1u=(1,-2,3)=u,\ u+(-u)=(0,0,0)

Conditions: none

Rule: coord_ops · Uses: G1, G2

Leaf basis: coord_ops + mul_one + add_inverse

1·(1,−2,3)=(1,−2,3)=u; −u=(−1,2,−3) and u+(−u)=(1−1, −2+2, 3−3)=(0,0,0), the zero vector.



S13 · impliesBefore

(1+1)\odot(1,0)\ \text{vs}\ 1\odot(1,0)+1\odot(1,0)

After

(2,0)=(1,0)+(1,0)

Conditions: none

Rule: def_unfold · Uses: G3

Leaf basis: def_unfold + numeric_evaluation

In the comparison structure of G3, check one instance of (a+b)⊙u=a⊙u+b⊙u: a=b=1, u=(1,0). Left: 2⊙(1,0)=(2·1, 0)=(2,0); right: 1⊙(1,0)+1⊙(1,0)=(1,0)+(1,0)=(2,0). The instance passes.



S14 · impliesBefore

(1+1)\odot(0,1)\ \text{vs}\ 1\odot(0,1)+1\odot(0,1)

After

(0,1)\neq(0,2)

Conditions: none

Rule: tuple_eq · Uses: G3

Leaf basis: def_unfold + tuple_eq + numeric_evaluation

Take u=(0,1): left 2⊙(0,1)=(2·0, 1)=(0,1); right (0,1)+(0,1)=(0,2). The second components differ, 1≠2, so the vectors differ and the axiom fails here.



S15 · impliesBefore

\exists a,b,u:\ (a+b)\odot u\neq a\odot u+b\odot u

After

(\mathbb{R}^2,+,\odot)\ \text{is not a real vector space}

Conditions: none

Rule: quantifier_negation · Uses: S08, S13, S14

Leaf basis: quantifier_negation + mko_rvs_def

The axiom (a+b)u=au+bu is a universal statement over all scalars and all vectors. S14 gives a counterexample, so by quantifier negation the universal statement is false and the comparison structure is not a real vector space, even though the instance in S13 passed. By contrast, a(u+v)=au+av in ℝ³ was proved for all elements in S08; the other checks in S07 and S10 to S12 are instances only.







## Substeps and lemmas

S08.1 · equivalentBefore

a(u+v)

After

(a(u_1+v_1),\,a(u_2+v_2),\,a(u_3+v_3))

Conditions: none

Rule: coord_ops · Uses: G1, coord_ops

Leaf basis: coord_ops + def_unfold

Take an arbitrary real a and arbitrary u, v∈ℝ³, with no extra assumption on them. Unfold the addition u+v=(u₁+v₁, u₂+v₂, u₃+v₃), then the scalar multiplication, multiplying each component by a.



S08.2 · equivalentBefore

(a(u_1+v_1),\,a(u_2+v_2),\,a(u_3+v_3))

After

(au_1+av_1,\,au_2+av_2,\,au_3+av_3)

Conditions: none

Rule: distributive · Uses: S08.1, distributive

Leaf basis: distributive + tuple_eq

Each component is a real number; apply the real distributive law a(u_k+v_k)=au_k+av_k to the k-th component (k=1,2,3). This is the only substantive move of the proof: the vector distributive law comes from the real one.



S08.3 · equivalentBefore

(au_1+av_1,\,au_2+av_2,\,au_3+av_3)

After

au+av

Conditions: none

Rule: coord_ops · Uses: S08.2, coord_ops, forall_intro

Leaf basis: coord_ops + def_unfold + forall_intro

Fold the definitions back: au=(au₁,au₂,au₃) and av=(av₁,av₂,av₃), and their componentwise sum is exactly the left-hand tuple. Since a, u, v were arbitrary, ∀-introduction gives a(u+v)=au+av for every real a and all u, v∈ℝ³. S08.1 to S08.3 together prove Lemma L_coord_distrib.







## Reverse audits


- S15 · sufficient_goal_reduction · S08, S14, quantifier_negation — Goal G: the comparison structure is not a vector space. Sufficient condition H: some axiom has a counterexample (H⇒G by the definition and quantifier negation). H is obtained by direct computation in S14; G is never used as a premise.
- S14 · premise_audit · G3, tuple_eq, numeric_evaluation — One differing component suffices for the vectors to differ; no converse is claimed.
- S13 · premise_audit · G3, def_unfold, numeric_evaluation — Only one vector u is checked, and its second component is 0, so the anomaly of ⊙ in the second component is invisible here.
- S12 · premise_audit · coord_ops, mul_one, add_inverse — The two instances come componentwise from the real facts 1·x=x and x+(−x)=0; the step checks the single vector u only.
- S11 · premise_audit · coord_ops, mul_assoc, numeric_evaluation — Each component is (ab)u_k=a(bu_k), an instance of associativity of real multiplication; the step checks these data only.
- S10 · premise_audit · S05, S09, tuple_eq, numeric_evaluation — Only this a, b, u is claimed. The + on the left is real addition and the + on the right is vector addition; they differ, and this axiom is exactly what links them.
- S09 · inverse_equivalence · coord_ops, neg_mul — Backward: multiplying by −1 again returns u, since (−1)(−1)=1.
- S08.3 · inverse_equivalence · coord_ops, forall_intro — Folding and unfolding definitions undo each other; ∀-introduction only requires that a, u, v were not given special values, and the proof gave them none.
- S08.2 · inverse_equivalence · distributive, tuple_eq — Each component is rewritten by an equation and tuples are equal componentwise, so the step is two-way.
- S08.1 · inverse_equivalence · coord_ops, def_unfold — This only unfolds definitions; folding them back returns a(u+v), so the step is two-way.
- S08 · premise_audit · L_coord_distrib — The lemma is proved in the sub-steps for arbitrary elements without using the numbers of S07; S07 is one special case of the general conclusion, and the general conclusion cannot be inferred from S07.
- S07 · premise_audit · S04, S06, eq_refl_symm_trans, tuple_eq — All three components must agree; the step claims the equation only for this a, u, v, not for all vectors.
- S06 · inverse_equivalence · coord_ops, numeric_evaluation — Backward: (10,−4,4)−av=(10−8, −4−0, 4+2)=(2,−4,6)=au.
- S05 · inverse_equivalence · coord_ops, mul_inverse_nonzero, two_nonzero — As in S04, multiplying by 1/2 restores u and v, so the step is two-way.
- S04 · inverse_equivalence · coord_ops, mul_inverse_nonzero, two_nonzero — Backward: since 2≠0, multiplying by 1/2 returns (5,−2,2); both sides name the same vector.
- S03 · inverse_equivalence · coord_ops, numeric_evaluation — Backward: (5,−2,2)+(−v)=(5−4, −2−0, 2+1)=(1,−2,3)=u, which restores u+v=(5,−2,2).
- S02 · premise_audit · G1, coord_ops — What is needed is equal dimension; the step does not claim that any two tuples can be added.
- S01 · premise_audit · G1, mko_rvs_def, vector_space_axioms — This step only lists the axioms to audit and derives no new fact. Each axiom is a statement quantified over all elements, which S08 and S15 will use.





## Error controls and negative controls

Vectors of different dimensions cannot be addedOne mistake the MKO names is adding vectors of different dimensions directly. (1,2)+(1,2,3) is undefined in the model; padding (1,2) to (1,2,0) first is an extra convention, not vector addition in ℝⁿ. S02 must confirm equal dimensions first.

A few examples do not prove an axiomAnother mistake identified in the MKO is passing off a few examples as a proof of a general axiom. The instance in S13 passes, but S14 fails on another vector; so the instances in S07 and S10 to S12 cannot replace a proof either. The only statement proved here for all elements is S08, which reduces the vector equation to the real distributive law for arbitrary components.

Keep the two additions apartIn (a+b)u the + is real addition; in au+bu it is vector addition. S09 computes a+b=−1 in the reals before scaling, while S10 adds vectors componentwise; confusing them removes the distinction the check is meant to test.


- (1,2)+(1,2,3)=(2,4,3) → reject — The vectors have different dimensions (2 and 3), so vector addition is undefined; padding with zeros is an extra convention.
- Since a(u+v)=au+av holds for a=2, u=(1,−2,3), v=(4,0,−1), the distributive law is proved for ℝ³ → reject — One instance supports only those data; the general proof is done separately in S08 for arbitrary a, u, v.
- (ℝ², +, ⊙) with a⊙(x,y)=(ax,y) is a vector space, because 1⊙u=u and (ab)⊙u=a⊙(b⊙u) hold for all u → reject — (a+b)⊙u=a⊙u+b⊙u fails at a=b=1, u=(0,1): (0,1)≠(0,2).
- 2(5,−2,2)=(10,−2,2) → reject — Scalar multiplication scales every component; the correct result is (10,−4,4).





## Result and limitations

In ℝ³, u and v have the same dimension and can be added; a(u+v)=au+av=(10,−4,4), (a+b)u=au+bu=(−1,2,−3), (ab)u=a(bu)=(−6,12,−18), 1u=u and u+(−u)=(0,0,0): all five instances hold exactly. Of these, a(u+v)=au+av is proved for every real a and all u, v∈ℝ³. The comparison structure (ℝ², +, ⊙) passes (a+b)⊙u=a⊙u+b⊙u at u=(1,0) but fails at u=(0,1), so it is not a real vector space: successful instances do not establish an axiom.


- Only a(u+v)=au+av is proved generally for ℝ³ here. The five concrete instances checked are a(u+v)=au+av, (a+b)u=au+bu, (ab)u=a(bu), 1u=u and u+(−u)=0. Associativity, commutativity and the additive zero-vector law are not separately checked as axiom instances here. The other general axiom proofs are also unwritten, although they can be reduced componentwise to properties of the reals.
- N6 is a polynomial-identity check on a grid matching the real distributive law of S08.2; it is a cross-check, and the proof in S08 does not depend on it.





## Verification and source binding

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: b6ac042765621bf0059bdacec69bbd5ab8eea063304339c44a944552c9a7b347
- original source SHA-256: 04c133c4b49ec86f0f5dcac73a472cdc65fcde21915a34e8bd8506fbe9184960
- 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-real-vector-space-01.json)