Singleton-or-constant query capacity

Abstract

Adaptive singleton-or-constant binary questions identify at most d+1 sources at depth d.

Theorem 1.1 (Linear capacity for exact adaptive identification).

$$\begin{array}{c}\forall X:\mathrm{Type},[\mathrm{Fintype}(X)],d:\mathbb{N},p:\mathrm{BinaryProtocol}(X,d),\\ \mathrm{Injective}(T)\wedge [\forall t:\mathrm{Fin}(d),\forall h:(\mathrm{Fin}(\mathrm{val}(t))\to \mathrm{Bool}),\\ (\exists b:\mathrm{Bool},\forall x:X,q(t,h,x)=b)\vee \mathrm{card}(\{x:X\mid q(t,h,x)=\mathrm{true}\})\le 1]\\ ⟹\mathrm{card}(X)\le d+1.\end{array}$$

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

Source. Repository-derived.

Commentary.

Let X be any finite source type and let p be a BinaryProtocol of depth d. Write T for its transcript and q(t,h,x) for its question at round t, history h and source x. Transcript consistency means that the t-th bit of T(x) equals q(t,T(x) restricted to earlier rounds,x).

Assume T is injective. Every question, at every history including unrealized histories, is either constant on X or true at at most one source. Both constant false and constant true are permitted.

After t rounds, retain a set of sources sharing one transcript prefix and having size at least the size of X minus t. A constant answer keeps the entire set. For a question with at most one true source, keeping the false answers removes at most one member. Transcript consistency extends the common prefix. At depth d, injectivity leaves at most one member, giving the stated bound.

No nonemptiness or positive-depth assumption is imposed. Repeated constant YES answers are allowed; the last remaining candidate can be inferred without an additional question. The questions may depend on the complete previous history, and no prior source information is supplied.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/SingletonQueryCapacity.singleton_or_constant_query_capacity
• Dependency: D5/S3/ConceptDynamics/Coding/FiberBinaryIdentification