CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-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.

Zero on finite sets and infinity on cofinite sets is finitely additive but not a premeasure

Statement refuted

Every finitely additive nonnegative function on an algebra that vanishes at the empty set is a premeasure.

Facts & Assumptions

Given: The finite-cofinite algebra $A_{0}$ of $N$ and $μ_{0} (A) = 0$ for finite $A$ , $μ_{0} (A) = + \infty$ for cofinite $A$ .

[F1]

A premeasure on an algebra $A_{0}$ vanishes at the empty set and is countably additive whenever a disjoint sequence in $A_{0}$ has its union in $A_{0}$ . (Premeasures on algebras of sets)

Counterexample

technique · direct

1.1

The finite-cofinite family is an algebra. For a disjoint pair, two cofinite members cannot occur; two finite members and their union all have value $0$ , while if one member is cofinite then both it and the union have value $+ \infty$ , so $μ_{0}$ is finitely additive.

givenalgebra

2.1

The disjoint singleton sequence has union $N \in A_{0}$ , but $μ_{0} (N) = + \infty$ and $\sum_{k = 0}^{\infty} μ_{0} ({k}) = 0$ , violating the countable-additivity clause of [F1].

step 1.1F1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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

T. Tao, An Introduction to Measure Theory, Exercises 1.7.4(iii) and 1.7.6 (standard reference, not scraped)