Knowledge Base / Long form
Textbook chapters that begin with a picture you can hold and climb through precise mathematics to reusable Lean proof architecture.
Deep Dives are the durable textbook layer of the project. Each chapter starts from first principles, gives the reader a physical and geometric mental model, derives the mathematics without hidden steps, and then explains how that mathematics is represented and proved in Lean.
Reading paths and prerequisites make the climb explicit. A newcomer can take the full route; a specialist can jump to the theorem, implementation choice, or proof boundary they need without losing context.
A real flow separates orbitwise forward stability, fixed equilibria, long-time attraction, and the conjunction called asymptotic stability.
An exact scalar family introduces signed growth before the chapter builds the finite integrated Fekete rate and the lower-liminf and upper-limsup squeeze behind RMT-35.
A worked scalar perturbation leads to the finite-horizon dominated-convergence and Fekete-infimum mechanism behind RMT-36.
A textbook derivation of why an ergodic Birkhoff time average converges almost everywhere to the correctly normalized space average on every finite nonzero measure space.
A textbook derivation of how finite centered bad blocks, orbit visit counts, greedy interval packing, and a negative-threshold limit produce a measure ratio before any lower-liminf theorem.
A textbook passage from uniformly controlled finite centered bad-block sets to the event with one bad witness at any positive length, with the extended-measure limit, finite-target real projection, cocycle …
Start with an exact two-state probability ledger in which one zero-mass state has a durable rational lower deviation, then climb through arbitrarily-late witnesses, threshold-relaxed preimages, almost-invariance, the …
Start with an exact two-state subadditive ledger whose block-two integral bound is sharp, then climb through centering, phase averaging, ordinary-map Birkhoff convergence, the eventual-lower-bound hypothesis for real …
A four-step scalar ledger and two noncommuting shears lead into the checked forward-and-inverse tail sandwich for finite-time signed log norms.
A concept-first ascent from rational lower-deviation events through totalized real liminf, a two-margin null cover, centered Birkhoff transfer, and the final almost-everywhere convergence of normalized log-positive …
Start with a two-state orbit whose averages converge to one and a bounded deterministic orbit whose averages oscillate, then climb through finite measurability, prefix invariance, convergence events, and conditional …
A textbook derivation of the finite-measure pointwise Birkhoff theorem with its limit identified as conditional expectation onto the exact invariant sigma-algebra.
Carry the exact ledger m = 1 - 2i and component variances 4 and 1 through moments, scaling, dependence, degeneracy, the Cartesian complex Gaussian law, and its checked Lean interfaces.
Cut an exact eleven-step process into two four-step blocks and a three-step remainder in both temporal orientations, then climb to the checked finite Birkhoff-sum bounds and their precise boundary assumptions.
At size two, follow four independent real Gaussian primitives through the Wigner variance ledger, Hermitian reflection, measurable assembly, and the exact finite Gaussian unitary ensemble matrix law.
A fair two-matrix law makes the sample measure, outer law, joined mean, and normalized moment numerically visible before the exact finite Gaussian unitary ensemble interfaces are built in Lean.
Build one exact two-by-two Hermitian matrix from four real coordinates, then climb through reconstruction, dimension counting, Frobenius geometry, measurability, Lean syntax, and the zero-dimensional boundary.
Diagonalize one exact two-by-two Hermitian matrix, place half an atom at each ordered eigenvalue, then climb carefully from a sample spectrum to a random measure, its law, and its mean.
A textbook construction of the finite Hopf maximal ergodic lemma: running maxima of orbit sums, the strict time-zero boundary, positive-maximizer peeling, measure-preserving integral cancellation, centered …
A textbook construction of gap-coded ordered half-open interval packings, a leftmost greedy cover of marked starts, exact coverage-to-cardinality bounds, and finite favorable-cost estimates for positive-horizon …
Start with ten negative orbit weights, compute three residue-phase totals exactly, and then climb to Lean's boundary-retaining and nonpositive phase-averaging inequalities.
A worked four-outcome experiment grows into finite product measures, mutual independence, canonical complex Gaussian fields, and the exact Lean interfaces connecting them.
Compute an exact four-state positive-log ledger, use a geometric expanding tail to exhibit nonintegrability, and then follow the checked Lean proof from one explicit generator hypothesis to every fixed finite horizon.
Follow one positive two-step cocycle product and one exact collapse through the row-sum norm, real positive logarithm, extended logarithm, and finite normalization without confusing their codomains or zero policies.
An exact size-two sample and probability ledger separates evaluation from expectation before deriving Bochner integrability and the first two finite Gaussian unitary ensemble trace moments.
A textbook passage from strict finite Birkhoff-average exceedance events to an infinite-horizon weak maximal estimate: positive-time witnesses, the exact increasing union, ordinary and null measurability, …
An exact size-two ledger shows why normalized Hermitian coordinates are isometric, how their full Gaussian product becomes the intrinsic and ambient Gaussian unitary ensemble laws, and why unitary invariance is equality …
Follow a noninvertible three-state base and three exact two-by-two matrices through horizons zero, one, and two, then climb to the checked one-sided cocycle, measurability, and measure-preserving Lean interfaces.
An exact two-by-two perturbation opens a textbook climb from a Frobenius Weyl bound to continuous ordered eigenvalues, measurable finite spectral observables, and a carefully typed Gaussian ensemble pushforward equality.
Compute a two-state cocycle exactly, integrate its finite log-positive values, and then climb declaration by declaration to the checked deterministic Fekete limit without turning it into a samplewise exponent.
An exact two-by-two congruence calculation grows into intrinsic Hermitian Euclidean geometry, Gaussian isometry symmetry, and the precise difference between Hermitian support and invariance of a matrix law.
Start with a two-state probability system you can calculate by hand and in Lean, then climb to the real L² Koopman operator, fixed-space projection, mean convergence, a dense pointwise-good core, and the maximal argument …
Two noncommuting two-by-two matrix histories make product order, event preimages, atom-by-atom pushforward weights, dependence, and equality in law concrete before the checked Lean interface generalizes the construction.
Compute an exact three-state orbit ledger, subtract its additive one-step majorant, catch a wrong shift that makes six less than or equal to three, and then follow the checked Lean interfaces for nonpositivity, …
Multiply one exact noncommuting two-step history in both orders, compute its row-sum operator norms and orbit growth, then climb to the checked finite-product bounds without assuming randomness or a Lyapunov exponent.
A textbook proof of full-sequence almost-everywhere convergence for real integrable Birkhoff averages on finite measure-preserving systems, built from weak maximal control, a dense L2 pointwise-good core, Cauchy …
Start with two weighted points and separate probability normalization, ergodic invariant rigidity, and finite-horizon integrability numerically before reading the exact Lean interfaces.
A worked three-coordinate experiment separates maps, realizations, data, marginal laws, mutual independence, product laws, degenerate Gaussians, and the normalization choice that must precede complex random matrices.
A worked ascent from one finite probability experiment to measurable matrix coordinates, Hermitian realizations, eigenvalues, empirical spectral measures, and a probability law on measures.
Start with a finite state basin, then separate convergence to a target, basin neighborhoods, Lyapunov stability, and distance-to-set attraction.
Begin with a four-state factor, derive all-iterate transport, then add continuity, surjectivity, and an invertible coordinate change one gate at a time.
Work from translated trajectories to the uniform-in-time epsilon-delta definition, then separate fixedness and attraction.
Use scalar sublevels to trap discrete orbits, while keeping positivity, descent, stability, and attraction as separate claims.
Solve a quadratic fixed-point family, separate parameter variation from iteration, and see how an invariant change witnesses a whole-state-space conjugacy obstruction.