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

1 · Prerequisites

2 · Summary

The deterministic layer beneath the electromagnetic empirical-testing page: a bounded-error comparison that confines the parameter of a monotone $C^{1}$ prediction to an explicit interval when the recorded indicator and the calibration error are separately bounded. The companion lemma on the preceding prerequisite page treats a real interval and a one-variable prediction; this page transports it to an open Euclidean domain along a declared unit direction, showing how the one-variable statement is applied to the restriction of a $C^{1}$ prediction to a line, with the directional derivative bounded below by a declared positive constant $m$ .

Nothing here is a sampling law or a statistical inference: the bounds $s$ , $δ$ and $m$ are parameters of the statement, and the conclusion $∣ θ ∣ \leq (s + δ) / m$ is a conditional inequality whose empirical reading belongs to the consuming physical item. The companion examples page records the sharpness of this bound for an explicitly displayed linear prediction and the failure of the conclusion once the positive lower bound is dropped.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Uncertainty analysis: bounded-error data confine the parameter of a $C^{1}$ prediction along a declared unit direction in $R^{n}$

Statement

Let $n \geq 1$ , let $U \subseteq R^{n}$ be open, let $θ_{0} \in U$ , and let $u \in R^{n}$ satisfy $∥ u ∥_{2} = 1$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). Let $I \subseteq R$ be an open interval with $0 \in I$ and such that $γ (θ) : = θ_{0} + θ u \in U$ for every $θ \in I$ . Let $F : U \to R$ be of class $C^{1}$ ( $C^{k}$ Euclidean maps and diffeomorphisms) with $F (θ_{0}) = 0$ , and suppose that for every $θ \in I$ the directional derivative of $F$ along $u$ satisfies

$D_{u} F (θ_{0} + θ u) = ⟨ \nabla F (θ_{0} + θ u), u ⟩ \geq m > 0$

(Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ , The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, For a differentiable scalar field, $D_{v} f (a) = ⟨ \nabla f (a), v ⟩$ and the unit direction of steepest ascent is the normalized gradient). Let a recorded scalar $\hat{y} \in R$ satisfy $∣ \hat{y} ∣ \leq s$ with $s \geq 0$ , and let a calibration-error bound $∣ y - \hat{y} ∣ \leq δ$ with $δ \geq 0$ hold for $y : = F (θ_{0} + θ u)$ at a candidate $θ \in I$ . Then

$∣ θ ∣ \leq \frac{s + δ}{m},$

and the corresponding configuration displacement $γ (θ) - θ_{0} = θ u$ has Euclidean length $∥ θ u ∥_{2} = ∣ θ ∣$ . The conclusion is a deterministic conditional statement about the stated bounds; it is not a sampling law, a statistical inference, or a claim about any historical report, and the parameters $s, δ, m$ are supplied by the user of the statement rather than estimated from data here.

Facts & Assumptions

Given: a natural $n \geq 1$ ; an open set $U \subseteq R^{n}$ ; a point $θ_{0} \in U$ ; a vector $u \in R^{n}$ with $∥ u ∥_{2} = 1$ ; an open interval $I \subseteq R$ with $0 \in I$ and $γ (θ) : = θ_{0} + θ u \in U$ for every $θ \in I$ ; a function $F : U \to R$ of class $C^{1}$ with $F (θ_{0}) = 0$ and $D_{u} F (θ_{0} + θ u) = ⟨ \nabla F (θ_{0} + θ u), u ⟩ \geq m > 0$ for every $θ \in I$ ; a recorded scalar $\hat{y} \in R$ with $∣ \hat{y} ∣ \leq s$ , $s \geq 0$ ; a calibration bound $∣ y - \hat{y} ∣ \leq δ$ , $δ \geq 0$ , for $y = F (θ_{0} + θ u)$ at a candidate $θ \in I$ .

[F1]

The intervals that are open in the sense of Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length are the four forms $(a, b)$ , $(a, \infty)$ , $(- \infty, b)$ and $(- \infty, \infty) = R$ , and a set $A \subseteq R$ is open when every $x \in A$ has a real $ε > 0$ with $N_{ε} (x) \subseteq A$ , where $N_{ε} (x)$ is the neighbourhood of Open subset of $R$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen.

[F2]

The punctured neighbourhood $N_{ε}^{*} (x) = {y : 0 < ∣ y - x ∣ < ε}$ is never empty: the element $x + ε / 2$ satisfies $∣ (x + ε / 2) - x ∣ = ε / 2$ , which is $> 0$ and $< ε$ (The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ).

[F3]

