Hermitian coordinate space

A Hermitian coordinate space records exactly the entries of a finite complex Hermitian matrix that can be chosen freely:

• one real number at every diagonal position; and
• one complex number at every position strictly above the diagonal.

Nothing is independently chosen below the diagonal. Hermitian symmetry fills that entry by conjugating its reflected partner above the diagonal.

This is bookkeeping before probability enters. The coordinate space alone does not say that the coordinates are random, Gaussian, independent, or normalized in any particular way.

Start with one actual \(3\times3\) matrix

Use row and column labels \(0,1,2\). Supply the three real diagonal coordinates

and the three complex strict-upper coordinates

The phrase strict upper means that the row index is smaller than the column index. For size three, the complete list is

There are no other strict-upper positions.

Insert those six supplied coordinate objects into a matrix. Reflect each upper entry across the diagonal and conjugate it:

For example,

and

The diagonal entries are already real, so conjugating them changes nothing. Every entry therefore satisfies

which is the entrywise form of \(H^*=H\).

Recover the coordinates without solving anything

Read the diagonal and strict upper triangle of the assembled matrix:

These are exactly the supplied \(d\)- and \(u\)-coordinates. Recovery needs no averaging, division, or rescaling. The project currently exposes this fact through separate diagonal and upper-entry simplification theorems. It does not yet package the recovery operation and assembly as a named equivalence.

Count the real degrees of freedom

For an \(n\times n\) matrix, there are \(n\) diagonal positions. Each stores one real degree of freedom.

There are

strict-upper positions. Each stores a complex number, hence two real degrees of freedom. The total is

For \(n=3\), this is

The six named inputs in the example are not six real numbers. Three are real and three are complex, so they contain \(3+6=9\) real scalar components. This matches the real dimension of the vector space of \(3\times3\) complex Hermitian matrices.

The dimension count is mathematical context for the representation. The current project module defines the coordinate type and forward assembler, but does not yet prove a named real-dimension theorem.

Near-miss: counting the lower triangle twice

Suppose someone records the diagonal as real but treats all six off-diagonal positions as independent complex inputs. The storage count becomes

real scalar slots instead of \(9\).

This creates two possible failures:

1. If the lower values are genuinely independent choices, the result is usually not Hermitian. In the example, choosing \(\ell_{10}=7+i\) conflicts with \(\overline{u_{01}}=1-2i\).
2. If constraints \(\ell_{ji}=\overline{u_{ij}}\) are imposed afterward, the representation can describe a Hermitian matrix, but it stores six redundant real scalar components and carries extra consistency proofs.

The lower triangle is not missing data. It is already encoded in the upper triangle.

There is another tempting construction. Start with an upper-triangular matrix \(X\) and form \(X+X^*\). This always produces a Hermitian matrix, but if the diagonal of \(X\) is the supplied real vector \(d\), then

The diagonal has been doubled. Dividing the whole result by two would also halve the supplied upper entries. The project’s direct three-branch assembler inserts every coordinate unchanged and keeps later normalization choices visible.

The abstract coordinate space

Let

The project uses

A point \(x=(d,u)\in\mathcal C_n\) is a pair of functions. The first function answers, “what real value belongs at diagonal index \(i\)?” The second answers, “what complex value belongs at strict-upper pair \((i,j)\)?”

The adjective strict matters. If the upper index set also contained the diagonal, those diagonal coordinates would be complex and an extra condition would be needed to force their imaginary parts to zero. A separate real diagonal makes the constraint true by the type itself.

In Lean: the coordinate point

x : NonlinearDynamics.Random.HermitianCoordinateSpace 3

The exact project definitions are short enough to read directly:

