TheoremStatement: Literature-sourcedProof: 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.

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

Statement

Assume AC, $σ_{0} > 0$ , $0 < α, β < 1 / 2$ , and $k_{Q} > 0$ . Consider the response-only experiment with concentration $c \in [0, \infty)$ and $X \sim N (c, σ_{0}^{2})$ under each $c$ . Reject the blank when $X > L_{C}$ . For the coefficient-of-variation criterion $CV (c) \leq k_{Q}$ , the exact critical level, detection limit for false-negative target $β$ , and quantification limit are $L_{C} = z_{1 - α} σ_{0}, L_{D} = (z_{1 - α} + z_{1 - β}) σ_{0}, L_{Q} = \frac{σ_{0}}{k_{Q}} .$ where $z_{q}$ 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$ ; $k_{Q} > 0$ ; and the experiment $X \sim N (c, σ_{0}^{2})$ for each concentration $c \geq 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, σ_{0}^{2})$ is the law of $c + σ_{0} Z$ . Standard normal and normal laws

[F2]

The standard normal CDF is continuous and strictly increasing, its $q$ -quantiles satisfy $Φ (z_{q}) = q$ , and $z_{1 - q} = - z_{q}$ ; in particular $z_{1 / 2} = 0$ . The standard normal CDF has unique symmetric quantiles

[F3]

For a location-scale normal law, $E_{c} [X] = c$ and ${Var}_{c} (X) = σ_{0}^{2}$ . Location-scale normal laws have their stated mean and variance

[F4]

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

[F5]

Every measurable $φ : R \to [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 $L_{D}$ and $L_{Q}$ 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 [1_{A}] = P (A)$ . The expectation of an indicator is the probability of the event

[F11]

For a probability measure, $P (A^{c}) = 1 - P (A)$ . Basic identities for a probability measure

[F12]

The CDF of a real random variable is $F_{X} (x) = P (X \leq x)$ . Cumulative distribution function of a real random variable

Proof

Given: The hypotheses in the Statement.

1.1A1F1F2F4F5F6F7F8F9F10F11algebra

Set $L_{C} = z_{1 - α} σ_{0}$ and $φ (x) = 1_{{x > L_{C}}}$ . For every Borel $B \subseteq [0, 1]$ , $φ^{- 1} (B)$ is one of $\emptyset, R, (L_{C}, \infty), (- \infty, L_{C}]$ ; these are Borel, so [F6] and [F7] make $φ$ measurable. By [F5] it defines a test in the experiment [F9]. Under the blank, $X = σ_{0} Z$ in law by [F1], hence $P_{0} (X > L_{C}) = 1 - Φ (z_{1 - α}) = α$ by [F2] and [F11]. By [F4], the simple-null size is $E_{0} [φ (X)]$ ; [F10] identifies it with $P_{0} (X > L_{C})$ . Thus $L_{C}$ is an exact critical level by [F8].

2.1A1F1F2F8F12step 1.1algebra

For any $c \geq 0$ , the affine law in [F1] and CDF definition [F12] give $P_{c} (X \leq L_{C}) = Φ ((L_{C} - c) / σ_{0})$ . By strict increase and uniqueness in [F2], this equals $β$ exactly when $(L_{C} - c) / σ_{0} = z_{β}$ . Hence the unique solution is $c = σ_{0} (z_{1 - α} - z_{β}) = σ_{0} (z_{1 - α} + z_{1 - β})$ , using the symmetry in [F2]. Since $z_{1 / 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 $L_{D}$ by [F8].

3.1A1F3F8algebra∎

For $c > 0$ , [F3] gives $CV (c) = \sqrt{{Var}_{c} (X)} / E_{c} [X] = σ_{0} / c$ . Since $σ_{0}, k_{Q} > 0$ , the inequality $σ_{0} / c \leq k_{Q}$ is equivalent to $c \geq σ_{0} / k_{Q}$ . Its least positive solution is therefore $L_{Q} = σ_{0} / k_{Q}$ 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.

Depends on

Used by

Dependency tree · two levels

61 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

A Century of Excellence in Measurements, Standards, and Technology: A Chronicle of Selected NBS/NIST Publications 1901–2000, NIST SP 958, pp. 177–179 (printed pp. 164–166) (standard reference, not scraped)
H. Cantwell (ed.), Eurachem Guide: The Fitness for Purpose of Analytical Methods, 3rd ed. (2025), §5.3.1 and Annex B (standard reference, not scraped)