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.

Born amplitude of a declared uniform ball potential with an explicit weak-coupling condition

Physical scope

The declared short-range scattering model with a uniform real ball potential of strength V_0 and radius R in the pair's stationary beam reading: the explicit Born amplitude as a function of the momentum transfer, its forward value, and an explicit Hilbert-Schmidt condition on V_0, R and m that makes the controlled Born error estimate of the pair applicable. Conditional on the declared model and cited mathematics; no measured cross section and no claim that the Born reading applies outside the stated explicit condition.

Example

Setup. Adopt the declared short-range scattering model The declared short-range scattering model: state space, potential classes, assigned energy observables, asymptotic vocabulary and units with mass $m > 0$ , spin zero, action constant $ℏ > 0$ and the uniform ball potential $V (x) : = {\begin{cases} V_{0}, & ∣ x ∣ < R, \\ 0, & ∣ x ∣ \geq R, \end{cases} V_{0} \in R, R > 0,$ read in joules and metres; adopt the stationary beam model at wave number $k > 0$ and direction $d$ , and let $W = (2 m / ℏ^{2}) V$ , $q = ∥ K_{k} ∥$ , $f_{k}$ and the Born amplitude $f_{B}$ be as in The controlled Born reading: operator-norm condition, uniform amplitude error and coupling scaling. Write $θ$ for the scattering angle, $\cos θ = Ω \cdot d$ , and $q_{t r} : = k (d - Ω)$ for the wave-vector transfer and $q_{t r} : = ∣ q_{t r} ∣ = 2 k \sin (θ / 2)$ for its magnitude.

Verification

Given: the declared model data, the Born theorem of the pair, and the polar-coordinates formula for Lebesgue measure.

1.1givenalgebra

By the Born theorem, $f_{B} (Ω) = - \frac{1}{4 π} \int_{B_{R}} e^{i q_{t r} \cdot y} W (y) d y$ with $W = V_{0} 2 m / ℏ^{2}$ constant on $B_{R}$ ; in polar coordinates the ball integral is $\int_{B_{R}} e^{i q \cdot y} d y = 2 π \int_{0}^{R} \int_{- 1}^{1} e^{i q r s} r^{2} d s d r = 4 π (\sin (q R) - q R \cos (q R)) / q^{3}$ for $q = q_{t r} > 0$ , and equals $4 π R^{3} / 3$ at $q = 0$ by continuity.

1.2givenalgebra

The kernel $G_{k} (x - y) W (y)$ on $B_{R} \times B_{R}$ has squared Hilbert-Schmidt norm $\int_{B_{R}} \int_{B_{R}} ∣ G_{k} (x - y) W (y) ∣^{2} d x d y = \frac{∣ V_{0} ∣^{2} (2 m / ℏ^{2})^{2}}{16 π^{2}} \int_{B_{R}} \int_{B_{R}} ∣ x - y ∣^{- 2} d x d y$ ; for each $y$ the inner integral over $x \in B_{R}$ is at most the integral over the ball of radius $2 R$ around $y$ , which is $8 π R$ . Hence $∥ K_{k} ∥ \leq ∥ K_{k} ∥_{H S} \leq \frac{2 m ∣ V_{0} ∣}{ℏ^{2}} R^{2} \sqrt{2 / 3} = : q_{H S}$ .

2.1step 1.1algebra

Therefore $f_{B} (Ω) = - \frac{2 m V_{0}}{ℏ^{2}} \cdot \frac{\sin (q_{t r} R) - q_{t r} R \cos (q_{t r} R)}{q_{t r}^{3}}$ for $q_{t r} > 0$ , with the forward value $f_{B} (θ = 0) = - \frac{2 m V_{0}}{ℏ^{2}} \frac{R^{3}}{3}$ ; the amplitude has the dimension of length, since $2 m V_{0} / ℏ^{2}$ is in $m^{- 2}$ and the bracket in $m^{3}$ .

2.2step 1.2givenalgebra

Consequently, if $\frac{2 m ∣ V_{0} ∣}{ℏ^{2}} R^{2} \sqrt{2 / 3} < 1$ , then $q = ∥ K_{k} ∥ \leq q_{H S} < 1$ and the controlled Born estimate of the theorem applies; since $t \mapsto t / (1 - t)$ is increasing on $[0, 1)$ and $∥ e_{i n c} ∥_{L^{2} (B_{R})} = ∣ B_{R} ∣^{1 / 2}$ , the uniform error bound is at most $∣ f_{k} (Ω) - f_{B} (Ω) ∣ \leq \frac{∥ W ∥_{\infty} ∣ B_{R} ∣}{4 π} \frac{q_{H S}}{1 - q_{H S}} = \frac{2 m ∣ V_{0} ∣}{ℏ^{2}} \frac{R^{3}}{3} \frac{q_{H S}}{1 - q_{H S}}$ in metres; this is an explicit condition on the declared strength, radius, mass and action constant, verified here without any numerical value of the constants.

3.1step 2.1step 2.2givenalgebra∎

Under the same condition the beam model reads $d σ / d Ω (0) = ∣ f_{k} (0) ∣^{2}$ , and the theorem controls the difference from $∣ f_{B} (0) ∣^{2}$ through the bound of 2.2; the pair asserts the display $∣ f_{B} (0) ∣^{2} = (\frac{2 m V_{0}}{ℏ^{2}})^{2} \frac{R^{6}}{9}$ as the Born forward reading, read in $m^{2} s r^{- 1}$ , and no measured value.

Remarks

Scope. The Born amplitude is a conditional model quantity; the explicit condition of 2.2 is sufficient for the controlled error bound of the pair and is not claimed to be necessary.
No weak-potential language. The pair avoids "for a weak potential"; the condition is the operator-norm condition $q < 1$ , verified here through the displayed Hilbert-Schmidt bound.

Born amplitude of a declared uniform ball potential with an explicit weak-coupling condition

Example

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources