Pipeline-generated

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.

✓ 2 results · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Identifiability and approximation bias in computational inference

1 · Prerequisites

2 · Summary

Objective

This page separates the full-data inferential target from changes introduced by algorithms, summaries, asymptotic approximations, and numerical computation. It defines a fixed-data posterior only after a measurable likelihood version and finite positive evidence have been supplied, then places that target in a declared metric space with a finite approximation chain.

Identifiability is a property of the full sampling laws: equal laws must give equal values of the estimand. The examples show that this property does not prevent a summary from discarding information, a positive ABC tolerance from changing the conditional target, a mean-field ELBO optimizer from losing correlation, a Gaussian synthetic likelihood from changing a posterior, or a local Laplace mode from missing another global mode. The total-variation expectation bounds use the event-supremum convention: factor two for functions bounded in absolute value by $M$ , and the sharper $M$ bound for nonnegative functions between $0$ and $M$ .

For scalar chains, the pathwise signed identity is exact. For probability laws or other objects, the metric theorem gives a triangle bound only when every adjacent comparison uses the same metric on the same space. Neither result supplies independence, variance addition, global optimizer convergence, posterior consistency, or calibration. In particular, a model's identifiability does not imply that an approximation procedure preserves its exact inferential target.

The Gaussian mean-field calculation takes its reference area measure as supplied and obtains the needed length measure from a fixed unit-height strip. A local Darboux comparison proves its density normalizers and moments without adding a choice axiom or constructing those measures.

3 · Logical flowchart

4 · Definitions, theorems and proofs

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Total variation controls expectations of bounded functions

Statement

Let $(E, E)$ be a measurable space, let $P$ and $Q$ be probability measures on it, and let $f : E \to R$ be measurable with $∣ f ∣ \leq M$ pointwise for some finite $M \geq 0$ . With the convention $∥ P - Q ∥_{T V} : = \sup_{A \in E} ∣ P (A) - Q (A) ∣,$ one has $∣ \int f d P - \int f d Q ∣ \leq 2 M ∥ P - Q ∥_{T V} .$ For every measurable $g : E \to R$ with $0 \leq g \leq M$ pointwise, one also has $∣ \int g d P - \int g d Q ∣ \leq M ∥ P - Q ∥_{T V} .$ Both integral differences are zero when $M = 0$ .

Facts & Assumptions

Given: A measurable space $(E, E)$ , probability measures $P, Q$ , and measurable real functions $f, g$ satisfying $∣ f ∣ \leq M < \infty$ and $0 \leq g \leq M$ .

[F1]

A probability measure has total mass one. Probability measures and probability spaces

[F2]

Total variation here is the event supremum $\sup_{A \in E} ∣ P (A) - Q (A) ∣$ and has no half-factor. Total variation distance for probability laws

[F3]

On nonnegative simple functions, the nonnegative Lebesgue integral agrees with the simple integral. The nonnegative integral agrees with the simple integral on simple functions

[F4]

The simple integral is the sum of the coefficients times the measures of the level sets; in particular, an indicator integrates to the measure of its set. The integral of a nonnegative simple function

[F5]

The nonnegative integral is additive, monotone, and nonnegatively homogeneous. Additivity of the nonnegative Lebesgue integral Monotonicity and nonnegative homogeneity of the nonnegative integral

[F6]

A real measurable function is integrable when its absolute value has finite nonnegative integral; the integral is linear on integrable functions. Integrable real and complex functions, and their integrals The Lebesgue integral is linear on $L^{1} (μ)$

[F7]

For every $η > 0$ there is an integer $n \geq 1$ with $1 / n < η$ . For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$

Proof

Given: The hypotheses in the Statement.

1.1givenconstruct

If $M = 0$ , then $f = 0$ and $g = 0$ pointwise, so both claims hold. To prove the nonnegative claim for an arbitrary finite bound $L > 0$ , let $w : E \to R$ be measurable with $0 \leq w \leq L$ , fix an integer $n \geq 1$ , put $Δ = L / n$ , and define $A_{k} = {x : w (x) \geq k Δ}$ for $1 \leq k \leq n$ and $s_{n} = Δ \sum_{k = 1}^{n} 1_{A_{k}}$ . The sets are measurable, $s_{n}$ is nonnegative simple, and $0 \leq w - s_{n} \leq Δ$ pointwise.

2.1F1F2F3F4F5step 1.1algebra

