ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12

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.

Lebesgue measure as Haar measure on rn

Example

Assume AC and $n \geq 1$ . Lebesgue measure restricted to the Borel sets of $(R^{n}, +)$ is a left and right Haar measure. All its Haar measures are positive multiples of Lebesgue measure, and the normalization $μ ([0, 1]^{n}) = 1$ singles out Lebesgue measure.

Facts & Assumptions

Given: $n \geq 1$ and AC.

[F1]

The Haar requirements are invariance, nonzeroness, compact finiteness and Radon regularity. (Left Haar integral and left Haar measure)

[F2]

Haar measures are positive scalar multiples. (Uniqueness of left Haar measure up to scale)

[F3]

Lebesgue measure is Radon under countable choice. (Lebesgue measure is a Radon measure on R^n)

[F4]

AC supplies countable choice and the uniqueness construction. (The Axiom of Choice)

[F5]

Lebesgue measure is translation invariant on measurable sets. (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation)

Verification

technique · direct

1.1

Euclidean addition and negation are continuous; closed bounded cubes give compact neighbourhoods and the Euclidean metric is Hausdorff. By [F3], AC makes the Borel restriction of Lebesgue measure Radon. For a box $B = \prod_{j = 1}^{n} [a_{j}, b_{j}]$ , its defining volume is $λ_{n} (B) = \prod_{j} (b_{j} - a_{j})$ ; in particular $λ_{n} ([0, 1]^{n}) = 1$ , so the measure is nonzero.

F1F3F4

2.1

[F5] gives $λ_{n} (E + h) = λ_{n} (E)$ for every Borel $E$ and every $h$ . Addition is commutative, so this is both left and right invariance. Thus [F1] identifies it as Haar, and [F2] gives $μ = c λ_{n}$ for any Haar measure. On the unit cube $μ ([0, 1]^{n}) = c$ , forcing $c = 1$ under the specified normalization. As an explicit translation calculation, $λ_{n} (h + [0, 2]^{n}) = λ_{n} ([0, 2]^{n}) = 2^{n}$ .

F1F2F4F5step 1.1∎

Sources

Knapp, Advanced Real Analysis, VI §2, pp.225–230, Lemmas 6.9–6.13. Local argument and conventions as displayed above.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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

Knapp, Advanced Real Analysis, VI §2, pp.225–230, Lemmas 6.9–6.13 (standard reference, not scraped)