Completion Point Intersection

Abstract

Paired zero-defect completion equals intersection of component completion conditions.

Theorem 1.1 (Paired vanishing is componentwise vanishing).

$$\begin{gathered} \forall first:X\to A,second:X\to B, \\ a0:A,b0:B,s:X,\mathrm{ZeroAt}\left(x\mapsto \mathrm{pair}\left(\mathrm{first}\left(x\right),\mathrm{second}\left(x\right)\right),\mathrm{pair}\left(a0,b0\right),s\right)⟺(\mathrm{ZeroAt}\left(first,a0,s\right)\wedge \mathrm{ZeroAt}\left(second,b0,s\right)). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Fix two defect readouts, their designated zero values, and a state.

The paired defect equals the paired zero exactly when each component defect equals its corresponding zero.

Theorem 1.2 (The paired zero set is the component intersection).

$$\begin{gathered} \forall first:X\to A,second:X\to B, \\ a0:A,b0:B,\mathrm{zeroSet}\left(x\mapsto \mathrm{pair}\left(\mathrm{first}\left(x\right),\mathrm{second}\left(x\right)\right),\mathrm{pair}\left(a0,b0\right)\right)=\mathrm{intersection}\left(\mathrm{zeroSet}\left(first,a0\right),\mathrm{zeroSet}\left(second,b0\right)\right). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Collect all states where the paired defect vanishes.

By componentwise pair equality, this set is exactly the intersection of the first and second zero sets.

References

• Truth anchor: D5/S3/Observer/CompletionPoints/CompletionPointIntersection.paired_zero_iff_component_zeros
• Truth anchor: D5/S3/Observer/CompletionPoints/CompletionPointIntersection.paired_zero_set_eq_intersection