Formalized Proof of Randomstrasse 101 19(a) in Lean

This repository contains a Lean 4 formalization of a proof about Randomstrasse 101 19(a).

File structure

The proof is divided into numbered files in PhaseRetrieval/:

_00_Core.lean
_01_Lemma31.lean
_02_Slice.lean
_03_NullCone.lean
_04_Lemma41.lean
_05_Lemma51.lean
_06_Lemma52.lean
_07_Proposition53.lean
_08_Lemma61.lean
_09_ProbTrans.lean

The root file PhaseRetrieval.lean only imports the final module which completes the proof. The pdf file ProofOnly.pdf contains a rough proof of the conjecture. OriginalReport_EN.pdf and OriginalReport_CN.pdf are the original reports in differnent languages generated by Qiushi Engine on June 2, 2026.

What is formalized?

The project verifies the main ingredients of the proof:

• a Hermitian-matrix criterion for failure of injectivity;
• the tangent space at the diagonal matrix Q0 = diag(1, -1, 0, ..., 0);
• the slice Sigma and its tangent space;
• the null cone and its separation property;
• the real dimension 4M - 5 of the tangent space of the slice;
• the construction of an open set of non-injective measurement matrices;
• the resulting probability statement for Gaussian measurement matrices;
• a transfer of the probability statement to the Grassmannian model.

Building the project

The project uses Lean 4.32.0. From the repository root, run:

lake build

The complete project currently builds without sorry, admit, or custom axiom declarations.