Type-offset quotient vector space

Let $\mathcal{G}$ be a set of formal type labels closed under the formal operations $(\mathrm{\Gamma },{\mathrm{\Gamma }}^{\mathrm{\prime }})\mapsto \mathrm{\Gamma }\times {\mathrm{\Gamma }}^{\mathrm{\prime }}$ and $(t,\mathrm{\Gamma })\mapsto t\mathrm{\Gamma }$ for every real $t>0$. Let $F:={\mathbb{R}}^{(\mathcal{G})}$ be the vector space of finite-support real functions on $\mathcal{G}$, and let $e_{\mathrm{\Gamma }}$ be the function equal to $1$ at $\mathrm{\Gamma }$ and $0$ elsewhere.

Form the set of relation vectors

$\mathcal{R}:=\{e_{\mathrm{\Gamma }\times {\mathrm{\Gamma }}^{\mathrm{\prime }}}-e_{\mathrm{\Gamma }}-e_{{\mathrm{\Gamma }}^{\mathrm{\prime }}}:\mathrm{\Gamma },{\mathrm{\Gamma }}^{\mathrm{\prime }}\in \mathcal{G}\}\cup \{e_{t\mathrm{\Gamma }}-t{e}_{\mathrm{\Gamma }}:t>0,\mathrm{\Gamma }\in \mathcal{G}\}\mathrm{.}$

Following Linear combination of a finite list, and the span $\mathrm{span}(S)$ as the smallest linear subspace containing $S$, let $N$ consist of exactly the vectors ${\sum }_{i<n}{a}_i{r}_i$ for $n\in \mathbb{N}$, scalar lists $a:n\to \mathbb{R}$ and vector lists $r:n\to \mathcal{R}$. The sum is computed in the additive group of $F$, starting with $s_0=0$ and recursively setting $s_{i+1}=s_i+a_i{r}_i$ for $i<n$; its value is $s_n$. In particular, the empty list contributes $0\in N$. Define the type-offset vector space

$V_{\mathcal{G}}:=F\mathrm{/}N\mathrm{.}$

The class of $c\in F$ is $[c]$. The defining relations are $[e_{\mathrm{\Gamma }\times {\mathrm{\Gamma }}^{\mathrm{\prime }}}]=[e_{\mathrm{\Gamma }}]+[e_{{\mathrm{\Gamma }}^{\mathrm{\prime }}}]$ and $[e_{t\mathrm{\Gamma }}]=t[e_{\mathrm{\Gamma }}]$. The set existence, subspace properties, quotient operations and vector-space laws are proved in Type-offset quotient is a real vector space ↗. These are formal algebraic type labels; no actual catalyst-chain cost or physical existence claim is built into $V_{\mathcal{G}}$.