The geometry of a low-rank posterior.
Three results that explain why a distribution over low-rank factors induces a singular distribution over weight matrices.
The induced posterior stays in the low-rank set.
This holds for every factor law, including dependent and discrete distributions.
Proof. The rank of a product is at most the rank of its first factor, and $A$ has $r$ columns. Thus every factor pair maps into $\mathcal R_r$. Its pushforward assigns probability one to that set.
Inspect the Lean proofThe low-rank set has zero ambient volume.
The condition is essential: if $r\ge\min(m,n)$, every $m$-by-$n$ matrix already has rank at most $r$.
Proof. Every $(r+1)$-by-$(r+1)$ minor vanishes on $\mathcal R_r$. Choose the leading minor: its determinant is a nonzero polynomial, as an identity block makes it equal to one. The formalization proves that a nonzero polynomial has a Lebesgue-null zero set by induction on its number of variables, using finite univariate root sets and Fubini's theorem. The low-rank set is contained in this null set.
Inspect the Lean proofThe induced posterior is singular to Lebesgue measure.
All posterior mass lies on a set that has zero Lebesgue measure in the full weight space.
Proof. The zero set of the chosen minor is closed, hence measurable. Its Lebesgue measure is zero, while its complement has zero induced-posterior measure. These two sets witness mutual singularity. The Lean theorem actually establishes this for any measure on the factor space, without requiring total mass one.
Inspect the Lean proofVerification and source
Build and axiom audit passed. All 39 project declarations use only Lean's standard axioms.
The scope is these three statements and the helper lemmas used to prove them; the paper's other theorems and empirical claims are outside this formalization.
| Lean | leanprover/lean4:v4.33.0-rc1 |
|---|---|
| Mathlib | 9944fe2973b8dc0b86949101ed98232c07cd54a0 |
Build instructions and file list / Browse the complete proof / Verification record
Download the project files
lake exe cache get
lake build
lake env lean Audit.lean