Finite Identification Capacity Bound

Abstract

Injective joint readout bounds a finite state space by the capacity of its dependent outcome space, equivalently by its base-two logarithmic cost at positive capacity.

Theorem 1.1 (Injective joint readout bounds state cardinality).

$$\begin{array}{r}\forall X,J:\mathrm{Type},O:J\to \mathrm{Type},\\ qJ:X\to \prod _{j:J}{O}_j,\\ \mathrm{Finite}\left(X\right)\wedge \mathrm{Fintype}\left(J\right)\wedge (\forall j:J,\mathrm{Fintype}\left(O_j\right))\wedge \mathrm{Injective}\left(qJ\right)\Rightarrow \mathrm{card}\left(X\right)\le \mathrm{Cap}\left(O\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Experiment/FiniteIdentificationCapacityBound.finite_identification_capacity_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite experiment family, capacity is the number of dependent joint outcome tuples, with one outcome chosen from each indexed outcome type.

An injective joint readout assigns different tuples to different states. The finite state space therefore embeds in the joint-outcome space, so its cardinality cannot exceed the experiment capacity.

Lemma 1.2 (The capacity bound implies the base-two cost bound).

$$\begin{array}{r}\forall X,J:\mathrm{Type},O:J\to \mathrm{Type},\\ qJ:X\to \prod _{j:J}{O}_j,\\ \mathrm{Finite}\left(X\right)\wedge \mathrm{Fintype}\left(J\right)\wedge (\forall j:J,\mathrm{Fintype}\left(O_j\right))\wedge 0<\mathrm{Cap}\left(O\right)\wedge \mathrm{Injective}\left(qJ\right)\Rightarrow \mathrm{logb}\left(2,\mathrm{card}\left(X\right)\right)\le \mathrm{Cost}\left(O\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Experiment/FiniteIdentificationCapacityBound.cost_form (✓ std3). ∎

Source. Repository-derived.

Commentary.

When capacity is positive, the injective readout first gives the finite cardinality bound. Taking logarithms to base two preserves that order, and the logarithm of capacity is exactly the defined cost.

If the state cardinality is zero, its base-two logarithm is zero and the positive capacity has nonnegative cost. Otherwise both cardinalities are positive, so ordinary logarithmic monotonicity applies directly.

Lemma 1.3 (Positive capacity equates cardinal and cost bounds).

$$\begin{array}{r}\forall X,J:\mathrm{Type},O:J\to \mathrm{Type},\\ \mathrm{Finite}\left(X\right)\wedge \mathrm{Fintype}\left(J\right)\wedge (\forall j:J,\mathrm{Fintype}\left(O_j\right))\wedge 0<\mathrm{Cap}\left(O\right)\Rightarrow \\ (\mathrm{card}\left(X\right)\le \mathrm{Cap}\left(O\right)⟺\mathrm{logb}\left(2,\mathrm{card}\left(X\right)\right)\le \mathrm{Cost}\left(O\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Experiment/FiniteIdentificationCapacityBound.cardinal_bound_iff_cost_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

At positive capacity, bounding the number of states by the joint-readout capacity is equivalent to bounding its base-two logarithm by the identification cost.

The forward implication is monotonicity of the base-two logarithm. For a nonempty finite state space, strict increase of that logarithm also reflects the cost inequality back to the cardinal inequality; the zero-cardinality case satisfies the cardinal bound automatically.

References

• Truth anchor: D5/S3/ConceptDynamics/Experiment/FiniteIdentificationCapacityBound.cardinal_bound_iff_cost_bound
• Truth anchor: D5/S3/ConceptDynamics/Experiment/FiniteIdentificationCapacityBound.cost_form
• Truth anchor: D5/S3/ConceptDynamics/Experiment/FiniteIdentificationCapacityBound.finite_identification_capacity_bound