Response-Completeness Cardinality Bound

Abstract

Response completeness forces enough protocol response classes for every table.

Theorem 1.1 (Complete response columns satisfy the finite counting bound).

$$\begin{array}{c}\forall X,P,Lambda:Type,\\ \mathrm{Fintype}(X),\mathrm{Fintype}(Lambda),\\ e:X\to P\to Lambda,\\ \forall f:X\to Lambda,\exists p:P,\forall x:X,e(x,p)=f(x)\Rightarrow \\ \mathrm{card}(Lambda{)}^{\mathrm{card}(X)}\le \mathrm{card}(\mathrm{Quotient}(\ker ((p\mapsto (x\mapsto e(x,p)))))).\end{array}$$

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

Source. Repository-derived.

Commentary.

The evaluation channel sends each protocol to its complete response column on X. Response completeness makes this map surjective onto all Lambda-valued response tables.

The equality-kernel quotient is canonically equivalent to the realized range, so it has at least card(Lambda)^card(X) classes. The proof uses the kernel quotient itself rather than choosing representatives.

The source assumes card(X) at least one and card(Lambda) at least two. Neither numerical bound is needed for this counting implication, so the machine theorem also covers empty or singleton carriers.

References

• Truth anchor: D5/S3/Observer/Budget/ResponseCompletenessCardinality.response_complete_card_lower_bound
• Dependency: D5/S3/Observer/Completion/DoubleExtensionalQuotientUniversality