The cost-zero offset construction is a real vector space

The relation ${\approx }_0$ is reflexive because $F(\mathrm{\Gamma },\mathrm{\Gamma })=0$, and symmetric by definition. Suppose $\mathrm{\Gamma }{\approx }_0{\mathrm{\Gamma }}^{\mathrm{\prime }}$ and ${\mathrm{\Gamma }}^{\mathrm{\prime }}{\approx }_0{\mathrm{\Gamma }}^{\mathrm{\prime }\mathrm{\prime }}$. The triangle inequality gives both directed costs between $\mathrm{\Gamma }$ and ${\mathrm{\Gamma }}^{\mathrm{\prime }\mathrm{\prime }}$ at most zero. For any $ϵ>0$, choose a finite reverse witness of cost $d<ϵ$; such a witness exists because the reverse infimum is at most zero; a value below $ϵ$ must exist by the greatest-lower-bound convention, even if that infimum were initially $-\mathrm{\infty }$. Every forward witness of cost $c$ closes with it, so [F2] gives $c+d\ge 0$, hence $c>-ϵ$. Letting $ϵ\downarrow 0$ shows every forward witness has nonnegative cost and its infimum is at least zero; the same argument reverses the direction. Both infima are therefore zero, proving transitivity. The same argument proves product compatibility: subadditivity makes both product costs at most zero, and any finite reverse witness bounds every forward product witness below by a quantity tending to zero. Positive homogeneity gives scaling compatibility directly. Thus ${\approx }_0$ is an equivalence compatible with product and positive scaling, and the quotient is a commutative monoid.

Reversible splitting [A1] gives accessible transitions in both directions between $(s+t)\mathrm{\Gamma }$ and $s\mathrm{\Gamma }\times t\mathrm{\Gamma }$. Extensivity makes each such edge have zero entropy cost. Any reverse witness bounds all forward costs below by [F2]'s closed-cycle inequality, so both infima are zero. Hence $(s+t)\mathrm{\Gamma }{\approx }_{0}s\mathrm{\Gamma }\times t\mathrm{\Gamma }$. The empty type $1$ is an identity under composition; its reassociation and permutation identifications have zero cost by the type conventions.

The pair relation $\equiv$ is reflexive using unit catalyst $1$ and symmetric by swapping the two sides. Suppose $(A,B)\equiv (A^{\mathrm{\prime }},B^{\mathrm{\prime }})$ via catalyst $C$, and $(A^{\mathrm{\prime }},B^{\mathrm{\prime }})\equiv (A^{\mathrm{\prime }\mathrm{\prime }},B^{\mathrm{\prime }\mathrm{\prime }})$ via catalyst $D$. Their witnesses are $A\times B^{\mathrm{\prime }}\times C{\approx }_0{A}^{\mathrm{\prime }}\times B\times C,A^{\mathrm{\prime }}\times B^{\mathrm{\prime }\mathrm{\prime }}\times D{\approx }_0{A}^{\mathrm{\prime }\mathrm{\prime }}\times B^{\mathrm{\prime }}\times D\mathrm{.}$ Multiply the first equivalence by $B^{\mathrm{\prime }\mathrm{\prime }}\times D$, the second by $B\times C$, and compose. Reassociating and permuting gives $A\times B^{\mathrm{\prime }\mathrm{\prime }}\times (B^{\mathrm{\prime }}\times C\times D){\approx }_0{A}^{\mathrm{\prime }\mathrm{\prime }}\times B\times (B^{\mathrm{\prime }}\times C\times D),$ which witnesses $(A,B)\equiv (A^{\mathrm{\prime }\mathrm{\prime }},B^{\mathrm{\prime }\mathrm{\prime }})$. Hence $\equiv$ is an equivalence relation.

Suppose $(A,B)\equiv (A^{\mathrm{\prime }},B^{\mathrm{\prime }})$ via $C$, so $A\times B^{\mathrm{\prime }}\times C{\approx }_0{A}^{\mathrm{\prime }}\times B\times C$. For an arbitrary pair $(D,E)$, multiply this witness by $D\times E$. Reassociation gives $(A\times D)\times (B^{\mathrm{\prime }}\times E)\times C{\approx }_0(A^{\mathrm{\prime }}\times D)\times (B\times E)\times C$, exactly the witness for $(A\times D,B\times E)\equiv (A^{\mathrm{\prime }}\times D,B^{\mathrm{\prime }}\times E)$. Apply the same argument to a change of representative of $(D,E)$ and use transitivity; addition is representative-independent. Scaling a catalyst witness by $t>0$ and using product compatibility from step 1.1 proves that positive scalar multiplication is representative-independent. Product commutativity and associativity give the additive laws, and the empty type gives $(A\times 1,B\times 1)=(A,B)$. Swapping a pair gives an inverse: its sum with $(A,B)$ is $(A\times B,B\times A)$, equivalent to $(1,1)$ with unit catalyst because the two product types agree up to permutation and have zero cost in both directions. Thus the classes form an abelian group with zero $[(1,1)]$.

For $t>0$, the displayed operation $t(A,B)=(tA,tB)$ satisfies $t(v+w)=tv+tw$ because scaling distributes over type composition, and $t(sv)=(ts)v$ for $s>0$ by associativity of type scaling. Also $1v=v$. The scalar-addition law for positive $s,t$ follows from step 1.2: $(s+t)[A,B]=[(s+t)A,(s+t)B]=[sA\times tA,sB\times tB]=s[A,B]+t[A,B]\mathrm{.}$ The zero scalar is defined as the additive identity, and $(-t)v$ is defined as $t(-v)$, where $-v$ swaps the pair.

The positive scalar laws extend to negative scalars by swapping pairs. For the scalar-addition law with opposite signs, write $s-t$ with $s,t\ge 0$. If $s\ge t$, positive scalar addition gives $sv=(s-t)v+tv$, so cancellation in the additive group gives $(s-t)v=sv-tv$; if $t>s$, apply the same identity to $t=(t-s)+s$ and negate. Cases with zero are immediate. For scalar composition, write each nonzero scalar as its sign times a positive magnitude; the defined action swaps the pair once for each negative sign and scales by the product of magnitudes, so $(rs)v=r(sv)$, with zero cases immediate. For distributivity over vector addition, positive scalars distribute by step 4.1 and a negative scalar distributes by taking the additive inverse of that identity. Together with the abelian-group laws in step 3.1, these are all real-vector-space axioms.