Finite Identification Output Capacity

Abstract

A separating finite protocol family obeys effective-output capacity bounds.

Theorem 1.1 (Effective outputs bound finite identification capacity).

$$\forall X\in Type,P\in Type,O\in P\to Type,c\in \prod _{p:P}X\to O\left(p\right),\left(\mathrm{Finite}\left(X\right)\wedge \left(\mathrm{Nonempty}\left(X\right)\wedge \left(\mathrm{Fintype}\left(P\right)\wedge \mathrm{Injective}\left(\mathrm{jointReadout}\left(c\right)\right)\right)\right)\right)\Rightarrow \left(\mathrm{card}\left(X\right)\le \prod _{p\in P}\mathrm{card}\left(\mathrm{range}\left(c\left(p\right)\right)\right)\wedge \left({\log }_2\left(\mathrm{card}\left(X\right)\right)\le \sum _{p\in P}{\log }_2\left(\mathrm{card}\left(\mathrm{range}\left(c\left(p\right)\right)\right)\right)\wedge \left(\forall m\in \mathbb{N},\left(1<m\wedge \left(\forall p\in P,\mathrm{card}\left(\mathrm{range}\left(c\left(p\right)\right)\right)\le m\right)\right)\Rightarrow \mathrm{natCeil}\left({\log }_m\left(\mathrm{card}\left(X\right)\right)\right)\le \mathrm{card}\left(P\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ExperimentBoundary/FiniteIdentificationOutputCapacity.finite_identification_output_capacity (✓ std3). ∎

Source. Repository-derived.

Commentary.

The state-class carrier is finite and nonempty, the protocol carrier is a finite type, and each protocol may have its own output type. The canonical jointReadout map is required to be injective.

Each effective output count is the cardinality of the actual range of that protocol on the state classes. The displayed formula expands both Lean let-bindings rather than introducing alternate objects.

The three public conclusions are the product capacity bound, its base-two logarithmic form, and the uniform-output lower bound for every natural base strictly greater than one.

References

• Truth anchor: D5/S3/ConceptDynamics/ExperimentBoundary/FiniteIdentificationOutputCapacity.finite_identification_output_capacity
• Dependency: D5/S3/ConceptDynamics/Experiment/FiniteIdentificationCapacityBound
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion