Intrinsic Hermitian Gaussian Symmetry and Matrix-Law Support

Base camp: one matrix you can audit entry by entry

Start with four real coordinates:

The two diagonal coordinates are real. The complex strict-upper coordinate is

The Hermitian reconstruction reflects that entry across the diagonal and takes its complex conjugate:

The conjugate transpose \(H^*\) transposes the entries and conjugates each one. The diagonal entries remain \(1\) and \(3\), and

Therefore \(H^*=H\). That equality is the definition of Hermiticity.

Act by a concrete unitary permutation

Let

The matrix \(P\) swaps the two coordinate axes. It is real and symmetric, so \(P^*=P\), and direct multiplication gives

A matrix satisfying \(P^*P=PP^*=I\) is unitary. Its congruence action on a matrix \(X\) is the two-sided map

Multiply the running example in two visible steps:

The sample changed: \(H'\ne H\), already because the upper-left entries are \(3\) and \(1\). But \(H'\) is still Hermitian because its lower-left entry is the conjugate of its upper-right entry.

Verify trace and Frobenius geometry numerically

The trace is the sum of diagonal entries:

The squared Frobenius norm is the sum of squared entry magnitudes. Because

we obtain

The intrinsic real coordinate vectors make the same norm visible:

Both have squared Euclidean norm

Pointwise change is not law change

A probability law assigns probability mass to measurable subsets of matrix space. If \(T=C_P\) is the congruence map, law invariance means the exact pushforward equality

This does not say \(T(H)=H\) for every sample. The running example is a counterexample to that pointwise claim: \(T(H)=H'\ne H\). An invariant law may redistribute individual points while leaving the total probability of every measurable event unchanged.

Support alone does not imply invariance

The support claim used in this chapter is the mass-one statement that a law assigns probability \(1\) to the measurable Hermitian subset of ambient matrix space. It says where the law lives, not how its mass is arranged there.

Consider the deterministic Dirac law \(\delta_H\), which places all mass on the single matrix \(H\). It has Hermitian mass one. Yet

For the measurable event \(\{H\}\), the original law gives mass \(1\), while the pushed law gives mass \(0\). A singleton is closed, hence Borel-measurable, in this finite-dimensional matrix space. Hermitian support has survived, but invariance has failed.

For comparison, take the balanced two-point law

Because applying \(T\) swaps \(H\) and \(H'\), the two weights are exchanged:

Every sampled point moves, but this law is unchanged under this one permutation. The balanced two-point law is not Gaussian and is not claimed to be invariant under every unitary congruence.

With the sample-versus-law distinction fixed numerically, we can climb to the intrinsic Euclidean carrier and Mathlib’s standard Gaussian.

The seventh random-matrix-theory milestone (RMT-07) supplies the geometry that the name Gaussian unitary ensemble had been promising but that the earlier coordinate construction had not proved. It equips finite complex matrices with their Frobenius Euclidean structure, cuts out the Hermitian matrices as a real Euclidean subspace, proves that unitary congruence acts by real linear isometries there, and invokes Mathlib’s isometry theorem to show that the intrinsic standard Gaussian is unchanged by that action.

On a separate track, RMT-07 proves that the matrix law constructed from independent Gaussian free coordinates assigns mass one to the measurable set of Hermitian matrices. Equivalently, the matrix is Hermitian almost everywhere and the non-Hermitian complement has mass zero.

Those are substantial results. They still do not prove that the coordinate-built Gaussian unitary ensemble (GUE) matrix law is unitarily invariant. That final implication needs a comparison theorem identifying the coordinate law with a scaled intrinsic standard Gaussian. RMT-07 exposes the two endpoints of that comparison and leaves the bridge to RMT-08.

Choose a route up

Learning objectives

By the summit, you should be able to:

1. reconstruct the running \(2\times2\) Hermitian matrix from its free coordinates and compute its permutation congruence;
2. verify Hermiticity, trace (4), squared Frobenius norm (20), and pointwise change in that exact example;
3. distinguish a moved sample from an invariant probability law;
4. use the Dirac nonexample to show why Hermitian support does not imply invariance;
5. distinguish an ambient matrix, an ambient Frobenius vector, an intrinsic Hermitian vector, and the Hermitian subset of matrix space;
6. explain why Hermitian matrices form a real rather than complex subspace;
7. derive \(\langle X,Y\rangle_F=\operatorname{Tr}(X^*Y)\);
8. derive the factor of two in the Hermitian Frobenius norm;
9. identify \(d_i,\sqrt2 x_{ij},\sqrt2 y_{ij}\) as the natural real orthonormal coordinates;
10. prove on paper that \(X\mapsto UXU^*\) has inverse \(X\mapsto U^*XU\) when \(U\) is unitary;
11. explain why cyclicity of trace turns that equivalence into an isometry;
12. explain why congruence restricts to the Hermitian subspace;
13. state Mathlib’s intrinsic standard-Gaussian isometry theorem;
14. separate intrinsic Gaussian invariance from invariance of an independently constructed coordinate law;
15. prove that a pushforward through a pointwise Hermitian map has Hermitian support; and
16. state the scaled-measure comparison that was still required at the RMT-07 stopping point and is proved in RMT-08.

Two paths and the bridge missing at RMT-07

The upper path begins with the RMT-06 coordinate probability measure \(\nu_n\), pushes it through the measurable Hermitian assembly map \(A_n\), and obtains the ambient matrix law

Because \(A_n(c)\) is Hermitian for every coordinate point \(c\), the preimage of the Hermitian set is the entire coordinate space. That yields \(\mu_n(\operatorname{Herm}_n)=1\).

The lower path begins with the intrinsic real Euclidean space \(\mathcal H_n\) of Hermitian matrices. Unitary congruence acts on this space by a real linear isometry. Mathlib’s intrinsic standard Gaussian \(\gamma_n\) is invariant under every such isometry, so

The RMT-07 module does not prove \(\mu_n=\gamma_n\), and the equality would in any case miss the Wigner scale. The expected statement uses the scalar \(\sqrt{s_n}\), where \(s_n\) is the RMT-06 variance scale, plus the map that forgets the intrinsic Hermitian subtype and returns an ordinary matrix.

Base camp: four related spaces

Fix \(n\in\mathbb N\). RMT-07 moves among four closely related objects.

The first is ordinary matrix space

This is the codomain of the existing matrix law. It is ideal for multiplication, conjugate transpose, entry evaluation, and measurable subsets.

The second is the finite complex Euclidean space

It contains the same \(n^2\) complex entries but carries bundled inner-product and finite-dimensional structures useful to Mathlib’s geometry APIs.

The third is the intrinsic Hermitian Euclidean space

It is a subtype of \(\mathcal F_n\), bundled as a submodule over \(\mathbb R\). Its points carry their proof of Hermiticity with them.

The fourth is the ambient Hermitian set

It is not a new data type. It is a measurable set used to ask how much mass an ambient matrix measure assigns to Hermitian matrices.

The conversions between them are simple, but keeping the roles distinct prevents type-correct but mathematically misleading claims.

Camp one: make the Hermitian locus measurable

The condition \(H=H^*\) can be checked entry by entry:

Therefore the Hermitian set is the finite intersection

Each matrix-entry projection is measurable, complex conjugation is continuous and hence measurable, and the equality set of two measurable functions into \(\mathbb C\) is measurable. Finite intersections preserve measurability. That is the complete reason the subset is measurable; no eigenvalue map or density is needed.

The prior module defines the matrix law as a pushforward :

where \(A_n\) assembles real diagonal coordinates and complex strict-upper coordinates into a Hermitian matrix. For the measurable set \(\operatorname{Herm}_n\), pushforward evaluation gives

The middle equality uses the pointwise RMT-05 theorem that every assembled matrix is Hermitian. The final equality uses the RMT-06 probability instance for \(\nu_n\).

Three theorem interfaces expose the same support fact in useful forms:

Mass one is convenient for direct measure calculations. The almost-everywhere form composes with facts stated using the almost-everywhere filter. Complement mass zero is often the cleanest support-language interface. They are logically close, but naming all three avoids reproving conversions downstream.

Camp two: package matrices as Euclidean vectors

Mathlib’s EuclideanSpace 𝕜 ι is an \(L^2\)-packaged finite function space. RMT-07 abbreviates

abbrev FrobeniusMatrix (n : ℕ) :=
  EuclideanSpace ℂ (Fin n × Fin n)

and defines entry-preserving maps in both directions:

def frobeniusToMatrix (x : FrobeniusMatrix n) :
    Matrix (Fin n) (Fin n) ℂ :=
  fun i j => x (i, j)

def matrixToFrobenius (A : Matrix (Fin n) (Fin n) ℂ) :
    FrobeniusMatrix n :=
  WithLp.toLp 2 (fun ij => A ij.1 ij.2)

The apparent asymmetry comes only from the \(L^2\) wrapper. Both composites reduce to the identity, and frobeniusMatrixLinearEquiv packages the conversions as a complex linear equivalence.

Why not work only with ordinary matrices? The ordinary matrix type is already a module, but the Euclidean-space presentation gives direct access to the canonical finite \(L^2\) inner product, its induced norm, finite-dimensional real and complex structure, Borel measurability, and the multivariate Gaussian API. The conversion lemmas let proofs cross back into matrix algebra whenever trace or multiplication is the natural language.

Camp three: recover the trace inner product

For \(x,y\in\mathcal F_n\), let \(X,Y\in\mathcal M_n\) be their matrix representatives. The Euclidean inner product expands as

Matrix multiplication gives

Summing the diagonal and exchanging the finite summation order yields

Hence

This identity is the hinge between Euclidean analysis and matrix algebra. It lets the congruence proof use unitary identities and cyclicity of trace, then return an exact inner-product equality to the Euclidean API.

Setting \(x=y\) gives the Frobenius norm:

The checked theorem is stated over the complex inner product. On the Hermitian subspace, Lean uses the inherited real inner product. The general identity between the two views is that the real inner product is the real part of the complex one.

Camp four: read the Hermitian metric in free coordinates

Write a Hermitian matrix in free real coordinates:

Then

The free coordinate list

is therefore not orthonormal with its naive coordinate metric. The orthonormal list is

This explains the exact RMT-06 variance ledger. There the diagonal variables have variance \(s_n\), while each upper real component has variance \(s_n/2\). Under the orthonormal rescaling,

Thus every intrinsic orthonormal coordinate has common variance \(s_n\). This calculation is the blueprint for RMT-08. It is not itself a measure equality: a formal comparison still needs a bundled measurable real-linear isometry and a proof that the full joint product law transports as claimed.

A two-by-two calculation

For

directly summing squared magnitudes gives

The real dimension is four, with orthonormal coordinates \((a,b,\sqrt2x,\sqrt2y)\). A standard Gaussian in this Euclidean structure therefore has \(a,b\sim N(0,1)\) and \(x,y\sim N(0,1/2)\) in the displayed entry coordinates. Scaling the entire Euclidean vector by \(\sqrt{s_n}\) changes these variances to \(s_n\) and \(s_n/2\), exactly as required.

Camp five: unitary congruence in the ambient space

For fixed \(U\in\mathcal M_n\), define

On ambient matrix space this is complex linear. If \(U\) is unitary, then \(U^*U=UU^*=I\), so

and similarly \(C_U(C_{U^*}(X))=X\). Thus \(C_U\) is a complex linear equivalence with inverse \(C_{U^*}\).

To show it is an isometry, use the trace inner product:

The fourth line is cyclicity of finite matrix trace. The Lean proof follows this calculation rather than expanding four matrix products entry by entry. The result is first a theorem about inner products and then a bundled complex linear isometric equivalence.

Notice the hierarchy:

1. frobeniusCongruence U is defined for every square matrix \(U\);
2. invertibility uses the bundled unitary hypotheses;
3. inner-product preservation uses unitarity and trace cyclicity; and
4. the linear isometry is bundled only after those proofs exist.

This keeps algebraic definitions general while attaching stronger structure only under the assumptions that justify it.

Camp six: restrict the action to Hermitian space

If \(H=H^*\), then

So congruence maps the Hermitian subspace into itself even when \(U\) is not unitary. The project packages this restricted function as hermitianCongruence U and proves two compatibility lemmas:

• forgetting the Hermitian subtype gives the ambient Frobenius congruence; and
• converting to an ordinary matrix gives the project’s pre-existing RandomMatrix.congruence U.

For unitary \(U\), the restricted action is an equivalence. Its scalar field is \(\mathbb R\), because the Hermitian subspace is closed only under real scalars. The ambient complex isometry supplies the norm equality needed to bundle the restriction as

This is the exact object accepted by Mathlib’s multivariate standard-Gaussian transport theorem.

Camp seven: the intrinsic standard Gaussian

Let \(E\) be a finite-dimensional real inner-product space. Mathlib defines stdGaussian E by choosing an orthonormal basis, taking independent standard real Gaussian coordinates, and transporting that product measure through the basis equivalence. The resulting measure is independent of the orthonormal basis used to construct it.

Its characteristic function is the coordinate-free expression

and its covariance form is the real inner product. These facts explain the name standard and the rotational symmetry, although RMT-07 does not need to reprove either formula.

Mathlib’s theorem stdGaussian_map says that for a real linear isometric equivalence \(f:E\simeq E'\),

Take \(E=E'=\mathcal H_n\) and let \(f=C_U\), the restricted unitary congruence isometry. RMT-07 obtains

This theorem is valid for every natural dimension, including \(n=0\). At zero dimension the Euclidean space has one point, so the intrinsic standard Gaussian is necessarily concentrated there. The module’s named theorem is the uniform isometry-invariance statement; it does not add a separate zero-size Dirac theorem for this intrinsic measure.

A Lean engineering note

The final proof installs a local canonical \(\mathbb R\)-module instance for the Hermitian subtype before applying stdGaussian_map. This resolves a definitional-instance mismatch between the inherited inner-product structure and the module structure expected by the theorem. It changes no mathematics: the map remains the same real linear isometry, and the conclusion remains exact equality of measures.

Camp eight: the bridge absent from RMT-07

Let \(s_n\) be the RMT-06 variance scale: \(s_0=0\) and \(s_n=1/n\) for positive \(n\). Let

on \(\mathcal H_n\), and let \(J_n:\mathcal H_n\to\mathcal M_n\) forget the subtype and Euclidean packaging. At the RMT-07 stopping point, the required comparison had the schematic form

Several Lean interfaces could express that equality: first on coordinate space, first on \(\mathcal H_n\), or directly in ambient matrix space. The invariant mathematical content is the same: the diagonal and the square-root-of-two-rescaled upper coordinates must become independent centered Gaussians of common variance \(s_n\). RMT-08 subsequently chooses and checks a normalized-coordinate route; its linked chapter audits that later module.

Once this equality is checked, unitary invariance of \(\mu_n\) follows because scalar multiplication commutes with unitary congruence and the intrinsic standard Gaussian is invariant. Schematically,

Every equality in that chain needs the relevant measurable-map composition or commutation lemma. RMT-07 supplies the third equality but not the first comparison, so the full chain is not a theorem of the RMT-07 module. The subsequent RMT-08 module checks the missing comparison and transport.

What the next milestone had to make visible

A trustworthy comparison should make all of the following visible:

1. the real-linear map from free coordinate data to the Hermitian Euclidean subtype;
2. its effect on diagonal, upper-real, and upper-imaginary coordinates;
3. the square-root-of-two metric correction for upper coordinates;
4. the common \(\sqrt{s_n}\) scale;
5. measurability or continuity of every transport;
6. the zero-dimensional branch; and
7. the final equality in the same ambient matrix space used by GUE.matrixLaw.

Invoking a familiar density is not a substitute. A density would require a chosen Lebesgue measure on \(\mathcal H_n\), a volume normalization, and a Jacobian calculation. The coordinate-to-intrinsic product-measure route can prove the comparison without introducing that extra layer.

In Lean: six bridges from entries to measure equality

Each bridge pairs a sentence a mathematician would say, the paper statement, the exact Lean spelling, and a token map. Together they separate representation, geometry, subtype preservation, measurability, Gaussian symmetry, and support.

Bridge 1: flattening does not change an entry

frobeniusToMatrix (matrixToFrobenius A) = A

Bridge 2: the Euclidean inner product is a trace

inner_frobenius_eq_trace x y

Bridge 3: congruence stays inside the Hermitian carrier

hermitianCongruence U x : HermitianEuclidean n

Bridge 4: unitary congruence is a measurable real isometry

hermitianUnitaryCongruenceLinearIsometryEquiv U

Bridge 5: the intrinsic standard Gaussian law is invariant

map_stdGaussian_hermitianUnitaryCongruence U

(stdGaussian (HermitianEuclidean n)).map
    (hermitianUnitaryCongruenceLinearIsometryEquiv U) =
  stdGaussian (HermitianEuclidean n)

Bridge 6: the ambient matrix law has Hermitian mass one

GUE.matrixLaw_hermitianSet n

Try it locally: execute the two-by-two ledger

The exact project matrix type belongs to Mathlib, so the laptop worksheet uses a small pair of integers for each complex entry and four fields for a two-by-two matrix. It checks the same multiplication and weight bookkeeping without entering the project. Save this as /tmp/HermitianCongruenceTutorial.lean:

import Std

namespace HermitianCongruenceTutorial

structure CInt where
  re : Int
  im : Int
  deriving DecidableEq, Repr

def cAdd (z w : CInt) : CInt :=
  ⟨z.re + w.re, z.im + w.im⟩

def cMul (z w : CInt) : CInt :=
  ⟨z.re * w.re - z.im * w.im,
   z.re * w.im + z.im * w.re⟩

def cConj (z : CInt) : CInt :=
  ⟨z.re, -z.im⟩

def normSq (z : CInt) : Int :=
  z.re * z.re + z.im * z.im

structure Matrix2 where
  a00 : CInt
  a01 : CInt
  a10 : CInt
  a11 : CInt
  deriving DecidableEq, Repr

def entries (A : Matrix2) : List (Int × Int) :=
  [⟨A.a00.re, A.a00.im⟩, ⟨A.a01.re, A.a01.im⟩,
   ⟨A.a10.re, A.a10.im⟩, ⟨A.a11.re, A.a11.im⟩]

def mmul (A B : Matrix2) : Matrix2 :=
  ⟨cAdd (cMul A.a00 B.a00) (cMul A.a01 B.a10),
   cAdd (cMul A.a00 B.a01) (cMul A.a01 B.a11),
   cAdd (cMul A.a10 B.a00) (cMul A.a11 B.a10),
   cAdd (cMul A.a10 B.a01) (cMul A.a11 B.a11)⟩

def conjTranspose (A : Matrix2) : Matrix2 :=
  ⟨cConj A.a00, cConj A.a10, cConj A.a01, cConj A.a11⟩

def congruence (U H : Matrix2) : Matrix2 :=
  mmul (mmul U H) (conjTranspose U)

def isHermitian (A : Matrix2) : Bool :=
  A.a00.im == 0 && A.a11.im == 0 && A.a10 == cConj A.a01

def trace (A : Matrix2) : CInt :=
  cAdd A.a00 A.a11

def frobeniusSq (A : Matrix2) : Int :=
  normSq A.a00 + normSq A.a01 + normSq A.a10 + normSq A.a11

def H : Matrix2 :=
  ⟨⟨1, 0⟩, ⟨1, 2⟩, ⟨1, -2⟩, ⟨3, 0⟩⟩

def P : Matrix2 :=
  ⟨⟨0, 0⟩, ⟨1, 0⟩, ⟨1, 0⟩, ⟨0, 0⟩⟩

def Hswap : Matrix2 :=
  congruence P H

def diracWeights : List Nat := [1, 0]
def balancedWeights : List Nat := [1, 1]
def pushBySwap (weights : List Nat) : List Nat := weights.reverse

#eval entries H
#eval entries Hswap
#eval (isHermitian H, isHermitian Hswap, H == Hswap)
#eval ((trace H).re, (trace Hswap).re)
#eval (frobeniusSq H, frobeniusSq Hswap)
#eval (diracWeights, pushBySwap diracWeights)
#eval (balancedWeights, pushBySwap balancedWeights)

example : entries Hswap = [(3, 0), (1, -2), (1, 2), (1, 0)] := by
  decide

example : isHermitian H = true ∧ isHermitian Hswap = true := by
  decide

example : trace H = trace Hswap := by
  decide

example : frobeniusSq H = 20 ∧ frobeniusSq Hswap = 20 := by
  decide

example : pushBySwap diracWeights ≠ diracWeights := by
  decide

example : pushBySwap balancedWeights = balancedWeights := by
  decide

end HermitianCongruenceTutorial

Type these commands on a normal macOS or Linux machine with Elan installed:

source "$HOME/.elan/env"
elan run leanprover/lean4:v4.32.0 lean /tmp/HermitianCongruenceTutorial.lean

Standalone tutorial: Lean plus Std, suitable for a normal macOS or Linux host. It does not import Mathlib, enter the Lake project, or check the repository module.

The file was executed with that exact command and printed:

[(1, 0), (1, 2), (1, -2), (3, 0)]
[(3, 0), (1, -2), (1, 2), (1, 0)]
(true, true, false)
(4, 4)
(20, 20)
([1, 0], [0, 1])
([1, 1], [1, 1])

Read the output from top to bottom: the first two lines are the entries of \(H\) and \(H'\) in row-major order; both Hermitian checks are true while matrix equality is false; trace and squared Frobenius norm are preserved; the Dirac weight vector changes under the swap; and equal half-weight numerators remain unchanged. The balanced weights use denominator \(2\), so [1, 1] means \((1/2,1/2)\).

The six example blocks are kernel-checked finite algebra. They do not prove that P inhabits Mathlib’s unitary group, construct a Borel measure, define an intrinsic Gaussian, or verify the project theorem.

Try it in the repository: inspect the exact module

import NonlinearDynamics.Random.RandomMatrices.GaussianUnitaryEnsembleGeometry

open Matrix MeasureTheory ProbabilityTheory
open scoped Matrix RealInnerProductSpace
open NonlinearDynamics.Random

#check RandomMatrix.frobeniusToMatrix_matrixToFrobenius
#check RandomMatrix.frobeniusMatrixLinearEquiv
#check RandomMatrix.hermitianSubmodule
#check RandomMatrix.measurable_hermitianToMatrix
#check RandomMatrix.inner_frobenius_eq_trace
#check RandomMatrix.frobeniusCongruence_inner
#check RandomMatrix.hermitianCongruence
#check RandomMatrix.hermitianToMatrix_hermitianCongruence
#check RandomMatrix.hermitianUnitaryCongruenceLinearIsometryEquiv
#check RandomMatrix.map_stdGaussian_hermitianUnitaryCongruence
#check RandomMatrix.measurableSet_hermitianSet
#check GUE.matrixLaw_hermitianSet
#check GUE.matrixLaw_ae_isHermitian
#check GUE.matrixLaw_compl_hermitianSet

cd formalization
lake env lean NonlinearDynamics/Random/RandomMatrices/GaussianUnitaryEnsembleGeometry.lean

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

The checked declaration map

The module NonlinearDynamics.Random.RandomMatrices.GaussianUnitaryEnsembleGeometry checks 27 public declarations. The first 24 live in namespace NonlinearDynamics.Random.RandomMatrix; the final three support theorems live in NonlinearDynamics.Random.GUE.

All 27 declarations compile under Lean 4.32.0 and the pinned Mathlib 4.32.0 dependency. The module contains no sorry or admit.

Validation boundary

The preceding repo-check gives the copyable import, exact declaration probe, module path, and full project command. It checks the geometry, support, and intrinsic Gaussian symmetry proofs. The standalone worksheet checks only the displayed two-by-two arithmetic. Neither command numerically samples a matrix, compares empirical histograms, or turns a support theorem into a density or law-invariance theorem.

Checked theorem versus classical GUE context

Classically, the Wigner-scaled GUE may be characterized by independent free Gaussian coordinates, by an invariant density proportional to

or as a scaled isotropic Gaussian on the real Euclidean space of Hermitian matrices. These descriptions are equivalent after every variance, metric, and reference-measure convention is aligned.

RMT-07 checks the Euclidean geometry, intrinsic isotropic-Gaussian symmetry, and support of the coordinate presentation. The RMT-07 module does not check the equivalence between the two presentations; RMT-08 subsequently does.

Physics window: symmetry without a preferred basis

In finite-dimensional quantum mechanics, an observable or Hamiltonian is represented by a Hermitian operator. Its eigenvalues are real, and changing an orthonormal basis replaces \(H\) by \(UHU^*\). A probability model intended to carry no preferred basis should assign the same law before and after every such deterministic unitary change of coordinates.

Dyson’s threefold classification distinguishes orthogonal, unitary, and symplectic symmetry classes. The unitary class is the complex Hermitian class associated, in the standard physical discussion, with the absence of the relevant antiunitary time-reversal constraint. The classical GUE is the Gaussian reference ensemble for this class.

RMT-07 formalizes neither a quantum Hamiltonian nor time-reversal symmetry. It does something more elementary and reusable: it proves the finite-dimensional geometric statement that basis change acts isometrically on Hermitian matrix space, and that the intrinsic isotropic Gaussian cannot distinguish those bases. The physical interpretation motivates the action; it does not replace the measure comparison needed for the coordinate-built ensemble.

Common wrong turns

Treating Hermitian matrices as a complex vector space

If \(H=H^*\), then \((iH)^*=-iH\). Except in the zero case, \(iH\) is not Hermitian. The intrinsic space is a real subspace, and its Gaussian and isometry theorems must use \(\mathbb R\)-linear structure.

Forgetting the reflected lower entry

The upper coordinate \(x_{ij}+iy_{ij}\) and lower coordinate \(x_{ij}-iy_{ij}\) have equal magnitude. Both enter the Frobenius sum, so the free upper real coordinates carry weight two. Missing that duplication gives the wrong orthonormal basis and the wrong Gaussian scale.

Proving norm preservation but claiming law preservation

A pointwise isometry preserves distances and norms. A measure is invariant only after its pushforward under that map is proved equal to itself. RMT-07 gets the intrinsic measure equality from stdGaussian_map; it does not infer invariance for every measure on the same space.

Reading support as a full distributional description

Many different laws have mass one on the Hermitian set. Support supplies no Gaussianity, independence, density, or unitary symmetry on its own.

Calling the coordinate-built law intrinsic by inspection

Matching scalar variances is persuasive but insufficient. Equality of full joint measures requires the correct bundled coordinate map, independence, and transport theorem. This is the obligation left open by RMT-07 and discharged in RMT-08.

Hiding scale in the word standard

Mathlib’s stdGaussian has variance one along orthonormal real directions. The RMT-06 Wigner scale is \(s_n=1/n\) in positive dimension. The comparison needs multiplication by \(\sqrt{s_n}\), not an unscaled equality.

Deriving invariance from a density that has not been defined

The classical density is useful context. Formal density reasoning requires a specific reference measure on Hermitian space and proof that unitary congruence preserves it. RMT-07 uses intrinsic Gaussian transport instead and makes no density claim.

Confusing congruence with left multiplication

The relevant action is \(H\mapsto UHU^*\), not \(H\mapsto UH\). The two-sided action preserves Hermiticity and represents basis change.

Claiming spectral consequences from Euclidean symmetry

RMT-07 defines no eigenvalue random variables, joint eigenvalue density, trace expectation, spectral form factor, empirical measure, or large-size limit. Those require new measurable and analytic layers.

Exercises

1. Running reconstruction. Starting from \(d_0=1,d_1=3,z=1+2i\), reconstruct \(H\), calculate \(H^*\), and multiply \(PHP^*\) entry by entry. Which single entry proves \(H'\ne H\)?
2. Running invariant ledger. Recompute both traces and both squared Frobenius norms without using the displayed answers. Then check the norm again from \(q\) and \(q'\).
3. Running law test. For the event \(\{H\}\), evaluate its mass under \(\delta_H\), \(T_*\delta_H\), \(\mu_{\mathrm{pair}}\), and \(T_*\mu_{\mathrm{pair}}\). Which equalities are pointwise and which are equalities of measures?
4. Packaging. Prove directly that frobeniusToMatrix and matrixToFrobenius preserve every entry.
5. Trace inner product. Expand \(\operatorname{Tr}(X^*Y)\) for \(2\times2\) matrices and compare it with the four-coordinate complex Euclidean inner product.
6. Real subspace. Show that Hermitian matrices are closed under real scalar multiplication and give a nonzero example for which multiplication by \(i\) takes the matrix outside the subspace.
7. Dimension. Count the real free coordinates of an \(n\times n\) Hermitian matrix and obtain \(n^2\).
8. Factor two. Derive the Frobenius squared norm of a \(3\times3\) Hermitian matrix from its diagonal and strict-upper coordinates.
9. Orthonormalization. Explain why multiplying both real components of every strict-upper coordinate by \(\sqrt2\) corrects the metric.
10. Inverse action. Verify \(C_{U^*}\circ C_U=\mathrm{id}\) using both unitary identities.
11. Trace cycle. Locate exactly where cyclicity of trace is used in the proof that congruence preserves the Frobenius inner product.
12. Restriction. Prove that \(UHU^*\) is Hermitian without assuming \(U\) unitary. Which later property does require unitarity?
13. Gaussian scale. If upper real and imaginary parts have variance \(s/2\), compute the variances after square-root-of-two rescaling.
14. Support. Starting from \(\mu=A_*\nu\), prove \(\mu(S)=1\) when \(A^{-1}(S)\) is the whole source and \(\nu\) is a probability measure.
15. Counterexample. Give a point mass with Hermitian support that is not invariant under every unitary congruence.
16. Lean. Find the declaration that connects restricted congruence to the pre-existing ambient RandomMatrix.congruence map.
17. Boundary. Explain what the intrinsic Gaussian and congruence action become at \(n=0\).
18. RMT-07 boundary design. Write a precise source type, target type, and coordinate formula for the real-linear isometry needed to identify free Hermitian coordinates with \(\mathcal H_n\), then compare your design with the linked RMT-08 chapter.

Summit register

RMT-07 gives finite complex matrices a canonical Frobenius Euclidean model and proves its inner product is the familiar trace expression. It identifies the Hermitian matrices as a real Euclidean subspace, packages unitary congruence as an ambient complex linear isometry and an intrinsic real linear isometry, and uses Mathlib’s multivariate Gaussian transport theorem to prove exact invariance of the intrinsic Hermitian standard Gaussian.

Separately, it proves that the RMT-06 coordinate-built matrix law assigns mass one to the measurable Hermitian locus, is Hermitian almost everywhere, and assigns zero mass to the non-Hermitian complement.

The factor-of-two identity explains how the paths should meet. In orthonormal Hermitian coordinates, diagonal variables remain unchanged while upper real and imaginary variables receive a factor \(\sqrt2\). The RMT-06 variances then all become \(s_n\), predicting a \(\sqrt{s_n}\)-scaled intrinsic standard Gaussian. That is the equality and symmetry transport absent from the RMT-07 module and subsequently checked in RMT-08.

No density, volume Jacobian, coordinate-law unitary invariance, eigenvalue law, moment, spectral statistic, semicircle theorem, or universality result is claimed here.

Where to continue

Use the Hermitian Frobenius geometry glossary entry for a compact statement of the metric and factor-two ledger. Finite GUE from Independent Gaussian Coordinates constructs the matrix law whose support is proved here, and the Gaussian unitary ensemble entry records its normalization.

Finite Hermitian Matrices from Coordinates develops the pointwise assembly map. Read unitary invariance for the law-level definition and counterexamples separating support, pointwise preservation, and distributional symmetry.

References

Mathlib contributors. Multivariate Gaussian distributions, Mathlib 4 documentation. The page defines stdGaussian E from independent standard real coordinates in an orthonormal basis and documents stdGaussian_map, which transports the measure along a real linear isometric equivalence.

Mathlib contributors. Pi-L2 Euclidean spaces, unitary matrices, and Hermitian matrices, Mathlib 4 documentation. These official API references underlie the ambient Euclidean representation, bundled unitary group, and Hermitian matrix identities used by the checked proofs.

Alice Guionnet. Rare Events in Random Matrix Theory, in Proceedings of the International Congress of Mathematicians 2022, volume 2, European Mathematical Society Press, 2022, doi:10.4171/ICM2022/174, pp. 1008-1052. Section 1.1.1 states the classical GUE entry variances \(1/n\) and \(1/(2n)\), the density \(\exp[-n\operatorname{Tr}(H^2)/2]\) under the unitary convention, and unitary-conjugation invariance. The density and the equivalence of presentations remain contextual here.

Freeman J. Dyson. Statistical Theory of the Energy Levels of Complex Systems. I, Journal of Mathematical Physics 3 (1962), 140-156. This primary paper develops the orthogonal, unitary, and symplectic symmetry-class framework and its quantum-spectral motivation.

The exact upstream Lean source audited for this chapter is Mathlib commit 81a5d257, the revision pinned by formalization/lake-manifest.json.