Your quote points out that a term can be a variable. A variable represents a value, but it is not a value itself. The same goes for compound expressions. There are distinctions between variables, values, and expressions, and these distinctions are significant. You may have a sloppy head canon that blurs all these concepts together, but that’s not how they’re treated formally.

Terms are a syntactic concept while Values are a semantic runtime concept. The key to understanding is that Values are Terms which have been reduced (i.e. evaluated) to normal form and hence cannot be reduced further. The nuance lies in the fact that while both unreduced Terms and reduced Values can have semantic meanings, only at the Value stage is it canonical and fully computed.

In fact the "Calculus of Constructions" (CoC) derived from Typed Lambda Calculus unifies everything into a Term like so;

Term ::= variable | lambda abstraction | lambda application | dependant product | sorts (type of types)

For reference see Brandl's work that i list here - https://news.ycombinator.com/item?id=50028902

Your own quote tells you why that’s wrong.

Do you seriously want to argue this point?

> you seem to have staked out the position that the compiler context is obligatory and the type theory context is somehow in error.

I used the compiler to illustrate the issue to people who clearly aren’t familiar with type theory. You imply that you are, but in that case, how do you justify the nonsense quoted above?