Formalization of Complex Vectors in Higher-Order Logic

TL;DR

This paper introduces a higher-order-logic formalization of complex vector spaces within HOL Light, enabling rigorous analysis of electromagnetic phenomena and the proof of physical laws.

Contribution

It extends HOL Light with a formalized complex vector space, integrating complex analysis and real vector theorems for advanced physical modeling.

Findings

Formalization of complex vectors in HOL Light

Application to electromagnetic field analysis

Proof of the law of reflection for planar waves

Abstract

Complex vector analysis is widely used to analyze continuous systems in many disciplines, including physics and engineering. In this paper, we present a higher-order-logic formalization of the complex vector space to facilitate conducting this analysis within the sound core of a theorem prover: HOL Light. Our definition of complex vector builds upon the definitions of complex numbers and real vectors. This extension allows us to extensively benefit from the already verified theorems based on complex analysis and real vector analysis. To show the practical usefulness of our library we adopt it to formalize electromagnetic fields and to prove the law of reflection for the planar waves.