Stabilizer Obstruction to Equivariant Selection

Abstract

A stabilizer without an admissible fixed action obstructs every equivariant selector.

Theorem 1.1 (No equivariant selector exists without a stabilizer-fixed action).

$$\begin{array}{c}\forall G,X,A:\mathrm{Type},\\ [\mathrm{Group}\left(G\right)],[\mathrm{MulAction}\left(G,X\right)],[\mathrm{MulAction}\left(G,A\right)],\\ admissible:X\to \mathrm{Set}\left(A\right),x:X,\\ (\forall a:A,a\in admissible\left(x\right)\Rightarrow \exists g:G,\mathrm{smul}\left(g,x\right)=x\wedge \mathrm{smul}\left(g,a\right)\ne a)\Rightarrow \neg \exists s:X\to A,\\ (\forall y:X,s\left(y\right)\in admissible\left(y\right))\wedge (\forall g:G,y:X,s\left(\mathrm{smul}\left(g,y\right)\right)=\mathrm{smul}\left(g,s\left(y\right)\right)).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let a group act on both states and actions. At the named state, every admissible action is moved by some group element that fixes the state; this states directly that the stabilizer has no admissible fixed action.

An admissible deterministic selector would choose one of those actions. Equivariance under the corresponding stabilizer element would both fix and move the selected action, a contradiction.

The existing finite-permutation culprit theorem is only a specialization. Repository and pinned-Mathlib searches found no general group-action theorem with the public admissible-set and stabilizer clauses.

References

• Truth anchor: D5/S3/ConceptDynamics/Attribution/StabilizerSelectorObstruction.no_equivariant_selector_of_stabilizer_without_fixed_action