CounterexampleConstruction: AI-adaptedVerification: 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.

A continuous image can raise Hausdorff dimension

Statement refuted

Assume the Axiom of Countable Choice. A continuous image can have strictly larger Hausdorff dimension than its domain. The Cantor function restricted to $C$ maps $C$ continuously onto $[0, 1]$ , raising dimension from $\log 2 / \log 3$ to one.

Facts & Assumptions

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

[F1]

The Cantor function is onto $[0, 1]$ , agrees with $γ$ on $C$ , and is constant on each gap interval $[u, v]$ with endpoints in $C$ ; every point outside $C$ lies in such a gap. The Cantor function is well defined, satisfies $c (x) \leq c (y)$ whenever $x \leq y$ , is surjective onto $[0, 1]$ , and is constant on every interval removed from the Cantor set

[F2]

The Cantor function is continuous on $[0, 1]$ . The Cantor function is continuous on $[0, 1]$

[F3]

Under the standing Countable Choice hypothesis, $\dim_{H} C = \log 2 / \log 3$ . The Cantor set has dimension log 2 / log 3 and critical measure one

[F4]

Under the standing Countable Choice hypothesis, positive-length subsets of $R$ have Hausdorff dimension one. Euclidean space and positive-volume sets have their Euclidean dimension

Counterexample

1.1

Given $y \in [0, 1]$ , surjectivity provides $x \in [0, 1]$ with $c (x) = y$ . If $x \in C$ this already suffices. Otherwise $x$ lies in a gap $(u, v)$ whose endpoints are in $C$ and $c (u) = c (x) = y$ . Thus $c (C) = [0, 1]$ . Restricting the continuous function to $C$ preserves continuity.

F1F2

2.1

The domain has dimension $\log 2 / \log 3 < 1$ , whereas the image interval has positive length and dimension one. This is the claimed strict increase; no injectivity is asserted for this example.

F3F4step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

53 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 264J; published Cantor-function ternary/binary formula (standard reference, not scraped)