What does it mean to be "gauging" a symmetry? I read this and other similar questions, but they all address the problem of gauging a global symmetry (implying that one could also gauge a local one).
This confused me a lot: in my mind gauge and local are synonyms when used for symmetries, and "gauging" meant something like "localizing". Is this wrong? What are the proper definitions of gauge symmetry and of the process of gauging a symmetry?
Edit: this answer seems to prove my point, saying that a gauge symmetry is a local symmetry after you add the gauge bosons to make the lagrangian usable. If this is correct, then what is the meaning of "gauging"?
Edit 2: this paper uses the wording

Therefore when one wishes to solve the equations of
motion describing the gauge field, the local gauge invariance of the Lagrangian, and so the action, is destroyed along with the possibility of additional observables. On the other hand, global gauge invariance still holds and one is left with the corresponding intrinsic conserved current and charge.

Which seems to be against what @CosmasZachos said in the comments. What does global gauge mean?
 A: *

*A gauge theory in the broadest sense is a theory with an action that has gauge symmetries parametrized by smooth functions of spacetime $\epsilon(x)$, i.e. the theory is invariant under infinitesimal changes of the coordinates/fields as $$\delta \phi = R\epsilon(x) + R^\mu \partial_\mu\epsilon(x) + R^{\mu\nu}\partial_\mu\partial_\nu \epsilon(x) + \dots$$ and these transformations are thought of to transform between physically equivalent states.
Such symmetries often occur in a Lagrangian theory in which the equations of motion are underdetermined, i.e. the general solution for initial data $(q,\dot{q})$ contains arbitrary functions of (space)time. This is the case when $\mathrm{det}\left(\frac{\partial L}{\partial \dot{q}^i \partial \dot{q}^j}\right) = 0$. Equivalently, the corresponding Hamiltonian theory is constrained - when there are first-class constraints, the theory is usually a gauge theory. See also this question and its linked questions. The invariance under gauge transformations is related to the existence of constraints via Noether's second theorem.


*A gauge theory in the narrow sense is a Lagrangian field theory with a gauge field $A$ that is valued in some Lie algebra $\mathfrak{g}$ and fields that transform in representations of a corresponding Lie group $G$, such that the transformations $$A\mapsto gAg^{-1} + \mathrm{d}\alpha, \phi \mapsto \rho(g)\phi$$
for a $\mathfrak{g}$-valued function $\alpha$ and $g(x) = \mathrm{exp}(\alpha(x))$ the corresponding group element are symmetries. This is a special case of the general gauge transformations from the first point. See this question and its answers for more on the basis of gauge theories in this narrow sense.


*"Gauging" a symmetry is the process of turning a Lagrangian theory with a symmetry Lie group $G$ into a gauge theory in the narrow sense. There is rarely a "good" reason to do this (see this answer of mine), but many seem to like to use this process as a "motivation" for gauge theory. You take a theory with global symmetry group $G$ and add the kinetic Yang-Mills term for a gauge field $A$ valued in its Lie algebra and then replace all derivatives with gauge covariant derivatives w.r.t. $A$. The resulting theory is a gauge theory in the narrow sense.


*The words "global" and "local" are often used inconsistently and confusingly in the context of gauge theories, as well as word "gauge group". Some people use "gauge group" for the Lie group $G$, some for the group of $G$-valued functions, and the latter then use "global gauge group" for $G$. In general, "global" will typically refer to the rigid symmetry of $G$, not to the "local" symmetry under $G$-valued functions.
A: OK, I collect my comments since their obviousness is evidently not unassailable.
You are exactly right that

in my mind gauge and local are synonyms when used for symmetries, and "gauging" meant something like "localizing".  ...
"local symmetry", "gauge symmetry" and "local gauge symmetry" all mean the same thing.

That's the point: you cannot localize a local symmetry, so you can't gauge it. Mere contrast. Don't overthink sloppy writing.
When you "promote" a global symmetry to a local one, you actually introduce redundant ("gauge") degrees of freedom, through coupling to a gauge field controlling them; they are then only removable by a "gauge fixing term", which lacks this  local invariance, but still has the original global invariance, as gauge fields still transform under that, lacking the telltale gradient term in their transformations, now. The gauge -fixed theory is now globally invariant, and without gauge-dross. You still call the vector fields involved "gauge fields"  for symbolic continuity.
As for your 2nd edit, that sentence is just bad-bad-nogood-terrible language, a magnificent oxymoron, which you misunderstood. Karatas, D. L., & Kowalski, K. L. (1990). Noether’s theorem for local gauge transformations. American Journal of Physics 58 (2), 123-131, section 3, after (19/3.5), indicates the gauge-fixed action has residual global symmetry, but not local (gauge) symmetry. It is the customary confusion between Noether's first & second theorems.
A: A global gauge symmetry means that the gauge group acts everywhere in the same way. We say it acts in a rigid fashion. Whilst a local gauge symmetry means that the gauge group acts in a position dependent fashion. We say a global gauge symmetry is gauged when it is made to depend in a position dependent fashion, that is in a local fashion. So we have a gauged gauge symmetry. Here, gauged and gauge is understood differently.
Note, the gauge group here is what in mathematics is called the structure group. The mathematics of fibre bundles makes all this clear in a geometric fashion.
