Solution (source code)

= Solution

For nonzero $x$, let $\phi$ be its <angle> to the <unit vector> $q_1$. The <scalar projection> on the oriented $q_1$ axis is $\|x\|\cos\phi$. Since $\|q_1\|=1$, the <dot product> identity gives $q_1^Tx=\|x\|\cos\phi$. Multiplying that signed <scalar> by $q_1$ places the foot at \b[$p=(q_1^Tx)q_1$].

The residual is perpendicular to the axis, because $q_1^T(x-p)=q_1^Tx-(q_1^Tx)(q_1^Tq_1)=0$. An obtuse <angle> gives a negative <scalar> and a foot on the negative side of the line; $x=0$ has projection zero without needing an <angle>.

\Image[/past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2019/digital-systems-linear-algebra-introduction-to-formal-proof-projection-stretch.png]
{title=Projection drops a perpendicular to a unit direction; directional stretching doubles only the parallel component}

The first panel is a constructed geometric illustration. The second illustrates the <directional stretch> used later in Question 6.