03-ilang-space / 07-random-records
07random recordsverified
Summary The witness geometry of a recording contract with random record operators: what the language gives generically, apart from hand-made examples.
# External verification: 07-random-records - **Subproject:** 03-ilang-space - **Package:** 07-random-records - **Verified version:** v1 - **External round:** 1 of 2 - **Date:** 2026-10-08T16:52:45+02:00 - **Focus points:** none --- VERDICT: correct ## Summary The Gaussian record laws, chi-square distance distributions, and almost-sure affine dimensions are derived correctly for both ensembles, with consistent normalization factors. The concentration argument correctly normalizes by the mean distance and establishes simultaneous convergence of all pairwise distances for fixed \(n\). The leading-order restriction and ensemble assumptions are explicit, and the additional real structure used by GOE is acknowledged. ## Issues None. ## Focus points None given.