CounterexampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

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.

Positive ABC tolerance changes an identity-summary target

Statement refuted

With the identity summary and positive prior-predictive acceptance probability, the tolerance $ϵ = 3 / 5$ gives an ABC target whose mass at $θ = 1$ is $9 / 17$ , while the exact posterior mass is $4 / 5$ ; the total-variation distance is exactly $23 / 85$ .

Facts & Assumptions

Given: Let $Θ = {0, 1}$ have equal prior mass, let $Y = {0, \frac{1}{2}, 1}$ , and define $\begin{array}{crrr} y & 0 & \frac{1}{2} & 1 \\ P_{0} (y) & 1 / 5 & 3 / 5 & 1 / 5 \\ P_{1} (y) & 1 / 10 & 1 / 10 & 4 / 5 \end{array}$ Give $Θ$ and $Y$ their discrete sigma-algebras, take $S (y) = y$ into $R$ , observe $y = 1$ , and set $ϵ = 3 / 5$ .

[F1]

The ABC target is the prior-simulator law conditioned on the closed ball event when its prior-predictive probability is positive. Approximate Bayesian computation and the tolerance-conditioned target

[F2]

If the proposal-simulator pairs are IID and acceptance probability is positive, ABC rejection terminates almost surely and its accepted parameter has exactly the tolerance-conditioned target. ABC rejection returns the tolerance-conditioned posterior

[F3]

A finite discrete space with its discrete metric is complete and separable, and its Borel sigma-algebra is its power set; a function from this finite measurable space into $(R, B (R))$ is measurable because every preimage is a subset of the finite source. Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric Complete metric space: every Cauchy sequence converges in the space Separability: the existence of an at most countable dense subset Polish spaces are separable completely metrizable spaces Standard Borel spaces The Borel sigma-algebra of a topological space

[F4]

Exact fixed-data posterior probabilities are obtained by normalizing likelihood times prior when evidence is finite and positive. Exact inferential targets and approximation chains

[F5]

Total variation is the supremum over measurable events. Total variation distance for probability laws

[F6]

A probability kernel assigns a probability measure at each parameter, and its probabilities of measurable events are measurable functions of the parameter. Measure kernel and probability kernel

Counterexample

Given: The table, equal prior, identity summary, observation, and positive tolerance in Facts & Assumptions.

1.1F3F6givenalgebra

Each row sums to one and has nonnegative entries, so it defines a probability measure at each parameter. Every event probability is measurable in the finite parameter space, hence the table defines a probability kernel by [F6]. Under the discrete metric a Cauchy sequence is eventually constant (take tail distances below $1 / 2$ ); each finite set is separable and all of its subsets are open. Hence both are standard Borel. The summary map $S$ is measurable to the real Borel sigma-algebra because every preimage is a subset of the finite measurable data space, by [F3].

1.2F1F4givenalgebra

At observation $1$ , the likelihoods are $1 / 5$ and $4 / 5$ , so the exact posterior mass at $θ = 1$ is $(4 / 5) / (1 / 5 + 4 / 5) = 4 / 5$ by [F4]. The closed $ϵ$ -ball around $1$ is ${1 / 2, 1}$ . Its conditional probabilities are $P_{0} (B) = 3 / 5 + 1 / 5 = 4 / 5$ and $P_{1} (B) = 1 / 10 + 4 / 5 = 9 / 10$ . Therefore the prior-predictive acceptance probability is $\frac{1}{2} (4 / 5 + 9 / 10) = 17 / 20 > 0$ .

2.1F1step 1.2algebra

Conditioning the prior-simulator law on this ball gives ABC mass at $θ = 1$ equal to $\frac{(1 / 2) (9 / 10)}{17 / 20} = 9 / 17$ by [F1]. The exact and ABC posterior masses differ by $∣ 4 / 5 - 9 / 17 ∣ = 23 / 85$ .

3.1F2F5step 2.1algebra∎

The measurable events in $Θ = {0, 1}$ are $\emptyset$ , ${0}$ , ${1}$ , and $Θ$ . The exact and ABC probabilities agree on $\emptyset$ and $Θ$ ; on ${1}$ their difference has absolute value $∣ 4 / 5 - 9 / 17 ∣ = 23 / 85$ , and on ${0}$ it has the same absolute value because both are probability measures. Thus [F5] gives total-variation distance exactly $23 / 85$ . If the proposal-simulator pairs $(Θ_{j}, Y_{j})$ are IID under the prior-kernel joint law, [F2] identifies this ABC target as the accepted-parameter law; the finite calculations make no additional convergence or efficiency claim.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

44 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

Jarno Lintusaari et al., Fundamentals and Recent Developments in Approximate Bayesian Computation (2017) (standard reference, not scraped)
Paul Fearnhead and Dennis Prangle, Constructing Summary Statistics for Approximate Bayesian Computation: Semi-automatic ABC (2012) (standard reference, not scraped)