Zero-Sum Gauge Invariance

Abstract

A zero-sum local gauge shift leaves the global completion sum unchanged.

Theorem 1.1 (Zero-sum shifts preserve the global sum).

$$\forall V:\mathrm{Type},localContribution,shift:V\to \mathbb{R},\mathrm{Summable}(localContribution)\wedge \mathrm{Summable}(shift)\wedge {\sigma }_{v}shift(v)=0\Rightarrow {\sigma }_v(localContribution(v)+shift(v))={\sigma }_{v}localContribution(v).$$

Proof. Machine-checked in Lean as D5/S3/AnalyticClosure/ZeroSumGaugeInvariance.zero_sum_gauge_invariance (✓ std3). ∎

Source. Repository-derived.

Commentary.

The local ledger is represented by an absolutely summable real family localContribution, and shift is another absolutely summable family. When the shift sums to zero, replacing each local term by localContribution plus shift preserves the global sum.

References

• Truth anchor: D5/S3/AnalyticClosure/ZeroSumGaugeInvariance.zero_sum_gauge_invariance