Physlib: The Lean Physics Library

The repository contains two distinct tiers for contributions:

Physlib

This is the main library. It has high review standards to ensure content is curated, reusable, and readable. It contains formalized physics results (definitions, theorems, lemmas, calculations) organized by physics topic, including tactics, notation, and syntax.

PhyslibAlpha

PhyslibAlpha sits downstream of Physlib and has lower review standards. It is intended for:

• Large Pull Requests
• AI-generated content
• Formalizations that are not yet perfect

Requirements for PhyslibAlpha PRs:

1. Must pass basic linter checks.
2. Must undergo a 'one-look' review to ensure content is mainstream physics, looks reasonable (no axioms, easy to read), and is placed in the correct location mirroring its place in Physlib.

Note: Because of the lower review bar, contributions to PhyslibAlpha may not be maintained if they break.

The location field tells readers and the linter exactly where declarations live.

Grammar

Use the format: FILE_PATH (NAME1, NAME2, ...).

Rules

• File Path: Use the exact repo-relative path ending in .lean.
• Declaration Names: List the exact names as they appear in the source (e.g., deriv_smul, Time.deriv).
• Instance Types: Name the class applied to arguments (e.g., AddCommGroup Time, InnerProductSpace ℝ (Space d)).
• Typed Declarations: Include the signature after a colon (e.g., slice : Space d.succ ≃L[ℝ] ℝ × Space d). The name before the colon is what is checked.
• Notations: Prefix with notation (e.g., notation ∂ₜ) or use the bare glyph (e.g., ⨯ₑ₃).
• Multiple Files: If one requirement spans multiple files, separate them with a semicolon ;.
• Unimplemented Work: For planned requirements (done: false), set location: N/A.

# Single file
location: "Physlib/SpaceAndTime/Time/Basic.lean (Time, AddCommGroup Time, toRealCLM)"

# Multiple files using semicolon
location: "Physlib/SpaceAndTime/Space/Module.lean (Norm, InnerProductSpace ℝ (Space d)); Physlib/SpaceAndTime/Space/Basic.lean (Dist, MetricSpace)"

# Multi-line block scalar for long lists
location: |
  Physlib/QuantumMechanics/Operators/Position.lean (positionCLM, notation 𝐱); Physlib/QuantumMechanics/Operators/Momentum.lean (momentumCLM, notation 𝐩)

In Lean, MState types are right-associative (e.g., MState (dA × dB × dC) is MState (dA × (dB × dC))). This means partial traces only act on the outermost split. To access different bipartitions (like dA × dC vs dB), you must use explicit permutation functions to rearrange the subsystems.

SWAP

Exchanges two subsystems.

• SWAP: def SWAP (ρ : MState (d₁ × d₂)) : MState (d₂ × d₁) := ρ.relabel (Equiv.prodComm d₁ d₂).symm
• Properties: Involutive (ρ.SWAP.SWAP = ρ), and swaps the behavior of traceLeft and traceRight.

Associators

Changes the grouping of a tripartite system.

• assoc: def assoc (ρ : MState ((d₁ × d₂) × d₃)) : MState (d₁ × d₂ × d₃) := ρ.relabel (Equiv.prodAssoc d₁ d₂ d₃).symm
• assoc': def assoc' (ρ : MState (d₁ × d₂ × d₃)) : MState ((d₁ × d₂) × d₃) := ρ.SWAP.assoc.SWAP.assoc.SWAP

Workflow Example: Computing Conditional Entropy $S(A|C)$

If you have $\rho_{ABC}$ and need to compute entropy of $A$ given $C$ (ignoring $B$), you cannot trace $B$ directly if $B$ is not the outermost subsystem.

1. Use SWAP and assoc to rearrange the state so $A$ and $C$ are adjacent.
2. Apply partial traces to obtain $\rho_{AC}$.
3. Compute the entropy on the resulting state.

In QuantumInfo, quantum channels are modeled as MatrixMap types rather than maps on states. A MatrixMap A B R is a linear map from $A imes A$ matrices to $B imes B$ matrices over a semiring $R$.

Choi Matrix Representation

Every MatrixMap can be converted to and from a Choi matrix:

• choi_matrix (M : MatrixMap A B R): Returns a matrix of size $(B imes A) imes (B imes A)$.
• of_choi_matrix (M : Matrix (B × A) (B × A) R): Constructs a map from a Choi matrix.

Kraus Representation

You can construct a map from Kraus operators using:

• of_kraus (M N : κ → Matrix B A R): Constructs the map $X \mapsto \sum_k M_k X N_k^\dagger$.

Duality

The adjoint map with respect to the Hilbert-Schmidt inner product is obtained via dual:

• dual (M : MatrixMap A B 𝕜) : MatrixMap B A 𝕜
• Property: $\text{Tr}[M(X) Y] = \text{Tr}[X M^\text{.dual}(Y)]$.

abbrev MatrixMap (A B R : Type*) [Semiring R] := Matrix A A R →ₗ[R] Matrix B B R

-- Example conversion functions:
def choi_matrix (M : MatrixMap A B R) : Matrix (B × A) (B × A) R
def of_choi_matrix (M : Matrix (B × A) (B × A) R) : MatrixMap A B R
def of_kraus (M N : κ → Matrix B A R) : MatrixMap A B R
def dual (M : MatrixMap A B 𝕜) : MatrixMap B A 𝕜

Instead of working with raw MatrixMap types and manually checking propositions, QuantumInfo provides bundled structures that combine a map with proofs of its properties. This allows for more type-safe quantum programming.

Hierarchy of Bundled Maps

• HPMap: Hermitian Preserving.
• PMap: Positive (extends HPMap).
• CPMap: Completely Positive (extends PMap).
• TPMap: Trace Preserving.
• PTPMap: Positive and Trace Preserving.
• PUMap: Positive and Unital.
• CPTPMap: Completely Positive and Trace Preserving (the standard representation for a Quantum Channel).
• CPUMap: Completely Positive and Unital.

Working with CPTPMaps (Quantum Channels)

CPTPMap dIn dOut is the primary object for quantum channels. It supports:

• Identity: CPTPMap.id
• Composition: M₂ ∘ₘ M₁ (sequential)
• Tensor Product: M₁ ⊗ₖ M₂ (parallel)
• Function-like application: You can apply a channel directly to a state: Λ ρ where ρ : MState dIn.

structure CPTPMap extends PTPMap dIn dOut, CPMap dIn dOut

-- Common channel examples:
-- of_unitary (U : Matrix.unitaryGroup d ℂ)
-- replacement (σ : MState dOut)
-- SWAP : CPTPMap (d₁ × d₂) (d₂ × d₁)
-- traceLeft : CPTPMap (d₁ × d₂) d₂

The library represents pure quantum states using basis-dependent vectors (d → ℂ) rather than abstract Hilbert spaces. This is chosen because the computational basis is canonical in quantum information and simplifies the connection to matrices.

Ket Vectors

Ket d represents a normalized quantum state (unit vector in ℂᵈ).

• Notation: |ψ〉
• Tensor Product: ψ₁ ⊗ᵠ ψ₂ (via Ket.prod)
• Uniform Superposition: uniform_superposition (the state |+⟩ = (1/√d) ∑ᵢ |i⟩)

Bra Vectors

Bra d is defined identically to Ket d but represents the conjugate transpose.

• Notation: 〈ψ∣
• Conversion: Use Ket.to_bra or Bra.to_ket for componentwise conjugation.

Inner Product

To compute the inner product between a bra ξ and a ket ψ, use dot ξ ψ (notation 〈ξ‖ψ〉).

Note: This is a 'mixed' form that does not automatically conjugate. To get the standard inner product ⟨φ|ψ⟩, use 〈φ.to_bra‖ψ〉.

structure Ket (d : Type*) [Fintype d] where
  vec : d → ℂ
  normalized' : ∑ x, ‖vec x‖ ^ 2 = 1

structure Bra (d : Type*) [Fintype d] where
  vec : d → ℂ
  normalized' : ∑ x, ‖vec x‖ ^ 2 = 1

def dot (ξ : Bra d) (ψ : Ket d) : ℂ := ∑ x, (ξ x) * (ψ x)