Adaptive Separation Depth Upper Bound

Abstract

Pair-separating readouts on a finite state quotient construct an identifying adaptive protocol tree with worst realized depth at most one less than the number of states.

Theorem 1.1 (Pair separation gives a state-count adaptive depth bound).

$$\begin{array}{r}\forall C,P,A:\mathrm{Type},\\ [\mathrm{Fintype}(C)],\\ \forall q:P\to C\to A,\\ (\forall x,y:C,x\ne y\Rightarrow \exists p:P,q(p,x)\ne q(p,y))\Rightarrow \\ \exists T:\mathrm{PassiveProtocol}(P,{(}_{:}P)\mapsto A),\mathrm{Injective}(\mathrm{runPassiveProtocol}(q,T))\wedge \\ \forall x:C,\mathrm{length}(\mathrm{runPassiveProtocol}(q,T)(x))\le \mathrm{card}(C)-1.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/AdaptiveSeparationDepthUpperBound.adaptive_separation_depth_upper_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Strong induction on the current finite candidate set chooses a readout separating two candidates. Every realized answer fiber is a strict subset, so recursion identifies that branch within one fewer query than the current candidate count.

References

• Truth anchor: D5/S3/Observer/Budget/AdaptiveSeparationDepthUpperBound.adaptive_separation_depth_upper_bound
• Dependency: D5/S3/ConceptDynamics/Experiment/PassiveAdaptiveTranscriptUpperBound