Wyner's spherical covering exponent

Informal statement

Fix an angle θ with 0 < θ < π/2, and for each n let M(n, θ) be the least number of spherical caps of angular radius θ, centred at points of the unit sphere of ℝⁿ, whose union is the whole sphere. Then

lim_{n → ∞} (1/n) · log M(n, θ) = -log sin θ,

that is, M(n, θ) = exp (n · (-log sin θ) · (1 + o(1))). The covering number grows exponentially in the dimension, with exponent exactly -log sin θ.

The cap of angular radius θ about a point c of the unit sphere is the set of unit vectors u with angle u c ≤ θ. For unit vectors ‖u - c‖ = 2 sin (angle u c / 2), so that cap is precisely the closed ball of radius 2 sin (θ/2) about c. The statement below therefore uses Mathlib's Metric.coveringNumber at radius 2 sin (θ/2) on Metric.sphere 0 1 in EuclideanSpace ℝ (Fin n), and defines no covering number of its own. Metric.coveringNumber requires the centres to lie in the set being covered, which is also what Wyner requires.

Two points of care in reading the Lean statement:

• Metric.coveringNumber takes values in ℕ∞, and the statement applies ENat.toNat, whose junk value at ⊤ is 0. coveringNumber_sphere_ne_top and coveringNumber_sphere_pos bound that: the covering number is finite for every n, and positive for every n ≥ 1, so from n = 1 onwards neither ENat.toNat nor Real.log is applied to a junk argument. n = 0 is the exception and is genuinely degenerate: the sphere of ℝ⁰ is empty, so the covering number is 0 at every radius and the summand collapses to Real.log 0 / (0 : ℝ) = 0, two junk conventions at once. A limit along atTop does not see it, but it is not excluded either.
• The radius is written Real.toNNReal (2 * sin (θ/2)). For 0 < θ < π/2 this is the honest value 2 sin (θ/2) and not a truncation to 0; the sanity checks pin it down at θ = π/3, where it is exactly 1.

Where this differs from the source. Wyner defines a θ-covering with open caps, angle u c < θ (p. 2112). Mathlib's Metric.IsCover is stated with closed balls, so what is proved below concerns closed caps, angle u c ≤ θ. The exponent is unaffected — a closed θ-cover is an open θ'-cover for every θ' > θ, and -log sin is continuous — but the two covering numbers are not literally equal, and it is the closed one that is formalised here.

Source

A. D. Wyner, Random packings and coverings of the unit n-sphere, Bell System Technical Journal 46 (1967), 2111-2118.

The result formalised here is the covering half of that paper: equations (2a) and (2b), restated as a limit on p. 2116, lim (1/n) log M_c(n, θ) = R_c(θ) with R_c(θ) = -log sin θ for θ < π/2. Both halves of Wyner's argument are reproduced — the elementary volume bound (Lemma 2, p. 2115) for the lower bound on the covering number, and the random-covering argument (Theorem 2 and its corollary, pp. 2115-2117) for the upper bound. The packing results of the same paper are not formalised.

Relation to Mathlib

Mathlib supplies the vocabulary but not the theorem. Mathlib/Topology/MetricSpace/ CoveringNumbers.lean defines Metric.coveringNumber, Metric.externalCoveringNumber and Metric.packingNumber along with the elementary inequalities relating them, but contains no asymptotics. Mathlib has no spherical cap measure and no metric-entropy estimate for any family of sets, so nothing here is a duplicate.

The theorem below is stated entirely in Mathlib's vocabulary and introduces no definition at the level of the statement. The auxiliary notions needed for the proof — the normalised surface measure of a cap, and the radial cone over a cap — are private to this file and do not appear in any exported statement. MeasureTheory.Measure.toSphere and EuclideanSpace.volume_ball provide the measure-theoretic input, and Metric.packingNumber together with Metric.maximalSeparatedSet provide the finite nets used by the random-covering argument.

Provenance

Result selected and specified by George A. Constantinides, who has read its advertised statements — tendsto_log_coveringNumber_sphere_div_atTop, the two junk-value guards coveringNumber_sphere_ne_top and coveringNumber_sphere_pos, and the two chord lemmas dist_eq_two_mul_sin_angle_div_two and angle_le_iff_dist_le, all stated in Mathlib's vocabulary — against the informal claim above on a best-effort basis. The statements and their proofs were generated by Claude, and are kernel-verified and axiom-audited; the proofs are read by nobody. Every other declaration in this file is private, is proof, and may be read by no one. A best-effort read is not a review — satisfy yourself that the statement says what you need before relying on it. See the repository README.

Before that read, the five advertised statements were read back blind: rendered into English by an agent given them and nothing else — no informal statement, no source, no docstring. The rendering agreed with the informal account above. It raised independently the two junk-value concerns already declared there, and observed that coveringNumber_sphere_ne_top adds nothing to coveringNumber_sphere_pos beyond the case n = 0. It also noted, correctly, that nothing in the statements settles whether the covering is by open or by closed balls: that rests entirely on Mathlib's definition of Metric.coveringNumber, so a reader who wants the closed reading recorded above must check it there rather than here.

Registered in Palomar, a registry of Lean-verified mathematics, as PALOMAR-2026-08-23-000001, at https://palomar-registry.org/entry?id=PALOMAR-2026-08-23-000001&version=1. That URL names version 1, the immutable snapshot in which these statements were the ones reviewed. The five declarations compared there are exactly the five advertised statements. Registration records that their proofs were replayed through Lean's kernel and through NanoDa, an independent kernel implementation, and that an automated review found no problem in the alignment between those statements and the informal account above.

That is a second and independent read of the one thing this file cannot check for itself. It is not peer review, not an endorsement, and not a human read of the proof; Palomar is explicit that it is none of those. The advice above stands — satisfy yourself that the statement says what you need before relying on it.

An earlier formalisation of this result, by George A. Constantinides and Codex as part of a paper coauthored with Bardia Zadeh, is at https://github.com/bardia01/Direction-Preserving-Number-Representations/blob/main/PaperProofs/PaperProofs/Wyner.lean. This file is a refactoring of that development: restructured into a single self-contained module, restated in terms of Metric.coveringNumber rather than a bespoke covering number, and reproved against a current Mathlib.

Chords and angles

theorem MiscMath.Geometry.dist_eq_two_mul_sin_angle_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : dist x y = 2 * Real.sin (InnerProductGeometry.angle x y / 2)

The chord joining two unit vectors has length 2 sin (θ/2), where θ is the angle between them.

theorem MiscMath.Geometry.angle_le_iff_dist_le {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) {θ : ℝ} (h0 : 0 ≤ θ) (hpi : θ ≤ Real.pi) : InnerProductGeometry.angle x y ≤ θ ↔ dist x y ≤ 2 * Real.sin (θ / 2)

For unit vectors, an angular cap of half-angle θ ∈ [0, π] is exactly a chordal closed ball of radius 2 sin (θ/2).

Volumes of Euclidean unit balls

Spherical caps and their normalised surface measure

Cap measure bounds

Caps around arbitrary centres, and the sphere probability measure

Finite angular nets

Finite angular covers

The random covering argument

The covering number in Mathlib's vocabulary

The asymptotic covering exponent

Wyner's theorem

theorem MiscMath.Geometry.tendsto_log_coveringNumber_sphere_div_atTop {θ : ℝ} (hθ0 : 0 < θ) (hθ : θ < Real.pi / 2) : Filter.Tendsto (fun (n : ℕ) => Real.log ↑(Metric.coveringNumber (2 * Real.sin (θ / 2)).toNNReal (Metric.sphere 0 1)).toNat / ↑n) Filter.atTop (nhds (-Real.log (Real.sin θ)))

Wyner's covering theorem. For a fixed angular radius θ ∈ (0, π/2), the minimum number of spherical caps of angular radius θ, centred at points of the unit sphere of ℝⁿ, whose union is that whole sphere grows like exp (n · (-log sin θ)): its logarithm, divided by n, converges to -log sin θ.

A cap of angular radius θ about a centre c on the sphere is exactly the closed ball of chordal radius 2 sin (θ/2) about c (angle_le_iff_dist_le), so the covering number is Mathlib's Metric.coveringNumber at that radius.

Two features of the statement that are easy to misread, both discussed at more length in the module docstring:

• Metric.coveringNumber is the internal covering number — the centres are required to lie on the sphere, which is what Wyner requires. This is load-bearing, not incidental: the result is false for Metric.externalCoveringNumber, since at θ = π/3 the chordal radius is 1 and the single ball of radius 1 about the origin already contains the whole sphere.
• The caps here are closed, angle u c ≤ θ, whereas Wyner's are open, angle u c < θ. The exponent is the same either way, but the two covering numbers are not literally equal, and it is the closed one that is formalised.

theorem MiscMath.Geometry.coveringNumber_sphere_ne_top (n : ℕ) {θ : ℝ} (hθ0 : 0 < θ) (hθpi : θ ≤ Real.pi) : Metric.coveringNumber (2 * Real.sin (θ / 2)).toNNReal (Metric.sphere 0 1) ≠ ⊤

The covering number appearing above is finite, so the ENat.toNat in its statement is not a junk value.

theorem MiscMath.Geometry.coveringNumber_sphere_pos {n : ℕ} (hn : 1 ≤ n) {θ : ℝ} (hθ0 : 0 < θ) (hθpi : θ ≤ Real.pi) : 0 < (Metric.coveringNumber (2 * Real.sin (θ / 2)).toNNReal (Metric.sphere 0 1)).toNat

... and it is nonzero in every dimension n ≥ 1, so its logarithm is not a junk value either. The hypothesis 1 ≤ n cannot be dropped: the sphere of ℝ⁰ is empty, so its covering number is 0 at every radius.

Sanity checks

Guards against the ways a correct proof can still accompany a useless statement. These are examples: elaborated by the build, so one that stops holding breaks it, and exporting no names. They are not reached by the axiom audit, which walks the named declarations a module contributes to the environment, and an example contributes none. What covers them instead is the textual escape-hatch scan in scripts/check-conventions.sh, which reads the file rather than the environment.