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.

Em Experiment Analysis Prerequisites — Examples

1 · Prerequisites

2 · Summary

Explicit mathematical boundary cases for the bounded-error comparison of the companion page. A linear prediction with slope $m > 0$ attains the confined bound $δ / m$ at both endpoints of the compatible interval, so the constant in the conclusion cannot be improved for that instance; and the identically zero prediction shows that the positive lower bound on the response is not removable, since with the same indicator value and the same two bounds every real parameter value remains compatible. Both constructions are mathematical observations about a hypothetical bounded-error model; no experimental data, sampling law or statistical inference is asserted.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Sharpness of the bounded-error uncertainty bound for a linear prediction, and failure once the response lower bound is dropped

Example

Identify $R$ with $R^{1}$ by $t \mapsto (t)$ , the function on ${0}$ with value $t$ . This bijection preserves distances because $∥ (t) - (r) ∥_{2} = ∣ t - r ∣$ ; the symbols $u = 1$ and $\nabla F = m$ below use this identification.

(i) Specialise Uncertainty analysis: bounded-error data confine the parameter of a $C^{1}$ prediction along a declared unit direction in $R^{n}$ to $n = 1$ , $U = R$ , $θ_{0} = 0$ , $u = 1$ , $I = R$ and $F (θ) = m θ$ with $m > 0$ . Then $F$ is $C^{1}$ , $F (0) = 0$ , $\nabla F (θ) = m$ and $⟨ \nabla F (θ), 1 ⟩ = m \geq m$ , so the theorem's hypothesis holds with equality. Fix the recorded value $\hat{y} = 0$ (so $s = 0$ ) and any $δ \geq 0$ . A candidate $θ \in R$ is compatible with the calibration bound exactly when $∣ F (θ) - \hat{y} ∣ = ∣ m θ ∣ \leq δ$ , that is, exactly when $∣ θ ∣ \leq δ / m$ ; this is precisely the theorem's bound $(s + δ) / m = δ / m$ , and the bound is attained (equality) at $θ = \pm δ / m$ . Hence the constant $(s + δ) / m$ cannot be improved for this instance, and the special case $δ = 0$ leaves $θ = 0$ as the only compatible candidate. (ii) The positive lower bound on the response is not removable. If it is dropped, take $m = 0$ and $F \equiv 0$ on $R$ : the hypothesis $⟨ \nabla F (θ), u ⟩ \geq m > 0$ fails, and with the same data $\hat{y} = 0$ , $s = 0$ , $δ \geq 0$ every $θ \in R$ is compatible, because $y = 0$ and $∣ y - \hat{y} ∣ = 0 \leq δ$ ; no finite parameter bound then follows from the indicator and the two bounds alone. (iii) These are mathematical observations about a hypothetical bounded-error model: no experimental data, sampling law or statistical inference is used or asserted, and the displayed numbers are stipulated parameters, not measurements.

Facts & Assumptions

Given: a real $m > 0$ ; a real $δ \geq 0$ ; the linear function $F (θ) = m θ$ on $R$ ; the recorded value $\hat{y} = 0$ with $s = 0$ ; and the alternative function $F \equiv 0$ on $R$ read with $m = 0$ .

[F1]

The uncertainty theorem: for open $U \subseteq R^{n}$ , unit $u$ , an open interval $I ∋ 0$ with $γ (θ) = θ_{0} + θ u \in U$ , a $C^{1}$ function $F$ with $F (θ_{0}) = 0$ and $D_{u} F (θ_{0} + θ u) = ⟨ \nabla F (θ_{0} + θ u), u ⟩ \geq m > 0$ on $I$ , and recorded $\hat{y}$ , $s \geq 0$ , $δ \geq 0$ with $∣ \hat{y} ∣ \leq s$ and $∣ F (θ_{0} + θ u) - \hat{y} ∣ \leq δ$ at a candidate $θ \in I$ , one has $∣ θ ∣ \leq (s + δ) / m$ , and then $∥ θ u ∥_{2} = ∣ θ ∣$ (Uncertainty analysis: bounded-error data confine the parameter of a $C^{1}$ prediction along a declared unit direction in $R^{n}$ ).

[F2]

$R = (- \infty, \infty)$ is the open interval of Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length containing $0$ , and $R$ is an open subset of itself (Open subset of $R$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen).

[F3]