By [F3]–[F5], $\int s_{n} d P = Δ \sum_{k = 1}^{n} P (A_{k})$ and likewise for $Q$ , so $∣ \int s_{n} d P - \int s_{n} d Q ∣ \leq n Δ ∥ P - Q ∥_{T V} = L ∥ P - Q ∥_{T V}$ . Also $0 \leq \int (w - s_{n}) d P \leq Δ$ and $0 \leq \int (w - s_{n}) d Q \leq Δ$ , because $w - s_{n} \leq Δ$ and both measures have mass one. The triangle inequality therefore gives $∣ \int w d P - \int w d Q ∣ \leq L ∥ P - Q ∥_{T V} + 2 L / n$ .

3.1F7step 2.1algebra

Given any $η > 0$ , choose $n$ by [F7] with $1 / n < η / (2 L)$ . The estimate in step 2.1 then gives $∣ \int w d P - \int w d Q ∣ < L ∥ P - Q ∥_{T V} + η$ . If the bound by $L ∥ P - Q ∥_{T V}$ failed, choosing $η$ to be half the positive excess would contradict this inequality. Taking $w = g$ and $L = M$ proves the stated nonnegative case when $M > 0$ .

4.1F1F3F4F5F6step 3.1algebra∎

For the signed case with $M > 0$ , let $h = f + M$ . Then $h$ is measurable and $0 \leq h \leq 2 M$ , so step 3.1 with $w = h$ and $L = 2 M$ gives $∣ \int h d P - \int h d Q ∣ \leq 2 M ∥ P - Q ∥_{T V}$ . Also $∣ f ∣ \leq M$ , so [F1], [F3]–[F5] give $\int ∣ f ∣ d P \leq M$ and $\int ∣ f ∣ d Q \leq M$ ; hence $f$ is integrable under both measures by [F6]. The constant $M$ has integral $M$ under each probability measure, so linearity [F6] gives $\int f d P - \int f d Q = \int h d P - \int h d Q$ . This proves the signed case.

DefinitionDefinition: Literature-sourcedProof: Not applicableOpen item page →

Exact inferential targets and approximation chains

Definition

Fix a measurable parameter space $(Θ, T)$ , a prior probability measure $Π_{0}$ on it, observed data $x$ , and an explicitly supplied $T$ -measurable likelihood version $ℓ_{x} : Θ \to [0, \infty)$ . Define the evidence $Z_{x} : = \int_{Θ} ℓ_{x} d Π_{0} .$ When $0 < Z_{x} < \infty$ , the exact inferential target is the probability measure $Π_{x} (A) : = \frac{1}{Z_{x}} \int_{A} ℓ_{x} d Π_{0} (A \in T) .$ The measure is well-defined by the indefinite-integral construction The indefinite integral of a nonnegative measurable function is a measure. This is a fixed-data definition: Likelihood densities selects, under AC, a measurable data-space density representative $p_{θ}$ for each parameter $θ$ , but does not guarantee measurability of $θ \mapsto p_{θ} (x)$ . Here the fixed-data likelihood version and its parameter measurability are supplied explicitly; no posterior is assigned when the evidence is zero or infinite.

For approximation accounting, declare a metric space $(M, d)$ and a finite chain of elements $T_{0}, T_{1}, \dots, T_{m}, \hat{T} \in M$ , where $m \geq 1$ and $T_{1} = Π_{x}$ whenever the exact target is included. The first distance $d (T_{0}, T_{1})$ is the declared reference-to-target discrepancy; later adjacent distances and $d (T_{m}, \hat{T})$ are approximation and computation discrepancies on the same metric scale. For probability measures on a common measurable space, total variation may be used with the event-supremum convention of Total variation distance for probability laws. For scalar random quantities on one probability space, the statistical and computational stages are the same-scale signed differences defined in Successive statistical and computational error targets. This notation does not assert independence, unbiasedness, convergence, or that any numerical method attains a global optimum.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Metric approximation error decomposes along a finite reference chain

Statement

Let $(M, d)$ be a metric space, let $m \geq 0$ be an integer, and take $T_{0}, T_{1}, \dots, T_{m}, \hat{T} \in M$ . Then $d (T_{0}, \hat{T}) \leq \sum_{j = 1}^{m} d (T_{j - 1}, T_{j}) + d (T_{m}, \hat{T}),$ where the sum is empty when $m = 0$ . If $m \geq 1$ and $T_{1}$ is the exact target from Exact inferential targets and approximation chains, the first term is the declared reference-to-target discrepancy and subsequent terms quantify adjacent approximation changes in the same metric. The scalar identity and absolute bound of Pathwise error decomposition along a reference chain are exact telescoping statements. No independence or default variance-addition rule follows; the MSE identity in MSE of a sum of error components includes covariance terms retains total bias and covariance terms.

Facts & Assumptions

Given: A metric space $(M, d)$ , an integer $m \geq 0$ , and points $T_{0}, \dots, T_{m}, \hat{T} \in M$ .

[F1]

A metric is symmetric and satisfies $d (x, z) \leq d (x, y) + d (y, z)$ . Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric

[F2]

Scalar ledger stages are adjacent signed differences on one stated scale; the definition alone asserts no independence, centering, or unbiasedness. Successive statistical and computational error targets

[F3]

A finite scalar ledger chain satisfies the signed telescoping identity and its absolute-value bound without an independence assumption. Pathwise error decomposition along a reference chain

[F4]

For square-integrable scalar error terms, the MSE of their sum includes squared total bias and covariance terms; summing component variances alone is generally not the identity. MSE of a sum of error components includes covariance terms

Proof

Given: The hypotheses in the Statement.

1.1givenF1inductionalgebra

We prove by induction on $m$ that $d (T_{0}, T_{m}) \leq \sum_{j = 1}^{m} d (T_{j - 1}, T_{j})$ . For $m = 0$ both sides are zero; for $m = 1$ this is equality. If it holds through $m$ , then the triangle inequality [F1] gives $d (T_{0}, T_{m + 1}) \leq d (T_{0}, T_{m}) + d (T_{m}, T_{m + 1}) \leq \sum_{j = 1}^{m + 1} d (T_{j - 1}, T_{j})$ .

2.1F2F3F4step 1.1algebra∎

Apply the triangle inequality once more to $T_{0}, T_{m}, \hat{T}$ and then step 1.1 to bound $d (T_{0}, \hat{T})$ by the displayed sum. For a scalar chain, [F2] specifies the same-scale adjacent errors and [F3] gives their exact signed telescope; when the terms are square-integrable, [F4] explains why squaring them retains bias and covariance terms rather than giving an automatic variance sum.

LemmaStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-6-luna)Open item page →

Gaussian density integrals for supplied length measures

Statement

For $d \in {1, 2}$ , suppose a countably additive measure $λ_{d}$ on $B (R^{d})$ is supplied and satisfies $λ_{d} ⁣ (\prod_{j = 1}^{d} (a_{j}, b_{j}]) = \prod_{j = 1}^{d} (b_{j} - a_{j}) (a_{j} < b_{j}) .$ No assertion about constructing these measures is made.

If $Q$ is a nondegenerate compact box and $h : Q \to R$ is bounded, Borel measurable and Riemann integrable, then its integral against the supplied measure equals its proper Riemann integral. Nonnegative Borel functions on the whole space are computed from increasing compact-box cutoffs by monotone convergence.
For the supplied $λ_{1}$ , every $m \in R$ , $v > 0$ and $g_{m, v} (x) = \frac{1}{\sqrt{2 π v}} e^{- (x - m)^{2} / (2 v)}$ satisfy $\int g_{m, v} d λ_{1} = 1, \int x g_{m, v} (x) d λ_{1} (x) = m, \int (x - m)^{2} g_{m, v} (x) d λ_{1} (x) = v .$ The signed first moment is absolutely integrable. These are density-integral statements and require no choice axiom in addition to the supplied measures.

Facts & Assumptions

Given: The supplied Borel measures and their half-open-box volumes in the Statement.

[F1]

Borel sets form the sigma-algebra generated by open sets. A continuous real function is Borel measurable: its inverse images of open sets are open, and the sets whose inverse images are Borel form a sigma-algebra. The Borel sigma-algebra of a topological space

[F2]

Measures are monotone; nonnegative simple integrals are finite sums of coefficients times cell measures and agree with the nonnegative integral. Measures are monotone, The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions

[F3]

Nonnegative integrals are monotone and homogeneous, and integrals are linear on absolutely integrable functions. Monotonicity and nonnegative homogeneity of the nonnegative integral, The Lebesgue integral is linear on $L^{1} (μ)$

[F4]

A bounded Riemann integrand has equal upper and lower Darboux integrals; continuous one-variable functions on compact intervals are Riemann integrable. The multidimensional Darboux and tagged-mesh definitions of the Riemann integral agree, A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion

[F5]

Monotone convergence and dominated convergence apply on a supplied measure space. Monotone convergence for the integral, Dominated convergence

[F6]

The improper Riemann Gaussian integral is $\int_{- \infty}^{\infty} e^{- t^{2}} d t = \sqrt{π}$ ; proper substitution and integration by parts hold on compact intervals. The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ , Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$ , If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$

[F7]

The exponential is continuously differentiable with derivative itself, and the chain rule applies. Exponential growth dominates each fixed polynomial, and a positive real has a positive square root. The exponential function is smooth and $(\exp)^{'} = \exp$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , The exponential dominates every fixed nonnegative integer power at $+ \infty$ , Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$

Proof

technique · finite Darboux bounds followed by explicit cutoffs

1.1givenF2algebra

Every compact box has finite supplied measure, since it is contained in a larger half-open box. A bounded coordinate face has measure zero: enclose it in a half-open slab of arbitrary positive thickness $η$ , with the other side lengths fixed and positive. Its measure is at most $C η$ by the given volume formula and [F2], and so must be zero. In dimension one this says that singletons are null. Consequently compact boxes have their usual volumes, and disjointifying a finite grid of closed cells only removes null faces.

2.1step 1.1F2F3F4F5construct

For a nonnegative bounded Borel Riemann integrand $h$ on $Q$ , take the infimum and supremum of $h$ on each cell of any finite grid. The corresponding disjoint-cell simple functions bound $h$ , and [F2] and step 1.1 make their integrals exactly the lower and upper Darboux sums. By [F3] and [F4], the integral of $h$ is squeezed to its Riemann value. For signed bounded $h$ , add a finite constant to make it nonnegative and subtract that constant's finite integral using [F3]. This proves the compact comparison. For nonnegative Borel $H$ on the whole space, $H 1_{[- n, n]^{d}} ↑ H$ , so [F5] gives the cutoff assertion. The grids, extrema, and cutoff sequence are finite or explicitly specified; no countable selection is used.

3.1F1F4F5F6F7step 2.1

Put $ϕ (t) = (2 π)^{- 1 / 2} e^{- t^{2} / 2}$ . It is continuous and Borel by [F1] and [F7]. On $[- n, n]$ , proper substitution $t = \sqrt{2} u$ in [F6] computes its Riemann integral. As $n \to \infty$ , [F6]'s improper Gaussian value makes this tend to one. Step 2.1 identifies each compact integral with its supplied-measure integral, and [F5] gives $\int ϕ d λ_{1} = 1$ .

4.1F4F5F6F7step 2.1step 3.1algebra

Since $ϕ^{'} = - t ϕ$ by [F7], compact integration by parts [F6] gives $\int_{- n}^{n} t^{2} ϕ (t) d t = \int_{- n}^{n} ϕ (t) d t - 2 n ϕ (n) .$ All functions and derivatives here are continuous, so the proper integral hypotheses hold by [F4]. Also $n ϕ (n) \to 0$ : for $n \geq 1$ , $n^{2} / 2 \geq n / 2$ , hence $0 \leq n e^{- n^{2} / 2} \leq n e^{- n / 2} \to 0$ by [F7]. Apply step 2.1 and monotone convergence [F5] to the nonnegative $t^{2} ϕ (t)$ cutoffs. Step 3.1 then gives $\int t^{2} ϕ (t) d λ_{1} = 1$ .

5.1F3F5F6step 2.1step 3.1step 4.1algebra

The bound $∣ t ∣ \leq 1 + t^{2}$ and steps 3.1, 4.1 make $∣ t ∣ ϕ (t)$ integrable. On each symmetric compact interval, the Riemann integral of $t ϕ (t)$ is zero by oddness, using the proper substitution $t = - u$ . Step 2.1 transfers these compact integrals to the supplied measure. Dominated convergence [F5], with majorant $∣ t ∣ ϕ (t)$ , yields $\int t ϕ (t) d λ_{1} = 0$ .

6.1F3F5F6F7step 2.1step 3.1step 4.1step 5.1constructalgebra∎

Fix $m \in R$ and $σ = \sqrt{v} > 0$ . On the explicitly specified intervals $[m - σ n, m + σ n]$ , proper substitution $x = m + σ t$ gives compact integrals of $g_{m, v}$ , $(x - m)^{2} g_{m, v}$ and $(x - m) g_{m, v}$ equal to the corresponding integrals of $ϕ$ , $σ^{2} t^{2} ϕ$ and $σ t ϕ$ on $[- n, n]$ . Step 2.1 and monotone convergence give mass one and centered second moment $σ^{2} = v$ . Since $∣ x - m ∣ \leq 1 + (x - m)^{2}$ , the centered first moment is absolutely integrable, and the same dominated-cutoff argument as step 5.1 gives centered mean zero. Linearity then gives raw mean $m$ . This proves both claims for the supplied measures without constructing any new measure or invoking a choice-dependent normal-law supplier.

5 · Examples, counterexamples and false statements

None yet.

Identifiability and approximation bias in computational inference

1 · Prerequisites

2 · Summary

Objective

3 · Logical flowchart

4 · Definitions, theorems and proofs

Total variation controls expectations of bounded functions

Statement

Facts & Assumptions

Proof

Exact inferential targets and approximation chains

Definition

Metric approximation error decomposes along a finite reference chain

Statement

Facts & Assumptions

Proof

Gaussian density integrals for supplied length measures

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources