mathlib-prs

Staging area for MendozaLab-authored Lean 4 contributions to mathlib4. Each subdirectory is a self-contained Lake project pinned to a specific Mathlib release, where individual contributions are developed and tested before upstream submission to the leanprover-community/mathlib4 repository.

Repository status

This repository holds in-development Lean 4 formal contributions. Each subdirectory is a standalone Lake project that targets a specific Mathlib version.

Contributions are staged in two phases:

• Proof architecture: Declarations with explicit axioms (cited to literature) and placeholder bodies. Axioms are used when supporting Mathlib infrastructure (e.g., matrix polar decomposition, CFC lemmas) has not yet landed. These files pass a local compilation gate and document their unproven claims transparently.

• Complete formal proof: All declarations closed (no axioms, no sorry). These files pass compilation and are ready for upstream submission.

Each subdirectory's own README documents its specific scope, axiom inventory, and compilation status.

Active drafts

Subdirectory	Mathlib pin	Target path	Build	Scope	Status
uhlmann-fidelity	v4.27.0	Mathlib/Analysis/Quantum/UhlmannFidelity.lean	PASS	1 definition + 4 proven theorems + 6 placeholder theorems with literature citations	Staged, not yet submitted
cfc-matrix-commutation	v4.27.0	Mathlib/LinearAlgebra/Matrix/CFCCommute.lean	PASS	2 matrix-specific corollaries of IsSelfAdjoint.commute_cfcHom (prerequisite for uhlmann-fidelity)	Staged, not yet submitted
frobenius-inner-product	v4.27.0	Mathlib/LinearAlgebra/Matrix/FrobeniusInner.lean	PASS	1 definition + 7 proven theorems + Cauchy-Schwarz lifting + InnerProductSpace ℂ instance on Matrix n n ℂ	Staged, not yet submitted
koopman-operator	v4.27.0	Mathlib/Dynamics/Ergodic/Koopman.lean	Pending first build	1 definition + 5 theorems for the Koopman operator U_T f = f ∘ T on L² of a measure-preserving system; foundational object for ergodic theory and Koopman–von Neumann theory	Scaffolded, not yet submitted
delay-coordinate-map	v4.27.0	Mathlib/Dynamics/DelayCoordinateMap.lean	Pending first build	1 definition + 3 theorems for the delay-coordinate map x ↦ (φ(x), φ(Tx), …, φ(Tⁿx)); named object underlying Takens 1981 (embedding theorem itself out of scope)	Scaffolded, not yet submitted

Building locally

Each subdirectory is self-contained. To build:

cd <subdirectory>
lake update    # one-time; downloads pinned Mathlib (~2–5 GB)
lake build     # subsequent builds use cached build artifacts

The lake update step downloads the pinned Mathlib version (specified in lean-toolchain). This may take 2–5 minutes and 2–5 GB of disk space on first run. Subsequent builds reuse cached artifacts and are much faster.

Submission protocol

Contributions move through the following stages before upstream submission:

1. Compilation gate: The file must pass lake build against its pinned Mathlib version with no errors. Axioms and sorry placeholders are acceptable at this stage.

2. Axiom inventory and audit: Every axiom must carry an explicit comment naming the external theorem, authors, and publication reference. The axiom's mathematical content must be stated fully and accurately.

3. Tactic realism check: For any tactic proof, confirm that the tactic can actually prove the stated result. Hidden axioms (tactics that claim to prove something they cannot) are not allowed.

4. Upstream submission: Convert axiom declarations to theorem ... := sorry with the reference comment preserved, if preferred by Mathlib reviewers. Open a PR against leanprover-community/mathlib4 with the file path mirroring the subdirectory layout under Mathlib/.

Conventions

• License: Apache License 2.0, matching Mathlib upstream. See LICENSE.
• Project layout: One self-contained Lake project per subdirectory. Each has its own lakefile.toml, lean-toolchain, and lake-manifest.json pinning specific versions.
• Version pinning: Mathlib versions are pinned per subdirectory (no shared toolchain). This allows independent update schedules and testing.
• Axioms in staging: Axioms are allowed and encouraged in staging files when supporting Mathlib infrastructure is not yet available. Mandatory rule: every axiom must have a citation comment.
• Build artifacts: .lake/ and lake-manifest.json changes are gitignored. Do not commit build artifacts.

Tooling

Files in this repository are prepared with assistance from Anthropic's Claude (Claude Code CLI) for proof drafting, Mathlib API search, and tactic iteration. All mathematical statements, axiom citations, and proof tactics are author-verified against Mathlib v4.27.0 source and the cited textbook references. The author is responsible for the final content.

Author

Kenneth A. Mendoza (MendozaLab)

License

Apache License 2.0 — see LICENSE.