Finite Internal Protocol Obstruction

Abstract

Finite internal protocol indexing cannot realize every response table.

Theorem 1.1 (Finite internal protocol indexing is not response complete).

$$\begin{array}{c}\forall X,P,Lambda:\mathrm{Type},\\ [\mathrm{Fintype}X][\mathrm{Fintype}P][\mathrm{Fintype}Lambda],\\ e:X\to P\to Lambda,\\ (2\le \mathrm{card}\left(Lambda\right)\wedge \mathrm{card}\left(P\right)\le \mathrm{card}\left(X\right))\Rightarrow \\ (\mathrm{card}\left(X\right)<\mathrm{card}{\left(Lambda\right)}^{\mathrm{card}\left(X\right)})\wedge \\ \neg (\forall f:X\to Lambda,\exists p:P,\forall x:X,e\left(x,p\right)=f\left(x\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/FiniteInternalProtocolNoGo.finite_internal_protocol_no_go (✓ std3). ∎

Source. Repository-derived.

Commentary.

The evaluation channel sends each protocol to its complete response table on the state carrier. Response completeness would make this map surjective onto all Lambda-valued tables.

There are card(Lambda)^card(X) such tables. With at least two responses this is strictly larger than card(X), while internal indexing allows at most card(X) protocols, contradicting surjectivity.

The source assumes a nonempty state carrier. The machine theorem is stronger and also proves the empty-carrier case, so that premise is not needed.

References

• Truth anchor: D5/S3/Observer/Budget/FiniteInternalProtocolNoGo.finite_internal_protocol_no_go