From Coordinates to Symmetry: Proving Finite GUE Unitary Invariance in Lean

This is the proof-to-prose companion for formalization/NonlinearDynamics/Random/RandomMatrices/GaussianUnitaryEnsembleInvariance.lean. Every named public declaration in that stable source is mapped below.

The immediate predecessor, The Geometry Behind GUE in Lean, proves the intrinsic isometry and standard-Gaussian symmetry while carefully not claiming symmetry of GUE.matrixLaw. The coordinate measure itself is constructed in A Finite GUE Law in Lean, and its deterministic matrix assembly comes from Hermitian Coordinate Assembly.

For the parallel textbook treatment of this milestone, see From Normalized Hermitian Coordinates to Gaussian Unitary Ensemble Invariance. Its slower prerequisite development continues in Intrinsic Hermitian Gaussian Symmetry and Matrix-Law Support, Finite GUE from Independent Gaussian Coordinates, and Finite Hermitian Matrices from Coordinates. Reusable definitions are indexed under gaussian-unitary-ensemble , hermitian-frobenius-geometry , normalized-hermitian-coordinates , normalization-convention , unitary-invariance , pushforward measure and independence .

Choose a route up

Learning objectives

By the summit, a reader should be able to:

1. explain why RMT-07’s intrinsic Gaussian symmetry does not automatically apply to RMT-06’s independently constructed coordinate law;
2. construct a disjoint real index with diagonal, upper-real, and upper-imaginary sectors;
3. derive the factor two in the Frobenius norm of a Hermitian matrix;
4. derive the corresponding \(\sqrt{2}\) rescaling of upper real and imaginary coordinates;
5. describe mutually inverse normalized analysis and synthesis maps;
6. explain why those maps are real linear and isometric;
7. turn a product of complex Cartesian Gaussian laws into two real product laws without assuming a density;
8. use sum-index and function-product equivalences to reassociate a finite product measure;
9. compute why division by \(\sqrt{2}\) changes common variance \(v\) into \(v/2\);
10. identify a common-variance Euclidean product as a scaled standard Gaussian;
11. state the intrinsic-to-ambient commuting square for unitary congruence;
12. prove the final measure equality by repeated pushforward composition;
13. understand why the same construction handles dimension zero; and
14. distinguish unitary invariance of the matrix law from density, spectral, moment, and asymptotic theorems.

The bridge in one picture

flowchart LR
  C["RMT-06 block coordinates"] --> M["coordinateMeasure n"]
  R["one real sum index"] --> P["common-variance real product"]
  P -->|"decode: divide upper sectors by sqrt(2)"| M
  R --> E["real Euclidean coordinate space"]
  E -->|"Frobenius linear isometry"| H["intrinsic Hermitian space"]
  P --> G["scaled intrinsic stdGaussian"]
  G -->|"ambient inclusion"| L["GUE.matrixLaw n"]
  U["intrinsic unitary isometry"] --> G
  G -->|"invariant"| G
  U -. "commuting square" .-> A["ambient unitary congruence"]
  A --> L

Figure. RMT-06 supplies the coordinate law and RMT-07 supplies intrinsic Gaussian symmetry. RMT-08 checks the product decoder, normalized Frobenius isometry, scaled-law identification, and final transfer. No density or Jacobian is needed: every step is an equality produced by a measurable map.

The temptation is to argue in one sentence: both laws are centered isotropic Gaussians on Hermitian matrices, so they are equal. That sentence hides four formal obligations:

1. the RMT-06 law is not initially a measure on the intrinsic Hermitian type;
2. its free coordinates are not orthonormal in their displayed normalization;
3. its probability law is packaged as a nested real/complex block product, not as Mathlib’s stdGaussian; and
4. the final project predicate is about an ambient matrix pushforward, not an intrinsic subtype measure.

RMT-08 is the deliberate discharge of those four obligations.

Camp one: one real index for all Hermitian degrees of freedom

Let

RMT-06 stores a coordinate point as

That is the natural representation for assembly: one real diagonal value and one complex number above the diagonal. It is not yet the natural real Euclidean representation. Split each complex number into its real and imaginary components and index the resulting coordinates by the disjoint sum

The three sectors mean:

• inl i: diagonal coordinate \(d_i\);
• inr (inl ij): normalized real part of \(u_{ij}\); and
• inr (inr ij): normalized imaginary part of \(u_{ij}\).

The nesting order is not deep mathematics. It is a concrete way to let Lean’s sum-type equivalences split and recombine finite dependent function spaces. It also makes the dimension ledger transparent:

That cardinality is the familiar real dimension of the Hermitian matrices. The bridge does not need to choose an arbitrary enumeration by Fin (n^2). The semantic sum index keeps the diagonal, real-upper, and imaginary-upper cases distinguishable in each proof.

The same index enumerates every matrix position

The inner-product proof needs to compare a sum over \(I_n\) with a sum over all matrix pairs. hermitianRealIndexToPair makes that comparison concrete. It sends a diagonal index to \((i,i)\), a real-upper index to \((i,j)\), and the corresponding imaginary-upper index to the reflected lower position \((j,i)\). The last choice is deliberate: the two copies of each strict-upper index account for the two ambient Frobenius entries.

pairToHermitianRealIndex performs the inverse classification by comparing the row and column. The simplification theorems pairToHermitianRealIndex_toPair and hermitianRealIndexToPair_pairTo check the two round trips, and hermitianRealIndexEquivMatrixIndex bundles them as a finite equivalence. The geometry proof later invokes its finite-sum transport theorem instead of proving a separate cardinality formula.

The Euclidean carrier

The corresponding Hilbert carrier is

A point of \(E_n\) is a real function on \(I_n\) wrapped in the finite \(\ell^2\) structure used by Mathlib. The wrapper supplies exactly the norm, inner product, Borel measurable space, finite-dimensional instances, and standard-Gaussian API that the bridge needs.

The index is empty at \(n=0\). Thus \(E_0\) has one point without any special quotient or arbitrary basis choice.

Why the upper triangle needs a square root of two

Take a Hermitian matrix \(H\) with diagonal entries \(d_i\in\mathbb R\) and strict-upper entries

Hermiticity forces \(H_{ji}=\overline{u_{ij}}\). The Frobenius norm counts both positions:

Therefore the orthonormal real coordinates are

This factor is forced simultaneously by geometry and probability. Omitting it would make the coordinate-to-matrix map fail to preserve norm. It would also leave diagonal coordinates with variance \(1/n\) and upper real coordinates with variance \(1/(2n)\), so the resulting real vector would not be isotropic.

Normalized analysis

The analysis map reads an intrinsic Hermitian point \(H\) into \(E_n\):

The diagonal is real because \(H\) is Hermitian. In Lean, extracting it as a real scalar may require an explicit proof that its imaginary part vanishes; the intrinsic subtype carries the Hermiticity evidence that supplies this fact.

This operation is RandomMatrix.normalizedHermitianAnalysis. It returns a point of EuclideanSpace ℝ (HermitianRealIndex n) directly, using WithLp.toLp 2 to install the finite \(\ell^2\) wrapper.

Normalized synthesis

The synthesis map sends \(z\in E_n\) back to a Hermitian matrix. Its free coordinates are

The existing deterministic Hermitian assembly then fills the lower triangle by conjugation. Division is only by the fixed positive number \(\sqrt{2}\), never by \(\sqrt{n}\). Consequently this definition remains valid when \(n=0\); there are no upper indices on which the formula can be evaluated.

RandomMatrix.realToHermitianCoordinates is the raw decoder from a real function on \(I_n\) to the RMT-06 product carrier, and RandomMatrix.measurable_realToHermitianCoordinates checks that decoder’s measurability. RandomMatrix.normalizedHermitianAssembly composes the decoder with the old Hermitian assembly and lands in the intrinsic subtype. RandomMatrix.hermitianToMatrix_normalizedHermitianAssembly records the corresponding commuting edge to ambient matrices.

