Formal proof of which microwave networks compute transforms including DFT
Toward a Lean Formalization of Analog Computing with Microwaves
Information Theory
Summary
Computers can use microwave signals to do certain math operations by passing signals through microwave components. This paper shows which kinds of mathematical transformations can be done using these networks made of couplers and phase shifters. The authors use a computer program called Lean to write down the rules and then prove these results mechanically, so no mistakes creep in. They also prove the well-known discrete Fourier transform can be done this way for sizes that are powers of two.
What this means in practice
- •For microwave engineers: Know exactly which linear transformations can be implemented with networks of couplers and phase shifters backed by formal proofs.
- •For hardware system designers: Design analog microwave computing systems with confidence that certain transformations like DFT are implementable at scale powers of two.
A theory result. No direct application yet.
Authors
Matteo Nerini, Xuekang Liu, Bruno Clerckx
Abstract
Analog computing with microwave signals can perform linear transformations directly in the analog domain, as the signals propagate through a microwave network. A fundamental question is which transformations can be computed with a given set of microwave components. In our previous work, we answered this question for networks of hybrid couplers and phase shifters by deriving a necessary and sufficient condition on the transformations these networks can compute, and we showed that the discrete Fourier transform (DFT) satisfies it. In this paper, we take a first step toward the formalization of analog computing with microwaves in Lean, a programming language and proof assistant that is increasingly adopted in mathematics. We formalize the considered components, their series and parallel connections, and the class of networks they can implement. Then, we formally prove the necessary and sufficient condition characterizing these networks, as well as the implementability of the DFT of any size power of two. All proofs are checked by the Lean kernel, and the code is openly available at: https://github.com/matteonerini/formalizing-analog-computing.