Theorem: Conditional operational Lorentz-cone assembly

Suppose the objects and certificates of Specification spec:certificates are supplied. Then, for every $D\in \mathcal{A}$, there is an invertible linear map

The represented comparisons satisfy

The representation spans its affine carrier, is generated as in (eq:generated), and is matched-affine-covariant.

The full cone determines the class, up to positive multiplication, of the Lorentzian quadratic form

Under (eq:affine-covariance),

Nonemptiness is inherited from (K1), not proved by classification. If homogeneity and strict convexity are assumed rather than operationally derived, the conclusion retains precisely that conditional status. No transport, calibration, metric field, or dynamics conclusion is included.

Proof. By (K2), $K_D$ is a proper cone in a space of dimension $m\ge 3$. By (K3), it is homogeneous and strictly convex. Ito and Lourenço's Theorem 7 classifies such cones: the lower-dimensional alternatives are excluded, leaving a Lorentz cone ItoLourenco (Theorem 7). This gives (eq:lorentz). Applying its linear bijection to the faithfulness equation proves (eq:lorentz-order). Spanning and generation are the supplied (K2) identities.

For covariance, comparable differences in $D^{\prime }$ are exactly the images under $A_f$ of those in $D$. An invertible linear map commutes with conical generation and closure, so

The marked embeddings are matched by (K4).

To prove quadratic uniqueness, work in Lorentz coordinates and write another quadratic form vanishing on the same nonzero null boundary as

Its vanishing on $(1,u)$ and $(1,-u)$ for all unit $u$ gives $b=0$ and $u^{\mathsf{T}}Cu=-a$. Thus $C=-aI$. Positivity on the future interior gives $a>0$. This proves the uniqueness in (eq:q). Apply it to $q_{D^{\prime }}\circ A_f$, whose null boundary and future interior agree with those of $q_D$, to obtain (eq:q-covariance).

The proof uses the supplied witness only to ensure the domain is nonempty. Clauses (K5)–(K6) state the scope and admission of the operational interpretation; classification does not prove them.