This is more of an extended comment, rather than an answer completely separate from what Urs and Moshe have already said. The axioms of AQFT are designed to capture a mathematical model of the *physical observables* of a theory, while OTOH gauge invariance is a feature of a *formulation* of a theory, though perhaps an especially convenient one. Yours and related questions are somewhat muddied by the fact that one physical theory may have several equivalent, but distinct formulations, which may also have different gauge symmetries. One example of this phenomenon is gravity, consider the metric and frame-field formulations, and another one according to Moshe is Seiberg duality. Another confounding factor is that some physical theories are only known in a formulation involving gauge symmetries (automatically rendering such formulations "especially convenient"), which naturally leads to your second question. However, one must remember that by design the gauge formulation should be visible in the AQFT framework only if it is detectable through physical observables.

Now, to be honest, I really have no idea about what is the state of the art in AQFT of figuring out when a given net of local algebras of observables admits an "especially convenient" formulation involving gauge symmetry. But I believe answering this kind of question will remain difficult until the notion of "especially convenient" is made mathematically precise. I don't know how much progress has been made on that front either. But I think a prototype of this kind of question can be analyzed, though somewhat sketchily, in the simplified case of classical electrodynamics.

Suppose we are given a local net of Poisson algebras of physical observables (the quantum counterpart would have *-algebras, but other than that, the geometry of the theory is very similar). The first step is to somehow recognize that this net of algebras is generated by polynomials in smeared fields, $\int f(F,x) g(x)$, where $g(x)$ is a test volume form, and $f(F,x)$ is some function of $F$ and its derivatives at $x$, with $F(x)$ a 2-form satisfying Maxwell's equations $dF=0$ and $d({*}F)=0$. Since we were handed the net of algebras with a given Poisson structure, as a second step we can compute the Poisson bracket $\{F(x),F(y)\}=(\cdots)$. The answer for electrodynamics would be the well known Pauli-Jordan / Lichnerowicz / causal propagator, which I will not reproduce here. Very roughly speaking, the components of $F(x)$ and the expression for the Pauli-Jordan propagator give a set of local "coordinates" on the phase space of the theory and an expression for the Poisson tensor on it. In the third step we can compute the inverse of the Poisson tensor, which if it exists would be a symplectic form. The answer for electrodynamics is well known and what's important is that the symplectic form is *not* given by some *local* expression like $\Omega(\delta F_1,\delta F_2) = \int \omega(\delta F_1, \delta F_2, x)$, where $\omega$ is a form depending only on the values of $\delta F_{1,2}(x)$ and their derivatives at $x$. Step four would consist of asking the question whether there is another choice of local "coordinates" on the phase space in which the symplectic form is local. The answer is again well known: extend the phase space by introducing the 1-form field $A(x)$ such that $F=dA$. The pullback of the symplectic form to the extended phase space now has a local expression $\Omega(\delta A_1,\delta A_2) = \int_\Sigma [{*}d(\delta A_1)(x)\wedge (\delta A_2)(x) - (1\leftrightarrow 2)]$, up to some constant factors, with $\Sigma$ some Cauchy surface. Note that $\Omega$ is no longer symplectic on the extended phase space, but only presymplectic, while its projection back to the physical phase space is. As a last step, one might try to solve the inverse problem of the calculus of variations and come up with a local action principle reproducing the the equations of motion for $A$ and the presymplectic structure $\Omega$.

Let me summarize. (1) Obtain fundamental local fields and their equations of motion. (2) Express the Poisson tensor and symplectic form in terms of local fields. (3) Introduce new fields to make the expression for the (pre)symplectic form local. (4) Obtain local action principle in the new fields. Note that gauge symmetry and all the issues associated with it appear precisely in step (3). In my limited understanding of it, the literature on AQFT has spent a significant amount of time on step (1), but perhaps not enough time on steps (2) and (3) even to formulate these problems precisely.

Finally, I should emphasize that the idea that redundant gauge degrees of freedom are introduced principally to give local structure to the (pre)symplectic structure on phase space is somewhat speculative. But it seems to fit in the field theories I am familiar with and I've not been able to identify a different yet equally competitive one.

This post has been migrated from (A51.SE)