Three simplification theorems expose the entries: RandomMatrix.normalizedHermitianAssembly_apply_diag, RandomMatrix.normalizedHermitianAssembly_apply_upper, and RandomMatrix.normalizedHermitianAssembly_apply_lower. They are the local API used by inverse and inner-product proofs, so downstream arguments do not need to unfold the nested conditional assembly definition.

Inverses, linearity, and isometry

The intended proof proceeds in increasing structural strength:

1. show that analysis after synthesis returns every diagonal, upper-real, and upper-imaginary coordinate;
2. show that synthesis after analysis returns every diagonal, upper, and lower matrix entry;
3. package synthesis and analysis as a real linear equivalence; and
4. use the factor-two norm identity to upgrade it to a real linear isometric equivalence.

The entry cases matter. Above the diagonal, one uses the supplied complex coordinate. Below the diagonal, equality follows only after conjugation is tracked. On the diagonal, Hermiticity turns the complex entry into its real part. A single ext without this trichotomy is unlikely to expose the right normal form.

Once bundled, the isometry automatically gives continuity and measurability. That matters twice: Mathlib’s Gaussian isometry theorem requires a bundled real linear isometry, and Measure.map_map requires the measurable maps whose composition is being reassociated.

The checked names follow that ladder exactly. RandomMatrix.normalizedHermitianAnalysis_assembly and RandomMatrix.normalizedHermitianAssembly_analysis are the inverse laws; RandomMatrix.normalizedHermitianLinearEquiv is the real linear bundle; RandomMatrix.normalizedHermitianAssembly_inner is the exact inner-product identity; and RandomMatrix.normalizedHermitianLinearIsometryEquiv is the final isometric equivalence. The inner proof reindexes all matrix pairs through hermitianRealIndexEquivMatrixIndex, splits the nested sum, uses \((\sqrt{2})^2=2\), and closes the remaining scalar identity by ring algebra.

Camp two: the probability ledger becomes isotropic

RMT-06 fixes the Wigner scale

Its coordinate law gives

After the geometric normalization,

and likewise for the imaginary part. Every coordinate indexed by \(I_n\) is therefore centered Gaussian with the same variance \(v_n\). The normalized real vector is isotropic before any matrix algebra is applied.

That variance calculation is necessary but not sufficient. Equal marginal variances do not identify a joint law. The formal bridge must also retain the product structure, hence independence, while it rearranges the three families.

Decode one common-variance real product law

The clean proof direction starts from the single real product

and decodes it into the nested RMT-06 coordinate space. This direction makes the upper-coordinate formula literally divide by \(\sqrt{2}\).

Step one: split the disjoint sum

A function on \(D_n\sqcup(T_n\sqcup T_n)\) is canonically the same thing as

Mathlib’s measurable equivalence for functions on a sum type supplies this reassociation. Its measure-preserving theorem says that a product measure on the sum index maps to the product of the two corresponding product measures. Applying it twice isolates the diagonal, upper-real, and upper-imaginary families (Mathlib finite function-space measures).

This is a structural probability theorem, not merely an equivalence of types. The map_eq field is what permits later rewrites of measures.

Step two: regroup two upper functions pointwise

The upper sectors initially have type

The RMT-06 complex product is more naturally decoded pointwise from

Mathlib’s measurable function/product equivalence turns one representation into the other, and its measure-preserving theorem changes a product of two function-space product measures into a function-space product of scalar product measures. This is precisely the exchange

Step three: divide and reassemble each complex coordinate

At one upper index, send

Mathlib’s real Gaussian scaling theorem gives

because \((\sqrt{2})^2=2\). Its finite product mapping theorem lifts that identity coordinatewise. The canonical real-pair/complex equivalence then reassembles the two independent scalar laws as the Cartesian complex Gaussian used by RMT-06.

The scalar identity is checked once as gaussianReal_map_div_sqrt_two. The function realUpperToComplex performs the pointwise pairing, and measurable_realUpperToComplex supplies its ordinary measurability. map_realUpperToComplex_gaussianProduct then proves the complete upper-family measure equality. Its proof names the scaling map, the function/product split, and complexification separately, making every Measure.map_map step visible.

The important words are exactly the law used by RMT-06. No uniqueness theorem for generic Gaussian vectors and no appeal to a density is required.

Step four: recover the nested coordinate measure

After the three transformations, the diagonal block is

and the upper block is

Their product is definitionally the shape of GUE.coordinateMeasure n once the RMT-06 abbreviations for diagonal and upper variances are unfolded. The resulting measure equality is the probability half of the bridge.

At the full three-sector level, GUE.map_realToHermitianCoordinates_gaussianProduct checks the exact map to coordinateMeasure. It applies measurePreserving_sumPiEquivProdPi first to separate the diagonal from the upper sectors and again to separate upper-real from upper-imaginary coordinates. No independence hypothesis needs to be recovered afterward because the source and target are compared as complete product measures.

From a common product to a scaled standard Gaussian

Let

If \(g\sim\mathcal N(0,1)\), then

Thus the common-variance product \(\Pi_n\) is the coordinatewise \(\sigma_n\)-scaling of a product of standard real Gaussians. Mathlib’s map_pi_eq_stdGaussian identifies the standard product, after the finite \(\ell^2\) wrapper, with the canonical standard Gaussian on \(E_n\) (Mathlib multivariate Gaussians).

Consequently the Euclidean image of \(\Pi_n\) is

map_gaussianProduct_toLp_eq_map_smul_stdGaussian proves this statement for an arbitrary finite index type and arbitrary nonnegative variance. It first maps the product coordinatewise with Measure.pi_map_pi, commutes scalar multiplication with WithLp.toLp 2, and finishes with Mathlib’s map_pi_eq_stdGaussian.

Now apply the normalized Frobenius isometry \(\Phi_n:E_n\simeq\operatorname{Herm}(n)\). Mathlib’s stdGaussian_map sends the unscaled standard Gaussian through a real linear isometric equivalence without changing its canonical form. Real linearity also gives

The resulting intrinsic measure is therefore

The project names the coordinate-built intrinsic measure GUE.intrinsicLaw. GUE.instIsProbabilityMeasureIntrinsicLaw records that it is a probability measure, and GUE.intrinsicLaw_eq_map_smul_stdGaussian proves the displayed scaled-Gaussian identity. The latter proof transports through RandomMatrix.normalizedHermitianLinearIsometryEquiv; at the final stdGaussian_map boundary it locally rebuilds that isometry under Mathlib’s canonical inner-product-derived real module instance. As in RMT-07, this is typeclass alignment, not a second mathematical structure.

For positive \(n\), \(v_n=1/n\), so \(\sigma_n=1/\sqrt{n}\). This is the Wigner-scaled intrinsic Gaussian anticipated in RMT-07. Writing the scale as \(\sqrt{\operatorname{varianceScale}(n)}\), instead of dividing by \(\sqrt{n}\), also makes the zero-dimensional branch total.

Scale and shape are different responsibilities

The standard Gaussian provides the rotationally symmetric shape. The scalar \(\sigma_n\) provides the ensemble’s dimension-dependent scale. Unitary congruence is a real linear isometry, so it preserves the first and commutes with the second:

It follows that the scaled intrinsic law \(\Gamma_n\) is also invariant. The proof is a pushforward calculation:

where \(S_{\sigma_n}(H)=\sigma_nH\) and RMT-07 supplies \((\mathcal C_U)_*\gamma_n=\gamma_n\).

GUE.map_intrinsicLaw_hermitianCongruence is the checked version of this calculation. It unfolds the scaled-Gaussian representation, commutes real scalar multiplication through the real linear congruence equivalence, and then invokes RMT-07’s standard-Gaussian invariance theorem.

Identify the coordinate-built matrix law

There are now two paths from a point in the common real product space to an ambient matrix.

The coordinate path is

The intrinsic path is

GUE.coordinateToHermitianEuclidean is the old coordinate path with its codomain restricted to intrinsic Hermitian space, and GUE.measurable_coordinateToHermitianEuclidean proves it measurable. GUE.coordinateToHermitianEuclidean_realToHermitianCoordinates checks that this path after real decoding is the normalized Euclidean assembly. The identity is reflexive: both definitions deliberately reuse the same direct matrix constructor.

On a diagonal entry both paths return the real diagonal coordinate. Above the diagonal both return \((r+\mathrm i s)/\sqrt{2}\). Below the diagonal both return its conjugate.

Once the functions agree, the measure proof is formal but still explicit:

Each equality has its own obligation:

• the RMT-06 definition expands matrixLaw as a map;
• the decoded-product theorem replaces coordinateMeasure;
• pointwise normalized assembly replaces one composite by the other;
• Measure.map_map reassociates measurable maps; and
• the scaled-Gaussian theorem identifies the intrinsic image.

This is the exact equality that RMT-07 refused to assume. Once checked, it converts the phrase “the coordinate GUE is the scaled intrinsic Gaussian” from motivation into a reusable theorem.

The reusable theorem is GUE.matrixLaw_eq_map_hermitianToMatrix_intrinsicLaw. It rewrites the ambient law as the pushforward of GUE.intrinsicLaw through RandomMatrix.hermitianToMatrix. This statement isolates all coordinate normalization behind the intrinsic measure, leaving later ambient arguments a single measurable inclusion to manage.

The commuting square that transfers invariance

For a unitary \(U\), RMT-07 already proves the pointwise square

flowchart LR
  H["intrinsic Hermitian H"] -->|"intrinsic congruence"| HU["intrinsic U H U*"]
  H -->|"hermitianToMatrix"| A["ambient matrix H"]
  HU -->|"hermitianToMatrix"| AU["ambient U H U*"]
  A -->|"RandomMatrix.congruence"| AU

In symbols,

The intrinsic scaled law is invariant, and the ambient GUE law is its pushforward through \(\iota_n\). Therefore

The project’s predicate expands to exactly this statement for every U : Matrix.unitaryGroup (Fin n) ℂ:

RandomMatrix.IsUnitaryConjugationInvariant (GUE.matrixLaw n)

GUE.matrixLaw_isUnitaryConjugationInvariant checks this statement for every natural dimension. It is the final theorem of the module.

Physics view: a random Hamiltonian without a preferred basis

A finite quantum Hamiltonian is represented by a Hermitian matrix only after an orthonormal basis is chosen. Replacing that basis by a unitary matrix \(U\) changes the coordinate matrix from \(H\) to \(UHU^*\). This is a passive change of description: the abstract operator has not changed.

The RMT-06 construction appeared to privilege one basis because it named independent diagonal and strict-upper coordinates. The theorem proved here says that preference disappears at the level of the assembled probability law:

This does not say that an individual sample satisfies \(UHU^*=H\) for every unitary \(U\). That much stronger pointwise statement would restrict the matrix drastically. It says that the ensemble of possible Hamiltonians, with its probabilities, looks identical after the same deterministic basis change is applied to every sample.

The normalized real-coordinate bridge explains why. The independent coordinates are not merely a convenient entry ledger; after the \(\sqrt{2}\) correction they form an orthonormal coordinate system for the real Hilbert space of Hermitian operators. Their common-variance Gaussian is radial in that geometry. Unitary congruence is one of its orthogonal rotations, so the probability measure cannot detect that rotation.

No unitary is sampled from Haar measure in this theorem, and \(UHU^*\) is not being interpreted as Schrödinger time evolution. The result is a symmetry of a finite probability law under deterministic basis changes. Spectral statistics and quantum-chaos interpretations require additional theorems. Guionnet states the classical coordinate normalization and unitary symmetry in the surrounding random-matrix theory (Guionnet, 2022); the contribution here is a checked derivation for this repository’s exact measure definitions.

