Start with the exact size-two ledger
The repository fixes one finite Gaussian unitary ensemble (GUE) convention before it proves any symmetry. In positive dimension \(n\), the variance scale is
\[ v_n=\frac1n. \]A Gaussian distribution is a bell-shaped probability law determined here by its mean and variance . “Centered” means mean zero; variance measures expected squared displacement from that mean. When this chapter says coordinates are mutually independent , it means their joint law is the product of the listed one-coordinate laws, not merely that their pairwise correlations vanish.
Diagonal entries have variance \(v_n\). The real and imaginary parts of each strict-upper entry have variance \(v_n/2\). The lower triangle is not sampled independently; it is forced by Hermitian conjugate reflection.
At \(n=2\), the ledger becomes
| Object | Number of real slots | Mean | Variance of each displayed real slot |
|---|---|---|---|
| diagonal entries | 2 | 0 | \(1/2\) |
| real part of the one strict-upper entry | 1 | 0 | \(1/4\) |
| imaginary part of the one strict-upper entry | 1 | 0 | \(1/4\) |
A \(2\times2\) Hermitian matrix has the form
\[ H= \begin{bmatrix} d_0 & a+ib\\ a-ib & d_1 \end{bmatrix}, \]where \(d_0,d_1,a,b\in\mathbb R\). “Hermitian” means \(H^*=H\), where \(H^*\) is the conjugate transpose . The diagonal is real, and the lower-left entry is the complex conjugate of the upper-right entry.
The four normalized real coordinates
The repository does not use \((d_0,d_1,a,b)\) as its orthonormal real coordinates. It uses
\[ z=(d_0,d_1,r,s) =\bigl(d_0,d_1,\sqrt2,a,\sqrt2,b\bigr). \]All four entries of the random vector \(z\) are mutually independent centered Gaussians with variance \(1/2\). Decoding divides the last two by \(\sqrt2\):
\[ H(z)= \begin{bmatrix} d_0 & r/\sqrt2+i\,s/\sqrt2\\ r/\sqrt2-i\,s/\sqrt2 & d_1 \end{bmatrix}. \]Because variance scales by the square of a deterministic multiplier,
\[ \operatorname{Var}(r/\sqrt2) =\operatorname{Var}(s/\sqrt2) =\frac12\cdot\frac12 =\frac14. \]The decoder therefore recovers exactly the entrywise variance ledger above. It does not add another normalization later.
One concrete coordinate point
Take the deterministic point
\[ z_0=(2,-1,\sqrt2,2\sqrt2). \]This is one point in the coordinate space, not a claim that a continuously distributed random vector assigns positive probability to that singleton. The decoder gives
\[ H_0=H(z_0)= \begin{bmatrix} 2 & 1+2i\\ 1-2i & -1 \end{bmatrix}. \]The Frobenius squared norm adds the squared complex magnitudes of all four matrix entries. Since an upper entry and its conjugate have the same magnitude,
\[ \begin{aligned} \lVert H_0\rVert_F^2 &=2^2+(-1)^2+|1+2i|^2+|1-2i|^2\\ &=4+1+5+5\\ &=15. \end{aligned} \]The Euclidean coordinate square is
\[ \lVert z_0\rVert_2^2 =2^2+(-1)^2+(\sqrt2)^2+(2\sqrt2)^2 =4+1+2+8 =15. \]The equality is not a coincidence. The decoder is designed to be an isometry.
The wrong-normalization near-miss
Suppose we omit both divisions by \(\sqrt2\) and place \(r+is\) directly above the diagonal. The same coordinate point would produce an upper entry \(\sqrt2+2\sqrt2 i\). Its matrix square would be
\[ 4+1+2(2+8)=25, \]not 15. At the law level, its upper real and imaginary parts would retain variance \(1/2\), not the repository’s required \(1/4\). The near-miss fails both the geometry test and the probability ledger.
Conjugate the concrete matrix by a unitary swap
A complex matrix \(U\) is unitary when \(U^*U=UU^*=I\). Unitary matrices encode changes between orthonormal bases. Their action on a Hermitian matrix is the congruence
\[ H\longmapsto UHU^*. \]For the exact example, choose the coordinate-swap matrix
\[ P= \begin{bmatrix} 0&1\\ 1&0 \end{bmatrix}. \]It satisfies \(P^*=P\) and \(P^2=I\), so it is unitary. Direct multiplication gives
\[ PH_0P^*= \begin{bmatrix} -1 & 1-2i\\ 1+2i & 2 \end{bmatrix}. \]The transformed matrix is visibly not \(H_0\). Its diagonal values have traded places and the sign of the upper imaginary part has changed. In normalized real coordinates, the action on this example is
\[ (d_0,d_1,r,s) \longmapsto (d_1,d_0,r,-s), \]so
\[ (2,-1,\sqrt2,2\sqrt2) \longmapsto (-1,2,\sqrt2,-2\sqrt2). \]This is a signed permutation of real coordinates. It preserves squared length:
\[ 1+4+2+8=15. \]A phase change gives a second concrete audit. Let
\[ D=\operatorname{diag}(1,i), \qquad D^*=\operatorname{diag}(1,-i). \]Then
\[ DH_0D^*= \begin{bmatrix} 2 & 2-i\\ 2+i & -1 \end{bmatrix}. \]On the normalized upper pair, this action is the quarter-turn
\[ (r,s)\longmapsto(s,-r). \]It sends \(z_0\) to \((2,-1,2\sqrt2,-\sqrt2)\), whose square is \(4+1+8+2=15\). The swap was a signed permutation; this phase is a genuine two-coordinate rotation. Both visibly move the displayed matrix while preserving the real Frobenius geometry.
Pointwise invariance is the wrong claim
The theorem in this chapter does not say
\[ UHU^*=H \quad\text{for every sample }H. \]That is false for \(H_0\) and \(P\). The theorem concerns the probability law \(\mu_2\) of the random matrix. A law is a measure on the value space. Pushing that law through the congruence map means applying the deterministic basis change to every possible matrix while transporting its probabilities. The checked equality is
\[ (H\mapsto UHU^*)_*\mu_2=\mu_2. \]Thus a random draw and its conjugate generally differ as matrices while having the same distribution. The pushforward measure is the layer at which invariance lives.
Type and run the size-two arithmetic yourself
The exact Gaussian measures and project theorems are full project checks:
they import Mathlib and may require substantial disk space and memory. The
finite matrix ledger is a standalone tutorial for macOS or Linux. It
imports only Lean’s Std library and stores
complex integers as pairs, checks Hermiticity plus the swap and phase
congruences, and records variances in quarter-units so that \(1/2\) is the
natural number 2 and \(1/4\) is 1.
Create /tmp/NormalizedGUE2Tutorial.lean in a text editor and type:
import Std
structure GaussianInt where
re : Int
im : Int
deriving Repr, DecidableEq
def GaussianInt.conj (z : GaussianInt) : GaussianInt :=
⟨z.re, -z.im⟩
def GaussianInt.normSq (z : GaussianInt) : Int :=
z.re * z.re + z.im * z.im
def GaussianInt.mul (z w : GaussianInt) : GaussianInt :=
⟨z.re * w.re - z.im * w.im,
z.re * w.im + z.im * w.re⟩
structure Matrix2 where
a00 : GaussianInt
a01 : GaussianInt
a10 : GaussianInt
a11 : GaussianInt
deriving Repr, DecidableEq
def matrixEntries (H : Matrix2) : List (Int × Int) :=
[(H.a00.re, H.a00.im), (H.a01.re, H.a01.im),
(H.a10.re, H.a10.im), (H.a11.re, H.a11.im)]
def isHermitian (H : Matrix2) : Bool :=
decide (H.a00.im = 0 ∧ H.a11.im = 0 ∧
H.a10 = H.a01.conj)
def frobeniusSq (H : Matrix2) : Int :=
H.a00.normSq + H.a01.normSq + H.a10.normSq + H.a11.normSq
def correctH : Matrix2 :=
⟨⟨2, 0⟩, ⟨1, 2⟩, ⟨1, -2⟩, ⟨-1, 0⟩⟩
def swapCongruence (H : Matrix2) : Matrix2 :=
⟨H.a11, H.a10, H.a01, H.a00⟩
def swappedH : Matrix2 := swapCongruence correctH
def phaseCongruence (H : Matrix2) : Matrix2 :=
let plusI : GaussianInt := ⟨0, 1⟩
let minusI : GaussianInt := ⟨0, -1⟩
⟨H.a00, H.a01.mul minusI, plusI.mul H.a10, H.a11⟩
def phasedH : Matrix2 := phaseCongruence correctH
def normalizedCoordinateSquares : List Int := [4, 1, 2, 8]
def swappedCoordinateSquares : List Int := [1, 4, 2, 8]
def normalizedNormSq : Int := normalizedCoordinateSquares.sum
def swappedNormalizedNormSq : Int := swappedCoordinateSquares.sum
def wrongUnnormalizedAssemblySq : Int :=
4 + 1 + 2 * (2 + 8)
def normalizedVarianceQuarters : List (String × Nat) :=
[("diagonal 0", 2), ("diagonal 1", 2),
("upper real normalized", 2), ("upper imaginary normalized", 2)]
def decodedEntryVarianceQuarters : List (String × Nat) :=
[("diagonal 0", 2), ("diagonal 1", 2),
("real part of upper entry", 1), ("imaginary part of upper entry", 1)]
#eval normalizedVarianceQuarters
#eval decodedEntryVarianceQuarters
#eval matrixEntries correctH
#eval matrixEntries swappedH
#eval matrixEntries phasedH
#eval (normalizedNormSq, frobeniusSq correctH,
wrongUnnormalizedAssemblySq)
#eval (!decide (correctH = swappedH),
decide (frobeniusSq correctH = frobeniusSq swappedH),
decide (normalizedNormSq = swappedNormalizedNormSq))
#eval (isHermitian correctH, isHermitian swappedH)
#eval (isHermitian phasedH,
decide (frobeniusSq correctH = frobeniusSq phasedH))
example : normalizedNormSq = 15 := by
native_decide
example : frobeniusSq correctH = 15 := by
native_decide
example : wrongUnnormalizedAssemblySq = 25 := by
native_decide
example : swappedH =
⟨⟨-1, 0⟩, ⟨1, -2⟩, ⟨1, 2⟩, ⟨2, 0⟩⟩ := by
native_decide
example : correctH ≠ swappedH := by
native_decide
example : phasedH =
⟨⟨2, 0⟩, ⟨2, -1⟩, ⟨2, 1⟩, ⟨-1, 0⟩⟩ := by
native_decide
example :
frobeniusSq correctH = frobeniusSq swappedH ∧
normalizedNormSq = swappedNormalizedNormSq := by
native_decide
example : isHermitian correctH = true ∧ isHermitian swappedH = true := by
native_decide
example : isHermitian phasedH = true ∧
frobeniusSq correctH = frobeniusSq phasedH := by
native_decide
Run the pinned compiler directly:
source "$HOME/.elan/env"
elan run leanprover/lean4:v4.32.0 lean /tmp/NormalizedGUE2Tutorial.lean
Resource label: small standalone Lean plus Std, suitable for an
ordinary macOS or Linux machine. The command neither enters the Lake project
nor downloads or builds Mathlib.
The executed output is:
[("diagonal 0", 2), ("diagonal 1", 2), ("upper real normalized", 2), ("upper imaginary normalized", 2)]
[("diagonal 0", 2), ("diagonal 1", 2), ("real part of upper entry", 1), ("imaginary part of upper entry", 1)]
[(2, 0), (1, 2), (1, -2), (-1, 0)]
[(-1, 0), (1, -2), (1, 2), (2, 0)]
[(2, 0), (2, -1), (2, 1), (-1, 0)]
(15, 15, 25)
(true, true, true)
(true, true)
(true, true)
The first two lines separate normalized-coordinate variances from decoded entry variances. The next three list the original, swapped, and phase-rotated matrix entries in row-major order. The triple \((15,15,25)\) compares coordinate square, correct Frobenius square, and wrong-decoder square. The remaining Booleans confirm pointwise change, norm preservation, coordinate-norm preservation, and Hermiticity for both concrete congruences.
The worksheet does not define a Gaussian probability measure, prove a full product law, construct Mathlib’s standard Gaussian, or establish measure invariance. Those claims require the exact project modules below.
Generalize the four slots to every finite dimension
Let \(T_n\) be the finite type of strict-upper positions \((i,j)\) with \(i\lt j\). The checked normalized real index is
\[ I_n =\operatorname{Fin}(n)\sqcup(T_n\sqcup T_n). \]Its sectors are semantic:
Sum.inl iis diagonal coordinate \(d_i\);Sum.inr (Sum.inl ij)is normalized upper-real coordinate \(r_{ij}\); andSum.inr (Sum.inr ij)is normalized upper-imaginary coordinate \(s_{ij}\).
The cardinality is
\[ |I_n|=n+2\binom n2=n^2, \]the real dimension of the Hermitian matrices. The source module does not need
to turn this into an arbitrary Fin (n^2) enumeration. The semantic
sum tells every decoder branch which role a coordinate has.
The definitions hermitianRealIndexToPair and
pairToHermitianRealIndex match those semantic slots with all
matrix positions. A diagonal slot maps to \((i,i)\), a real-upper slot to
\((i,j)\), and its imaginary partner to the reflected position \((j,i)\).
The two inverse theorems package this as
hermitianRealIndexEquivMatrixIndex. That equivalence later
reindexes the Frobenius sum without choosing a basis ordering.
Decode, analyze, and prove the real isometry
The coordinate carrier is
\[ E_n=\operatorname{EuclideanSpace}(\mathbb R,I_n). \]A point in \(E_n\) is a real function on the finite index wrapped in a finite \(\ell^2\) structure. The target is \(\mathcal H_n\), the intrinsic real Euclidean space of Hermitian matrices with the inherited Frobenius inner product.
Why real? If \(H\) is Hermitian, then \(rH\) is Hermitian for every real \(r\). Multiplication by an arbitrary complex scalar need not preserve \(H^*=H\). The Hermitian locus is a real subspace of the complex Frobenius carrier, not generally a complex subspace.
The synthesis map \(\Phi_n:E_n\to\mathcal H_n\) uses
\[ (\Phi_n z)_{ii}=d_i, \qquad (\Phi_n z)_{ij} =\frac{r_{ij}}{\sqrt2}+i\frac{s_{ij}}{\sqrt2} \quad(i\lt j), \]and conjugate reflection below the diagonal. The analysis map reads
\[ d_i=H_{ii}, \qquad r_{ij}=\sqrt2\operatorname{Re}(H_{ij}), \qquad s_{ij}=\sqrt2\operatorname{Im}(H_{ij}). \]The source proves both round trips, real linearity, and the stronger inner product identity
\[ \langle\Phi_n x,\Phi_n y\rangle_F =\langle x,y\rangle_2. \]The norm identity from the opening example is the case \(x=y=z_0\).
Lean bridge: read one strict-upper entry
(normalizedHermitianAssembly x : FrobeniusMatrix n) ij.1 = ⟨x (.inr (.inl ij)) / Real.sqrt 2, x (.inr (.inr ij)) / Real.sqrt 2⟩ij : StrictUpperIndex ncontains a pair and proof that its row is strictly less than its column..inr (.inl ij)selects the real-upper sector;.inr (.inr ij)selects the imaginary-upper sector.⟨re, im⟩constructs the complex number with those two Cartesian coordinates.- The exact theorem is
RandomMatrix.normalizedHermitianAssembly_apply_upper.
Run boundary. Replay the theorem with the full primary-module check near the end. The local worksheet checks only its displayed size-two arithmetic.
Lean bridge: the decoder preserves the real inner product
inner ℝ (normalizedHermitianAssembly x) (normalizedHermitianAssembly y) = inner ℝ x yinner ℝmakes the scalar field explicit. The intrinsic Hermitian carrier is real.- The two appearances of
normalizedHermitianAssemblyare compared in the Frobenius geometry inherited by the subtype. - The theorem is
RandomMatrix.normalizedHermitianAssembly_inner. normalizedHermitianLinearIsometryEquiv nthen bundles the inverse maps, real linearity, and norm preservation for downstream Gaussian transport.
Run boundary. The exact proof reindexes finite sums and uses Mathlib, so it is a full project check. The numeric \(15=15\) case is safe in the standalone worksheet.
The coordinate law is a complete product law
Geometry alone does not define probability. Put the common centered Gaussian law of variance \(v_n\) on every normalized real slot:
\[ \Pi_n=\bigotimes_{k\in I_n}\gamma_{0,v_n}. \]At size two this is the fourfold product of \(\gamma_{0,1/2}\). The word product carries the mutual-independence structure. It is stronger than a list of four marginal law statements.
The decoder splits \(I_n\) into the diagonal, upper-real, and upper-imaginary families. It divides both upper families by \(\sqrt2\), pairs them pointwise as complex numbers, and produces the earlier coordinate carrier
\[ (\operatorname{Fin}(n)\to\mathbb R) \times(T_n\to\mathbb C). \]The scalar transport identity is
\[ (x\mapsto x/\sqrt2)_*\gamma_{0,v_n} =\gamma_{0,v_n/2}. \]Two real upper products therefore become the exact Cartesian complex product whose real and imaginary variances are both \(v_n/2\). At \(n=2\), this is \(1/4\) and \(1/4\).
Why matching marginals would not be enough
Four variables could each have law \(\gamma_{0,1/2}\) while being completely dependent. For example, copying one Gaussian variable into all four slots gives the right scalar marginals and the wrong joint law. RMT-08 does not infer independence from variance calculations. It transports the complete finite product measure through measurable sum/product equivalences.
Lean bridge: decode the entire product at once
(gaussianProductMeasure (fun _ : HermitianRealIndex n ↦ 0) (fun _ ↦ varianceScale n)).map RandomMatrix.realToHermitianCoordinates = coordinateMeasure ngaussianProductMeasureis the finite product of exact real Gaussian measures.- The first function supplies mean zero at every semantic index.
- The second supplies the same variance
varianceScale nat every normalized index. .map RandomMatrix.realToHermitianCoordinatesis the pushforward through the decoder.coordinateMeasure nis the earlier nested diagonal/complex-upper law, including all block independence.- The theorem is
GUE.map_realToHermitianCoordinates_gaussianProduct.
Run boundary. This equality uses Mathlib finite product measures and must be checked through the full project check. No claim in the local integer worksheet substitutes for it.
Standard Gaussian transport supplies the basis-neutral shape
Mathlib’s stdGaussian E is the canonical centered standard
Gaussian on a finite real Euclidean space \(E\). On a coordinate Euclidean
space, a product of unit-variance real Gaussians becomes this measure after
the finite \(\ell^2\) packaging. A real linear isometric equivalence transports
it to the standard Gaussian on the target Euclidean space.
For a common variance \(v\), first scale a unit-variance coordinate vector by \(\sqrt v\). Coordinatewise,
\[ \sqrt v\,G\sim\gamma_{0,v} \quad\text{when}\quad G\sim\gamma_{0,1}. \]The source proves the full finite-product version:
\[ (\operatorname{toLp})_*\bigotimes_i\gamma_{0,v}= (x\mapsto\sqrt v\,x)_*\operatorname{stdGaussian}(E). \]Now use the normalized isometry \(\Phi_n\). Standard Gaussian shape is unchanged by an isometric coordinate change, while uniform scalar multiplication commutes with real linear maps. The intrinsic GUE law is
\[ \Gamma_n =(H\mapsto\sqrt{v_n}\,H)_* \operatorname{stdGaussian}(\mathcal H_n). \]At size two, the common scale is
\[ \sqrt{v_2}=\sqrt{1/2}=1/\sqrt2. \]The standard Gaussian supplies isotropic shape. The scalar supplies the dimension-dependent Wigner scale. These are separate responsibilities.
Lean bridge: identify the intrinsic law
GUE.intrinsicLaw n = (stdGaussian (RandomMatrix.HermitianEuclidean n)).map (fun H ↦ Real.sqrt (GUE.varianceScale n : ℝ) • H)GUE.intrinsicLaw nis a measure whose values are intrinsically Hermitian points.stdGaussiansupplies the canonical basis-neutral Euclidean law.Real.sqrt (GUE.varianceScale n : ℝ)converts the nonnegative variance parameter to its real standard-deviation scale.• His real scalar multiplication in the intrinsic Hermitian space.- The theorem is
GUE.intrinsicLaw_eq_map_smul_stdGaussian.
Run boundary. The exact statement and its stdGaussian_map
proof require the full project module. The local worksheet checks the size-two
normalization but does not define stdGaussian.
Keep coordinate, intrinsic, and ambient carriers distinct
The proof uses several spaces because each carries different useful structure.
| Layer | Carrier | Measure or map | What the layer contributes |
|---|---|---|---|
| normalized real coordinates | \(I_n\to\mathbb R\), then \(E_n\) | common product \(\Pi_n\) | exact independent scalar law and Euclidean coordinates |
| old assembly coordinates | diagonal reals times strict-upper complexes | coordinateMeasure n | the repository’s explicit entrywise variance convention |
| intrinsic Hermitian space | \(\mathcal H_n\) | GUE.intrinsicLaw n | real inner product, isometries, and standard Gaussian symmetry |
| ambient matrix space | all \(n\times n\) complex matrices | GUE.matrixLaw n | the public random-matrix law and its ambient congruence action |
The intrinsic carrier is a subtype: a point contains a Frobenius vector and a proof that its matrix is Hermitian. The ambient carrier contains Hermitian and non-Hermitian matrices alike. The inclusion
\[ \iota_n:\mathcal H_n\to\operatorname{Matrix}_n(\mathbb C) \]forgets the subtype proof without changing any entry.
The intrinsic law is the coordinate law pushed through intrinsic assembly. The ambient law is the intrinsic law pushed through inclusion:
\[ \mu_n=(\iota_n)_*\Gamma_n. \]This equality is the bridge from basis-neutral geometry back to the exact entrywise law defined earlier.
Matrix-law support means full mass here
The preceding geometry module proves that the ambient Hermitian set is measurable and
\[ \mu_n\{H:H^*=H\}=1, \qquad \mu_n\{H:H^*\ne H\}=0. \]It also states the almost-everywhere Hermitian property. These are
measure-theoretic full-mass claims. They do not identify Mathlib’s topological
Measure.support, prove a density on the Hermitian subspace, or
show that every ambient matrix lies in the image.
Lean bridge: move the intrinsic law into ambient matrices
GUE.matrixLaw n = (GUE.intrinsicLaw n).map RandomMatrix.hermitianToMatrixGUE.matrixLaw nis a measure on all complex matrices of sizen.GUE.intrinsicLaw nis a measure on the Hermitian subtype.RandomMatrix.hermitianToMatrixforgets intrinsic packaging and returns the same entries in ambient matrix space..mappushes the complete measure through that measurable map.- The theorem is
GUE.matrixLaw_eq_map_hermitianToMatrix_intrinsicLaw.
Run boundary. The full module check elaborates the exact carrier types and measurability. The local tutorial contains only the concrete matrices.
The checked route to unitary invariance
Let \(U\) be any deterministic bundled unitary matrix. RMT-07 proves that intrinsic congruence
\[ \mathcal C_U(H)=UHU^* \]is a real linear isometric equivalence of \(\mathcal H_n\). Therefore the canonical intrinsic standard Gaussian is invariant:
\[ (\mathcal C_U)_*\operatorname{stdGaussian}(\mathcal H_n) =\operatorname{stdGaussian}(\mathcal H_n). \]Uniform real scaling commutes pointwise with congruence:
\[ \mathcal C_U(\sqrt{v_n}H) =\sqrt{v_n}\,\mathcal C_U(H). \]Repeated use of measurable pushforward composition then gives
\[ \begin{aligned} (\mathcal C_U)_*\Gamma_n &=(\mathcal C_U)_*(H\mapsto\sqrt{v_n}H)_*\gamma_n\\ &=(H\mapsto\sqrt{v_n}H)_*(\mathcal C_U)_*\gamma_n\\ &=(H\mapsto\sqrt{v_n}H)_*\gamma_n\\ &=\Gamma_n, \end{aligned} \]where \(\gamma_n=\operatorname{stdGaussian}(\mathcal H_n)\). This is
GUE.map_intrinsicLaw_hermitianCongruence.
The inclusion intertwines intrinsic and ambient congruence pointwise:
\[ \iota_n(\mathcal C_U H) =\widehat{\mathcal C}_U(\iota_nH). \]Since \(\mu_n=(\iota_n)_*\Gamma_n\), another pushforward calculation gives
\[ (\widehat{\mathcal C}_U)_*\mu_n=\mu_n. \]Every arrow needs ordinary measurability before Measure.map_map
can reassociate it. Every commuting square is proved as a pointwise function
identity before it is used to rewrite a measure. The proof does not infer
measure equality from a picture.
Lean bridge: the final law-level statement
RandomMatrix.IsUnitaryConjugationInvariant (GUE.matrixLaw n)IsUnitaryConjugationInvariantexpands to a universal statement overU : Matrix.unitaryGroup (Fin n) ℂ.GUE.matrixLaw nis the exact ambient law constructed from the specified coordinate measure.- The predicate compares
Measure.mapwith the original measure. It never asks forU * H * Uᴴ = Hpointwise. - The checked theorem is
GUE.matrixLaw_isUnitaryConjugationInvariant.
Run boundary. This is the primary full project theorem. The swap worksheet checks one deterministic congruence but cannot establish equality of Gaussian measures.
Why no density theorem is imported
Classically, finite GUE is often presented using a density proportional to
\[ \exp\!\left(-\frac n2\operatorname{Tr}(H^2)\right) \]with respect to a specified Euclidean volume on Hermitian space. Unitary congruence preserves \(\operatorname{Tr}(H^2)\), so that formula suggests invariance. Guionnet records this normalization and symmetry in the standard random-matrix presentation cited below.
That route would require the formal development to define the reference volume, prove the coordinate Jacobian, normalize the density, identify the entrywise law with that density, and prove change of variables. RMT-08 imports none of those conclusions. Its route is instead
\[ \text{exact finite product law} \longrightarrow \text{real isometric decoding} \longrightarrow \text{scaled intrinsic standard Gaussian} \longrightarrow \text{commuting pushforwards} \longrightarrow \text{ambient law invariance}. \]This proves the desired measure equality without claiming a density or a Jacobian theorem. A future density proof may identify another presentation of the same law, but it cannot be treated as already formalized here.
Dimension zero stays inside the same construction
At \(n=0\), Fin 0 and the strict-upper index are empty, so
HermitianRealIndex 0 is empty. There is one function from an empty
type to \(\mathbb R\), one empty Hermitian matrix, and one empty ambient
matrix.
The project defines
\[ v_0=0. \]The empty finite Gaussian product is Dirac at the unique empty coordinate
function. The coordinate, intrinsic, and ambient laws are all Dirac at their
unique zero points. The theorem
GUE.intrinsicLaw_zero states the intrinsic equality explicitly.
The fixed geometric factor \(\sqrt2\) and the dimension scale
\(\sqrt{v_n}\) must not be conflated. The former orthonormalizes upper entries
and is always nonzero. The latter scales the probability law and becomes zero
at dimension zero. Because the source uses varianceScale rather
than the partial-looking expression \(1/n\), the general invariance theorem
includes \(n=0\) without a separate positive-dimension premise.
What is checked in each source module
The geometry predecessor establishes the carrier and symmetry before the law comparison. The primary RMT-08 module establishes the comparison and final transport.
| Source layer | Checked results | Explicitly absent |
|---|---|---|
GaussianUnitaryEnsembleGeometry | Frobenius carrier, intrinsic real Hermitian subspace, unitary congruence isometries, intrinsic standard-Gaussian invariance, measurable Hermitian locus, full-mass ambient Hermitian law | equality with scaled intrinsic GUE, final ambient invariance, densities, spectra |
GaussianUnitaryEnsembleInvariance | normalized real index, analysis/synthesis, real isometry, exact product decoding, scaled intrinsic law, intrinsic probability and zero law, ambient inclusion law, intrinsic and ambient invariance | density, Jacobian, eigenvalues, moments, asymptotics |
Inspect the geometry and support interfaces
Full project check: predecessor project module plus Mathlib. Put these lines in a temporary project scratch file after installing the repository’s pinned dependencies:
import NonlinearDynamics.Random.RandomMatrices.GaussianUnitaryEnsembleGeometry
open Matrix MeasureTheory ProbabilityTheory
open scoped Matrix RealInnerProductSpace
open NonlinearDynamics.Random
#check RandomMatrix.FrobeniusMatrix
#check RandomMatrix.HermitianEuclidean
#check RandomMatrix.hermitianToMatrix
#check RandomMatrix.hermitianUnitaryCongruenceLinearIsometryEquiv
#check RandomMatrix.map_stdGaussian_hermitianUnitaryCongruence
#check RandomMatrix.hermitianSet
#check RandomMatrix.measurableSet_hermitianSet
#check GUE.matrixLaw_hermitianSet
#check GUE.matrixLaw_ae_isHermitian
#check GUE.matrixLaw_compl_hermitianSet
The #check commands inspect existing declarations; they do not
sample a matrix. The full project command rendered below checks the exact
source file and may require substantial disk space and memory.
cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomMatrices/GaussianUnitaryEnsembleGeometry.leanResource note: this exact file uses the repository's
pinned Lean and Mathlib dependencies. Initial project setup can require
substantial disk space and build time. For a lightweight first step on
macOS or Linux, use the page's standalone Lean-core or Std
tutorial.
Inspect the normalization and invariance interfaces
Full project check: primary project module plus Mathlib. Type this exact probe in a temporary project scratch file:
import NonlinearDynamics.Random.RandomMatrices.GaussianUnitaryEnsembleInvariance
open Matrix MeasureTheory ProbabilityTheory
open scoped Matrix NNReal ENNReal RealInnerProductSpace
open NonlinearDynamics.Random
#check HermitianRealIndex
#check hermitianRealIndexEquivMatrixIndex
#check RandomMatrix.normalizedHermitianAssembly
#check RandomMatrix.normalizedHermitianAnalysis
#check RandomMatrix.normalizedHermitianAssembly_apply_upper
#check RandomMatrix.normalizedHermitianAssembly_inner
#check RandomMatrix.normalizedHermitianLinearIsometryEquiv
#check gaussianReal_map_div_sqrt_two
#check GUE.map_realToHermitianCoordinates_gaussianProduct
#check GUE.intrinsicLaw
#check GUE.intrinsicLaw_eq_map_smul_stdGaussian
#check GUE.intrinsicLaw_zero
#check GUE.matrixLaw_eq_map_hermitianToMatrix_intrinsicLaw
#check GUE.map_intrinsicLaw_hermitianCongruence
#check GUE.matrixLaw_isUnitaryConjugationInvariant
import loads the pinned source and dependencies. Each
#check elaborates an exact declaration and displays its
type. The full project command below checks the whole authoritative leaf.
cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomMatrices/GaussianUnitaryEnsembleInvariance.leanResource note: this exact file uses the repository's
pinned Lean and Mathlib dependencies. Initial project setup can require
substantial disk space and build time. For a lightweight first step on
macOS or Linux, use the page's standalone Lean-core or Std
tutorial.
The complete RMT-08 declaration map
The primary module exports 35 public declarations. The table records what each one checks and prevents prose from attributing a later theorem to an earlier definition.
| Declaration | Checked content |
|---|---|
HermitianRealIndex | semantic diagonal, upper-real, and upper-imaginary index |
hermitianRealIndexToPair | map each semantic real slot to one matrix position |
pairToHermitianRealIndex | classify every matrix position into one semantic sector |
pairToHermitianRealIndex_toPair | first index/pair round trip |
hermitianRealIndexToPair_pairTo | second pair/index round trip |
hermitianRealIndexEquivMatrixIndex | equivalence with all matrix-entry pairs |
RandomMatrix.realToHermitianCoordinates | raw normalized decoder into the old coordinate carrier |
RandomMatrix.measurable_realToHermitianCoordinates | ordinary measurability of that decoder |
RandomMatrix.normalizedHermitianAssembly | normalized Euclidean coordinates to intrinsic Hermitian space |
RandomMatrix.normalizedHermitianAnalysis | intrinsic Hermitian point to normalized coordinates |
RandomMatrix.hermitianToMatrix_normalizedHermitianAssembly | intrinsic forgetting exposes the old assembled matrix |
RandomMatrix.normalizedHermitianAssembly_apply_diag | diagonal entry formula |
RandomMatrix.normalizedHermitianAssembly_apply_upper | strict-upper formula with both \(1/\sqrt2\) factors |
RandomMatrix.normalizedHermitianAssembly_apply_lower | conjugate-reflected lower formula |
RandomMatrix.normalizedHermitianAnalysis_assembly | analysis after assembly is identity |
RandomMatrix.normalizedHermitianAssembly_analysis | assembly after analysis is identity |
RandomMatrix.normalizedHermitianLinearEquiv | real linear equivalence between coordinate and intrinsic carriers |
RandomMatrix.normalizedHermitianAssembly_inner | exact real inner-product preservation |
RandomMatrix.normalizedHermitianLinearIsometryEquiv | bundled real linear isometric equivalence |
map_gaussianProduct_toLp_eq_map_smul_stdGaussian | common-variance product becomes a scaled Euclidean standard Gaussian |
gaussianReal_map_div_sqrt_two | division by \(\sqrt2\) halves centered real Gaussian variance |
realUpperToComplex | pair two upper real families after normalization |
measurable_realUpperToComplex | measurability of the complex pairing map |
map_realUpperToComplex_gaussianProduct | exact two-real-products to Cartesian-complex-product law |
GUE.coordinateToHermitianEuclidean | old GUE coordinates assembled into intrinsic space |
GUE.measurable_coordinateToHermitianEuclidean | ordinary measurability of intrinsic assembly |
GUE.coordinateToHermitianEuclidean_realToHermitianCoordinates | old assembly after decoding equals normalized assembly |
GUE.map_realToHermitianCoordinates_gaussianProduct | full normalized product decodes to the earlier coordinate measure |
GUE.intrinsicLaw | intrinsic law as a coordinate-measure pushforward |
GUE.instIsProbabilityMeasureIntrinsicLaw | intrinsic law is a probability measure in every dimension |
GUE.intrinsicLaw_eq_map_smul_stdGaussian | intrinsic law is scaled canonical standard Gaussian |
GUE.intrinsicLaw_zero | zero-dimensional intrinsic law is Dirac at zero |
GUE.matrixLaw_eq_map_hermitianToMatrix_intrinsicLaw | ambient matrix law is the included intrinsic law |
GUE.map_intrinsicLaw_hermitianCongruence | unitary congruence preserves intrinsic GUE |
GUE.matrixLaw_isUnitaryConjugationInvariant | every unitary congruence preserves ambient GUE law |
The checked source has no sorry or admit. Its
recorded project build compiled the leaf and aggregators with warnings treated
as errors against Lean 4.32.0 and pinned Mathlib 4.32.0.
Physics window: basis neutrality, stated narrowly
A finite quantum Hamiltonian is represented by a Hermitian matrix after an orthonormal basis is chosen. A deterministic basis change by \(U\) replaces the coordinate matrix by \(UHU^*\). The abstract operator has not acquired new physics; its coordinate description changed.
The entrywise GUE construction initially appears to favor one basis because it names diagonal and upper coordinates. The normalized real-coordinate bridge shows why that preference disappears from the probability law. After the \(\sqrt2\) correction, the primitive variables are common-variance Gaussian coordinates in the real Frobenius geometry. Their intrinsic law has no preferred orthonormal real basis. Unitary congruence is one real orthogonal transformation of that space, so the law cannot detect it.
Dyson’s unitary symmetry class supplies historical physical context. The Lean theorem is narrower: for each finite \(n\), every deterministic bundled unitary matrix preserves the specified ambient probability measure. It does not sample \(U\) from Haar measure, define time evolution, formalize time reversal, unfold energy levels, or prove universal spectral statistics.
Common wrong turns
| Wrong turn | Why it fails | Checked repair |
|---|---|---|
| Place normalized upper slots directly into the matrix. | Frobenius square becomes 25 instead of 15 in the example, and upper component variance is wrong. | Divide both upper slots by \(\sqrt2\). |
| Match all scalar variances and declare the vector laws equal. | Marginals do not encode mutual independence or the full joint law. | Transport the complete product measure. |
| Say unitary invariance means \(UHU^*=H\) for every sample. | The swap example is an explicit counterexample. | Compare the pushed-forward matrix law with itself. |
Apply intrinsic standard-Gaussian symmetry directly to matrixLaw. | The measures initially live on different carriers. | Prove the intrinsic representation and ambient inclusion pushforward first. |
| Treat Hermitian space as a complex vector space. | Multiplication by a general complex scalar can destroy Hermiticity. | Use the intrinsic real submodule and real isometries. |
Treat Measure.map_map as syntax-only reassociation. | The composition theorem needs measurability evidence. | Prove each deterministic map measurable before rewriting pushforwards. |
| Call full mass “topological support.” | A mass-one measurable locus is not an equality with Measure.support. | State the full-mass and complement-zero theorems exactly. |
| Import the classical density into the proof. | No reference volume, Jacobian, or density equivalence is formalized here. | Use finite product transport and standard-Gaussian isometries. |
| Divide by \(\sqrt n\) in the geometric decoder. | That confuses dimension scale with upper-entry orthonormalization and fails at zero. | Keep fixed \(1/\sqrt2\) decoding separate from \(\sqrt{v_n}\) law scaling. |
| Infer eigenvalue or moment results from invariance. | Law symmetry alone does not define or integrate those observables. | Build each spectral and integrability layer separately. |
Exercises: keep the size-two matrix in view
- Index. List the four semantic elements of
HermitianRealIndex 2and their sum-type constructors. - Decode. Decode \((0,3,-2\sqrt2,\sqrt2)\) into a Hermitian matrix.
- Analyze. Apply the inverse formulas to that matrix and recover the four normalized coordinates.
- Metric. Compute both squared norms for the new point and verify equality.
- Wrong decoder. Omit \(1/\sqrt2\) for the new point and compute the norm discrepancy.
- Variance. Starting with normalized variance \(1/2\), derive each decoded entry-component variance.
- Dependence near-miss. Let all four normalized coordinates equal one common \(\gamma_{0,1/2}\) variable. Which marginal facts remain true, and which product-law fact fails?
- Swap. Multiply \(PH_0P\) by hand, one row and column at a time.
- Point versus law. State separately the false pointwise equation, the true norm equation, and the checked measure equation.
- Phase unitary. Try a diagonal unitary \(\operatorname{diag}(1,i)\). Compute how it changes the upper entry of \(H_0\).
- Real carrier. Give one complex scalar \(c\) and one Hermitian matrix \(H\) for which \(cH\) is not Hermitian.
- Pushforward. Write the preimage formula that defines \((\iota_n)_*\Gamma_n(B)\) for a measurable ambient set \(B\).
- Support language. Explain why mass one on the Hermitian locus does not by itself identify topological support.
- Standard Gaussian. Separate the shape-preserving isometry from the scalar \(\sqrt{v_n}\) in the intrinsic-law formula.
- Zero dimension. Count every coordinate index and explain why the law is Dirac without evaluating \(1/\sqrt0\).
- Lean tokens. Change
correctHin the local worksheet to the matrix from exercise 2 and update every displayed output and example. - Resource boundary. Explain why the standalone worksheet is small while the two full project checks load the repository’s pinned Mathlib dependencies.
- Density boundary. List the reference-volume and change-of-variables obligations needed before the classical exponential formula could become a checked alternative construction.
Summit summary
The proof dependency chain is now visible in one exact example and in the general declarations:
\[ \begin{aligned} &\text{common independent real Gaussian product}\\ &\quad\longrightarrow\text{normalized decoder with }1/\sqrt2\\ &\quad\longrightarrow\text{exact coordinate law and real Frobenius isometry}\\ &\quad\longrightarrow\text{scaled intrinsic standard Gaussian}\\ &\quad\longrightarrow\text{intrinsic unitary-law invariance}\\ &\quad\longrightarrow\text{ambient matrix-law invariance}. \end{aligned} \]For the concrete swap, the matrix changes while its norm remains 15. For the random ensemble, the pushforward law remains exactly the same. The first fact illustrates a real isometry; the second is a probability theorem. Neither requires a density, and neither should be rewritten as pointwise fixedness.
Where to continue
- Normalized Hermitian coordinates gives the compact coordinate and factor-two ledger.
- Unitary invariance isolates the measure-level symmetry definition and its pointwise near-miss.
- Finite GUE from Independent Gaussian Coordinates constructs the entrywise coordinate and ambient laws used here.
- Intrinsic Hermitian Gaussian Symmetry and Matrix-Law Support proves the geometry and full-mass Hermitian facts transported here.
- First Exact Finite Gaussian Unitary Ensemble Trace Moments adds the separate integrability and expectation layer.
- Finite Hermitian Spectra and Empirical Measures constructs finite spectral observables without treating invariance as a substitute for measurability.
References
Mathlib contributors.
Multivariate Gaussian distributions,
Mathlib 4 documentation. This is the official API source for
stdGaussian, map_pi_eq_stdGaussian, and
stdGaussian_map under real linear isometries.
Mathlib contributors. Real Gaussian distributions, indexed product measures, and measure maps, Mathlib 4 documentation. These official references specify variance parameterization, scalar Gaussian transport, finite products, and measurable pushforward composition.
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 records the GUE diagonal variance \(1/n\), upper real and imaginary variances \(1/(2n)\), invariant density convention, and unitary symmetry. This chapter’s checked proof does not use that density.
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 in formalization/lake-manifest.json.