Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Four-state obstruction to the coefficient-two reverse bound

Abstract

A four-state CAR pair has equal pair collisions and directed deficiencies 1/9 and 5/18; an actual common public partition seed preserves the counterexample after halving.

Let A = Fin 4 = {0,1,2,3}. The observation alphabet B consists of all fifteen nonempty subsets: {0}, {1}, {2}, {3}, {0,1}, {0,2}, {0,3}, {1,2}, {1,3}, {2,3}, {0,1,2}, {0,1,3}, {0,2,3}, {1,2,3}, and A. Zero-weight letters remain present. D5/S3/Estimation/DecisionRisk/CARApproximateRecovery.row assigns u(B) when i belongs to B and zero otherwise. D5/S3/Estimation/DecisionRisk/CARApproximateRecovery.pair sums u(B) over the blocks containing both states.

D5/S3/Estimation/SequentialDecisionRisk/FiniteDeficiencyRiskTransfer.finiteDeficiency takes the target first and source second. Write d(u,z) for toReal(finiteDeficiency(row(z),row(u))). It is the infimum of the maximum statewise half-L1 error over every stochastic kernel on the full alphabet. All fifteen input rows are probability rows. One kernel acts at every state, with no support or block-containment restriction. Kernels can output zero-weight letters and blocks not containing the state. ENNReal.ofReal, denoted ofReal below, embeds nonnegative real values into the extended nonnegative reals.

Theorem 1.1 (A complete certificate refutes the proposed reverse inequality).

Proof. Machine-checked in Lean as D5/S3/Estimation/DecisionRisk/CARFourStateReverseObstruction.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

The formal conclusion is Not claim, where claim is the implication from the entire Certificate displayed below to the coefficient-two upper bound. The proof constructs that certificate and its strict violation; none of its Bayes values, deficiencies, or public realizations is an assumed input. Classically the negative implication entails the certificate itself. There is one public theorem, result, and no separately asserted positive companion.

Every weight is nonnegative. Each w row sums to 5/9 + 4/9 = 1; each v row sums to 3(2/9) + 3(1/9) = 1. For distinct i,j, the only common w block is A, while v has their pair and two triples, giving 4/9 on both sides. Consequently every signed pair difference is zero and R(w,v) = 0.

The common forward kernel H sends each singleton uniformly to its three containing pairs, and sends A uniformly to the four triples. Its other rows are identity rows. For state i it produces 5/27 on each containing pair, a deficit of 1/27 against 2/9, and 1/9 on every triple. The three containing triples match the target; the unique triple omitting i has excess 1/9. Hence the half-L1 error of this single H is 1/9 at every state.

The common reverse kernel J sends a pair to A with probability 1/6 and to each endpoint singleton with probability 5/12; every triple goes to A. Its other rows are identity rows. At state i the output gives 5/18 to {i}, 5/54 to each of the other three singletons, and 4/9 to A. The target gives 5/9 to {i}, zero to the other singletons, and 4/9 to A. The error is 5/18. Both kernels are stochastic on all letters, including unused input letters.

For the matching lower bounds use the uniform prior pi(i)=1/4 and two genuine bounded decision tasks. Bayes risk optimizes over all stochastic decision kernels from blocks to actions, using the same decision rule at every state. For each block, every randomized row is a convex combination of its action costs and is at least their minimum. Choosing a minimizing action at each block forms one deterministic decision kernel attaining all block minima simultaneously. The certificate exposes one such common deterministic kernel for each task, together with its block minima, its costs under both w and v, and optimality against every randomized decision kernel under both profiles. Thus the displayed values are unrestricted Bayes optima, including at zero-weight blocks.

The identification-or-rejection task has actions 0,1,2,3 and reject. Correct identification costs zero, an incorrect label costs one, and reject costs one half at every state. For block sizes 1,2,3,4, the weighted minima are respectively 0,1/4,3/8,1/2. A singleton chooses its label; a pair can choose an endpoint or reject; triples and the full block choose reject. Its Bayes risks are 2/9 under w and 1/2 under v, a reverse gap of 5/18.

