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.

✓ 1 result · 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; all 1 also cleared it.

Method agreement

1 · Prerequisites

2 · Summary

Method agreement compares paired measurements of the same target under a declared population of measurement conditions. The signed difference has a population bias and spread; under an exact normal-difference model, its central 95% quantiles are the bias plus or minus the standard-normal 97.5th percentile times the spread. The customary 1.96 display is rounded. Sample plug-in limits are point estimates, not endpoint confidence intervals. Repeated measurements need their within-target dependence stated, and correlation alone does not establish agreement or calibration.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Method agreement and limits of agreement

Definition

Let $(Ω, F, P)$ be the declared probability model for a pre-specified target population of measurement conditions. Let $A$ and $B$ be real random variables giving quantitative measurements of the same target under the same stated conditions. The choice of target population and the scientific applicability of its probability law are model assumptions; this definition does not verify them.

Assume the paired difference $D : = A - B$ is square-integrable. It is measurable because measurable real functions are closed under finite sums and scalar multiples (Closure properties of measurable functions used by the integral). Since $0 \leq (∣ D ∣ - 1)^{2}$ , we have $∣ D ∣ \leq (D^{2} + 1) / 2$ . Monotonicity, homogeneity, and additivity of the nonnegative integral, together with $P (Ω) = 1$ , give $E [∣ D ∣] \leq \frac{1}{2} E [D^{2}] + \frac{1}{2} < \infty$ (Monotonicity and nonnegative homogeneity of the nonnegative integral, Additivity of the nonnegative Lebesgue integral). Thus define the finite population bias $μ_{D} : = E [D]$ . Put $H : = D - μ_{D}$ , which is measurable by the same closure result. Its square $H^{2}$ is measurable by Arithmetic and lattice operations preserve measurability whenever they are defined. Since $H^{2} \leq 2 D^{2} + 2 μ_{D}^{2},$ monotonicity, homogeneity, and additivity of the nonnegative integral give $E [H^{2}] \leq 2 E [D^{2}] + 2 μ_{D}^{2} < \infty$ (Monotonicity and nonnegative homogeneity of the nonnegative integral, Additivity of the nonnegative Lebesgue integral). Therefore $σ_{D} : = \sqrt{Var (D)} = \sqrt{E [H^{2}]}$ is a finite real standard deviation, since $Var (D) = E [H^{2}]$ by Moments, variance, and covariance on a probability space and every nonnegative real has a square root by Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ . The sign convention is $D = A - B$ , so positive bias means that $A$ reads larger than $B$ on average. The conventional rounded normal-reference limits of agreement are $μ_{D} - 1.96 σ_{D}$ and $μ_{D} + 1.96 σ_{D}$ .

For an iid sample $D_{1}, \dots, D_{n}$ of paired differences from the declared target population, with $n \geq 2$ and observed values $d_{1}, \dots, d_{n}$ , define $\overset{ˉ}{d} : = \frac{1}{n} \sum_{i = 1}^{n} d_{i}, s_{D} : = \sqrt{\frac{1}{n - 1} \sum_{i = 1}^{n} (d_{i} - \overset{ˉ}{d})^{2}} .$ The sample plug-in limits are $\overset{ˉ}{d} \pm 1.96 s_{D}$ : they substitute the sample mean and sample standard deviation into the conventional population formula. They are point estimates; no unbiasedness, consistency, confidence coverage, or exact finite-sample coverage for either endpoint is asserted here.

Repeated measurements on one target are not iid merely because there are many recorded pairs. Their within-target dependence must be stated and modeled, for example with a covariance or random-effects model. When defined, correlation measures linear association and does not by itself establish agreement. Limits of agreement describe the distribution of differences; they do not decide whether those differences are acceptable for a particular use or whether either method is calibrated to a known truth.

Remarks

The exact central normal quantile formula is established by a separate result on this page. The customary $1.96$ display is a rounded normal quantile convention.

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

Normal differences have limits at their central quantiles

Statement

Assume the Axiom of Choice. Use $D$ , $μ_{D}$ , and $σ_{D}$ from Method agreement and limits of agreement, and suppose the law of $D$ is $N (μ_{D}, σ_{D}^{2})$ with $σ_{D} \geq 0$ . Put $Φ (x) : = N (0, 1) ((- \infty, x]), z_{.975} : = \inf {x \in R : Φ (x) \geq .975} .$ For $D$ , put $F_{D} (x) : = P (D \leq x)$ and, for $0 < p < 1$ , define the lower $p$ -quantile by $q_{p} (D) : = \inf {x \in R : F_{D} (x) \geq p} .$ Then $z_{.975}$ is the unique real number with $Φ (z_{.975}) = .975$ , and $z_{.975} > 0$ . The exact central normal quantiles satisfy $q_{.025} (D) = μ_{D} - z_{.975} σ_{D}, q_{.975} (D) = μ_{D} + z_{.975} σ_{D} .$ If $σ_{D} > 0$ , the closed interval $[q_{.025} (D), q_{.975} (D)]$ has probability $0.95$ . If $σ_{D} = 0$ , both quantiles equal $μ_{D}$ and the singleton has probability $1$ . Thus $μ_{D} \pm 1.96 σ_{D}$ is the customary rounded display; the exact endpoints use $z_{.975}$ .

Facts & Assumptions

Given: AC; a square-integrable paired difference $D = A - B$ under a declared probability model; the law identity $L (D) = N (μ_{D}, σ_{D}^{2})$ with $σ_{D} \geq 0$ ; $F_{D} (x) = P (D \leq x)$ ; and the definitions of $Φ$ , $z_{.975}$ , and $q_{p} (D)$ in the Statement.

[A1]

The Axiom of Choice says that every family of nonempty sets has a choice function. The Axiom of Choice

[F1]

Assume AC. The standard normal law has density $ϕ (t) = e^{- t^{2} / 2} / \sqrt{2 π}$ , and $N (m, σ^{2})$ is the law of $x \mapsto m + σ x$ under $N (0, 1)$ for $σ \geq 0$ ; when $σ = 0$ , $N (m, 0) = δ_{m}$ . Standard normal and normal laws

[F2]

Under AC, $ϕ$ is positive and Borel measurable on $R$ and has Lebesgue integral one. The standard normal density has total mass one

[F3]

The Axiom of Countable Choice says every sequence of nonempty sets has a choice sequence. The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F4]

A one-dimensional box with equal endpoints has Lebesgue measure zero; the box theorem assumes countable choice. A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included

[F5]

The nonnegative integral over a measurable null set is zero. A nonnegative integral over a null set vanishes

[F6]

The real exponential maps $R$ into $(0, \infty)$ . The power-series, product-limit, IVP, functional-equation, and Picard definitions agree

[F7]

The real exponential is smooth with derivative equal to itself. The exponential function is smooth and $(\exp)^{'} = \exp$

[F8]

The mean value theorem gives $f (b) - f (a) = f^{'} (c) (b - a)$ for some $c \in (a, b)$ when $f$ is continuous on $[a, b]$ and differentiable on $(a, b)$ . The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$

[F9]

Probability measures are continuous from below and, for decreasing events, continuous from above. Basic identities for a probability measure

[F10]

For a differentiable change of variable on a compact interval and a continuous integrand, the oriented integral obeys the substitution formula. 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 φ) φ^{'}$

[F11]

The paired difference is $D = A - B$ , with bias $μ_{D} = E [D]$ and spread $σ_{D} = \sqrt{Var (D)}$ . Method agreement and limits of agreement

[F12]

A continuous real function on a closed bounded interval attains every value between its endpoint values; the constructive theorem uses no additional choice principle. Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$

[F13]

The nonnegative integral is monotone and homogeneous for positive scalars (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F14]

A continuous real function on a compact nondegenerate interval is bounded and Riemann integrable. A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion

[F15]

Under countable choice, a bounded Riemann integrable function on a compact interval has the same Lebesgue and Riemann integrals. A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral

Proof

technique · direct

1.1A1F1F2F3F4F5givenconstruct

AC in [A1] applies to the normal-law construction [F1]. It also supplies countable choice: for any sequence of nonempty sets, apply AC to the family of its values and compose the resulting choice function with the sequence, which is the property in [F3]. Thus the countable-choice hypothesis in [F4] is available. Taking the one-dimensional box with equal endpoints $x = x$ in [F4] gives $λ ({x}) = 0$ ; the density in [F1] is nonnegative measurable by [F2], so [F5] gives $N (0, 1) ({x}) = 0$ . Thus the standard normal law has no atoms.

1.2F1F2F4F6F7F8F9F13algebra

For $x < y$ , probability subtraction and the density definition give $Φ (y) - Φ (x) = N (0, 1) ((x, y]) = \int_{(x, y]} ϕ d λ$ . Let $M = \max {∣ x ∣, ∣ y ∣}$ . Positivity [F6], derivative [F7], and the mean value theorem [F8] show that the exponential is increasing. Hence on $[x, y]$ , $α : = e^{- M^{2} / 2} / \sqrt{2 π} \leq ϕ (t) \leq β : = 1 / \sqrt{2 π}$ , with $α > 0$ . By [F4, F13], $0 < α (y - x) \leq Φ (y) - Φ (x) \leq β (y - x)$ . Therefore $Φ$ is strictly increasing and continuous.

2.1F1F7F9F10F14F15step 1.1step 1.2algebra

By [F9], $Φ (n) \to 1$ and $Φ (- n) \to 0$ as $n \to \infty$ . The density is continuous by [F7] and even. On each compact interval below, [F14, F15] identify its Riemann and Lebesgue integrals, using countable choice from step 1.1. For $n > ∣ x ∣$ , substitution $u = - t$ in [F10] gives $\int_{- n}^{- x} ϕ (t) d t = \int_{x}^{n} ϕ (u) d u$ . Passing to the tail limits gives $Φ (- x) = P (Z \geq x)$ for $Z \sim N (0, 1)$ . By the no-atom result in step 1.1, $P (Z \geq x) = 1 - Φ (x)$ , so $Φ (- x) = 1 - Φ (x)$ and $Φ (0) = 1 / 2$ .

3.1F12step 1.2step 2.1choosealgebra

By step 2.1, choose an integer $b > 0$ with $Φ (b) > .975$ , while $Φ (0) = 1 / 2 < .975$ . Step 1.2 makes $Φ$ continuous on the finite closed interval $[0, b]$ , so [F12] gives $z \in (0, b)$ with $Φ (z) = .975$ . Strict increase from step 1.2 makes $z$ unique, and step 2.1 gives $Φ (- z) = .025$ . Strict increase makes these the unique lower quantiles at those levels, so $z = z_{.975}$ , the set ${x : Φ (x) \geq .975}$ has infimum $z$ , and the set ${x : Φ (x) \geq .025}$ has infimum $- z$ .

4.1F1F11step 1.1step 3.1algebra

If $σ_{D} > 0$ , [F1] gives $F_{D} (x) = Φ ((x - μ_{D}) / σ_{D})$ , since $μ_{D} + σ_{D} t \leq x$ exactly when $t \leq (x - μ_{D}) / σ_{D}$ . The increasing affine change of variable carries the quantiles from step 3.1 to $μ_{D} - z_{.975} σ_{D}$ and $μ_{D} + z_{.975} σ_{D}$ . By [F1] and step 1.1, this affine image of the standard normal law has no atoms. The endpoint CDF values are $.025$ and $.975$ , so the closed interval between them has probability $.975 - .025 = .95$ , as stated.

5.1F1F11algebra∎

If $σ_{D} = 0$ , [F1] gives $N (μ_{D}, 0) = δ_{μ_{D}}$ . Its distribution function is $0$ below $μ_{D}$ and $1$ at or above $μ_{D}$ , so both lower quantiles are $μ_{D}$ and the singleton has probability $1$ . This is exactly the formula in the Statement with $σ_{D} = 0$ .

5 · Examples, counterexamples and false statements

None yet.