Weyl's law concept

Definition	The asymptotic rule for how the number of eigenvalues of a continuum Laplacian below a value grows with that value, whose exponent reveals the dimension of the space. Reading it from a finite graph needs the conditions under which the graph Laplacian converges. Equation 0.31. Also Weyl.
Example	On a surface, dimension two, the eigenvalue count grows linearly with the value; on a curve, as the square root.
Book	Data Mining as Observation, draft 0.2, commit `f3914f0`; entry id `weyls-law`, kind concept.
Status	no ledger row names this entry. Corrections: none recorded.
Defining equation	Book equation 0.31.
Assumptions and scope	An asymptotic statement about the continuum Laplacian. The number of eigenvalues below a value grows like that value to the power of half the dimension, so the dimension is in the exponent and is read from the slope of the count against the value on log axes. The Lean file checks that arithmetic and not the law. Carrying it to a finite neighbourhood graph needs sampling, graph-construction, normalization, and scaling conditions under which the graph Laplacian converges, and only the low part of the spectrum is read. The recognizer’s battery recovered dimensions of 1.81, 2.80, and 1.74 on three sealed templates under those conditions and against a finite list.
Prior art	none recorded
Evidence	`geometric-observation/chapters/ch11_the_recognizer.md:1-95`, `lean/DataMiningAsObservation/IntrinsicDimension.lean`
Reviewed	semantic review 2026-09-06; generated 2026-09-10 from records at the commits on the provenance page.

The eigenvalue count grows like the value to half the dimension.

Equation

Book equation 0.31.

\[N(\lambda)=\#\{k:\lambda_k\le\lambda\}\ \sim\ C_d\,\lambda^{d/2}.\]

Book equation 9.2.

\[N(\lambda)=\#\{k:\lambda_k\le\lambda\}\ \sim\ C_d\,\lambda^{d/2}\qquad\Rightarrow\qquad d=2\,\frac{d\log N}{d\log\lambda}.\]

Conditions

An asymptotic statement about the continuum Laplacian. The number of eigenvalues below a value grows like that value to the power of half the dimension, so the dimension is in the exponent and is read from the slope of the count against the value on log axes. The Lean file checks that arithmetic and not the law.
Carrying it to a finite neighbourhood graph needs sampling, graph-construction, normalization, and scaling conditions under which the graph Laplacian converges, and only the low part of the spectrum is read. The recognizer’s battery recovered dimensions of 1.81, 2.80, and 1.74 on three sealed templates under those conditions and against a finite list.

Conditions are curated in entries.toml rather than read from a record.

Ledger

none

First stated

Weyl, 1911, as chapter 0 section 0.15 of Data Mining as Observation states it, with the program’s dimension reading in geometric-observation/chapters/ch11_the_recognizer.md:1-95.

Measurements

Where the book states it	Numbers, as the book’s sources table records them	Source
chapter 9 section 9.2	the recognizer’s mechanism, low multiplets and angular distances, dimension before shape by Weyl’s law, refusal, the growth gotcha	`geometric-observation/chapters/ch11_the_recognizer.md:1-95`

Failures and corrections

none

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/IntrinsicDimension.lean, theorems log_weyl, dimension_from_slope, weyl_double, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation chapters 0, 9.

intrinsic dimension; manifold; Laplacian; multiplet; recognizer.

Status

Generated 2026-09-10 by encyclopedia/generate.py; book at observation-data-mining f3914f0; the commit of every record is listed in the encyclopedia’s provenance.

← water-fillingwhitening →