CounterexampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 particle proposal can miss positive target mass

Statement refuted

False claim: The transition support condition $M_{k} (x, \cdot) ≪ R_{k} (x, \cdot)$ may be dropped while the same proposal-weighted particle measure still represents the Feynman–Kac target.

Facts & Assumptions

Given: The finite model and proposal in the Counterexample.

[F1]

Feynman–Kac path targets and normalizers: The unnormalized path law is the initial/transition path law weighted by the product of the specified potentials.

[F2]

Sequential importance resampling for Feynman–Kac path targets: Particle paths are proposed using $R_{k}$ and then weighted using the target-to-proposal kernel derivative; the procedure requires the support and derivative hypotheses in its definition.

Counterexample

1.1F1givenalgebra

Let $X_{0} = {*}$ and $X_{1} = {a, b}$ . Take $μ_{0} = ν_{0} = δ_{*}$ , $M_{1} (*, {a}) = M_{1} (*, {b}) = 1 / 2$ , $R_{1} (*, {a}) = 1$ , $R_{1} (*, {b}) = 0$ , and $G_{0} = G_{1} = 1$ . By [F1], $γ_{1}$ is the transition law itself, $Z_{1} = 1$ , and the normalized target assigns mass $1 / 2$ to $b$ .

2.1F2step 1.1given

The support premise fails because $M_{1} (*, {b}) = 1 / 2$ while $R_{1} (*, {b}) = 0$ . A proposal path drawn from $Q_{1} = ν_{0} R_{1}$ equals $(*, a)$ with probability one, so every empirical measure formed from such paths assigns mass zero to the event ${x_{1} = b}$ .

3.1step 1.1step 2.1algebra∎

If a kernel derivative $r_{1}$ represented $M_{1} (*, \cdot)$ with respect to $R_{1} (*, \cdot)$ , then $M_{1} (*, {b}) = \int_{{b}} r_{1} (*, y) R_{1} (*, d y) = 0$ , contradicting the value $1 / 2$ . Thus the required importance weight does not exist on this target-positive, proposal-null set, and the false claim fails.

Remarks

The example refutes target coverage after support failure; it does not assert that every numerical normalizer estimate must be biased when support fails.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

Arnaud Doucet and Adam M. Johansen, A Tutorial on Particle Filtering and Smoothing: Fifteen Years Later, §3.2 (standard reference, not scraped)
Simo Särkkä and Lennart Svensson, Bayesian Filtering and Smoothing, 2nd ed., §11.2 (standard reference, not scraped)