Dimension zero is part of the theorem

Dimension zero is not a limit argument. It is a concrete finite case in which all relevant index types are empty.

Geometry

Fin 0 is empty, and RMT-05 gives an IsEmpty instance for StrictUpperIndex 0. Their nested sum is empty. A real function on that index is unique, the Euclidean carrier has one point, and the intrinsic Hermitian space contains only the empty zero matrix. The normalized analysis and synthesis maps are the unique maps between singleton carriers, and their norm identity is an empty-sum identity.

Probability

Mathlib’s finite product over an empty type is a Dirac measure at the unique empty function. RMT-06 already proves that both coordinateMeasure 0 and matrixLaw 0 are Dirac at zero. The scale satisfies

Mapping any intrinsic standard Gaussian by zero scalar multiplication gives the same Dirac mass. Because the underlying space is already a singleton, there is no tension between this fact and the canonical standard-Gaussian definition.

GUE.intrinsicLaw_zero records the resulting equality with Measure.dirac (0 : RandomMatrix.HermitianEuclidean 0). Its proof is a direct rewrite by the scaled-standard-Gaussian representation and GUE.varianceScale_zero; empty-product details have already been absorbed by the general law theorem.

Symmetry

Every unitary congruence fixes the zero matrix, so the final invariance equation holds. More importantly, the general proof architecture already reduces to that fact. There is no need to introduce the undefined expression \(1/\sqrt{0}\), prove a positive-dimension theorem, and bolt on a disconnected special theorem later.

The complete declaration map

The following table maps all thirty-five public declarations in the checked module. Private helper lemmas, imports, namespace openings, and locally rebuilt isometries are not counted.

Checked proof order

The source follows the dependency order from geometry to probability to symmetry:

1. define the semantic real index and Euclidean carrier;
2. define normalized decoding, synthesis, and analysis;
3. prove their pointwise formulas and inverse laws;
4. package the real linear isometry;
5. decode the common-variance product into coordinateMeasure;
6. identify the Euclidean common product with scaled stdGaussian;
7. identify coordinateMeasure with the scaled intrinsic law;
8. identify matrixLaw with the ambient image of that intrinsic law;
9. prove the scaled intrinsic law invariant; and
10. transport the equality through the commuting square to the ambient unitary-invariance predicate.

Reversing that order would create large goals containing nested maps, product equivalences, subtype coercions, and congruence simultaneously. Named intermediate measure equalities keep each seam auditable.

Lean implementation seams encountered

Function equality versus bundled equality

The normalized maps may appear through a LinearEquiv, a LinearIsometryEquiv, a measurable equivalence, or a raw function. These bundles can be pointwise identical without being definitionally the same term. Short change, funext, or extensionality steps should expose the underlying function before applying Measure.map_congr or Measure.map_map.

Scalar actions on the Hermitian subtype

RMT-07 already encountered two compatible real module instances on the intrinsic Hermitian subtype. The scaled-Gaussian proof encounters the same API boundary and locally rebuilds the coordinate-to-Hermitian real linear isometry under InnerProductSpace.toNormedSpace.toModule. That local instance alignment is an elaboration maneuver, not an extra mathematical assumption or a new scalar multiplication.

Product measures need sigma-finiteness instances

The finite Gaussian factors are probability measures, hence sigma-finite. Mathlib’s measure-preserving product equivalences discover those facts through typeclass inference. If inference stalls, exposing the individual real Gaussian factors is more faithful than adding an unrelated global instance.

Equality of maps needs ordinary measurability

The project distinguishes Measurable from AEMeasurable. Reassociating pushforwards with Measure.map_map should use the bundled continuous linear or isometric maps, whose ordinary measurability is available. Exact coordinate laws alone would provide only almost-everywhere measurability and are not a substitute.

Normalize algebra before measure algebra

The identity

