Uniform CAR reverse obstruction
Abstract
For every state count at least four, two CAR experiments with identical pair readouts have exact asymmetric deficiencies and a common whole-seed public realization.
Theorem 1.1 (Exact deficiencies, attained risks, and a common public seed).
Proof. Machine-checked in Lean as D5/S3/Estimation/DecisionRisk/CARUniformReverseObstruction.result (✓ std3). ∎
Source. Repository-derived.
Commentary.
The quantifier ranges over every natural n at least four. The state space is Fin n and the observation alphabet consists of every nonempty subset of that space. Letters of zero profile weight and letters not containing the current state remain present. All denominators below are real; n and n minus one are positive.
The four cardinality classes used by the profiles are distinct. For each state there are n minus one containing pairs and n minus one containing complements of singletons. For two different states there is one containing pair and n minus two containing complements of singletons. These counts give nonnegative unit rows and the common off-diagonal pair value b. On the diagonal both pair readouts equal one. Every signed pair difference and the star budget vanish.
A simulation kernel is one nonnegative matrix with unit row sums, used for every state. The deficiency infimum ranges over all such matrices on the full alphabet. It imposes no support restriction. The notation d(X,Y) means simulation from X to Y; the Lean function finiteDeficiency takes Y first and X second. The generic observation types O and T below are finite; A = Fin n is finite and nonempty. Total variation is half the sum of absolute differences.
The forward kernel sends a singleton uniformly to its containing pairs and sends the full block uniformly to all complements of singletons. The reverse kernel sends a pair to the full block with probability x and to each of its two singletons with probability (1 minus x)/2; it sends every complement of a singleton to the full block. Every other input row is the identity row. Thus both kernels are defined on every letter, including unused letters.
In the forward output each containing pair has mass (1 minus b)/(n minus one), and every complement of a singleton has mass c. Compared with V, the total deficit on containing pairs is c and the unique noncontaining complement has excess c. The reverse output has full-block mass b, singleton mass rho at the true state, and rho/(n minus one) at each other state. Its total deficit and excess are both rho. These computations give the exact error at every state.
The prior is uniform. In the identification-or-rejection task an incorrect identification costs one, a correct identification costs zero, and rejection costs one half. In the list task an action is a subset of cardinality exactly two and the loss is one precisely when the state is outside that subset. Both losses lie between zero and one.
For a block of size k, identifying a member has total loss k minus one, rejection has total loss k/2, and a two-element list has total loss at least the natural truncated difference k minus two. Identify the unique member on singletons and reject on larger blocks to attain the first minimum. For the second minimum choose two members when possible; on a singleton include its member and one different state. These choices depend only on the input block.
Interchanging finite sums expresses the cost as a nonnegative profile-weighted sum of block costs. Each randomized decision is a convex combination of the action costs and hence is bounded below by the block minimum. For each task, the same deterministic block decision attains the minimum for both profiles. The resulting equalities are true Bayes infima over all randomized decision kernels, with an attaining decision and a lower bound for every competitor.
The list-risk difference bounds the forward deficiency below by epsilon, and the rejection-risk difference bounds the reverse deficiency below by rho, by bounded-loss risk transport. The explicit common kernels attain those bounds. Thus the equalities concern unrestricted deficiencies, rather than an optimization within the displayed kernel families.
Consequently any coefficient bounding reverse deficiency by forward deficiency for every CAR pair with equal pair readouts must be at least n minus three halves. This is a necessary coefficient bound. Whether that coefficient is sufficient for all such pairs is not asserted. For every n at least four the present pair strictly violates the candidate n/2 bound even with its original minimum-with-one truncation.
For the public realization mix each profile with complete revelation at t = 2/n. There is one probability distribution p on Option(Block) times Option(Block), independent of the state, and two actual partition-valued maps P and Q. Each observation includes the entire common seed and its partition block containing the state. The whole-seed requirement includes both coordinates of the seed at either end.
The partition marginals can be described explicitly. For w prime, choose the full-block partition with mass 2/[3(n minus one)] and the discrete partition with the remaining mass. For v prime, each pair-block partition has mass 4/[3n(n minus one)], each complement-of-singleton partition has mass 2/[3n(n minus one)], and the discrete partition has mass (n minus three)/[3(n minus one)]. A block partition consists of that block and singleton parts outside it. The binomial count of pairs and the n complements give total mass one.
One construction takes independent partition selectors on the two Option coordinates and exposes their product seed. At n = 4, the v-prime selector assigns mass 1/9 to each of six pair partitions, 1/18 to each of four triple partitions, and 1/9 to the discrete partition; the w-prime selector gives 2/9 to the full partition and 7/9 to the discrete partition. The theorem obtains actual maps and a common distribution from the CAR revelation-scaling existence result. It does not identify those existential witnesses with a prescribed encoding of this product construction.
For each end, forgetting the seed is a stochastic kernel to its mixed block experiment. In the reverse direction, condition the seed distribution on occurrence of the input block when its profile weight is positive, and use a fixed probability row when the weight is zero. This supplies all four exact normalization kernels, with the same entire seed in both reverse outputs. The formulas below apply once with T = P and u prime = w prime, and once with T = Q and u prime = v prime; o star is any fixed public output letter.
Exact normalization in both directions transports deficiency by composition of kernels and contraction of total variation. Revelation scaling multiplies both original directed deficiencies by t. The public pair difference is t times the original pair difference, so it and the public star budget are zero. The actual public experiments therefore have the following exact deficiencies and ratio, and retain the strict truncated obstruction.
References
- Truth anchor:
D5/S3/Estimation/DecisionRisk/CARUniformReverseObstruction.result - Dependency: D5/S3/Estimation/DecisionRisk/CARRevelationScaling
- Dependency: D5/S3/TotalVariation/DataProcessing