Finite Realization Certificate

Abstract

Every unrealizable real protocol signature has a finite strict linear certificate.

Theorem 1.1 (Unrealizable signatures have finite linear witnesses).

$$\begin{array}{r}\forall State,Protocol:\mathrm{Type},\\ [\mathrm{TopologicalSpace}(State)],[\mathrm{AddCommGroup}(State)],[\mathrm{Module}(\mathbb{R},State)],\\ \forall X:\mathrm{Set}(State),\\ \mathrm{IsCompact}(X)\wedge \mathrm{Convex}(\mathbb{R},X),\\ \forall e:Protocol\to \mathrm{ContinuousAffineMap}(\mathbb{R},State,\mathbb{R}),y:Protocol\to \mathbb{R},\\ letSigma:State\to Protocol\to \mathbb{R}=\mathrm{jointReadout}(e);\\ \neg (y\in \mathrm{image}(Sigma,X))\Rightarrow \\ \exists S:\mathrm{Finset}(Protocol),\exists c:Protocol\to \mathbb{R},\\ \mathrm{withBotCoe}(\sum _{p\in S}\mathrm{apply}(c,p)\cdot \mathrm{apply}(y,p))>{\mathrm{supWithBot}}_{x\in X}\mathrm{withBotCoe}(\sum _{p\in S}\mathrm{apply}(c,p)\cdot \mathrm{apply}(e,p,x)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Residuals/FiniteRealizationCertificate.finite_realization_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

A compact convex state set and its continuous affine real readouts construct the realization image through the canonical joint readout.

Strict separation produces a continuous linear functional on the product signature space. Continuity at zero forces that functional to depend on only finitely many protocol coordinates.

The displayed lower-completion coercions make the supremum equal negative infinity when the state set is empty. For every nonempty state set, they reduce to the ordinary attained real supremum.

References

• Truth anchor: D5/S3/Observer/Residuals/FiniteRealizationCertificate.finite_realization_certificate
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion