Finite-group orbit-rank validity

Fix a positive-probability orbit $O$ and points $x,y\in O$. Choose $h\in G$ with $y=h\cdot x$. Invariance gives $P(X=y)=P(h\cdot X=y)=P(X=h^{-1}\cdot y)=P(X=x)$. Thus all $\mathrm{\mid }O\mathrm{\mid }$ distinct points have equal mass; by [F3] their conditional probabilities given $X\in O$ are each $1\mathrm{/}\mathrm{\mid }O\mathrm{\mid }$.

For fixed $x\in O$, define its stabilizer $G_x:=\{g\in G:g\cdot x=x\}$. If $y=h\cdot x$, then $\{g:g\cdot x=y\}=h{G}_x$: every $hg$ with $g\in G_x$ sends $x$ to $y$, and if $g\cdot x=y$ then $h^{-1}g\in G_x$. Hence every distinct point of $O$ occurs exactly $\mathrm{\mid }{G}_x\mathrm{\mid }$ times in the group-transformed list. The strict and tied counts and denominator in [F2] all have this same factor, so the group-average ranks equal the ranks computed on the distinct orbit points.

Conditional on $O$, [step 1.1] makes the observed orbit point a uniform index in the finite list $(T(y){)}_{y\in O}$. By [F5] and [A2], the randomizer remains independent and uniform. Apply [F4] to this list and use [step 2.1]: $p_U$ is Uniform$(0,1)$ and $P(p_0\le u\mid X\in O)\le u$ for every $u\in [0,1]$.

The positive-probability orbits form a finite partition up to null orbits. Summing the conditional superuniform bounds from step 3.1 with weights $P(X\in O)$ gives $P(p_0\le u)\le u$; summing the conditional uniform laws gives $p_U\sim \mathrm{Unif}(0,1)$. The argument applies to each invariant null law. Only finite counting is used, so no choice axiom is needed.