Every point of a nondegenerate interval is a limit point of it, and a limit point of $A$ is a point every punctured neighbourhood of which meets $A$ (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[F4]

The identity $p_{1} (x) = x$ is differentiable at every real with $p_{1}^{'} (c) = 1$ , and the constant $p_{0} \equiv 1$ is differentiable at every real with derivative $0$ (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term).

[F5]

At a limit point $c$ of a common domain $A \subseteq R$ , sums and scalar multiples of functions differentiable at $c$ are differentiable at $c$ with $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ and $(α f)^{'} (c) = α f^{'} (c)$ (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[F6]

For $f$ on a subset of $R$ , the derivative at a limit point $c$ is the limit of the difference quotient (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set), and the directional derivative in the direction $e_{0} = 1$ is the limit of $t \mapsto (f (c + t) - f (c)) / t$ , the two limits coinciding under the substitution $x = c + t$ (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ); in $R^{1}$ the only standard basis vector is $e_{0} = 1$ (The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ ).

[F7]

The gradient of a scalar function is the vector of its partial derivatives, $\nabla f (a) = (\partial_{0} f (a), \dots)$ (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[F8]

The Euclidean inner product on $R^{n}$ is $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ with norm $∥ x ∥_{2} = \sqrt{⟨ x, x ⟩}$ , and a nonnegative real has a unique nonnegative square root, so $∥ (1) ∥_{2} = \sqrt{1} = 1$ in $R^{1}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[F9]

Absolute value: $∣ x ∣ \geq 0$ , $∣ x ∣ = 0$ if and only if $x = 0$ , and $∣ x y ∣ = ∣ x ∣ ∣ y ∣$ (Basic properties of the absolute value), with the case definition $∣ x ∣ = x$ for $x \geq 0$ and $∣ x ∣ = - x$ for $x < 0$ (Absolute value in an ordered field).

[F10]

A scalar function on an open set is of class $C^{1}$ when the function and all its first coordinate partial derivatives exist and are continuous there ( $C^{k}$ Euclidean maps and diffeomorphisms, $C^{k}$ maps and multi-index derivative notation in Euclidean space). Continuity at $c$ means that for every $ε > 0$ there is $r > 0$ such that $∣ x - c ∣ < r$ implies $∣ f (x) - f (c) ∣ < ε$ (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

Verification

technique · direct

1.1F2F3F4F5F10F6F7F8

For $F (θ) = m θ$ the theorem's hypotheses are met at $n = 1$ , $U = R$ , $θ_{0} = 0$ , $u = 1$ , $I = R$ with lower bound $m$ : $R$ is an open interval containing $0$ and is open in itself [F2], the identity on $R$ is differentiable everywhere with derivative $1$ [F4], so the scalar multiple $F = m p_{1}$ is differentiable everywhere with $F^{'} (θ) = m \cdot 1 = m$ at every real, a limit point of the domain [F3, F5]; for $ε > 0$ , taking $r = ε / m > 0$ gives $∣ F (x) - F (c) ∣ = m ∣ x - c ∣ < ε$ whenever $∣ x - c ∣ < r$ , so $F$ is continuous; the derivative function is the constant $m$ , whose differences are zero, hence it too is continuous, so $F$ is of class $C^{1}$ [F10]; $F (0) = 0$ ; the only partial derivative is $\partial_{0} F (θ) = D_{1} F (θ) = F^{'} (θ) = m$ [F6], so $\nabla F (θ) = (m)$ [F7] and $⟨ \nabla F (θ), 1 ⟩ = m \cdot 1 = m \geq m$ [F8]; and $∥ u ∥_{2} = ∥ (1) ∥_{2} = 1$ [F8].

1.2F1F9algebra

With the recorded $\hat{y} = 0$ , $s = 0$ and $y = F (θ) = m θ$ the two bounds read $0 \leq 0$ and $∣ m θ ∣ \leq δ$ ; since $∣ m θ ∣ = m ∣ θ ∣$ and $m > 0$ , the inequality $∣ m θ ∣ \leq δ$ is equivalent to $∣ θ ∣ \leq δ / m$ [F9]. By the theorem [F1] every compatible $θ$ satisfies $∣ θ ∣ \leq (s + δ) / m = δ / m$ , so the compatible set is exactly the set of $θ$ with $∣ θ ∣ \leq δ / m$ ; at $θ = \pm δ / m$ one has $∣ m θ ∣ = m (δ / m) = δ$ , so these candidates are compatible and the bound is attained, and no smaller constant can replace $δ / m$ for this instance; if $δ = 0$ then $∣ m θ ∣ = 0$ forces $θ = 0$ , the only compatible candidate [F9].

1.3F4F5F6F7F9algebra

For $F \equiv 0$ and $m = 0$ the function is the scalar multiple $0 \cdot p_{1}$ , differentiable everywhere with derivative $0$ [F4, F5], so $\partial_{0} F (θ) = 0$ and $\nabla F (θ) = (0)$ [F6, F7], whence $⟨ \nabla F (θ), 1 ⟩ = 0$ ; this is not $\geq m$ for any $m > 0$ , so the theorem's hypothesis fails and the theorem supplies no bound. Nevertheless $y = F (θ) = 0 = \hat{y}$ for every real $θ$ , so $∣ y - \hat{y} ∣ = 0 \leq δ$ and $∣ \hat{y} ∣ = 0 \leq s$ hold for every $θ \in R$ : with the same indicator and the same two bounds every real $θ$ is compatible, and no finite bound $∣ θ ∣ \leq C$ follows from those data alone [F9].

2.1given∎

Every quantity above is a stipulated real parameter or a value of the explicitly displayed functions $θ \mapsto m θ$ and $θ \mapsto 0$ ; no experimental data, sampling law, likelihood or statistical inference is used or asserted, and the displayed numbers are parameters of the construction, not measurements.

Remarks

What is and is not claimed. The example proves sharpness of the conditional inequality of Uncertainty analysis: bounded-error data confine the parameter of a $C^{1}$ prediction along a declared unit direction in $R^{n}$ for one explicitly displayed family, and it exhibits a family in which the conclusion fails once the positive lower bound on the response is dropped. It asserts nothing about any experiment, detector, calibration procedure or historical report, and the "data" mentioned in the statement are the stipulated bounds $∣ \hat{y} ∣ \leq s$ and $∣ y - \hat{y} ∣ \leq δ$ alone.
The equal case at $δ = 0$ . At $\hat{y} = 0$ and $δ = 0$ the calibration bound is $∣ m θ ∣ \leq 0$ , so the singleton ${θ = 0}$ is the compatible set; the general bound $(s + δ) / m$ degenerates to $0$ , which is consistent rather than exceptional.

Sources

J. Lebl, Basic Analysis I: Introduction to Real Analysis, Volume I (open textbook), section 4.1.1 (Example 4.1.3 and Proposition 4.1.7: affine derivatives and linearity) and section 4.2.4 (monotonicity from the sign of the derivative), printed pp. 154-168, version 6.3 (May 15, 2026); used only as the published companion of the cited derivative items, not as the source of the computed sharpness example