Completion Locus Calculus

Abstract

Structural completion loci compose by intersection, pull back along arbitrary parameter maps, and retain gauge stability under conjunction.

Theorem 1.1 (Completion Locus Pair eq Inter).

$\forall A : T y p e, D_{1} : T y p e, D_{2} : T y p e, n or ma l i z a t i o n_{1} : S e t A, n or ma l i z a t i o n_{2} : S e t A, d e f ec t_{1} : A \to D_{1}, d e f ec t_{2} : A \to D_{2}, zer o_{1} : D_{1}, zer o_{2} : D_{2}, (co m pl e t i o n P o in tS e t (n or ma l i z a t i o n_{1} in t ersec t i o nn or ma l i z a t i o n_{2}) (λa \mapsto (d e f ec t_{1} a, d e f ec t_{2} a)) (zer o_{1}, zer o_{2}) = co m pl e t i o n P o in tS e t n or ma l i z a t i o n_{1} d e f ec t_{1} zer o_{1} in t ersec t i o n co m pl e t i o n P o in tS e t n or ma l i z a t i o n_{2} d e f ec t_{2} zer o_{2}) .$

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

Source. Repository-derived.

Commentary.

Conjoining two normalizations and pairing their defects gives exactly the intersection of their completion loci.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.2 (Completion Locus Preimage).

$\forall A : T y p e, A^{'} : T y p e, D : T y p e, p a r am e t er M a p : A^{'} \to A, n or ma l i z a t i o n : S e t A, d e f ec t : A \to D, zeroD : D, (co m pl e t i o n P o in tS e t (p a r am e t er M a p^{- 1} n or ma l i z a t i o n) (d e f ec t \circ p a r am e t er M a p) zeroD = p a r am e t er M a p^{- 1} (co m pl e t i o n P o in tS e t n or ma l i z a t i o n d e f ec t zeroD)) .$

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

Source. Repository-derived.

Commentary.

Completion loci pull back exactly along arbitrary parameter maps.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.3 (Completion Locus Intersection Gauge Stable).

$\forall G : T y p e, A : T y p e, D_{1} : T y p e, D_{2} : T y p e, n or ma l i z a t i o n_{1} : S e t A, n or ma l i z a t i o n_{2} : S e t A, d e f ec t_{1} : A \to D_{1}, d e f ec t_{2} : A \to D_{2}, zer o_{1} : D_{1}, zer o_{2} : D_{2}, [Group (G)], [MulAction (G, A)], (\forall (g : G) {a : A}, a \in co m pl e t i o n P o in tS e t n or ma l i z a t i o n_{1} d e f ec t_{1} zer o_{1} \Rightarrow g \cdot a \in co m pl e t i o n P o in tS e t n or ma l i z a t i o n_{1} d e f ec t_{1} zer o_{1}) \land (\forall (g : G) {a : A}, a \in co m pl e t i o n P o in tS e t n or ma l i z a t i o n_{2} d e f ec t_{2} zer o_{2} \Rightarrow g \cdot a \in co m pl e t i o n P o in tS e t n or ma l i z a t i o n_{2} d e f ec t_{2} zer o_{2}) \Rightarrow (\forall (g : G) {a : A}, a \in co m pl e t i o n P o in tS e t (n or ma l i z a t i o n_{1} in t ersec t i o nn or ma l i z a t i o n_{2}) (λ v a l u e \mapsto (d e f ec t_{1} v a l u e, d e f ec t_{2} v a l u e)) (zer o_{1}, zer o_{2}) \Rightarrow g \cdot a \in co m pl e t i o n P o in tS e t (n or ma l i z a t i o n_{1} in t ersec t i o nn or ma l i z a t i o n_{2}) (λ v a l u e \mapsto (d e f ec t_{1} v a l u e, d e f ec t_{2} v a l u e)) (zer o_{1}, zer o_{2})) .$

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

Source. Repository-derived.

Commentary.

If two completion loci are stable under the same gauge action, their conjoined locus is stable as well.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

References

Truth anchor: D5/S3/Observer/Completion/CompletionLocusCalculus.completion_locus_intersection_gauge_stable
Truth anchor: D5/S3/Observer/Completion/CompletionLocusCalculus.completion_locus_pair_eq_inter
Truth anchor: D5/S3/Observer/Completion/CompletionLocusCalculus.completion_locus_preimage
Dependency: D5/S3/Observer/Completion/StructuralCompletionSignature

Keyboard shortcuts

trureturing Blueprint

Completion Locus Calculus

Abstract

References