ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck pass

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.

Chain versus string on the normalized standing wave: exact discrete error, the N=100 bounds, and physical circumference 2π m

Physical scope

A worked comparison in SI-normalized numerical variables of the cyclic mass-spring chain and continuum string on the standing wave sin(x)cos(t), using a physical circumference of 2π m, linear density 1 kg m^{-1}, tension 1 N, and speed 1 m s^{-1}. It computes the exact chain solution and frequency, nodal error, the theorem's nodal and full interpolation bounds at N=100 (both O(a^{3/2}) for fixed positive time, with interpolation remainder Aa^2/8), the sharper O(a^2) nodal and interpolation errors for these standing-wave data, and the dispersion-relation error a^2/12. The normalized results are model calculations, not measurements.

Example

Take the periodic string model of The continuum string model as the proved limit of the mass-spring chain, with explicit convergence and dispersion error with physical circumference $L_{*} = 2 π m$ , linear mass density $ρ_{ℓ, *} = 1 k g m^{- 1}$ and tension $τ_{s, *} = 1 N = 1 k g m s^{- 2}$ . Then $c_{*} : = \sqrt{τ_{s, *} / ρ_{ℓ, *}} = 1 m s^{- 1}$ . Use reference units $ℓ_{*} = 1 m$ , $τ_{*} = 1 s$ and displacement scale $A_{*} = 1 m$ . In the equations below, $x, t, L, c$ denote numerical values in these units, so $L = 2 π$ , $c = 1$ , and the dimensionless displacement $u = u_{p h y s} / A_{*}$ has the exact travelling-standing solution with physical wave number $1 m^{- 1}$ and angular frequency $1 s^{- 1}$

$u (t, x) : = A \sin x \cos t (A > 0),$

where $A$ is dimensionless. Physical displacements and their error bounds are obtained by multiplying the displayed values by $A_{*}$ . The normalized density and tension values are $ρ_{ℓ} = ρ_{ℓ, *} / (1 k g m^{- 1}) = 1$ and $τ_{s} = τ_{s, *} / (1 N) = 1$ ; these are numerical values of different dimensioned quantities. The normalized field is $2 π$ -periodic and solves $u_{t t} = u_{x x}$ . For $N \geq 2$ put $a = 2 π / N$ and consider the cyclic spring chain of The cyclic spring chain, its discrete energy, and the finite-regularity periodic comparison class with parameter $c = 1$ and spacing $a$ , i.e. the normalized node mass is $m = ρ_{ℓ} a$ in units of $1 k g$ and the normalized spring constant is $k_{s} = τ_{s} / a$ in units of $1 N m^{- 1}$ . Then:

$M = \sup ∣ \partial_{x}^{4} u ∣ = A$ , $M_{2} = \sup ∣ \partial_{x}^{2} u ∣ = A$ and the theorem's constant is $C = \sqrt{2 π} A / 12 \approx 0.20889 A$ ;
the exact chain solution with the sampled data is $q_{j} (t) = A \sin (j a) \cos (ω_{a} t)$ with $ω_{a} = 2 \sin (a / 2) / a$ (positive for $0 < a < π$ ), the exact nodal error is $e_{j} (t) = A \sin (j a) [\cos (ω_{a} t) - \cos t]$ , and the theorem's bounds read $∥ e (t) ∥_{a} \leq C a^{2} t^{2} / 2$ , $\max_{j} ∣ e_{j} (t) ∣ \leq \frac{1}{2} C a^{3 / 2} t^{2}$ and $\sup_{x} ∣ I_{a} q - u ∣ \leq \max_{j} ∣ e_{j} ∣ + A a^{2} / 8$ ;
at $N = 100$ (so $a = 2 π / 100 \approx 0.062832$ ) and $t = 1$ the evaluated bounds are $∥ e (1) ∥_{a} \leq 0.0004124 A$ , $\max_{j} ∣ e_{j} (1) ∣ \leq 0.001645 A$ and $\sup ∣ I_{a} q - u ∣ \leq 0.002139 A$ , while the exact error satisfies $∣ e_{j} (1) ∣ \leq A ∣ ω_{a} - 1 ∣ \approx 0.00016449 A$ , so the theoretical bound is verified and visibly conservative;
the exact dispersion relation is $ω_{a}^{2} = (4 / a^{2}) \sin^{2} (a / 2)$ , and the theorem's bound $∣ ω_{a}^{2} - 1 ∣ \leq a^{2} / 12$ gives $\leq 0.00032899$ at $N = 100$ , while the exact value satisfies $∣ ω_{a}^{2} - 1 ∣ \approx 0.00032894$ .

Facts & Assumptions

