Field record / every checked step explained
Every Lean module gets a companion field entry: physical motivation, mathematical construction, proof architecture, code, commands, and what remains open.
This is the expedition log. Each entry begins with a phenomenon worth understanding, builds the mathematical objects it needs, and then opens the corresponding Lean file line by line. You can read chronologically to watch the library grow or enter through the topic that brought you here.
An entry is not a changelog. It is a complete guided lesson with runnable commands, proof-state commentary, explicit limitations, and links into the stable textbook material in the Knowledge Base. New entries begin as local Hugo drafts until their claims, references, code, and teaching path are ready to share. The current corpus is published openly as work in progress: an Open working note badge means that publication has not been represented as completed editorial, technical, or external review.
Continuous-time forward stability is uniform control over every nonnegative real time, while equilibrium, attraction, and asymptotic stability remain separate predicates.
A deterministic stability interface defines forward stability as equicontinuity of all natural-number iterates, then separates reference-orbit stability from fixedness and attraction.
A discrete-time attraction interface separates orbit convergence, point and set basins, local and global attraction, and asymptotic stability.
A discrete Lyapunov interface separates positivity, one-step descent, sublevel geometry, orbit-energy convergence, stability, and attraction.
A discrete conjugacy interface separates orbit intertwining, continuous semiconjugacy, surjective factor maps, and invertible topological coordinate changes.
A parameterized-map interface separates fixed and specified-period branches, classifier changes, and failure of nearby whole-state-space topological conjugacy.
Random-matrix-theory milestone 35 constructs the finite signed Fekete rate and proves almost-everywhere convergence of normalized real-log cocycle growth from pointwise invertibility, two integrable generator tails, and …
RMT-36 formalizes sequential upper semicontinuity of the signed integrated real-log growth rate under uniform convergence of finite-dimensional matrix generators with shared forward and inverse bounds.
Random-matrix-theory milestone 28 (RMT-28) proves that conditional expectation onto the exact invariant sigma algebra is almost everywhere the normalized space average on every finite nonzero pre-ergodic system. …
Random-matrix-theory milestone 29 (RMT-29) combines a corrected finite phase-average bound with ergodic Birkhoff convergence under the original map to prove a samplewise upper limsup estimate for subadditive processes …
Random-matrix-theory milestone 30 (RMT-30) converts finite ordered interval packing into a finite-measure estimate for points with a short centered block below a negative slope. It counts bad-set visits exactly, …
Random-matrix-theory milestone 31 (RMT-31) removes the finite witness cap from the centered bad-block estimate. It identifies the all-positive-length event as an increasing union, passes first through extended measure …
Random-matrix-theory milestone 32 (RMT-32) replaces a once-bad centered block event with a countably generated strict lower-deviation event. Rational slack makes one-sided shift stability provable, finite-measure …
Random-matrix-theory milestone 33 (RMT-33) turns the null rational lower-deviation events of RMT-32 into an almost-everywhere lower-liminf bound with an explicit boundedness guard, adds back the one-step Birkhoff …
Random-matrix-theory milestone 34 (RMT-34) defines the total real logarithm of a finite cocycle norm, proves its finite-horizon integrability from pointwise units and integrable forward and inverse generator tails, …
A declaration-by-declaration ascent from two exact independent real Gaussian laws to a complex law with explicit coordinate variances, finite moments, degenerate cases, and no unearned circular or GUE convention.
A guided ascent from one exact Cartesian complex Gaussian law to measurable mutually independent families, finite joint product laws, canonical coordinate spaces, real scaling, and the empty-family boundary.
A guided construction of complex Hermitian matrices from a real diagonal and complex strict upper triangle, with exact entry rules, pointwise symmetry, measurability, bundling, and a total zero-dimensional boundary.
A guided construction of the finite-dimensional Gaussian unitary ensemble from an explicit Wigner normalization ledger, independent Gaussian coordinate blocks, a measurable Hermitian assembly map, exact entry laws, and a …
A guided construction of the Euclidean geometry behind finite Hermitian matrices: matrix flattening, the intrinsic real Hermitian subspace, Frobenius trace pairing, unitary-congruence isometries, invariant intrinsic …
A guided checked proof of the normalized real-coordinate bridge behind finite GUE symmetry: the square-root-of-two Frobenius isometry, exact transport of the coordinate product measure, the scaled intrinsic standard …
A first-principles, machine-checked climb from measurable trace observables to their complex Bochner integrability and the exact finite-GUE identities E Tr(H) = 0 and E Tr(H^2) = n, including the zero-dimensional …
A machine-checked finite spectral layer: decreasingly ordered Hermitian eigenvalues with multiplicity, exact trace identities, unitary-congruence invariance, counting and zero-aware empirical measures, and conditional …
A machine-checked finite-dimensional perturbation argument: Frobenius control of every decreasing Hermitian eigenvalue, exact 1-Lipschitz spectrum maps in the sup metric, and unconditional measurability of spectral …
A declaration-complete account of the finite Wigner-scaled Gaussian unitary ensemble (GUE) empirical spectral law: raw and probability-valued law packages, the mean empirical measure, exact zero-dimensional behavior, and …
A declaration-complete construction of forward finite matrix products: newest factor on the left, exact shifted splitting, constant-system powers, chronological vector action, and finite-time growth bounds in the …
A declaration-complete account of finite random-matrix products: pointwise ordered algebra, measurability from exactly the used factor prefix, proof-carrying pushforward laws, zero- and one-step laws, and a …
A declaration-complete construction of generator-presented, one-sided matrix cocycles: sample a matrix generator along finite base iterates, multiply newest factor on the left, prove the exact cocycle identity and …
A declaration-complete finite-time growth layer for one-sided complex matrix cocycles: select the maximum absolute row-sum operator norm, prove its exact formula and measurability, pass to an extended-real logarithm that …
A declaration-complete bridge from measurable finite-time matrix-cocycle norms to real-valued log-positive observables: prove subadditivity, dominate every horizon by a finite orbit sum, and propagate one explicit …
A declaration-complete passage from integrable finite-horizon log-positive matrix-cocycle growth to a subadditive real sequence and its deterministic Fekete limit, with raw-measure semantics and every samplewise or …
A declaration-complete separation of finite-horizon integrability, probability normalization, and ergodic rigidity for one-sided matrix cocycles, including deterministic rate bounds, an expectation alias justified by …
A declaration-complete climb from shifted subadditivity to exact finite block-and-remainder Birkhoff bounds, including the time-zero obstruction, total natural-number division, block-map integrability, cocycle …
An eighteen-declaration Lean reduction subtracts the one-step Birkhoff majorant from a shifted-subadditive process, preserving subadditivity, preserving finite-horizon integrability under one-step measure preservation, …
Eight public Lean declarations turn residue-phase block sums into one sliding Birkhoff sum and prove a finite upper bound for nonpositive shifted-subadditive processes at the corrected horizon bq+b+r, while keeping the …
A gap-indexed Lean packing builds positive-length half-open intervals with ordering and disjointness by construction, selects a subfamily that covers every marked start, and turns per-start favorable costs into finite …
Random-matrix-theory milestone 22 (RMT-22) isolates the points where real Birkhoff averages converge, proves that adding or deleting one orbit prefix preserves convergence and its finite limit, and turns exact event …
Random-matrix-theory milestone 23 (RMT-23) formalizes a finite Hopf-style maximal ergodic lemma: a positive running Birkhoff-sum maximum can be peeled into the first observation plus a shifted maximum, and measure …
Random-matrix-theory milestone 24 (RMT-24) identifies the positive-time Birkhoff-average exceedance event with the increasing union of its finite-horizon approximations, proves continuity first for extended nonnegative …
Random-matrix-theory milestone 25 (RMT-25) constructs the real square-integrable Koopman operator for an arbitrary measure-preserving map, proves von Neumann mean convergence to the fixed-subspace projection, isolates …
Random-matrix-theory milestone 26 (RMT-26) combines an absolute weak maximal estimate with an L¹-dense core of fixed observables and simple Koopman coboundaries to prove full-sequence almost-everywhere convergence of …
Random-matrix-theory milestone 27 (RMT-27) identifies the almost-everywhere limit of every real integrable Birkhoff average on a finite measure-preserving system as conditional expectation onto the exact invariant sigma …
The first substantive Lean module turns matrix-valued maps into measurable objects one coordinate at a time, then builds the operations needed for Hermitian random matrices.
A declaration-by-declaration ascent through pointwise Hermitian symmetry, almost-sure reasoning, measurable trace, bundling, and congruence transforms in Lean.
A declaration-by-declaration climb from measurable matrix-valued maps to pushforward laws, congruence actions, probability preservation, and the exact statement of unitary invariance.
A line-by-line ascent through the Lean module that turns powers of finite random matrices into measurable scalar observables and proves those observables are real on Hermitian samples.
A declaration-by-declaration ascent from one exact real Gaussian law to finite independent families, joint product laws, coordinatewise scaling, and a canonical product sample space.