Congruence Kernel Sensor Fusion

Abstract

Forward-congruence completion commutes with arbitrary sensor intersections.

Theorem 1.1 (Congruence kernel commutes with sensor intersections).

$$\begin{gathered} \forall tau:Y\to Y,R:I\to \mathrm{StateRelation}\left(Y\right), \\ \mathrm{congruenceKernel}\left(tau,\mathrm{iInter}\left(i\mapsto R\left(i\right)\right)\right)=\mathrm{iInter}\left(i\mapsto \mathrm{congruenceKernel}\left(tau,R\left(i\right)\right)\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Refinement/CongruenceKernelSensorFusion.congruence_kernel_iInter (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix a state endomorphism and an arbitrary indexed family of state relations.

Membership in the congruence kernel of the intersection means that every iterate lies in every sensor relation.

Exchanging the universal quantifiers over iterates and sensor indices gives the intersection of the individual congruence kernels. No finiteness of the sensor index is required.

References

• Truth anchor: D5/S3/Observer/Refinement/CongruenceKernelSensorFusion.congruence_kernel_iInter
• Dependency: D5/S3/Observer/Separation/CongruenceKernel