Local CAR Deficiency
Abstract
A local change of a CAR profile preserves every pair readout and has two exact directed deficiencies.
Theorem 1.1 (Exact local deficiencies in an arbitrary common background).
Proof. Machine-checked in Lean as D5/S3/Estimation/DecisionRisk/LocalCARDeficiency.result (✓ std3). ∎
Source. Repository-derived.
Commentary.
A is any finite nonempty state set, and Block(A) consists of all nonempty subsets of A. For a profile w, experiment(w,i,B) is w(B) when i belongs to B and is zero otherwise. The profile is nonnegative and each experiment row sums to one. No partition-mixture representation is assumed.
Fix U contained in A with m = card(U) at least three. The local direction is one at U, m minus two at each singleton in U, minus one at each two-element block contained in U, and zero elsewhere. The new profile is v = w + a direction(U), where a is nonnegative. The capacity hypothesis applies only to the weight of each exact internal two-element block; it is not a bound on the sum of weights of all blocks containing that pair.
The common background is arbitrary, including blocks meeting both U and its complement. Every pair of distinct states in A has the same readout r before and after the change. The new profile is nonnegative and normalized at every state.
finiteDeficiency takes its target experiment first and its source experiment second. It is the infimum, over all stochastic kernels on the full nonempty-block alphabet, of the maximum statewise half-L1 total-variation error. Thus finiteDeficiency(experiment(w),experiment(v)) describes simulation from v to w, and the reverse expression describes simulation from w to v. The lower bounds in the statement hold separately for every unrestricted kernel, including kernels that output target zero-weight blocks or blocks not containing the true state.
There is one globally defined attaining kernel in each direction, used for all states simultaneously. Write Q for the two-element blocks contained in U, let delta(B,C) be one when B equals C and zero otherwise, and write indicator(P) for the indicator of a condition. Set b(B) = w(B) - a indicator(B in Q). The following probability rows and nonnegative mass flows give explicit attaining kernels.
P is uniform on Q, and S(j) is uniform on its blocks containing j, for j in U. The row sums of FP and FM are respectively v(B) and w(B). When an input weight is zero, its entire nonnegative flow row is zero; the displayed identity row completes the kernel on that input. Consequently both kernels are defined on every input block. For a = 0 both constructions are the identity kernel and both errors are zero. No division by a is required.
KP has error ep = a(m-2)/m at every state in U and zero error at every state outside U. KM has error em = a(m-2)/2 at every state in U and zero outside U. Both retain every background block outside the changed coordinates, including all crossing blocks.
For optimality, put k(B) = card(B intersect U). Two bounded losses on the full output alphabet have optimal unnormalized block costs max(k(B)-2,0) and, respectively, zero for k(B) at most one and k(B)/2 otherwise. The identity decision attains each block cost. Averaging over the uniform prior on U gives risk gaps ep in the first direction and em in the second. All unchanged background terms cancel separately. Bounded-loss risk transport bounds each gap by the maximum statewise simulation error of every stochastic kernel, giving the two lower bounds and hence equality with the explicit upper bounds.