The list task has the six pairs as actions, in the order {0,1}, {0,2}, {0,3}, {1,2}, {1,3}, {2,3}. Its loss is one precisely when the state lies outside the chosen pair. The minima by block size are 0,0,1/4,1/2. Choose a containing pair for a singleton, the block itself for a pair, a two-element subblock for a triple, and any pair for A. The risks are 2/9 under w and 1/9 under v, a forward gap of 1/9.

D5/S3/Estimation/SequentialDecisionRisk/FiniteDeficiencyRiskTransfer.deficiency_risk_bound transports a bounded loss through every common simulation kernel. Source Bayes risk is no larger than target Bayes risk plus maximum state TV. The list task therefore bounds every forward kernel below by 1/9; the rejection task bounds every reverse kernel below by 5/18. Taking the infimum and combining with H and J proves both exact deficiencies. This argument uses bounded risk transfer and attained finite decision minima, without a duality assumption.

At this pair the proposed coefficient-two right side is 2/9, and the reverse deficiency exceeds it by 1/18. If any real c bounds the reverse deficiency by c times the forward deficiency here, c is at least 5/2. Therefore every universally valid coefficient on four-state equal-pair CAR experiments is at least 5/2. Sufficiency of 5/2 is not proved.

D5/S3/Estimation/DecisionRisk/CARRevelationScaling.result applies at t=1/2 in [0,2/4]. Mixing with complete revelation gives w’=mix(w), v’=mix(v), pair collisions 2/9, R(w’,v’)=0, and exact deficiencies 1/18 and 5/36. The coefficient-two violation is 1/36.

For an explicit ordinary-partition law, let P0 be the discrete partition and PA the one-part partition. The w’ law gives P0 mass 7/9 and PA mass 2/9. The v’ law gives P0 mass 1/9, each of the six partitions consisting of a pair and two remaining singletons mass 1/9, and each of the four partitions consisting of a triple and its complementary singleton mass 1/18. Its mass is 1/9+6/9+4/18=1; a given singleton has mass 1/9+3/9+1/18=1/2. These are ordinary partitions of the same state space.

The Lean seed is Seed=Option(B) times Option(B), with the product of the two selector laws constructed by revelation scaling. A none selector gives P0, and some(B) gives B with every outside state as a singleton. The law p is nonnegative, sums to one, and is independent of the state. P reads the first selector and Q the second. Both actual observations reveal the entire same seed s and the part P_s(i) or Q_s(i). The public experiment E(p,T)(i,(s,B)) is p(s) when T_s.part(i)=B and zero otherwise.

For each T=P,Q, forgetting the seed is a deterministic common kernel F. If the induced block weight h(B) is positive, reconstruct the whole seed with probability p(s) indicator(B is a part of T_s)/h(B), keeping B in the output. This law does not depend on the unknown state. At a zero-weight input block, use any fixed output point mass, which completes a stochastic row. Nonnegativity ensures that p(s)=0 whenever h(B)=0 and B is a part of T_s. Since T_s.part(i)=B exactly when B is a part and i belongs to B, both channel identities hold at every state.

Precompose and postcompose any simulation kernel with these four exact equivalence kernels. Stochastic composition and TV contraction give both inequalities between each public deficiency and its block deficiency, hence equality. The public forward value is 1/18, the public reverse value is 5/36, and their coefficient-two gap is 1/36. The certificate supplies an actual common state-independent full-seed realization and its equivalence kernels, not merely the marginal profiles.

This refutes universal sufficiency of n/2 at n=4, including ordinary public partition experiments. It preserves the original half-L1 normalization, maximum over states, all fifteen letters, and unrestricted common kernels. It does not settle the optimal four-state coefficient or the optimal replacement bound for general n at least four.

References