Gauge Stable Zero Defect

Abstract

Gauge-invariant normalization and defect data preserve completion status.

Theorem 1.1 (Gauge transport preserves completion).

$$\begin{gathered} \forall normalize:X\to N,target:N,defect:X\to D, \\ zero:D,gauge:X\to X,x:X, \\ ((\forall x:X,\mathrm{normalize}\left(\mathrm{gauge}\left(x\right)\right)=\mathrm{normalize}\left(x\right))\wedge (\forall x:X,\mathrm{defect}\left(\mathrm{gauge}\left(x\right)\right)=\mathrm{defect}\left(x\right)))\Rightarrow (\mathrm{CompletedAt}\left(normalize,target,defect,zero,x\right)⟺\mathrm{CompletedAt}\left(normalize,target,defect,zero,\mathrm{gauge}\left(x\right)\right)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/CompletionPoints/GaugeStableZeroDefect.gauge_preserves_completion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume a gauge transformation preserves both normalization and defect values at every state.

For a fixed normalization target, defect zero, and state, the two invariances transport both conjuncts of completion in either direction.

The equivalence is pointwise; invertibility of the gauge map is not assumed.

Theorem 1.2 (Defect invariance preserves zero defect).

$$\forall x2\in \left(\forall x2\in \cdot ,\cdot \right),\forall x3\in \cdot ,\forall x4\in \left(\forall x4\in \cdot ,\cdot \right),\left(\forall x5\in \cdot ,x2\left(x4\left(x5\right)\right)=x2\left(x5\right)\right)\Rightarrow \left(\forall x6\in \cdot ,x2\left(x6\right)=x3\iff x2\left(x4\left(x6\right)\right)=x3\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/CompletionPoints/GaugeStableZeroDefect.gauge_preserves_zero_defect (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume only that the defect value is invariant under the gauge map at every state.

At a fixed state, equality to the designated zero is then equivalent before and after gauge transport.

References

• Truth anchor: D5/S3/Observer/CompletionPoints/GaugeStableZeroDefect.gauge_preserves_completion
• Truth anchor: D5/S3/Observer/CompletionPoints/GaugeStableZeroDefect.gauge_preserves_zero_defect