Adaptive Binary Protocol Depth Lower Bound

Abstract

Identifying a target by adaptive binary questions requires logarithmic fiber depth.

Theorem 1.1 (Binary identification depth is bounded below by fiber diversity).

$$\begin{array}{c}\forall X,C,Target:\mathrm{Type},\\ [\mathrm{Fintype}(X)],[\mathrm{Fintype}(C)],\\ c:\mathrm{Concept}(X,C),t:\mathrm{Concept}(X,Target),\\ d:\mathbb{N},pi:\mathrm{BinaryProtocol}(X,d),\\ identifies:\mathrm{IdentifiesGiven}(c,t,pi),\\ \mathrm{clog}(2,\mathrm{worstFiberDiversity}(c,t))\le d.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/BinaryProtocolDepthLowerBound.adaptive_binary_protocol_depth_lower_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The current concept partitions the finite state carrier into fibers. Worst fiber diversity is the greatest number of distinct target values realized inside any one of those fibers.

A depth-d adaptive binary protocol records one bit per round. It identifies the target when equal current records and equal full transcripts force equal target values.

Reading every transcript bit as a fixed-width auxiliary label makes that label target-determining. The least-label theorem then forces d to be at least the ceiling logarithm to base two of worst fiber diversity.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/BinaryProtocolDepthLowerBound.adaptive_binary_protocol_depth_lower_bound
• Dependency: D5/S3/ConceptDynamics/Coding/BinaryRepairCost