I would like to know if there is a procedure to completely fix a gauge, which I believe we must do in order to make sense of the path integral?
In chapter 74 Sredniki introduces the Lagrangian $$ \mathcal{L} = \mathcal{L}_{YM} + \delta_B \mathcal{O}\ .\tag{74.17} $$ The operator $\mathcal{O}$ has to be Grassmann-odd, therefore (I believe) it is sometimes referred to as the gauge-fixing-fermion. Sredniki proceeds to make the choice $$ \mathcal{O} = Tr\left[\bar{c}\left(\frac{\xi}{2}B - G\right) \right] \ .\tag{74.18} $$ It is clear to me that by making the choice $$G = \partial_\mu A^\mu\tag{74.19}$$ we obtain the ghost Lagrangian and gauge-fixing terms in $R_\xi$ gauge. I would like to know why is $\mathcal{O}$ chosen in such a way? It appears like any Grassmann-odd function would work, and this choice is made simply to give an easy realization of $R_\xi$ gauge and the Faddeev-Popov delta function.
Let us suppose we picked some form for $\mathcal{O}$. How do we ensure that this gauge fixing condition has no residual gauge freedom? To consider a simple example, Lorenz gauge has the residual gauge freedom $$ A_\mu \rightarrow A_\mu + \partial_\mu \Lambda $$ where $\square\Lambda=0$. How would I eliminate this freedom? And, what most interests me, how do we do this for general gauge choices? I suppose that we would require the gauge-fixing function to fix a gauge such that "the solutions to $G=0$ are unique". Is there a useful way of encoding this as constraints on the form of $\mathcal{O}$ or $G$? Just fixing a gauge and then guessing additional gauge transformations seems a bit unsystematic, since I would not know what forms of gauge transformations I should be guessing.