Symmetric Responsibility Allocation

Abstract

A normalized equivariant allocation is uniform at a fully symmetric event.

Theorem 1.1 (Symmetry forces equal responsibility).

$$\begin{array}{c}\forall n:\mathbb{N},Event:\mathrm{Type},\\ act:\mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right)\to Event\to Event,\\ allocation:Event\to \mathrm{Fin}\left(n\right)\to \mathbb{R},event:Event,\\ (\forall i:\mathrm{Fin}\left(n\right),0\le \mathrm{allocation}\left(event,i\right))\wedge \\ \sum _{i:\mathrm{Fin}\left(n\right)}\mathrm{allocation}\left(event,i\right)=1\wedge \\ (\forall sigma:\mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),even{t}^{\prime }:Event,i:\mathrm{Fin}\left(n\right),\mathrm{allocation}\left(act(sigma,even{t}^{\prime }),sigma(i)\right)=\mathrm{allocation}\left(even{t}^{\prime },i\right))\wedge \\ \mathrm{IsCompletelySymmetric}\left(act,event\right)\Rightarrow \\ ((\forall sigma:\mathrm{Perm}\left(\mathrm{Fin}\left(n\right)\right),i:\mathrm{Fin}\left(n\right),\mathrm{allocation}\left(event,sigma(i)\right)=\mathrm{allocation}\left(event,i\right))\wedge \\ (\forall i:\mathrm{Fin}\left(n\right),\mathrm{allocation}\left(event,i\right)=\frac{1}{n})).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Attribution/SymmetricResponsibilityAllocation.symmetric_responsibility_is_uniform (✓ std3). ∎

Source. Repository-derived.

Commentary.

Equivariance and complete symmetry first make the allocation invariant under every relabeling. Swaps then identify every pair of coordinates, and normalization fixes their common value at one divided by the number of labels.

References

• Truth anchor: D5/S3/ConceptDynamics/Attribution/SymmetricResponsibilityAllocation.symmetric_responsibility_is_uniform
• Dependency: D5/S3/ConceptDynamics/Attribution/SymmetricEventNoUniqueCulprit