Structural Completion Signatures

Abstract

A structural completion signature is the one-orbit quotient of the constrained zero-defect carrier, and a gauge-fixed completion constant is its sole value.

Theorem 1.1 (Completion points, signatures, and constants).

$$\begin{gathered} \forall G,A,D,\mathrm{Group}\left(G\right)\wedge \mathrm{MulAction}\left(G,A\right)\wedge (\forall g:G,a:A,a\in K\left(\mathcal{N},\Delta ,0_D\right)\Rightarrow \mathrm{smul}\left(g,a\right)\in K\left(\mathcal{N},\Delta ,0_D\right))\Rightarrow \\ (\forall a:A,a\in K\left(\mathcal{N},\Delta ,0_D\right)⟺(a\in \mathcal{N}\wedge \mathrm{Delta}\left(a\right)=0_D))\wedge \\ (\mathrm{HasStructuralCompletionSignature}\left(\mathcal{N},\Delta ,0_D\right)⟺\mathrm{Nonempty}\left(\mathrm{Unique}\left(\mathrm{CompletionSignature}\left(K\left(\mathcal{N},\Delta ,0_D\right),G\right)\right)\right))\wedge \\ (\forall R,S:\mathrm{Set}\left(R\right),\kappa :R,\mathrm{IsCompletionConstant}\left(S,\kappa \right)⟺S=\{\kappa \}). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/StructuralCompletionSignature.completion_vocabulary (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let N be the supplied normalization constraint, Delta the structural defect, and zero_D its distinguished zero. The completion carrier K consists exactly of the parameters in N with zero defect. It is implemented as Mathlib’s SubMulAction, so the displayed gauge stability premise is the closure needed to act on K.

The signature Sigma is Mathlib’s canonical orbitRel quotient K/G. The source’s one-orbit naming condition is represented by nonemptiness of K together with IsPretransitive G K. Mathlib’s exact pretransitive_iff_unique_quotient_of_nonempty theorem identifies that condition with Sigma carrying a Unique instance.

The completion-constant predicate contains both halves of uniqueness: kappa belongs to the gauge-fixed value set and every value in that set equals kappa. It is therefore equivalent to the fixed value set being the singleton containing kappa; an empty set cannot satisfy the predicate vacuously.

The unconditioned quotient is not forced to collapse: the Lean probes construct a two-point, gauge-stable completion carrier with two distinct orbit classes. Collapse occurs exactly after the nonempty pretransitive naming condition is supplied.

References

• Truth anchor: D5/S3/Observer/Completion/StructuralCompletionSignature.completion_vocabulary