Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 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.

The Cantor set has dimension log 2 / log 3 and critical measure one

Statement

Assume the Axiom of Countable Choice. For the middle-thirds Cantor set C and s=log2/log3,

Hs(C)=1,dimHC=s.

These values use the unnormalised diameter-power convention.

Facts & Assumptions

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

[F1]

Under the standing Countable Choice hypothesis, for the Cantor probability measure, every nonempty bounded set U has μc(U)(diamU)s at s=log2/log3. The sharp interval bound for Cantor measure

[F2]

Under the standing Countable Choice hypothesis, a finite Borel measure with outer mass on A positive and diameter bound C0rs gives Hs(A)μ(A)/C0. The mass distribution principle

[F3]

Finite positive Hausdorff measure at s forces dimension s. Hausdorff dimension is the unique critical exponent

[F5]

Positive real powers obey the multiplication and power-of-power laws. The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents

[F6]

Under the standing Countable Choice hypothesis, μc is a probability measure concentrated on C. The Cantor measure is a singular atomless probability measure concentrated on the Cantor set

[F7]

Under Countable Choice, μc=μFc, where the extended Cantor function Fc is nondecreasing and right-continuous on R. The Cantor measure

[F8]

Under Countable Choice, the Lebesgue–Stieltjes measure μF of a nondecreasing right-continuous real function F is a Borel measure on R. Assuming countable choice, a nondecreasing right-continuous function defines a Borel measure on R

Proof

1.1

The 2m length-3m basic intervals cover C and have total s-cost 2m(3m)s=1. At each positive scale take m sufficiently large. Thus Hs(C)1, including the level-zero cover at its own scale.

F4F5
2.1

The defining function in F7 satisfies F8, so μc is a Borel measure; F6 makes it finite with total mass one and μc(RC)=0. Every Borel superset B of C has μc(RB)=0 by monotonicity, hence μc(B)=1. Thus the Borel-hull outer measure in F2 satisfies μc(C)=1. F1 supplies its diameter bound with constant one, in particular for every nonempty set of diameter less than r0=1. F2 gives Hs(C)1. Together with step 1.1 this gives finite positive measure one, so F3 gives dimHC=s.

F1F2F3F6F7F8step 1.1

Depends on

Used by

Dependency tree · two levels

52 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