Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A Neumann Coulomb-gauge correction by contraction

Statement

Assume full AC and work on the closed Euclidean unit ball in four dimensions. Use sums of Lp norms of Euclidean ordered derivative tensors for Sobolev norms; these are equivalent to the cited scalar Sobolev norms and invariant under orthogonal coordinate changes. Let X be the mean-zero W2,3 closure of su(2)-valued polynomials with zero normal derivative on the sphere. Let Y be the W1,3 closure of smooth su(2)-valued one-forms with zero normal component on the sphere. Let GN be the W2,3 closure of smooth maps to SU(2) with zero normal derivative on the sphere.

There exist fixed positive constants ρ,η,δ,C such that, if a∈Y satisfies d∗a=0, ∥a∥4≤ρ, and λ∈Y satisfies ∥λ∥W1,3≤δ, there exists u∈X, unique among ∥u∥W2,3≤η, such that h=eu∈GN and b=h−1dh+h−1(a+λ)h∈Y,d∗b=0. Moreover ∥u∥W2,3≤C∥λ∥W1,3,∥b−a∥W1,3≤C(1+∥a∥W1,3)∥λ∥W1,3. All constants are independent of the higher norm of a.

Given a finite Γ≤O(4) and an action τ of Γ on SU(2) by constant unitary conjugations, suppose γ∗a=dτγ(a) and γ∗λ=dτγ(λ). Then u(γx)=dτγ(u(x)) and h(γx)=τγ(h(x)). A representation into PU(2) supplies such a conjugation action; no lift of that representation to SU(2) is required.

Facts & Assumptions

[F1]

The constructed inverse S for −Δ maps L03 boundedly onto the complete normalized space X, with ∥Sf∥W2,3≤KN∥f∥3. It preserves prescribed finite orthogonal equivariance (A strong Lp Neumann inverse on four-dimensional balls).

[F2]

Every R∈Y satisfies ∫d∗R=0, by the normal-boundary integration identity tested with constants (The normal-boundary Hodge estimate on four-dimensional balls).

[F3]

On the ball W2,3↪L∞ and ∥Dv∥12≤K∥v∥W2,3; also W1,3↪L12. These follow from the proved higher-order and first-order embeddings and the ball's extension property (Higher-order Sobolev embedding, Sobolev embedding on bounded extension domains for p<n, Bounded C^k domains admit integer-order Sobolev extension).

[F4]

Holder controls products and changes of exponent on the fixed ball. L3 is complete, smooth approximation is available, and a contraction on a nonempty complete metric space has a unique fixed point (Holder's inequality for integrals, including the endpoint cases, Riesz-Fischer completeness of Lp for 1≤p≤∞, Meyers–Serrin density on an arbitrary open set, A contraction of a nonempty complete metric space into itself has exactly one fixed point, the limit of the iterates from any starting point).

[F5]

Full AC is inherited through the analytic suppliers (The Axiom of Choice).

Proof

Given: Full AC and the classes X,Y,GN and data of the statement. All norms in this proof are on the fixed unit ball.

1.1F1F3F4constructalgebra

Sobolev matrix algebra and boundary approximation. By [F3]–[F4] and the weak product rule obtained by smooth approximation, ∥vw∥W2,3≤KA∥v∥W2,3∥w∥W2,3: the second-derivative cross terms obey ∥DvDw∥3≤∥Dv∥6∥Dw∥6, and [F3] controls both L6 norms. Similarly ∥cv∥W1,3+∥vc∥W1,3≤KA∥c∥W1,3∥v∥W2,3. Passing the derivative test identities to L3 limits proves completeness of the ambient Sobolev spaces from [F4]. The power series for eu therefore converges in W2,3, locally uniformly in that norm, and defines a continuously differentiable composition there; termwise differentiation is justified by the convergent exponential majorants. For u∈su(2) pointwise, u2=−s2I for a real s, so eu=cos⁡s I+(sin⁡s/s)u (with the continuous value at zero) is unitary with determinant one. Polynomial Neumann approximants to u∈X exponentiate to smooth SU(2) maps with zero normal derivative; continuity gives eu∈GN. Products of maps in GN remain in it, and inverse is matrix adjoint and hence continuous. Gauge transformation by such maps sends Y to Y, by approximating both inputs with smooth zero-normal inputs and using the above product estimates. Also du∈Y for u∈X.

2.1step 1.1algebra

The exact nonlinear remainder. Put h=eu and define R(u)=h−1dh−du+h−1(a+λ)h−a. By step 1.1, R(u)∈Y whenever u∈X. Let E(u)=e−ud(eu)−du. Differentiating the convergent matrix series, or integrating the series termwise, gives e−ud(eu)=∫01e−tu(du)etu dt, hence E(u)=A(u)du where A(0)=0 and A and its first two matrix derivatives are uniformly bounded for ∣u∣≤1. More precisely ∣A(u)∣≤C∣u∣ there. Thus R(u)=E(u)+(e−uaeu−a)+e−uλeu, with R(0)=λ.

3.1F3F4step 1.1step 2.1algebra

The quadratic differential term. Suppose ∥u∥W2,3,∥v∥W2,3≤η with η small enough that [F3] gives ∣u∣,∣v∣≤1. The formula in step 2.1 gives ∣d∗E(u)∣≤C(∣u∣∣D2u∣+∣Du∣2). Subtracting the two formulas, using bounded first and second derivatives of A, and applying [F3]–[F4] gives ∥d∗E(u)∥3≤C∥u∥W2,32 and ∥d∗(E(u)−E(v))∥3≤Cη∥u−v∥W2,3. Indeed terms with two first derivatives use L6⋅L6⊂L3, while a second derivative is paired with an L∞ factor; differences of coefficients are bounded by C∣u−v∣, and the resulting terms use the same two estimates. These formulas hold for the Sobolev classes by the smooth approximation and product continuity of step 1.1.

4.1F3F4step 1.1step 2.1step 3.1algebra

The critical Coulomb coefficient and the perturbation. In d∗(e−uaeu−a) the term e−u(d∗a)eu−d∗a vanishes. Only derivatives falling on the exponentials remain, so their pointwise norm is at most C∣a∣∣Du∣ for ∣u∣≤1. Subtracting at u,v gives at most C∣a∣(∣D(u−v)∣+∣u−v∣(∣Du∣+∣Dv∣)). By L4⋅L12⊂L3, this gives a difference bound C∥a∥4∥u−v∥W2,3 when η≤1. The contracted derivative of e−uλeu consists of e−u(d∗λ)eu and terms bounded by C∣λ∣∣Du∣. The same subtraction, [F3] and Holder give a difference bound C∥λ∥W1,3∥u−v∥W2,3. Thus, after choosing one universal C0, the preceding estimates prove ∥d∗(R(u)−R(v))∥3≤C0(η+∥a∥4+∥λ∥W1,3)∥u−v∥W2,3. The cancellation of d∗a is why no higher norm of a occurs in this bound.

5.1F1F2F4step 2.1step 3.1step 4.1chooseconstructalgebra

A well-defined contraction, including compatibility. Define T(u)=S(−d∗R(u)) on the closed radius-η ball in X. Step 2.1 and [F2] show −d∗R(u)∈L03, so the Neumann solve is well defined for every iterate. Choose positive η,ρ so that η≤1, the L∞ restriction of step 3.1 holds, and KNC0(η+ρ)≤1/4. Then choose δ>0 so small that KNC0δ≤1/4 and KN∥d∗λ∥3≤η/4 whenever ∥λ∥W1,3≤δ; the latter follows from the fixed finite coefficient bound for d∗. For ∥a∥4≤ρ and such λ, step 4.1 gives contraction constant at most 1/2, and ∥T(0)∥W2,3≤η/4. Hence ∥T(u)∥W2,3≤3η/4 on that ball. It is a complete metric space by [F1] and the equivalence of its domain norm with W2,3.

6.1F1F4step 1.1step 2.1step 5.1constructalgebra

The correction and uniqueness. By [F4], uj+1=T(uj) starting at zero converges to the unique fixed point u in that ball. The equation −Δu=−d∗R(u) and d∗du=−Δu give d∗(du+R(u))=0. Since d∗a=0, the form b=a+du+R(u)=h−1dh+h−1(a+λ)h is Coulomb and belongs to Y by step 1.1. Conversely any u∈X in the stated ball for which b is Coulomb satisfies this same Neumann equation, so uniqueness of [F1] makes it a fixed point and thus this u. Also ∥u∥W2,3≤∥T(0)∥W2,3+12∥u∥W2,3≤KN∥d∗λ∥3+12∥u∥W2,3, giving the first quantitative bound.

7.1F3F4step 1.1step 6.1algebra

The correction size in the connection norm. The matrix power series and product estimates of step 1.1 imply ∥e−ud(eu)∥W1,3≤C∥u∥W2,3, ∥e−uaeu−a∥W1,3≤C∥a∥W1,3∥u∥W2,3, and ∥e−uλeu∥W1,3≤C∥λ∥W1,3 on the fixed small ball. For the middle bound, write e−uaeu−a=(e−u−1)aeu+a(eu−1); the terms with derivatives on a have a factor bounded by C∥u∥∞, and the other terms use L4⋅L12⊂L3. Adding the three bounds and using step 6.1 proves the claimed estimate for b−a, with C independent of ∥a∥W1,3.

8.1F1F5step 1.1step 2.1step 5.1step 6.1step 7.1algebra∎

Prescribed finite equivariance. Orthogonal pullback preserves the Laplacian, codifferential, means and all the domain norms. Constant unitary conjugation preserves matrix products, the Frobenius norm and the exponential. Therefore the transformation u(x)↦dτγ−1(u(γx)) preserves X and commutes with T when a,λ have the stated equivariance; this uses the equivariant inverse of [F1]. The zero starting iterate is invariant, so every iterate and its limit are invariant. Exponentiation gives the assertion for h. A central unitary scalar acts trivially by conjugation, which explains why a PU(2) action suffices. The existence, uniqueness, estimates and boundary compatibility are all supplied in steps 5.1–7.1; full AC is inherited as stated in [F5].

Source notes

The full exponential Neumann iteration in Tao–Tian, Proposition 9.2, Step 3 (PDF pp.38–39), was read. Here its linear solve is the constructed local strong Neumann inverse, and every iterate's mean-zero compatibility is proved through the normal approximation class. The nonlinear estimates exploit the critical L4 norm of the Coulomb coefficient, with its contracted derivative cancelling exactly. This lemma corrects nearby given Coulomb data; a subsequent scaling-path construction is needed to obtain a gauge from small curvature alone.

Depends on

Used by

Dependency tree · two levels

94 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources