# Dual basis and covector change

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-dual-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-dual-vector-space-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

For b1=(1,1),b2=(1,-1), phi1=(x+y)/2,phi2=(x-y)/2 form the dual basis.

Explicit R2 functionals, universal linearity and four pairings; no canonical identification without extra structure.





## Givens and symbols


- calc


- G1 — V=R2, B=((1,1),(1,-1)), P=[[1,1],[1,-1]] is the basis-column matrix.


- V^* — real linear dual
- \phi_i — dual-basis functional
- P — primal basis columns





## 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 uses finite-dimensional V=R^n. A row covector gives a symbolic linearity certificate, and a dual basis is checked by phi_i(v_j)=delta_ij. A primal vector and a dual functional are distinct; without extra structure no canonical identification V→V* is claimed. · mko-dual-vector-space





## Main derivation

S01 · impliesBefore

\alpha b_1+\beta b_2=(\alpha+\beta,\alpha-\beta)

After

(x,y)=\frac{x+y}{2}b_1+\frac{x-y}{2}b_2\text{ uniquely}

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

Every vector has this unique representation, qualifying B as a basis first.



S02 · impliesBefore

\phi_1(x,y)=\frac{x+y}{2},\quad\phi_2(x,y)=\frac{x-y}{2}

After

\phi_i(au+bv)=a\phi_i(u)+b\phi_i(v)\quad(i=1,2)

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Each fixed row covector is linear by distributivity for all real a,b.



S03 · impliesBefore

b_1=(1,1)

After

\phi_1(b_1)=1,\quad\phi_2(b_1)=0

Conditions: none

Rule: calc · Uses: G1, S02

Leaf basis: calc

Evaluating the first basis vector checks the first delta column.



S04 · impliesBefore

b_2=(1,-1)

After

\phi_1(b_2)=0,\quad\phi_2(b_2)=1

Conditions: none

Rule: calc · Uses: G1, S02, S03

Leaf basis: calc

Evaluating the second vector completes the four-pairing matrix I2.



S05 · impliesBefore

\ell\in V^*,\quad v=\alpha b_1+\beta b_2

After

\ell(v)=\alpha\ell(b_1)+\beta\ell(b_2)=\ell(b_1)\phi_1(v)+\ell(b_2)\phi_2(v)

Conditions: none

Rule: calc · Uses: G1, S01, S02, S03, S04

Leaf basis: calc

An arbitrary linear functional is determined by its basis values, so the two phi functionals span V*.



S06 · impliesBefore

a\phi_1+b\phi_2=0\text{ as functions}

After

\text{evaluate at }b_1,b_2:\quad a=b=0

Conditions: none

Rule: mko_definition · Uses: G1, S03, S04, S05

Leaf basis: mko_definition

Evaluation directly proves independence, completing the dual basis with spanning.



S07 · impliesBefore

[v]_{\rm std}=P[v]_B

After

[v]_B=P^{-1}[v]_{\rm std},\quad P^{-1}=\frac12\begin{pmatrix}1&1\\1&-1\end{pmatrix}

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Primal coordinates use the inverse; P^2=2I exactly verifies it.



S08 · impliesBefore

\ell(x,y)=3x+y,\quad[\ell]_{\rm std}=(3,1)

After

[\ell]_B=(3,1)P=(4,2),\quad\ell(v)=4\alpha+2\beta

Conditions: none

Rule: calc · Uses: G1, S01, S07

Leaf basis: calc

The covector row multiplies P rather than P inverse, opposite to primal coordinate change.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S01, S07 — Substitution x=alpha+beta,y=alpha-beta gives 4alpha+2beta, checking the same functional.
- S07 · premise_audit · G1, S01 — P and P inverse cannot be interchanged even though they differ by a scalar here.
- S06 · premise_audit · G1, S03, S04, S05 — The zero functional vanishes on all inputs, so in particular on both basis vectors.
- S05 · premise_audit · G1, S01, S02, S03, S04 — Ell is arbitrary, not a few sampled functions.
- S04 · premise_audit · G1, S02, S03 — phi2(b2)=(1-(-1))/2=1, with the minus sign retained.
- S03 · premise_audit · G1, S02 — (1-1)/2 is zero; both entries cannot be one.
- S02 · premise_audit · G1, S01 — phi_i returns a real number; a functional is not a primal vector.
- S01 · premise_audit · G1 — Division by 2 is valid; the dual basis being constructed is not used to qualify B.





## Error controls and negative controls

Four pairingsCheck all delta_ij pairings, not only diagonal entries.

TypesV* is a function space, and row coordinates require a chosen basis.


- b1 and phi1 are canonically the same object. → reject — One is a vector, the other a function V to R.
- phi1(b2)=1. → reject — (1+(-1))/2=0.
- Covectors also multiply P inverse. → reject — Here ell's B-values are (4,2), not (2,1).





## Result and limitations

For b1=(1,1),b2=(1,-1), phi1=(x+y)/2,phi2=(x-y)/2 form the dual basis.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 284271845add69df42d2cff4d06bc73a7247e856826b15e73926becaccedbd91
- original source SHA-256: 284271845add69df42d2cff4d06bc73a7247e856826b15e73926becaccedbd91
- 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-dual-vector-space-01.json)