def StrictUpperIndex (n : ℕ) := {ij : Fin n × Fin n // ij.1 < ij.2}

abbrev HermitianCoordinateSpace (n : ℕ) :=
  (Fin n → ℝ) × (StrictUpperIndex n → ℂ)

In the first line, braces form a subtype: a pair ij is admitted only together with a proof of ij.1 < ij.2. That proof prevents a diagonal or lower pair from being used as an upper-coordinate key.

In Lean: assemble and certify Hermiticity

On paper, the assembly rule is

The three branches are exhaustive and disjoint. Lean implements exactly this case split.

hH : (NonlinearDynamics.Random.RandomMatrix.hermitianFromCoordinates d u).IsHermitian := NonlinearDynamics.Random.RandomMatrix.hermitianFromCoordinates_isHermitian d u

Exact project excerpts

Full project check. This uses the repository’s pinned Lean and Mathlib dependencies and may require substantial disk space and memory. The authoritative source is formalization/NonlinearDynamics/Random/RandomMatrices/HermitianCoordinates.lean. The checked assembler is:

def hermitianFromCoordinates {n : ℕ} (d : Fin n → ℝ)
    (u : StrictUpperIndex n → ℂ) : Matrix (Fin n) (Fin n) ℂ :=
  fun i j ↦
    if hij : i < j then
      u ⟨(i, j), hij⟩
    else if hji : j < i then
      star (u ⟨(j, i), hji⟩)
    else
      d i

Read the nested conditional from top to bottom:

1. if \(i\lt j\), use the supplied upper coordinate;
2. otherwise, if \(j\lt i\), reverse the index pair and apply star, which is complex conjugation here; and
3. otherwise the indices are equal, so use the real diagonal value, coerced into \(\mathbb C\) by the expected matrix-entry type.

The exact lower-entry recovery theorem is:

@[simp]
theorem hermitianFromCoordinates_apply_lower {n : ℕ} (d : Fin n → ℝ)
    (u : StrictUpperIndex n → ℂ) {i j : Fin n} (hji : j < i) :
    hermitianFromCoordinates d u i j = star (u ⟨(j, i), hji⟩) := by
  have hnot : ¬ i < j := not_lt_of_ge (le_of_lt hji)
  simp [hermitianFromCoordinates, hji, hnot]

The proof first rules out the upper branch, then simplifies the definition to the reflected conjugate branch. Its hypothesis hji : j < i is the typed evidence that the requested entry lies below the diagonal.

The pointwise Hermiticity theorem is:

theorem hermitianFromCoordinates_isHermitian {n : ℕ} (d : Fin n → ℝ)
    (u : StrictUpperIndex n → ℂ) :
    (hermitianFromCoordinates d u).IsHermitian := by
  rw [Matrix.IsHermitian.ext_iff]
  intro i j
  rcases lt_trichotomy i j with hij | rfl | hji
  · rw [hermitianFromCoordinates_apply_upper d u hij]
    rw [hermitianFromCoordinates_apply_lower d u hij]
    simp
  · simp
  · rw [hermitianFromCoordinates_apply_lower d u hji]
    rw [hermitianFromCoordinates_apply_upper d u hji]

The three goals correspond to upper, diagonal, and lower positions. This is a direct proof of the same trichotomy visible in the diagrams.

Standalone tutorial: coordinate worksheet

Standalone tutorial. This worksheet imports only Std. It models the concrete size-three ledger with rational real and imaginary parts. It checks the arithmetic, reflection, degree count, and round trip, but it does not import Mathlib or prove the project’s matrix theorem.

Save this as HermitianCoordinates3Scratch.lean:

import Std

structure ComplexRat where
  re : Rat
  im : Rat
deriving Repr, BEq

def ComplexRat.conj (z : ComplexRat) : ComplexRat :=
  { re := z.re, im := -z.im }

def ComplexRat.ofReal (x : Rat) : ComplexRat :=
  { re := x, im := 0 }

structure Coordinates3 where
  d0 : Rat
  d1 : Rat
  d2 : Rat
  u01 : ComplexRat
  u02 : ComplexRat
  u12 : ComplexRat
deriving Repr, BEq

structure Matrix3 where
  a00 : ComplexRat
  a01 : ComplexRat
  a02 : ComplexRat
  a10 : ComplexRat
  a11 : ComplexRat
  a12 : ComplexRat
  a20 : ComplexRat
  a21 : ComplexRat
  a22 : ComplexRat
deriving Repr

def assemble (c : Coordinates3) : Matrix3 :=
  { a00 := ComplexRat.ofReal c.d0
    a01 := c.u01
    a02 := c.u02
    a10 := c.u01.conj
    a11 := ComplexRat.ofReal c.d1
    a12 := c.u12
    a20 := c.u02.conj
    a21 := c.u12.conj
    a22 := ComplexRat.ofReal c.d2 }

def recover (A : Matrix3) : Coordinates3 :=
  { d0 := A.a00.re
    d1 := A.a11.re
    d2 := A.a22.re
    u01 := A.a01
    u02 := A.a02
    u12 := A.a12 }

def strictUpperCount (n : Nat) : Nat :=
  n * (n - 1) / 2

def realDegreesOfFreedom (n : Nat) : Nat :=
  n + 2 * strictUpperCount n

def exampleCoordinates : Coordinates3 :=
  { d0 := 2, d1 := -1, d2 := 4
    u01 := { re := 1, im := 2 }
    u02 := { re := -3, im := 1 }
    u12 := { re := 5, im := -2 } }

#eval realDegreesOfFreedom 3
#eval (assemble exampleCoordinates).a10
#eval (assemble exampleCoordinates).a21
#eval recover (assemble exampleCoordinates) == exampleCoordinates

Run it with:

elan run leanprover/lean4:v4.32.0 lean HermitianCoordinates3Scratch.lean

The outputs should report \(9\), then the conjugates \(1-2i\) and \(5+2i\) as structures with rational re and im fields, then true for the recovered-coordinate comparison.

Try the exact declarations in the project

import NonlinearDynamics.Random.RandomMatrices.HermitianCoordinates

#check NonlinearDynamics.Random.StrictUpperIndex
#check NonlinearDynamics.Random.HermitianCoordinateSpace
#check NonlinearDynamics.Random.StrictUpperIndex.instFintype
#check NonlinearDynamics.Random.StrictUpperIndex.instDecidableEq
#check NonlinearDynamics.Random.RandomMatrix.hermitianFromCoordinates
#check NonlinearDynamics.Random.RandomMatrix.hermitianFromCoordinates_apply_diag
#check NonlinearDynamics.Random.RandomMatrix.hermitianFromCoordinates_apply_upper
#check NonlinearDynamics.Random.RandomMatrix.hermitianFromCoordinates_apply_lower
#check NonlinearDynamics.Random.RandomMatrix.hermitianFromCoordinates_isHermitian
#check NonlinearDynamics.Random.RandomMatrix.measurable_hermitianFromCoordinates
#check NonlinearDynamics.Random.RandomMatrix.hermitianCoordinateMap
#check NonlinearDynamics.Random.RandomMatrix.measurable_hermitianCoordinateMap
#check NonlinearDynamics.Random.RandomMatrix.hermitianFromCoordinates_zero
#check NonlinearDynamics.Random.RandomMatrix.hermitianCoordinateMap_zero
#check NonlinearDynamics.Random.HermitianRandomMatrix.ofCoordinates

cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomMatrices/HermitianCoordinates.lean

Measurability enters only when coordinates vary

For fixed \(d\) and \(u\), assembly is purely deterministic. If the coordinates depend on an outcome \(\omega\), then

is a matrix-valued sample map. The project proves it measurable when every coordinate function \(\omega\mapsto d_i(\omega)\) and \(\omega\mapsto u_{ij}(\omega)\) is measurable. Entrywise measurability is enough because every matrix entry is one coordinate, a coerced real coordinate, or the conjugate of one coordinate.

The named function RandomMatrix.hermitianCoordinateMap n packages assembly on the complete product coordinate space. The theorem measurable_hermitianCoordinateMap certifies its measurable structure. Read measurable space for why this is a well-formedness condition rather than a probability distribution.

The empty \(n=0\) boundary

At \(n=0\), both Fin 0 and StrictUpperIndex 0 are empty. A function out of an empty type has no values to choose, so the coordinate product has one point. A matrix indexed by Fin 0 also has no entries and is the unique empty matrix, written \(0\).

The checked theorems hermitianFromCoordinates_zero and hermitianCoordinateMap_zero say that assembly returns that empty matrix. No division by \(n\) occurs in this deterministic layer.

Distinctions and failure modes

Where to continue

Finite Hermitian Matrices from Coordinates develops this representation, its Hermiticity proof, and its measurable sample-map role in textbook detail. Read conjugate transpose for the symmetry operation and random matrix for the later probability-space layer.

Finite Product Probability Spaces and Independent Gaussian Fields explains how finite coordinate families acquire a joint law. The subsequent Finite GUE from Independent Gaussian Coordinates chooses the diagonal and upper Gaussian laws, fixes their scales and independence, and pushes that coordinate measure through this assembler.

References

Mathlib contributors. Hermitian matrices, Mathlib 4 documentation. This is the official API for Matrix.IsHermitian, conjugate transpose, and the entrywise criterion used by the checked proof.

Mathlib contributors. Finite index types, Mathlib 4 documentation. This documents Fin n, including the empty zero-dimensional index type used by the boundary theorems.

Terence Tao. Topics in Random Matrix Theory, Graduate Studies in Mathematics 132, American Mathematical Society, 2012. This monograph supplies broader Hermitian and random-matrix context. It is not used to infer a probability law for the deterministic coordinate space.

Nonlinear Dynamics in Lean contributors. HermitianCoordinates.lean, the checked project source for the coordinate type, direct assembler, entrywise recovery lemmas, Hermiticity, measurability, and zero-dimensional boundary.

The upstream Mathlib revision audited for this entry is commit 81a5d257, pinned by formalization/lake-manifest.json.