Binary Identification and Repair Depth Equality

Abstract

Unconstrained binary identification has the same least depth as exact repair width.

Theorem 1.1 (Least adaptive depth equals least binary repair width).

$$\begin{array}{c}\forall X,C,Target:\mathrm{Type},\\ [\mathrm{Fintype}(X)],[\mathrm{Fintype}(C)],\\ c:X\to C,t:X\to Target,\\ \exists dAdaptive,dRepair\in \mathbb{N},\\ \mathrm{IsLeast}(\{d\in \mathbb{N}\mid \exists pi:\mathrm{BinaryProtocol}(X,d),\mathrm{IdentifiesGiven}(c,t,pi)\},dAdaptive)\wedge \\ \mathrm{IsLeast}(\{k\in \mathbb{N}\mid \mathrm{BinaryRepairFeasible}(c,t,k)\},dRepair)\wedge \\ dAdaptive=dRepair\wedge \\ dRepair=\mathrm{clog}(2,\mathrm{worstFiberDiversity}(c,t)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Identifiability/BinaryIdentificationRepairDepthEquality.unconstrained_binary_identification_depth_equals_repair_bits (✓ std3). ∎

Source. Repository-derived.

Commentary.

Worst fiber diversity counts the largest number of target values realized under one current-concept coordinate.

The public statement exposes both least-element claims. The adaptive membership clause contains an identifying protocol, while the repair membership clause contains a target-determining bit label.

The frozen construction, adaptive lower bound, and exact repair-cost theorem give the common ceiling binary logarithm.

References

• Truth anchor: D5/S3/ConceptDynamics/Identifiability/BinaryIdentificationRepairDepthEquality.unconstrained_binary_identification_depth_equals_repair_bits
• Dependency: D5/S3/ConceptDynamics/Coding/BinaryProtocolDepthLowerBound