CounterexampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

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.

No normalized translation-invariant Haar probability on the real line

Statement refuted

The averaging construction of the compact theory does not extend to noncompact groups by normalizing Haar measure. Every nonzero left Haar measure $μ$ on the additive group $R$ has infinite total mass, so no positive scalar multiple of $μ$ is a left-invariant probability: there is no translation-invariant Haar probability on $R$ , and the compactness hypothesis in the compact-group construction is genuine rather than a convenience. This implication is choice free once the Haar measure is given.

Facts & Assumptions

Given: the additive group $R$ with its usual topology, which is a locally compact Hausdorff group with continuous addition and negation (Topological group: multiplication and inversion are continuous, The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded), and a nonzero left Haar measure $μ$ on it (Left Haar integral and left Haar measure). No choice principle is used: the measure $μ$ is given.

[F1]

A left Haar measure is left invariant and finite on compact sets: for every Borel $E$ and every $a$ one has $μ (a + E) = μ (E)$ , and $μ (K) < \infty$ for compact $K$ . (Left Haar integral and left Haar measure)

[F2]

Every Haar measure is positive on every nonempty open set. (Haar measure is positive on nonempty open sets and finite on compact sets)

[F3]

A measure is countably additive on pairwise disjoint sequences, with the extended nonnegative sum. (Measures on sigma-algebras)

[F4]

A subset of $R$ is compact exactly when it is closed and bounded; in particular every closed bounded interval is compact, and $R$ itself is not compact. (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line)

Counterexample

technique · direct

1.1F1F4

For every $n \geq 0$ the interval $E_{n} : = (2 n, 2 n + 1)$ is open and bounded, and its closure $[2 n, 2 n + 1]$ is compact, so $E_{n}$ is Borel with $μ (E_{n}) \leq μ ([2 n, 2 n + 1]) < \infty$ ; the intervals $E_{n}$ are pairwise disjoint.

2.1F2step 1.1

The interval $E_{0} = (0, 1)$ is nonempty and open, so $c : = μ (E_{0})$ satisfies $0 < c < \infty$ .

3.1F1F3F4step 1.1step 2.1∎

For every $n \geq 0$ the interval $E_{n} = 2 n + E_{0}$ is the translate of $E_{0}$ by $2 n$ , so $μ (E_{n}) = μ (E_{0}) = c$ by left invariance; applying countable additivity to the pairwise disjoint sequence consisting of the complement $R ∖ ⋃_{n \geq 0} E_{n}$ and the sets $E_{n}$ gives $μ (R) = μ (R ∖ ⋃_{n \geq 0} E_{n}) + \sum_{n \geq 0} c = + \infty$ , because $c > 0$ ; hence no scalar multiple $λ μ$ with $λ > 0$ is a probability, so the compact-group normalization has no analogue on $R$ , and $R$ is indeed noncompact since it is unbounded.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

49 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

Bekka, de la Harpe and Valette, Kazhdan's Property (T), Appendix A §A.5 (standard reference, not scraped)
Emmanuel Kowalski, An Introduction to the Representation Theory of Groups, §§5.2–5.6 (standard reference, not scraped)