Minimal Appeal Label Count

Abstract

Maximum target diversity in a record fiber is the exact appeal label count.

Theorem 1.1 (Fiber diversity gives the exact number of appeal labels).

$$\begin{array}{c}\forall X,B,Y:Type,\\ [\mathrm{Fintype}(X)],[\mathrm{Fintype}(B)],\\ r:X\to B,t:X\to Y,\\ (\exists el{l}_{exact}:X\to \mathrm{Fin}(\mathrm{worstFiberDiversity}(r,t)),\mathrm{AppealDetermines}(r,t,el{l}_{exact}))\wedge \\ (\forall m:\mathbb{N},el{l}_{candidate}:X\to \mathrm{Fin}(m),\\ \mathrm{AppealDetermines}(r,t,el{l}_{candidate})\Rightarrow \mathrm{worstFiberDiversity}(r,t)\le m).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Appeal/MinimalAppealLabelCount.minimal_appeal_label_count (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let d be the largest number of distinct target outcomes realized in any one record fiber. The state and record carriers are finite, while the target carrier itself need not be finite.

There is a label with d possible values that makes the target exact once the original record is fixed. It is obtained by indexing the realized target outcomes inside each fiber, and the same labels may be reused in different fibers.

Conversely, any exact label with m possible values is injective on one representative of each realized target outcome in every fiber. Each fiber therefore has at most m target outcomes, so d is at most m. Together the two directions make d the exact minimum.

References

• Truth anchor: D5/S3/ConceptDynamics/Appeal/MinimalAppealLabelCount.minimal_appeal_label_count
• Dependency: D5/S3/ConceptDynamics/Coding/FiberBinaryIdentification