Alphabeta Math
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.

✓ 3 results · all verified · 3 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 3 also cleared it.

Detection and quantification limits

1 · Prerequisites

2 · Summary

Objective

This page separates the blank decision threshold LC, the concentration LD meeting a specified false-negative target, and the concentration LQ meeting a declared precision criterion. The exact normal formulas are proved for the known-blank, equal-variance model, with the normal quantile and location-scale moments established locally.

Scope and limitations

The formulas depend on the response law and calibration convention. An estimated blank changes the variance used for the calculation; concentration- dependent variance can change or eliminate a finite detection or quantification limit. The page makes no universal claim for estimated-blank, heteroscedastic, discrete, or empirically unvalidated procedures. A report that a value lies below a limit is a censored observation and requires its measurement likelihood.

3 · Logical flowchart

4 · Definitions, theorems and proofs

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

Critical, detection, and quantification levels

Definition

Let C=[0,∞) be a concentration parameter set and let E=((R,B(R)),C,(Pc)c∈C) be a statistical experiment (Statistical experiments). The response X(x)=x is a real random variable (Random elements and real random variables) with law Pc at concentration c; P0 is the blank law. Since each (t,∞) is open, it is Borel (The Borel sigma-algebra of a topological space), so the indicator rule below is measurable. For a threshold t∈R, the positive-decision rule is φt(x)=1{x>t}. Its blank false-positive probability is P0(X>t), and its false-negative probability at c>0 is Pc(X≤t). These are the null rejection probability and one minus the power for the simple null {0} and point alternative {c} (Randomized tests, Test size and power, The expectation of an indicator is the probability of the event, Basic identities for a probability measure).

For a target α∈(0,1), an exact critical level LC is a threshold satisfying P0(X>LC)=α. A threshold with probability at most α is an α-level threshold; equality need not be attainable for a discrete response. For a target β∈(0,1), a detection limit LD is the least c>0 satisfying Pc(X≤LC)=β, when such a least concentration exists. Thus LC is measured in response units, whereas LD is measured in concentration units.

When 0<Ec[X]<∞ and Var⁡c(X)<∞, the coefficient of variation is CV⁡(c):=Var⁡c(X)Ec[X]. Expectation under Pc is as in Expectation of a nonnegative or integrable random variable, and variance has the meaning in Moments, variance, and covariance on a probability space. For a declared tolerance kQ>0, a quantification limit LQ is the least c>0 satisfying CV⁡(c)≤kQ, when such a least concentration exists. This definition does not make the three limits universal: each is tied to the response law and the stated error or precision criterion.

Remarks

The measurement procedure and its observation law must include any blank correction used in routine reporting. A below-threshold report is an event such as X≤LC; its likelihood contribution is determined by the declared measurement law, not by substituting LC as though it were an observed response.

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

The standard normal CDF has unique symmetric quantiles

Statement

Assume the Axiom of Choice. Let Z have the standard normal law and let Φ(x)=P(Z≤x) be its cumulative distribution function. Then Φ is continuous and strictly increasing, with limits 0 and 1 at −∞ and +∞, and P(Z=x)=0 for every x∈R. For each q∈(0,1) there is a unique real zq with Φ(zq)=q, and z1−q=−zq.

Facts & Assumptions

Given: AC; the standard normal law N(0,1); its CDF Φ; and a probability q∈(0,1) when a quantile is considered.

[A1]

The Axiom of Choice is assumed in the construction of the standard normal probability law. The Axiom of Choice Standard normal and normal laws

[A2]

AC implies countable choice, which is the hypothesis needed for the zero-width-box measure result used to show singleton sets have zero normal probability. The Axiom of Choice implies countable choice The Axiom of Countable Choice (ACω)

[F1]

The standard normal law is a probability measure with density ϕ(x)=e−x2/2/2π; a probability measure is finitely additive on disjoint events. Standard normal and normal laws Probability measures and probability spaces

[F2]

The density ϕ is positive and Borel measurable, with integral one. The standard normal density has total mass one

[F3]

The CDF of a real random variable is Φ(x)=P(Z≤x). Cumulative distribution function of a real random variable

[F4]

For increasing measurable sets, measure of the union is the limit of their measures. Continuity from below for measures

[F5]

For decreasing measurable sets whose first member has finite measure, measure of the intersection is the limit of their measures. Continuity from above when one set has finite measure

[F7]

A monotone differentiable substitution with the stated local integrability hypotheses preserves a convergent improper integral, with orientation handled by the sign. Change of variable in an improper integral

[F9]

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

[F10]

The real exponential is smooth, so the displayed density ϕ is continuous. The exponential function is smooth and (exp⁡)′=exp⁡

[F11]

If A⊆B, then P(B∖A)=P(B)−P(A); in particular P(Ac)=1−P(A) for a probability measure. Basic identities for a probability measure

Proof

Given: The hypotheses in the Statement.

1.1A1F1F2F3F10F11algebra

For a<b, the density formula in [F1] and set-difference identity [F11] give Φ(b)−Φ(a)=∫(a,b]ϕ(x) dx. The density is continuous by [F10] and positive by [F2]; continuity at (a+b)/2 gives a subinterval of positive length on which ϕ has a positive lower bound, so this integral is positive. Also 0<ϕ(x)≤1/2π, hence 0<Φ(b)−Φ(a)≤(b−a)/2π. Therefore Φ is strictly increasing and continuous.

1.2A1A2F1F2F3F7F8F9F11algebra

The density in [F1] is even. For any x∈R, substitution u=−t in [F7] gives Φ(−x)=∫x∞ϕ(u) du. By [A2] and [F8], the singleton {x} is Lebesgue null; [F9] then gives P(Z=x)=∫{x}ϕ dλ=0. Since [F2] gives total mass one, [F11] identifies the last tail integral as 1−Φ(x). Hence Φ(−x)=1−Φ(x).

2.1F2F3F4F5F6step 1.1choose

The sets (−∞,n] increase to R and the sets (−∞,−n] decrease to the empty set. The normal law has total mass one by [F2], so [F4] and [F5] give Φ(n)→1 and Φ(−n)→0. Given q∈(0,1), choose n with Φ(−n)<q<Φ(n). Applying [F6] on [−n,n] gives zq with Φ(zq)=q; strict increase from step 1.1 makes this zq unique.

3.1step 2.1step 1.2algebra∎

Set x=zq in step 1.2. Then Φ(−zq)=1−q. By the uniqueness in step 2.1, −zq=z1−q. In particular, q=1/2 gives z1/2=−z1/2, hence z1/2=0.

Source notes

The quantile existence, uniqueness, and symmetry are proved locally from the published standard normal density and measure definitions; the source references document the normal-law convention and its use in detection-limit calibration.

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

Location-scale normal laws have their stated mean and variance

Statement

Assume AC. For m∈R, σ≥0, and a real random variable X with law N(m,σ2), E[X]=m,Var⁡(X)=σ2.

Facts & Assumptions

Given: AC, a standard normal random variable Z, and X with law N(m,σ2) for m∈R and σ≥0.

[A1]

AC is required by the standard normal probability-law definition and the Gaussian even-moment supplier. The Axiom of Choice Standard normal and normal laws Gaussian even moments for Brownian increments

[F1]

N(0,1) is the law with density ϕ(x)=e−x2/2/2π, and N(m,σ2) is the law of x↦m+σx under N(0,1). Standard normal and normal laws

[F2]

For a standard normal Z, E[Z2]=1. Gaussian even moments for Brownian increments

[F3]

Cauchy–Schwarz gives E∣Z∣≤(E[Z2])1/2, so the standard normal is integrable. Cauchy-Schwarz for random variables

[F4]

A nonnegative measurable function of a random element has expectation equal to its integral against the law, allowing infinity; the same identity holds for a signed function once its composite is integrable. Change of variables for expectation

[F5]

Expectation is linear, and variance is E[(X−E[X])2] for square-integrable X. Linearity, monotonicity, and the modulus bound for expectation Moments, variance, and covariance on a probability space

[F6]

A pointwise-convergent sequence dominated by one integrable function has convergent integrals. Dominated convergence

Proof

Given: The hypotheses in the Statement.

1.1A1F1F2F3F4F7algebra

By [F2], E[Z2]=1. Since Z has a probability law by [F1], E[12]=1, and Cauchy–Schwarz [F3] gives E∣Z∣≤1; hence Z is integrable. For each integer n≥1, xϕ(x) is odd because ϕ is even; [F7] with u=−x therefore gives E[Z1{∣Z∣≤n}]=∫−nnxϕ(x) dx=0 by [F4].

2.1step 1.1F3F6

As the integer n→∞, Z1{∣Z∣≤n}→Z pointwise and ∣Z1{∣Z∣≤n}∣≤∣Z∣, which is integrable by step 1.1. Dominated convergence [F6] gives E[Z]=0.

3.1step 2.1F1F2F3F4F5algebra∎

Put W=m+σZ. Since W2≤2m2+2σ2Z2, [F2] gives E[W2]<∞. The nonnegative clause of [F4] and the common law in [F1] give E[X2]=E[W2]<∞; Cauchy–Schwarz [F3] with the constant 1 then makes both X and W integrable. By [F1] and [F4], E[X]=E[m+σZ]. Linearity [F5] and step 2.1 give E[X]=m+σE[Z]=m. Applying the same change of variables to (X−m)2 gives Var⁡(X)=E[(X−m)2]=σ2E[Z2]=σ2 by [F2] and [F5]. When σ=0, the affine map is constant and the same equalities give variance zero.

Source notes

The moment calculation is supplied locally from the library's proved Gaussian even-moment result and the normal-law push-forward definition. The cited sources document the scale-as-standard-deviation convention used in the detection-limit model.

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

Exact limits in the known-blank equal-variance normal model

Statement

Assume AC, σ0>0, 0<α,β<1/2, and kQ>0. Consider the response-only experiment with concentration c∈[0,∞) and X∼N(c,σ02) under each c. Reject the blank when X>LC. For the coefficient-of-variation criterion CV⁡(c)≤kQ, the exact critical level, detection limit for false-negative target β, and quantification limit are LC=z1−ασ0,LD=(z1−α+z1−β)σ0,LQ=σ0kQ. where zq is the unique standard normal q-quantile from The standard normal CDF has unique symmetric quantiles. These formulas are conditional on the known-blank, equal-variance normal model.

Facts & Assumptions

Given: AC; σ0>0; 0<α,β<1/2; kQ>0; and the experiment X∼N(c,σ02) for each concentration c≥0.

[A1]

AC is required by the standard normal-law construction. The Axiom of Choice Standard normal and normal laws

[F1]

The response laws are location-scale images of the standard normal law: N(c,σ02) is the law of c+σ0Z. Standard normal and normal laws

[F2]

The standard normal CDF is continuous and strictly increasing, its q-quantiles satisfy Φ(zq)=q, and z1−q=−zq; in particular z1/2=0. The standard normal CDF has unique symmetric quantiles

[F3]

For a location-scale normal law, Ec[X]=c and Var⁡c(X)=σ02. Location-scale normal laws have their stated mean and variance

[F4]

For a simple null {0}, the size is E0[φ(X)] for the test function φ. Test size and power

[F5]

Every measurable φ:R→[0,1] defines a randomized test under the binary-action convention. Every measurable rejection function defines a randomized test Randomized tests

[F6]

The Borel sigma-algebra of R is generated by its open sets. The Borel sigma-algebra of a topological space

[F7]

Measurability means inverse images of measurable target sets are measurable. A measurable function between measurable spaces

[F8]

An exact critical level and the least-concentration definitions of LD and LQ are those of Critical, detection, and quantification levels.

[F9]

A statistical experiment is a measurable data space with a parameter-indexed family of probability laws. Statistical experiments

[F10]

For every measurable event A, E[1A]=P(A). The expectation of an indicator is the probability of the event

[F11]

For a probability measure, P(Ac)=1−P(A). Basic identities for a probability measure

[F12]

The CDF of a real random variable is FX(x)=P(X≤x). Cumulative distribution function of a real random variable

Proof

Given: The hypotheses in the Statement.

1.1A1F1F2F4F5F6F7F8F9F10F11algebra

Set LC=z1−ασ0 and φ(x)=1{x>LC}. For every Borel B⊆[0,1], φ−1(B) is one of ∅,R,(LC,∞),(−∞,LC]; these are Borel, so [F6] and [F7] make φ measurable. By [F5] it defines a test in the experiment [F9]. Under the blank, X=σ0Z in law by [F1], hence P0(X>LC)=1−Φ(z1−α)=α by [F2] and [F11]. By [F4], the simple-null size is E0[φ(X)]; [F10] identifies it with P0(X>LC). Thus LC is an exact critical level by [F8].

2.1A1F1F2F8F12step 1.1algebra

For any c≥0, the affine law in [F1] and CDF definition [F12] give Pc(X≤LC)=Φ((LC−c)/σ0). By strict increase and uniqueness in [F2], this equals β exactly when (LC−c)/σ0=zβ. Hence the unique solution is c=σ0(z1−α−zβ)=σ0(z1−α+z1−β), using the symmetry in [F2]. Since z1/2=0 and Φ is strictly increasing by [F2], while 1−α,1−β>1/2, both quantiles in the sum are positive. This solution is therefore the least positive concentration and is LD by [F8].

3.1A1F3F8algebra∎

For c>0, [F3] gives CV⁡(c)=Var⁡c(X)/Ec[X]=σ0/c. Since σ0,kQ>0, the inequality σ0/c≤kQ is equivalent to c≥σ0/kQ. Its least positive solution is therefore LQ=σ0/kQ by [F8].

Source notes

The exact formulas are derived from the stated normal law and the local quantile and moment lemmas. NIST SP 958 reports rounded known-blank values under α=β=0.05, constant σ0, and 10% relative standard deviation; Eurachem's normal-tail discussion uses the corresponding approximate 1.65+1.65 factor. Neither source is used in place of the local derivation.

5 · Examples, counterexamples and false statements

None yet.

Sources