I am confused by the approach to gauging given in this answer, which I summarise below.
Suppose we start with a scalar field with a global $U(1)$ symmetry $\phi \rightarrow \phi + \alpha$, $$ S_0 = \int d\phi \wedge \star d\phi. $$
The conserved current is $j = 2 \star d\phi$. To gauge the symmetry we introduce a one-form gauge field $A$ which transforms as $A\rightarrow A + d\alpha$, and a term which couples $A$ to the current: $$ S_1 = \int d\phi \wedge \star d\phi + A\wedge j. \tag{1} \label{eqone} $$
This is not yet gauge invariant, but we are allowed to 'add local terms possibly depending on $\phi$ and at least secord order in $A$' [1] - we add $A\wedge \star A$ and get the gauge-invariant $$ S_2 = \int (d\phi - A ) \wedge (d\phi - A) \tag{2} \label{eqtwo} $$
I'm not sure how to think about this.
Viewpoint 1: eq. ($\ref{eqone}$) is the correct theory, but this is equivalent in some way to eq. ($\ref{eqtwo}$), because we are 'allowed' to add some sort of 'local term'.
Q: What counts as a local term? Everything in the action is local in that it depends only on a point $x$ - we could add a `local' term of the form $-d\phi \wedge \star d\phi$ and set the action to zero.
Q: Why not just go straight to eq. $\ref{eqtwo}$? What is important about setting down eq. $\ref{eqone}$ first?
Viewpoint 2: we are passing from an ungauged theory (T1), defined as a theory of $\phi$ with the global symmetry, to a gauged theory (T2), defined as a theory of $\phi$ with a gauged symmetry and possibly extra things. To gauge a transformation, we must minimally couple a gauge field to the matter field. This will necessarily imply that the gauge field will be sourced by any current of the matter field in whatever experiment we run. T2 must therefore contain a term which accounts for that - $A\wedge j$. But eq. ($\ref{eqone}$) is not T2 - instead eq. ($\ref{eqtwo}$) is the minimal possible T2. We are not saying eq. ($\ref{eqone}$) is equivalent to eq. ($\ref{eqtwo}$) in a way that involves somehow-irrelevant 'local terms'.
Q: still - why not just go straight to eq. ($\ref{eqtwo}$)? It will obviously contain the $A\wedge j$ coupling we know must be there. When would that not be true?
