Papers With

← All papers
First page of A complex-analytic proof of square-restricted stable phase retrieval in Fock space

A complex-analytic proof of square-restricted stable phase retrieval in Fock space

Cynthia Bortolotto, João P. G. Ramos

math.CV Aug 26, 2026 · v1 math.AP math.CA math.FA
formalization analysis
Read PDF arXiv abstract Code
TL;DR
Every result, including the coercivity inequality and stable phase retrieval theorem in Fock space, was formalized and kernel-checked in Lean 4 against Mathlib.
Abstract
We give a short complex-analytic proof of a square-restricted form of local stable phase retrieval at the Gaussian in one-dimensional Fock space. The main estimate is a coercivity inequality for the map $F\mapsto F^2$: \[ \|F^2-F(0)^2|_{\mathcal{F}^2(\mathbb{C})} \lesssim \inf_{c\in\mathbb{R}}\||F|^2-c\|_{L^2(d γ)}. \] The proof uses a weighted derivative norm, two integrations by parts, and a weighted Cauchy inequality. The proof has been completely verified in Lean with the aid of Large Language Models.
Problem

Establishing a square-restricted form of local stable phase retrieval at the Gaussian in one-dimensional Fock space. The goal is a coercivity inequality for the map F↦F² in the natural Fock-space topology.

Approach

After the Bargmann–Fock reduction, an entirely complex-analytic argument is used. It removes the constant mode via a weighted derivative-norm equivalence, converts the modulus defect into a gradient energy, and closes the estimate with weighted Cauchy integral bounds and two integrations by parts. All definitions, lemmas, and theorems were formalized in Lean 4 (v4.30.0) against Mathlib, with the Fock norm interpreted as a Gaussian L² norm.

Results

The coercivity inequality ‖F²−F(0)²‖ ≲ inf_c ‖|F|²−c‖ is proved and fully verified in Lean, with no sorry, admit, or extra axioms beyond propext, Classical.choice, and Quot.sound.