Entropy representation for finite separated products

Construct the represented-state interpretation of [A7] directly: give each primitive label its unit amount function and each scaled or joined type its aggregate amount function; a raw coefficient $a$ at $(\mathrm{\Gamma },x)$ denotes the preparation $(a\mathrm{/}{w}_{\mathrm{\Gamma }})x$. Finite sums denote separated preparations, and their mass and composition are the sums of these factor amounts. Pull back the common endpoint relation through this interpretation. The full-domain scaling and coherent transport in [A5], with A1–A6 and reversible splitting, supply the exact scaling and product conventions in [A7]; this construction is not an additional conclusion attributed to a pairwise comparison theorem. Every finite list of simple types has finitely many primitive generators, so the Statement's assumption supplies the complete contact branch on their join closure. Consequently [A2] applies to every pair, including a repeated primitive type, and [A3]'s whole-family hypotheses hold: each chart, pair, or finite comparison lies in one such closure with the same relation.

Since $I$ is nonempty, choose a primitive meter label $m$. Apply [A2] on the closure generated by $\{m\}$ to obtain a strict meter pair $z_0\prec \prec z_1$. For each $j\mathrm{\ne }m$, use the closure generated by $\{j,m\}$ to obtain $a_j\prec \prec b_j$ and $c_j\prec \prec d_j$ with $(a_j,d_j)\sim (b_j,c_j)$, the calibrator orientation required by [A3]. Choice [A1] supplies the simultaneous reference, entropy-representative and calibrator choices. Apply [A3] to the interpretation from step 1.1. It yields one entropy on separated primitive products, $\tilde{S}(A)={\sum }_{\mathrm{\ell }}{t}_{\mathrm{\ell }}{S}_{i_{\mathrm{\ell }}}(x_{\mathrm{\ell }})$, representing both directions of every equal-composition comparison. Finite sums are invariant under permutation and reassociation, additive on concatenation and homogeneous under positive scaling. The empty unit has the empty sum zero; no infinite sum is introduced even when $I$ is infinite.

For a joined state, repeatedly choose the reversible split in [A6] until its finite join expression has only scaled primitive factors. Spectator consistency and transitivity make the original state equivalent to this separated primitive product, of the same aggregate composition. Define its entropy as that product's entropy from step 2.1. Two such splits are equivalent to each other, so the representation in step 2.1 makes their entropies equal; the definition is independent of all split choices. For any finite compound, concatenate these expansions. Scaling an expansion gives a reversible expansion of the scaled state by the accessibility scaling axiom in [A6] and the coherent transport in [A5], so this extension is extensive as well as additive. If $A,B$ have the same composition, their expansions $A^{\mathrm{\prime }},B^{\mathrm{\prime }}$ do also; reversibility and transitivity give $A\prec B$ exactly when $A^{\mathrm{\prime }}\prec B^{\mathrm{\prime }}$, hence exactly when $\tilde{S}(A)\le \tilde{S}(B)$. This extends the same representation to every finite joined or separated state without identifying distinct raw tags.

Let $x,y$ lie in one simple chart and $0<t<1$. By [A4], the scaled pair $(tx,(1-t)y)$ compares to the recombined state $tx+(1-t)y$. Step 3.1's representation, additivity and extensivity give $t\tilde{S}(x)+(1-t)\tilde{S}(y)\le \tilde{S}(tx+(1-t)y)\mathrm{.}$ This is concavity on the admitted convex chart; at $t=0,1$ the inequality is equality.