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.

Euclidean Hausdorff measure is proportional to Lebesgue measure

Statement

Assume the Axiom of Countable Choice. For each integer $n \geq 1$ there is a finite $c_{n} \in [1, n^{n / 2}]$ such that

$H^{n} (B) = c_{n} λ_{n} (B) (B Borel), H^{n} (A) = c_{n} λ_{n}^{*} (A) (A \subseteq R^{n}) .$

Here $c_{n} = H^{n} ((0, 1]^{n})$ and $c_{1} = 1$ . For $n \geq 2$ no exact identification of $c_{n}$ is proved here.

Facts & Assumptions

Given: The objects, conventions, and hypotheses in the statement above.

[F1]

Under the standing Countable Choice hypothesis, the Hausdorff measure of $(0, 1]^{n}$ lies between one and $n^{n / 2}$ . Elementary lower and upper bounds on a unit cube

[F2]

Under the standing Countable Choice hypothesis, isometries, including translations, preserve Hausdorff outer measure. Similarities scale Hausdorff measure exactly

[F3]

Under the standing Countable Choice hypothesis, hausdorff outer measure restricts to a measure on the Borel sets. Hausdorff measure is metric and measures every Borel set

[F4]

Under the standing Countable Choice hypothesis, every set has an equal-Hausdorff-measure Borel hull. Hausdorff measure is Borel regular

[F5]

Under Countable Choice, a translation-invariant Borel measure on $R^{n}$ giving $(0, 1]^{n}$ value one equals Lebesgue measure on Borel sets. A translation-invariant measure on the Borel sets of $R^{n}$ giving the unit cube measure one is the restriction of Lebesgue measure

[F6]

Under Countable Choice, every subset of $R^{n}$ has a Borel (indeed $G_{δ}$ ) superset of equal Lebesgue outer measure. Every subset of $R^{n}$ has a $G_{δ}$ measurable hull of the same outer measure

[F7]

Under the standing Countable Choice hypothesis, on the line $H^{1} = λ_{1}^{*}$ on all subsets. One-dimensional Hausdorff measure on the line is Lebesgue outer measure

Proof

1.1

Set $c_{n} = H^{n} ((0, 1]^{n})$ , which is finite and positive. The Borel function $ν (B) = c_{n}^{- 1} H^{n} (B)$ is a measure, since multiplication by a fixed positive scalar preserves nonnegative sums.

F1F3

2.1

Translations preserve $ν$ and $ν ((0, 1]^{n}) = 1$ . The uniqueness theorem therefore gives $ν (B) = λ_{n} (B)$ for every Borel $B$ . Its hypotheses include Countable Choice, the Borel domain, and precisely the half-open normalising cube used here.

F2F5step 1.1

3.1

For arbitrary $A$ , take its Hausdorff Borel hull $G$ . Then $c_{n} λ_{n}^{*} (A) \leq c_{n} λ_{n} (G) = H^{n} (A)$ . Take instead a Lebesgue Borel hull $H$ ; then $H^{n} (A) \leq H^{n} (H) = c_{n} λ_{n}^{*} (A)$ . Both inequalities remain valid for infinite values, and the empty set has zero value.

F4F6step 2.1

4.1

The line equality gives $c_{1} = 1$ by evaluation on $(0, 1]$ . The higher-dimensional proof used only the finite positive cube bounds, so it has established no sharper constant.

F7step 1.1∎

Depends on

Used by

Dependency tree · two levels

46 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

Fremlin 264I statement (weaker constant); design MT-21 prescribed uniqueness route (standard reference, not scraped)