Every point of a nondegenerate interval is a limit point of it (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).

[F4]

A limit point of $A \subseteq R$ is a point $p$ with $N_{η}^{*} (p) \cap A \neq \emptyset$ for every real $η > 0$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[F5]

The derivative of $h : A \to R$ at a limit point $c$ of $A$ is $h^{'} (c) = \lim_{x \to c} (h (x) - h (c)) / (x - c)$ , the limit of the difference quotient, and $h$ is differentiable at $c$ when that limit exists (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).

[F6]

If $B \subseteq A$ , if $c \in B$ is a limit point of $B$ and if $h : A \to R$ is differentiable at $c$ , then the restriction $h ∣_{B} : B \to R$ is differentiable at $c$ with $(h ∣_{B})^{'} (c) = h^{'} (c)$ (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).

[F7]

For a natural number $n \geq 1$ the function $p_{n} (x) = x^{n}$ is differentiable at every real, with derivative $n c^{n - 1}$ at $c$ when the natural number $n$ is read as a real number, and the constant function $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).

[F8]

If $f, g : A \to R$ are differentiable at a limit point $c$ of $A$ and $α \in R$ , then $f + g$ and $α f$ 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$ , claims 1 and 2).

[F9]

For $U^{'} \subseteq R^{m}$ , $a \in U^{'}$ , $v \in R^{m}$ and $f : U^{'} \to R^{n}$ , if the line map $t \mapsto f (a + t v)$ is defined near $0$ , its derivative at $0$ is the directional derivative $D_{v} f (a) = \lim_{t \to 0} (f (a + t v) - f (a)) / t$ , and for a standard basis vector $e_{j}$ one writes $\partial_{j} f (a) = D_{e_{j}} f (a)$ (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ). For one-dimensional domains and codomains we identify $R$ with $R^{1}$ by the bijection $t \mapsto (t)$ , the function on ${0}$ with value $t$ ; it is isometric because $∥ (t) - (r) ∥_{2} = \sqrt{(t - r)^{2}} = ∣ t - r ∣$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). Under this identification 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$ ).

[F10]

For $h : A \to R$ with $A \subseteq R$ and $c$ a limit point of $A$ , the statement $\lim_{x \to c} h (x) = L$ means: for every real $ε > 0$ there is a real $δ > 0$ such that every $x \in A$ with $0 < ∣ x - c ∣ < δ$ satisfies $∣ h (x) - L ∣ < ε$ (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

[F11]

For $A \subseteq R$ , $c$ a limit point of $A$ , $f : A \to R^{m}$ and $L \in R^{m}$ , one has $\lim_{x \to c} f (x) = L$ if and only if $\lim_{x \to c} f_{i} (x) = L_{i}$ for every $i < m$ (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, clause 2).

[F12]

A vector-valued $f : A \to R^{m}$ on $A \subseteq R$ is continuous at $a \in A$ when for every real $ε > 0$ there is a real $δ > 0$ such that every $x \in A$ with $∣ x - a ∣ < δ$ satisfies $∥ f (x) - f (a) ∥_{2} < ε$ (Vector-valued functions $f : A \to R^{m}$ , their limits and continuity, with the dictionary to the metric notions).

[F13]

A map $f : U^{'} \to R^{n}$ on an open $U^{'} \subseteq R^{m}$ is totally differentiable at $a \in U^{'}$ when there is a linear map $L : R^{m} \to R^{n}$ with $∥ f (a + h) - f (a) - L h ∥_{2} / ∥ h ∥_{2} \to 0$ as $h \to 0$ , and then $L$ is written $D f (a)$ (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder).

[F14]

If every partial derivative $\partial_{j} f$ of $f : U^{'} \to R^{n}$ exists on a neighbourhood of $a \in U^{'}$ and is continuous at $a$ , then $f$ is totally differentiable at $a$ and $D f (a)$ is the linear map with matrix $J f (a)$ (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

[F15]

If $f : U^{'} \to R^{n}$ is totally differentiable at $a$ , then $D_{v} f (a)$ exists for every $v$ and equals $D f (a) v$ ; in particular $\partial_{j} f (a) = D f (a) e_{j}$ (A total derivative computes every directional derivative, and its matrix is the Jacobian).

[F16]

A map is of class $C^{1}$ when each component is; for a scalar function on an open set this means that the function and each of its first coordinate partial derivatives exist and are continuous on the domain ( $C^{k}$ Euclidean maps and diffeomorphisms, $C^{k}$ maps and multi-index derivative notation in Euclidean space).

[F17]

If a scalar-valued $f$ is totally differentiable at $a$ , then $D_{v} f (a) = ⟨ \nabla f (a), v ⟩$ for every $v$ (For a differentiable scalar field, $D_{v} f (a) = ⟨ \nabla f (a), v ⟩$ and the unit direction of steepest ascent is the normalized gradient).

[F18]

For scalar $f$ whose partial derivatives exist at $a$ , the gradient is $\nabla f (a) = (\partial_{0} f (a), \dots, \partial_{m - 1} f (a)) \in R^{m}$ (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[F19]

The Euclidean inner product is $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ with norm $∥ x ∥_{2} = \sqrt{⟨ x, x ⟩}$ ; for $n \geq 1$ one has $∥ x - y ∥_{2} = d_{2} (x, y)$ ; and two elements of $R^{n}$ are equal exactly when they agree at every $k < n$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F20]

If $f$ is totally differentiable at $a$ and $g$ is totally differentiable at $f (a)$ , then $g \circ f$ is totally differentiable at $a$ with $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F21]

Real continuity (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), metric continuity (Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form), the choice-free equivalence of continuity with openness of preimages (Metric continuity characterisations, with countable choice for the sequential converse, conditions (a) and (b)), the agreement of the real and metric notions on subsets of $R$ (Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace), and continuity of sums and scalar multiples at a point of a common domain $A \subseteq R$ (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, claim 1).

[F22]

For every norm $N$ on a real vector space and all $λ$ in $R$ one has $N (λ v) = ∣ λ ∣ N (v)$ (axiom (N2) of A norm on a real vector space, the induced metric, and the dictionary with the metric axioms), and $∥ \cdot ∥_{2}$ is a norm on $R^{n}$ for every natural number $n$ , inducing the metric $d_{2}$ whenever $n \geq 1$ (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation, clause 2).

[F23]

Images and preimages of sets under a function are those of the induced relation, and $f^{- 1} [V]$ denotes the preimage of $V$ under $f$ (Injection, surjection, bijection).

[F24]

The bounded-error model comparison: for an interval $I$ with at least two elements, $θ_{0} \in I$ and $f : I \to R$ of class $C^{1}$ with $f (θ_{0}) = 0$ and $f^{'} \geq m > 0$ on $I$ , every candidate $θ \in I$ for which a recorded scalar $\hat{y}$ satisfies $∣ \hat{y} ∣ \leq s$ , $s \geq 0$ , and $y = f (θ)$ satisfies $∣ y - \hat{y} ∣ \leq δ$ , $δ \geq 0$ , obeys $∣ θ - θ_{0} ∣ \leq (s + δ) / m$ (Bounded-error model comparison: a derivative lower bound confines compatible parameters).

Proof

technique · direct

1.1givenF1F2F3F4

The interval $I$ is one of the four open forms of [F1], hence an open subset of $R$ ; fix a real $ε > 0$ with $N_{ε} (0) \subseteq I$ . By [F2] the punctured neighbourhood $N_{ε}^{*} (0)$ is a nonempty subset of $N_{ε} (0) \subseteq I$ , so $I$ contains $0$ and at least one further point and is therefore nondegenerate; by [F3] every point of $I$ is a limit point of $I$ , that is, by [F4], $N_{η}^{*} (θ) \cap I \neq \emptyset$ for every $θ \in I$ and every real $η > 0$ .

1.2givenF16F14F17

The function $F$ is totally differentiable at $p : = γ (θ) = θ_{0} + θ u$ , and $D_{u} F (p) = ⟨ \nabla F (p), u ⟩$ : as $F$ is of class $C^{1}$ , each first partial derivative $\partial_{j} F$ exists and is continuous on the open set $U$ by [F16], so [F14] gives total differentiability of $F$ at $p \in U$ , and [F17] gives $D_{u} F (p) = ⟨ \nabla F (p), u ⟩$ .

1.3givenF19F22F21

The path $γ : I \to U$ is continuous at every $θ^{'} \in I$ : given a real $ε > 0$ take $δ : = ε$ ; for $θ^{''} \in I$ with $∣ θ^{''} - θ^{'} ∣ < δ$ one has $d_{2} (γ (θ^{''}), γ (θ^{'})) = ∥ γ (θ^{''}) - γ (θ^{'}) ∥_{2} = ∥ (θ^{''} - θ^{'}) u ∥_{2} = ∣ θ^{''} - θ^{'} ∣ ∥ u ∥_{2} = ∣ θ^{''} - θ^{'} ∣ < ε$ , by [F19], the homogeneity axiom (N2) of [F22] and $∥ u ∥_{2} = 1$ ; this is continuity in the metric sense of [F21].

1.4F19F22given

The configuration displacement has Euclidean length $∥ γ (θ) - θ_{0} ∥_{2} = ∥ θ u ∥_{2} = ∣ θ ∣ ∥ u ∥_{2} = ∣ θ ∣$ , by the Euclidean norm of [F19], the homogeneity axiom (N2) of [F22] and $∥ u ∥_{2} = 1$ .

2.1step 1.1F7F6F8algebra

For every $θ \in I$ the components of the path satisfy $γ_{j} (θ + t) = γ_{j} (θ) + t u_{j}$ for every real $t$ with $θ + t \in I$ , since $γ_{j} (θ + t) = (θ_{0})_{j} + (θ + t) u_{j} = (θ_{0})_{j} + θ u_{j} + t u_{j} = γ_{j} (θ) + t u_{j}$ by field arithmetic; on $I$ the functions $1_{I} : = p_{0} ∣_{I}$ , constantly $1$ , and ${i d}_{I} : = p_{1} ∣_{I}$ , the identity, are differentiable at $θ$ with derivatives $0$ and $1$ , because the power functions $p_{0}$ and $p_{1}$ have those derivatives at every real by [F7] and $θ$ is a limit point of $I$ by step 1.1, so [F6] restricts; since $γ_{j} = (θ_{0})_{j} \cdot 1_{I} + u_{j} \cdot {i d}_{I}$ on $I$ , the sum and scalar rules of [F8] give that $γ_{j}$ is differentiable at $θ$ with $γ_{j}^{'} (θ) = (θ_{0})_{j} \cdot 0 + u_{j} \cdot 1 = u_{j}$ .

2.2step 1.3F16F23F21

Each composite $\partial_{j} F \circ γ : I \to R$ is continuous: for open $V \subseteq R$ the preimage $(\partial_{j} F \circ γ)^{- 1} [V]$ is, by [F23], the preimage $γ^{- 1} [\partial_{j} F^{- 1} [V]]$ ; the set $\partial_{j} F^{- 1} [V]$ is open in the domain $U$ of the continuous $\partial_{j} F$ by the choice-free equivalence (a) $\Leftrightarrow$ (b) of [F21], and its preimage under the continuous $γ$ is therefore open in $I$ ; the same equivalence then gives continuity of $\partial_{j} F \circ γ$ on $I$ .

3.1step 2.1F9F5F10algebra

For every $θ \in I$ the partial derivative of $γ_{j}$ in the direction $e_{0} = 1$ equals its ordinary derivative, so $\partial_{0} γ_{j} (θ) = u_{j}$ : by [F9] the directional derivative $D_{e_{0}} γ_{j} (θ)$ is the limit at $0$ of $t \mapsto (γ_{j} (θ + t) - γ_{j} (θ)) / t$ , while by [F5] the derivative $γ_{j}^{'} (θ) = u_{j}$ of step 2.1 is the limit at $θ$ of $x \mapsto (γ_{j} (x) - γ_{j} (θ)) / (x - θ)$ ; the substitution $x = θ + t$ carries one punctured domain bijectively onto the other and the two $ε$ - $δ$ conditions of [F10] are the same condition, so $D_{e_{0}} γ_{j} (θ) = γ_{j}^{'} (θ) = u_{j}$ .

4.1step 2.1step 3.1F9F11F19

For every $θ \in I$ the partial derivative of the path is the vector $\partial_{0} γ (θ) = u$ : the quotient $q_{θ} (t) : = (γ (θ + t) - γ (θ)) / t$ on its domain ${t : t \neq 0, θ + t \in I}$ is identically $u$ by the component identity in step 2.1, so its limit exists and defines $\partial_{0} γ (θ)$ by [F9], the $j$ -th component of $q_{θ}$ is $t \mapsto (γ_{j} (θ + t) - γ_{j} (θ)) / t$ with limit $\partial_{0} γ_{j} (θ)$ , and step 3.1 gives $\partial_{0} γ_{j} (θ) = u_{j}$ ; by the componentwise limit criterion [F11] the $j$ -th coordinate of $\partial_{0} γ (θ)$ equals $u_{j}$ for every $j < n$ , and two vectors in $R^{n}$ with equal coordinates are equal by [F19], so $\partial_{0} γ (θ) = u$ .

5.1step 4.1F12

The only partial derivative of $γ$ is the constant $\partial_{0} γ \equiv u$ on $I$ by step 4.1 applied at every $θ \in I$ , and it is continuous at $θ$ : given a real $ε > 0$ , every $δ > 0$ serves for the continuity condition of [F12], because $∥ \partial_{0} γ (θ^{'}) - \partial_{0} γ (θ) ∥_{2} = ∥ u - u ∥_{2} = 0 < ε$ for every $θ^{'} \in I$ .

6.1step 4.1step 5.1F13F14F15

The path $γ$ is totally differentiable at $θ$ with $D γ (θ) (1) = u$ : the partial derivative $\partial_{0} γ$ exists on the neighbourhood $I$ of $θ$ in the open domain $I \subseteq R$ and is continuous at $θ$ by step 5.1, so $D γ (θ)$ exists by [F14]; moreover $D γ (θ) (1) = D γ (θ) (e_{0}) = \partial_{0} γ (θ) = u$ by [F15] and step 4.1.

7.1step 1.2step 3.1step 6.1F20F15F9F5

The composite $g : = F \circ γ : I \to R$ is totally differentiable at every $θ \in I$ with $D g (θ) = D F (γ (θ)) \circ D γ (θ)$ by the chain rule [F20], applied to the totally differentiable $γ$ of step 6.1 and $F$ of step 1.2; consequently $g^{'} (θ) = D g (θ) (1) = D F (γ (θ)) (D γ (θ) (1)) = D F (γ (θ)) (u) = D_{u} F (γ (θ)) = ⟨ \nabla F (γ (θ)), u ⟩ \geq m$ for every $θ \in I$ , where the first equality identifies the ordinary derivative with the total derivative applied to $1$ (the limits of [F9] and [F5] coincide as in step 3.1) and the remaining equalities are step 6.1, [F15] and step 1.2.

8.1step 2.2step 7.1F18F19F21F24

The derivative $g^{'}$ is continuous on $I$ : on $I$ one has $g^{'} (θ) = \sum_{j < n} u_{j} (\partial_{j} F \circ γ) (θ)$ by step 7.1, the gradient definition [F18] and the inner product of [F19]; the composites are continuous by step 2.2, the dictionary of [F21] transfers this to the real reading, and finite sums and scalar multiples of functions continuous at each point of $I$ are continuous there by the algebra clause of [F21]; in particular $g^{'}$ is continuous on $I$ in the sense required by [F24].

9.1step 1.1step 7.1step 8.1given

The value of $g$ at the centre is $g (0) = F (θ_{0} + 0 \cdot u) = F (θ_{0}) = 0$ , and $I$ has at least two elements with $0 \in I$ by step 1.1; the function $g : I \to R$ is differentiable at every point of $I$ with continuous derivative by steps 7.1 and 8.1, and $g^{'} \geq m > 0$ on $I$ by step 7.1.

10.1step 1.4step 9.1F24given∎

The bounded-error model comparison [F24] now applies to $g$ on $I$ with centre $θ_{0} : = 0$ and the recorded scalar $\hat{y}$ , $s$ , $δ$ of the statement, because a model value $y = g (θ) = F (θ_{0} + θ u)$ at the candidate $θ \in I$ is exactly the quantity the calibration bound constrains; its conclusion is $∣ θ - 0 ∣ \leq (s + δ) / m$ , that is $∣ θ ∣ \leq (s + δ) / m$ , and the equivalent contrapositive form says that a proposed $θ$ violating this bound is incompatible with the two stated bounds; with the displacement identity of step 1.4 the statement is proved.

Remarks

What the statement does not assert. The bounds $s, δ, m$ are parameters of the statement, not estimates: no sampling distribution, likelihood, confidence level or measurement precision is introduced or claimed, and the conclusion is the deterministic conditional inequality alone. The consumer on the empirical-testing page must supply and qualify $s$ , $δ$ and $m$ from an explicit detector and calibration model before any physical reading.
Where the hypotheses are used. The unit length of $u$ gives the exact distance identity in the continuity estimate of step 1.3 and the displacement identity of step 1.4; the lower bound $D_{u} F \geq m$ enters through the bounded-error lemma and is exactly the hypothesis the companion example shows cannot be dropped; the openness of $I$ and $0 \in I$ make every point of $I$ a limit point of $I$ and $I$ nondegenerate, which is what lets the one-variable and total-differential machinery apply on $I$ .
No choice principle is used. The proof invokes only the choice-free parts of Metric continuity characterisations, with countable choice for the sequential converse, namely the equivalence of continuity with openness of preimages, and nothing is selected from a family of nonempty sets. The single application of the bounded-error lemma inherits no choice assumption.

5 · Examples, experiments and counterexamples

None yet.