ora-0098
7.3 Finite active identification
Suppose the initial residual fiber has \(N{\lt}\infty \) observational-equivalence classes, the true class is never eliminated, probe responses are sound, and the policy selects a probe that eliminates at least one false class whenever more than one remains. Then UOCL behaviorally identifies the target after at most \(N-1\) separating probe responses.
Each separating response strictly decreases the finite number of viable false equivalence classes and never deletes the true one. At most \(N-1\) such decreases leave a single class, which answers every admissible query as the target does.
The theorem does not promise explanatory identification. Nor does it cover infinite fibers without a topology, rank, measure, or compactness condition. It shows exactly where the work moves in harder settings: one must prove separation, sound elimination, and a well-founded decrease.