Fixed-Symmetry Obstruction to Equivariant Selection

Abstract

One fixed-state symmetry without admissible fixed actions obstructs equivariant selection.

Theorem 1.1 (No equivariant deterministic selector exists under a fixed-point-free stabilizer).

$$\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),\\ (\exists x:X,g:G,\mathrm{smul}\left(g,x\right)=x\wedge (\forall a:A,a\in admissible\left(x\right)\Rightarrow \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/FixedSymmetrySelectorObstruction.no_equivariant_selector_of_common_fixed_symmetry (✓ std3). ∎

Source. Repository-derived.

Commentary.

A single group element and state are quantified together. The element fixes that state but moves every action in its admissible set.

Any everywhere-admissible equivariant selector would choose an action in that set. Equivariance at the fixed state would force the chosen action to be fixed by the same element, contradicting the public premise.

References

• Truth anchor: D5/S3/ConceptDynamics/Attribution/FixedSymmetrySelectorObstruction.no_equivariant_selector_of_common_fixed_symmetry
• Dependency: D5/S3/ConceptDynamics/Attribution/StabilizerSelectorObstruction