mixes reals, nonnegative reals, square roots, division, and coercions. It is best isolated as a scalar lemma. Leaving that arithmetic inside a product- measure rewrite makes an otherwise structural proof brittle.

What this milestone does not prove

Even with the unitary-invariance theorem checked, the scope remains finite and precise.

• No Lebesgue density or normalizing constant is derived.
• No Jacobian or change-of-variables formula for matrix entries is proved.
• No eigenvalue map, spectral theorem, or eigenvalue joint density is added.
• No Vandermonde determinant or eigenvalue-repulsion theorem appears.
• No trace moment, resolvent, empirical spectral measure, or Stieltjes transform is evaluated.
• No semicircle law, edge law, spacing statistic, or universality limit is proved.
• No claim identifies all unitarily invariant Hermitian laws with GUE.
• No infinite-dimensional Gaussian measure or random operator is constructed.
• No physical claim about a particular quantum Hamiltonian follows solely from ensemble symmetry.

What the milestone establishes is still fundamental: this exact finite matrix probability measure, constructed from explicitly normalized independent coordinates, is unchanged by every finite unitary basis change.

Run the checked source

From the repository root on macOS or Linux, load elan and run the stable module through the pinned Lake environment:

source "$HOME/.elan/env"
cd formalization
lake env lean -DwarningAsError=true \
  NonlinearDynamics/Random/RandomMatrices/GaussianUnitaryEnsembleInvariance.lean

The direct command checks the complete RMT-08 module with warnings promoted to errors. Starting from the repository root, build the full Lean library and check the public teaching content with:

cd formalization
lake build

cd ..
make content-hygiene
make site-check

This complete Lean snippet inspects the main bridge and symmetry interfaces:

import NonlinearDynamics.Random.RandomMatrices.GaussianUnitaryEnsembleInvariance

open Matrix MeasureTheory ProbabilityTheory
open scoped Matrix NNReal ENNReal RealInnerProductSpace

open NonlinearDynamics.Random

#check HermitianRealIndex
#check hermitianRealIndexEquivMatrixIndex
#check RandomMatrix.normalizedHermitianLinearIsometryEquiv
#check map_realUpperToComplex_gaussianProduct
#check GUE.map_realToHermitianCoordinates_gaussianProduct
#check GUE.intrinsicLaw
#check GUE.instIsProbabilityMeasureIntrinsicLaw
#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

Save it inside formalization and run lake env lean on that file. All names are checked public declarations; the snippet contains no omitted terms or noncompiling ellipses.

Failure modes the bridge is designed to block

Exercises with solutions

Exercise 1: count the real coordinates

Why does the index \(D_n\sqcup(T_n\sqcup T_n)\) have \(n^2\) elements?

Solution. There are \(n\) diagonal indices and \(|T_n|=n(n-1)/2\) strict-upper indices. The two copies of \(T_n\) store real and imaginary parts. Hence \(n+2[n(n-1)/2]=n+n(n-1)=n^2\).

Exercise 2: find the isometric normalization

Suppose one strict-upper entry is \(u=x+\mathrm i y\). Which real coordinates make its Frobenius contribution a sum of coordinate squares?

Solution. The upper and lower entries contribute \(|u|^2+|\overline u|^2=2x^2+2y^2\). The normalized real coordinates are \(\sqrt{2}x\) and \(\sqrt{2}y\), whose squares sum to the same quantity.

Exercise 3: check the variance conversion

If \(X\sim\mathcal N(0,v)\), what is the variance of \(X/\sqrt{2}\)?

Solution. Scaling a real random variable by \(c\) multiplies variance by \(c^2\). Here \(c=1/\sqrt{2}\), so the new variance is \(v(1/\sqrt{2})^2=v/2\). This is why a common normalized variance \(v_n\) decodes to the RMT-06 upper Cartesian variance \(v_n/2\).

Exercise 4: explain the product regrouping

Why is \((T_n\to\mathbb R)\times(T_n\to\mathbb R)\) the right intermediate type for building a complex upper family?

