Static Effect And Sequential Law Separation

Abstract

Equal instrument effects do not determine sequential outcome laws.

Theorem 1.1 (Equal effects can yield different two-step weights).

$$\begin{array}{c}{P}_0:QubitMatrix=basisZeroDensity,P_1:QubitMatrix=I-P_0;\\ K_a^L:QubitMatrix=\mathrm{if}\left(a,P_1,P_0\right),a:Bool;\\ K_a^J:QubitMatrix=qubitX\cdot K_a^L,a:Bool;\\ E_a^M:QubitMatrix={M_a}^{\ast }\cdot M_a,M:Bool\to QubitMatrix,a:Bool;\\ {\mathcal{I}}_a^M(\rho ):QubitMatrix=M_a\cdot \rho \cdot {M_a}^{\ast },M:Bool\to QubitMatrix,a:Bool,\rho :QubitMatrix;\\ (\forall a:Bool,E_a^L=E_a^J)\wedge \\ \sum _{a\in Bool}{E}_a^L=I\wedge \\ \sum _{a\in Bool}{E}_a^J=I\wedge \\ \mathrm{bornProbability}\left({\mathcal{I}}_{false}^L(P_0),P_1\right)=0\wedge \\ \mathrm{bornProbability}\left({\mathcal{I}}_{false}^J(P_0),P_1\right)=1.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/StaticEffectSequentialSeparation.same_effects_different_two_step_joint_law (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two Boolean-outcome qubit instruments are constructed explicitly. The first measures the computational projections, while the second applies the canonical bit flip after the same coordinate branch.

Their effect matrices agree outcome by outcome and both effect families sum to the identity. Starting from the basis-zero density after the false branch, however, the complementary second effect has weight zero for the projective instrument and weight one for the flipped instrument.

The branch maps and effect maps are displayed from their Kraus formulas. Thus the static agreement and sequential separation use the same constructed instruments rather than independent witnesses.

References

• Truth anchor: D5/S3/Quantum/Measurement/StaticEffectSequentialSeparation.same_effects_different_two_step_joint_law
• Dependency: D5/S3/Observer/StateNotPath