Penrose — every real matrix has a unique Moore–Penrose inverse

Proved

LocalDistanceNetwork.moore_penrose_exists_unique

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

least-squareslinear-algebrastatistics

For every real matrix $M\in\mathbb R^{m\times k}$ there is exactly one matrix $P\in\mathbb R^{k\times m}$ satisfying the four Penrose equations

MPM=M,\qquad PMP=P,\qquad (MP)^{\mathsf T}=MP,\qquad (PM)^{\mathsf T}=PM .

This makes "the" Moore–Penrose inverse $M^{+}$ well defined, so that replacing $C^{-1}$ by $C^{+}$ in Eq. (B.1) for a singular covariance matrix $C$ is an unambiguous prescription.

Preamble

import Mathlib
import Definitions.Def_LocalDistanceNetwork_GLS

open Matrix

Formal statement

namespace LocalDistanceNetwork
theorem moore_penrose_exists_unique {m k : Type*} [Fintype m] [Fintype k]
    (M : Matrix m k ℝ) :
    ∃! P : Matrix k m ℝ, IsMoorePenroseInverse M P := by sorry
end LocalDistanceNetwork

Source

H0DN Collaboration (S. Casertano et al.), The Local Distance Network: A community consensus report on the measurement of the Hubble constant at ~1% precision, A&A 708, A166 (2026), https://doi.org/10.1051/0004-6361/202557993, Appendix B (p. 34) and Appendix B.2 (pp. 34-35), Eqs. (B.1)-(B.2)

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph