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

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

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

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

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

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

u+v

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

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

(10,-4,4)

au,\ av

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

au+av

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

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

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

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

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

(a+b)u

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

au+bu

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

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

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

1u,\ u+(-u)

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

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

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

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

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

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

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

Substeps and lemmas

a(u+v)

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

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

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

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

au+av

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 added

One 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 axiom

Another 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 apart

In (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)