Solution. The first function stores every real part and the second stores every imaginary part. The canonical function/product equivalence regroups them pointwise into \(T_n\to(\mathbb R\times\mathbb R)\). At each index, the real-pair/complex equivalence then produces one complex number. Its measure-preserving theorem ensures this regrouping transports the whole product law, not just individual coordinates.

Exercise 5: scale the intrinsic Gaussian

For \(n\gt0\), why is the intrinsic scale \(1/\sqrt{n}\)?

Solution. RMT-06 sets \(v_n=1/n\). A standard Gaussian coordinate has variance one, and multiplication by \(\sigma\) produces variance \(\sigma^2\). Choosing \(\sigma_n=\sqrt{v_n}=1/\sqrt{n}\) makes every normalized real coordinate have variance \(1/n\).

Exercise 6: prove scaled invariance on paper

Let \(T\) be a linear isometry with \(T_*\gamma=\gamma\). Prove that \(T_* (S_\sigma)_*\gamma=(S_\sigma)_*\gamma\).

Solution. Linearity gives \(T\circ S_\sigma=S_\sigma\circ T\). Therefore

Exercise 7: transfer through inclusion

Assume \(\iota\circ T=\widehat T\circ\iota\), \(T_*\Gamma=\Gamma\), and \(\mu=\iota_*\Gamma\). Show that \(\widehat T_*\mu=\mu\).

Solution. Reassociate pushforwards and use the commuting square:

Exercise 8: audit dimension zero

Why does the proof not need division by zero when \(n=0\)?

Solution. The only coordinate decoder division is by the fixed nonzero number \(\sqrt{2}\). The dimension-dependent factor is represented as \(\sqrt{v_0}=0\) and used by scalar multiplication, not division. Since the real index is empty, the Euclidean and Hermitian spaces are singletons, and zero scaling gives the correct Dirac law automatically.

The next ridge

With this bridge checked, the finite GUE law finally justifies the adjective unitary at the measure level. That is a structural summit, not the end of random-matrix theory.

The First Exact GUE Trace Moments in Lean: Centering, Energy, and Wigner Scale now proves the first two integrable trace moments from this bridge. The next ridge is a measurable finite-spectrum interface and an empirical spectral measure. Those layers should consume the invariant law proved here rather than reconstructing coordinate symmetry from scratch. Asymptotic statements such as the semicircle law require an additional limit architecture and must remain separate from this exact finite-dimensional theorem.

References

The external links below were opened and checked on 2026-07-21. The pinned local Mathlib 4.32.0 source remains the API authority for the eventual Lean proof.

Alice Guionnet. “Rare Events in Random Matrix Theory”, Proceedings of the International Congress of Mathematicians 2022, volume 2, pages 1008–1052. DOI 10.4171/ICM2022/174. Section 1.1.1 records the classical finite GUE coordinate normalization, matrix density convention, and unitary-conjugation invariance. This chapter uses it for mathematical context and does not import its density or eigenvalue conclusions into the formal claim.

Mathlib contributors. Mathlib 4.32.0 release, 2026. This is the exact dependency release selected by formalization/lakefile.toml.

Mathlib contributors. Multivariate Gaussian distributions, Mathlib 4 documentation. This page defines stdGaussian, proves map_pi_eq_stdGaussian, proves basis independence, and proves invariance under real linear isometric equivalences via stdGaussian_map.

Mathlib contributors. Real Gaussian distributions, Mathlib 4 documentation. This is the official interface for exact real Gaussian scaling, including gaussianReal_map_div_const.

Mathlib contributors. Measures on finite function spaces, Mathlib 4 documentation. This module supplies Measure.pi_map_pi and the measure-preserving sum/function-product equivalences used to rearrange finite Gaussian blocks without a density argument.

Mathlib contributors. Euclidean spaces and inner products, Mathlib 4 documentation. This page supplies the finite \(\ell^2\) carrier and real Euclidean geometry used by the normalized coordinate isometry.