Given: the physical parameters $L_{*} = 2 π m$ , $ρ_{ℓ, *} = 1 k g m^{- 1}$ , $τ_{s, *} = 1 N$ , the reference units and normalized values $L = 2 π$ , $c = 1$ , $ρ_{ℓ} = 1$ , $τ_{s} = 1$ ; the dimensionless amplitude $A > 0$ ; the standing wave $u$ ; and the integer $N \geq 2$ and normalized spacing $a = 2 π / N$ .

[F1]

Chain and norms (The cyclic spring chain, its discrete energy, and the finite-regularity periodic comparison class): the cyclic chain equation is $q_{j}^{''} = (c^{2} / a^{2}) (q_{j + 1} - 2 q_{j} + q_{j - 1})$ with discrete norm $∥ \cdot ∥_{a}$ , and the sampled data are $q_{j} (0) = u (0, j a)$ , $q_{j}^{'} (0) = u_{t} (0, j a)$ .

[F2]

Continuum-limit theorem (Finite-time continuum limit of the cyclic spring chain: uniform $O (a^{3 / 2})$ nodal and uniform interpolation convergence): under the stated smoothness and periodicity hypotheses on $u$ and its wave equation, the chain solution exists and is unique on $[0, T]$ , and with $e_{j} = q_{j} - u (t, j a)$ and $C = c^{2} \sqrt{L} M / 12$ one has $∥ e (t) ∥_{a} \leq C a^{2} t^{2} / 2$ , $∥ e^{'} (t) ∥_{a} \leq C a^{2} t$ , $\max_{j} ∣ e_{j} (t) ∣ \leq \frac{1}{2} C a^{3 / 2} t^{2}$ and $\sup_{x} ∣ I_{a} q (t, x) - u (t, x) ∣ \leq \max_{j} ∣ e_{j} (t) ∣ + M_{2} a^{2} / 8$ .

[F3]

Dispersion theorem (Exact dispersion relation $ω^{2} = (4 c^{2} / a^{2}) \sin^{2} (κ a / 2)$ for the cyclic chain and its continuum error bound): for $A \neq 0$ and $κ N a \in 2 π Z$ , $q_{j} (t) = A \cos (κ j a - ω t)$ solves the chain equation if and only if $ω^{2} = (4 c^{2} / a^{2}) \sin^{2} (κ a / 2)$ ; when this dispersion relation holds and $∣ κ a ∣ \leq 1$ , $∣ ω^{2} - c^{2} κ^{2} ∣ \leq c^{2} κ^{4} a^{2} / 12$ .

[F4]

Trigonometry and calculus (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive, The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, 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)$ , The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine, The derivatives of sine and cosine are cosine and minus sine, Sine and cosine defined by their real power series): the difference formula for the cosine, $∣ \cos x - \cos y ∣ \leq ∣ x - y ∣$ for real $x, y$ (mean value theorem bound for the derivative $- \sin$ , $∣ \sin ∣ \leq 1$ ), and $\sin^{2} z \leq z^{2}$ . For the sine and cosine used here, their derivatives are continuous on every compact interval, hence Riemann integrable; the second part of the fundamental theorem evaluates their derivative integrals. The addition formulas give the centered second differences in step 1.2.

[F5]

Model scales (The continuum string model as the proved limit of the mass-spring chain, with explicit convergence and dispersion error, Continuum body data, the fixed inertial frame and the dimensions of the fields): with $c = 1$ and $L = 2 π$ the theorem's constant for this data is $C = c^{2} \sqrt{L} M / 12 = \sqrt{2 π} A / 12$ .

Verification

technique · direct; verify the standing wave and the exact discrete solution, evaluate the theorem's bounds at $N=100$, and compare with the exact error and dispersion values

1.1givenF4F5algebra

Data: $\partial_{x}^{4} u = A \sin x \cos t$ and $\partial_{x}^{2} u = - A \sin x \cos t$ , so $M = M_{2} = A$ ; by [F5], $C = \sqrt{2 π} A / 12$ .

1.2givenF1F3F4algebra

Exact chain solution: with $q_{j} (t) = A \sin (j a) \cos (ω_{a} t)$ one has $q_{j}^{''} = - ω_{a}^{2} q_{j}$ and $q_{j + 1} - 2 q_{j} + q_{j - 1} = - 4 \sin^{2} (a / 2) q_{j}$ , so the chain equation $q_{j}^{''} = a^{- 2} (q_{j + 1} - 2 q_{j} + q_{j - 1})$ holds for the chosen frequency $ω_{a}^{2} = 4 \sin^{2} (a / 2) / a^{2}$ , i.e. $ω_{a} = 2 \sin (a / 2) / a$ for $a \in (0, π]$ , since $N \geq 2$ ; at $N = 2$ the sampled values $\sin (j π)$ vanish and the zero chain solves independently of frequency. The sampled data match because $q_{j} (0) = A \sin (j a) = u (0, j a)$ and $q_{j}^{'} (0) = 0 = u_{t} (0, j a)$ .

2.1step 1.2F4algebra

Exact nodal error: $e_{j} (t) = q_{j} (t) - u (t, j a) = A \sin (j a) [\cos (ω_{a} t) - \cos t]$ , hence by [F4] $∣ e_{j} (t) ∣ \leq A ∣ ω_{a} - 1 ∣ t$ for $t \geq 0$ .

2.2step 1.1F2algebra

Bounds at $N = 100$ : with $a = 2 π / 100$ one has $a^{2} = 4 π^{2} / 10^{4}$ and $a^{3 / 2} = (2 π / 100)^{3 / 2}$ . Hence at $t = 1$ the three right-hand sides of [F2] are $C a^{2} / 2 = \sqrt{2 π} π^{2} A / 60000$ , $\frac{1}{2} C a^{3 / 2} = π^{2} A / 6000$ and $π^{2} A / 6000 + π^{2} A / 20000 = 13 π^{2} A / 60000$ , using $M_{2} a^{2} / 8 = A a^{2} / 8 = π^{2} A / 20000$ .

3.1step 2.1step 2.2algebra

Exact comparison: with $a = π / 50$ one has $ω_{a} = 2 \sin (a / 2) / a = 100 \sin (π / 100) / π$ , so by step 2.1 the exact nodal error at $t = 1$ obeys $∣ e_{j} (1) ∣ \leq A ∣ 100 \sin (π / 100) / π - 1 ∣$ , while the theorem's nodal bound at $t = 1$ is $π^{2} A / 6000$ by step 2.2; the comparison of the two explicit numerical factors is a finite check recorded in the Remarks.

4.1step 1.2F3F4algebra∎

Dispersion for all $N \geq 2$ : put $z = a / 2 > 0$ . By [F4] and the fundamental theorem, $\sin z - z = \int_{0}^{z} (\cos s - 1) d s$ and $\cos s - 1 = - \int_{0}^{s} \sin r d r$ ; hence $∣ \sin z - z ∣ \leq \int_{0}^{z} \int_{0}^{s} r d r d s = z^{3} / 6$ , using $∣ \sin r ∣ \leq r$ , while $∣ \sin z + z ∣ \leq 2 z$ . Therefore $∣ ω_{a}^{2} - 1 ∣ = 4 ∣ \sin^{2} z - z^{2} ∣ / a^{2} \leq 4 (z^{3} / 6) (2 z) / a^{2} = a^{2} / 12$ . At $N = 100$ this equals $π^{2} / 30000$ ; here $a < 1$ also permits the bound of [F3] with $c = κ = 1$ and the chosen solving-mode frequency. Moreover $ω_{a}^{2} = \sin^{2} (a / 2) / (a / 2)^{2} = 1 - a^{2} / 12 + O (a^{4})$ by the power series of sine, so the exact error equals the bound to leading order in $a$ .

Remarks

The comparison is a finite, exact check: the chain's standing mode has frequency $ω_{a}$ and the continuum mode frequency $1$ ; the nodal error is the interference of the two cosines, so the discrepancy is a purely discrete-dispersion effect and decays like $a^{2}$ for the exact standing-wave data, while the theorem's uniform-in-data bound grows like $a^{3 / 2}$ through the worst-case nodal factor $a^{- 1 / 2}$ of the discrete norm comparison.
Numerical readings at $N = 100$ for the bounds of step 2.2: $\sqrt{2 π} π^{2} / 60000 \approx 0.0004124$ , $π^{2} / 6000 \approx 0.001645$ and $13 π^{2} / 60000 \approx 0.002139$ , while the frequency-difference upper bound of step 3.1 is $∣ 100 \sin (π / 100) / π - 1 ∣ \approx 0.0001645$ , while the exact maximum nodal error factor is $∣ \cos (100 \sin (π / 100) / π) - \cos 1 ∣ \approx 0.0001384$ (nodes $j = 25, 75$ have $∣ \sin (j a) ∣ = 1$ ) and the dispersion bound of step 4.1 is $π^{2} / 30000 \approx 0.000329$ ; the exact dispersion error $∣ ω_{a}^{2} - 1 ∣ = 1 - \sin^{2} (π / 100) / (π / 100)^{2}$ agrees to leading order. The theorem's bounds are therefore satisfied and conservative on these data.
The evaluated numbers are properties of the model's bounds under the stated scaling $m = ρ_{ℓ} a$ , $k_{s} = τ_{s} / a$ ; they are not measured errors of any physical chain, and no measured stiffness or density is used.

Chain versus string on the normalized standing wave: exact discrete error, the N=100 bounds, and physical circumference 2π m

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources