Zero-Sum Gauge Invariance of the Structural Completion Signature

Abstract

A zero-sum redistribution preserves the global additive defect and the structural completion signature K(C)/G.

Theorem 1.1 (A zero-sum local gauge preserves the global defect and signature).

$$\begin{array}{r}{V}_f,V_{\infty }:Type,\mathrm{Nonempty}\left(V_f\right),\mathrm{Nonempty}\left(V_{\infty }\right)\\ D:Type,\mathrm{AddCommGroup}\left(D\right),\mathrm{TopologicalSpace}\left(D\right),\mathrm{IsTopologicalAddGroup}\left(D\right),T2Space\left(D\right)\\ V:=\mathrm{Sum}\left(V_f,V_{\infty }\right)=\mathrm{AdelicPlace}\left(V_f,V_{\infty }\right)\\ L:\mathrm{AdelicLocalLedger}\left(V_f,V_{\infty },D\right),\mathrm{Summable}\left(\mathrm{localContribution}\left(L\right)\right)\\ b:\mathrm{ZeroSumGauge}\left(V_f,V_{\infty },D\right),\mathrm{HasSum}\left(\mathrm{shift}\left(b\right),0\right)\\ {\Delta }_{glob}(L):=\sum _{v\in V}{L}_v\\ N(C)=\mathrm{AdelicLocalLedger}\left(V_f,V_{\infty },D\right)\\ K(C)=\{L\in N(C)\mid {\Delta }_{glob}(L)=0\}\\ G(C)=\mathrm{ZeroSumGauge}\left(V_f,V_{\infty },D\right),\Sigma (C)=K(C)/G(C)\\ \forall L,b,({\Delta }_{glob}(\mathrm{gaugeTransform}\left(L,b\right))=\sum _{v\in V}(L_v+b_v)=\sum _{v\in V}{L}_v={\Delta }_{glob}(L))\wedge \\ (\forall k:K(C),\mathrm{structuralCompletionSignatureClass}\left(\mathrm{gaugeTransformCompletionPoint}\left(k,b\right)\right)=\mathrm{structuralCompletionSignatureClass}\left(k\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Adelic/ZeroSumGaugeGlobalCompletion.zero_sum_gauge_preserves_global_completion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite and infinite place types are both nonempty, and their disjoint sum is the full place type. The defect codomain is any Hausdorff topological additive commutative group. An adelic local ledger is a summable family in that codomain, while ZeroSumGauge is the additive subgroup of summable shift families with total zero.

The normalization set N is the full ledger space. GlobalCompletionPoint is the subtype K(C) of normalized ledgers whose globalAdditiveDefect vanishes. Zero-sum gauges act on K(C), and StructuralCompletionSignature is the orbit quotient K(C)/G.

Summable.tsum_add proves that a gauge transform preserves globalAdditiveDefect, so it maps completion points to completion points. Quotient.sound then proves that every transformed completion point has the same structuralCompletionSignatureClass. These are the two conjuncts of the public theorem.

References

• Truth anchor: D5/S3/Analytic/Adelic/ZeroSumGaugeGlobalCompletion.zero_sum_gauge_preserves_global_completion