CounterexampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

An outer measure on two points need not be regular

Statement refuted

Every outer measure is regular: every subset has a Carathéodory measurable hull of the same outer measure.

Facts & Assumptions

Given: The set $X = {0, 1}$ and $μ^{*} (\emptyset) = 0$ , $μ^{*} ({0}) = μ^{*} ({1}) = 1$ , $μ^{*} (X) = 3 / 2$ .

[F1]

An outer measure on a set $X$ is a function $μ^{*} : P (X) \to [0, + \infty]$ that vanishes at the empty set, is monotone, and is countably subadditive. (Outer measures)

[F2]

A set $E \subseteq X$ is Carathéodory measurable for $μ^{*}$ when $μ^{*} (A) = μ^{*} (A \cap E) + μ^{*} (A ∖ E)$ for every $A \subseteq X$ . (Carathéodory measurable sets)

[F3]

A measurable hull of $E$ is a Carathéodory measurable set $H \supseteq E$ with $μ^{*} (H) = μ^{*} (E)$ ; the outer measure is regular when every subset has a measurable hull. (Measurable hulls and regular outer measures)

Counterexample

technique · direct

1.1

Exhausting the four subsets proves normalization and monotonicity. For subadditivity, a union equal to a singleton has a singleton member of total cost at least $1$ , while a union equal to $X$ either has an $X$ member of cost $3 / 2$ or contains both singleton contributions of total cost $2 \geq 3 / 2$ ; hence [F1] holds.

F1algebra

2.1

For either singleton $E$ , the test $A = X$ in [F2] would require $3 / 2 = 1 + 1$ , so neither singleton is measurable; $\emptyset$ and $X$ are measurable directly.

step 1.1F2algebra

3.1

The only measurable superset of a singleton is $X$ , whose outer measure $3 / 2$ is larger than the singleton value $1$ ; therefore [F3] gives no measurable hull for either singleton, and the outer measure is not regular.

step 2.1F3algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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.