Toward a Lean Formalization of Analog Computing with Microwaves

Matteo Nerini; Xuekang Liu; Bruno Clerckx

Home/Archive/arXiv

arXiv · 2610.04774

Toward a Lean Formalization of Analog Computing with Microwaves

Matteo Nerini·Xuekang Liu·Bruno Clerckx

View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

eess.SP cs.IT math.IT physics.app-ph

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Matteo Nerini, Xuekang Liu, Bruno Clerckx. 2026-10-03. Toward a Lean Formalization of Analog Computing with Microwaves. https://arxiv.org/abs/2610.04774

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

PyDPF: A Python Package for Differentiable Particle Filtering

State-space models (SSMs) are a widely used tool in time series analysis. In the complex systems that arise from real-world data, it is common to employ particle filtering (PF), an efficient Monte Carlo method for estimating the hidden state corresponding to a sequence of observations. Applying particle filtering requires specifying both the parametric form and the parameters of the system, which are often unknown and must be estimated. Gradient-based optimisation techniques cannot be applied directly to standard particle filters, as the filters themselves are not differentiable. However, several recently proposed methods modify the resampling step to make particle filtering differentiable. In this paper, we present an implementation of several such differentiable particle filters (DPFs) with a unified API built on the popular PyTorch framework. Our implementation makes these algorithms easily accessible to a broader research community and facilitates straightforward comparison between them. We validate our framework by reproducing experiments from several existing studies and demonstrate how DPFs can be applied to address several common challenges with state space modelling.

eess.SP↗

arXiv2026

Rigid Body Localization via Gaussian Belief Propagation with Quadratic Angle Approximation

Gaussian belief propagation (GaBP) is a technique that relies on linearized error and input output models to yield low-complexity solutions to complex estimation problems, which has been recently shown to be effective in the design of range-based GaBP schemes for stationary and moving rigid body localization (RBL) in three-dimensional (3D) space, as long as the relative rotation between the prior position and the target rigid body is sufficiently small. In this article we present a novel range-based RBL scheme via GaBP that relaxes the latter limitation significantly. To this end, the proposed method incorporates a quadratic angle approximation to linearize the relative orientation between the prior and the target rigid body, enabling high precision estimates of corresponding rotation angles even for large deviations. Leveraging the resulting linearized model, we derive the corresponding message-passing (MP) rules to obtain estimates of the translation vector and rotation matrix of the target rigid body, relative to a prior reference frame. Numerical results corroborate the good performance of the proposed angle approximation itself, as well as the consequent RBL performance in terms of root mean square errors (RMSEs) in comparison to the state-of-the-art (SotA), while maintaining a low computational complexity.

eess.SP↗

arXiv2026

Radar Intelligent Detection with Coarse-Grained Labels

Many deep learning based radar target detectors rely on range-cell level labels for training, which are expensive to obtain. To reduce the labeling burden, this paper presents a training strategy that uses only range-window level labels. Specifically, two sub-echoes are randomly cropped from the same window echo, resulting in a known relative shift between them. A siamese Transformer is then used to identify target-salient responses from one sub-echo and form pseudo labels, which are mapped to the paired sub-echo according to the known shift. In addition, a shift-equivariant consistency (SEC) constraint is imposed to align the predicted responses of the two sub-echoes after shift compensation. By exploiting shift priors within each labeled window, the proposed approach learns reliable detection without requiring cell-level labels. Experimental results show that it consistently surpasses classical constant false alarm rate (CFAR) detectors and achieves performance close to range-cell level labels training, while substantially reducing labeling cost.

eess.SP↗