TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Margulis family has uniform spectral gap

Statement

For every $m \geq 2$ the normalized Margulis adjacency has absolute nontrivial norm $α \leq 73 / 80$ , hence algebraic gap at least $7 / 80$ . For $m = 1$ the mean-zero space is zero and $α = 0$ .

Facts & Assumptions

Given: the objects and hypotheses in the statement above.

[F1]

For every integer $m \geq 1$ and every nonnegative function $g$ on $(Z / m Z)^{2}$ with $g (0) = 0$ , the quadratic expression $Q$ in the Fourier reduction satisfies $Q (g) \leq \frac{73}{20} \sum_{z} g (z)^{2} .$ Consequently, for the forward/full adjacency operators and normalized transform in that reduction, $∣ ⟨ f, A f ⟩ ∣ \leq (73 / 10) ∥ f ∥^{2}$ for real mean-zero $f$ . (Margulis diamond weight bound).

[F2]

Let $V$ be a finite-dimensional real inner product space and let $T : V \to V$ be self-adjoint. Then $V$ has an orthonormal basis consisting of eigenvectors of $T$ . (Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis).

Proof

1.1F1

The diamond bound and its Fourier consequence give $∣ ⟨ f, A f ⟩ ∣ \leq (73 / 10) ∥ f ∥^{2}$ for every real mean-zero $f$ . Divide by the degree eight to get $∣ ⟨ f, M f ⟩ ∣ \leq (73 / 80) ∥ f ∥^{2}$ .

2.1F2step 1.1∎

The mean-zero subspace is invariant and $M$ is real symmetric. In its orthonormal eigenbasis the preceding bound applied to each eigenvector gives $∣ μ ∣ \leq 73 / 80$ , so the operator norm has that bound. This controls negative as well as positive eigenvalues; in particular $1 - μ_{2} \geq 7 / 80$ . For $m = 1$ use the zero-space norm convention directly.

Depends on

Used by

Expander walk hits dense bad sets Example
Expander size adjustment and laziness Lemma

Dependency tree · two levels

6 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Hoory–Linial–Wigderson, Expander Graphs and Their Applications, May 2006 draft; Theorem8.2 with fully proved weaker bound at end §8.2, pp69–73. (standard reference, not scraped)