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.

Finite square well: an exactly solvable bound state and exact bound-state counts

Physical scope

Finite checks in the declared line model of the pair for the finite square well: an exactly solvable depth at which the unique bound state has energy minus one half of the depth, and exact bound-state counts and branch parities for declared depths. The example is a conditional computation in the model; it reports no measurement, no material well and no empirical value, and asserts no conclusion about nature.

Example

Work in the declared line model The declared one-dimensional line model: state space, Hamiltonian, bound states and generalized stationary solutions with mass parameter $m > 0$ and action constant $ℏ > 0$ , energies, lengths and the depth $U$ read in the units of Dimensions, SI unit conventions and quantity types of the framework, and consider the finite square well $V (x) = - U$ for $∣ x ∣ \leq a$ , $V (x) = 0$ for $∣ x ∣ > a$ of Finite square well: bound-state conditions, simplicity and count with half-width $a > 0$ and depth $U > 0$ .

(i) Exact boundary case of the first branch. Declare $U : = \frac{ℏ^{2} π^{2}}{16 m a^{2}} .$ Then $K = \sqrt{2 m U} / ℏ = π \sqrt{2} / (4 a)$ , the count parameter is $2 a K / π = \sqrt{2} / 2$ , there is exactly one bound state, it is an even (cosine-type) state, and its binding energy is exactly $E = - \frac{U}{2} = - \frac{ℏ^{2} π^{2}}{32 m a^{2}} .$ For this declared depth the root of the even condition is exactly $k = κ = π / (4 a)$ .

(ii) Exact counts at declared depths. With $U : = \frac{25 ℏ^{2} π^{2}}{32 m a^{2}}$ one has $K = 5 π / (4 a)$ and $2 a K / π = 5 / 2$ , so there are exactly three bound states, with types even, odd and even in order of increasing energy. With $U : = ℏ^{2} π^{2} / (8 m a^{2})$ one has $K = π / (2 a)$ and exactly one bound state; with $U : = ℏ^{2} π^{2} / (2 m a^{2})$ one has $K = π / a$ and exactly two bound states. For every declared depth $U > 0$ there is at least one bound state.

(iii) Rational bracket of the first case. $\frac{707}{1000} < \frac{2 a K}{π} = \frac{\sqrt{2}}{2} < \frac{708}{1000},$ so the count $⌈ 2 a K / π ⌉$ equals one in case (i).

The example is a conditional computation in the declared well model and asserts no measured binding energy; the identities in (i) and (ii) are exact in the model at the displayed declared data.

Verification

Proof technique: direct; verify the exact root condition at the declared depth using the special value $\tan (π / 4) = 1$ , read the count and branch criterion from the finite-well theorem with exact rational comparisons, and bracket the count parameter by rationals.

Given: The line model and the finite-well theorem Finite square well: bound-state conditions, simplicity and count; half-width $a > 0$ , mass $m > 0$ , action $ℏ > 0$ ; the depths declared in (i) and (ii).

[F1] Finite-well conclusions. For every $a, U > 0$ the assigned well operator is self-adjoint, its negative eigenvalues are exactly the numbers $E \in (- U, 0)$ whose parameters $κ = \sqrt{2 m (- E)} / ℏ$ , $k = \sqrt{2 m (U + E)} / ℏ$ satisfy $k \tan (k a) = κ$ or $- k \cot (k a) = κ$ , each such eigenvalue is simple with the stated parity of the eigenfunction, there are no eigenvalues outside $(- U, 0)$ , the count is $⌈ 2 a K / π ⌉$ with $K = \sqrt{2 m U} / ℏ$ , the solutions lie one in each branch $(n π / 2 a, (n + 1) π / 2 a)$ whose left endpoint satisfies $n π / 2 a < K$ and nowhere else, and the types alternate with the parity of $n$ (Finite square well: bound-state conditions, simplicity and count clauses (a)-(c)).

[F2] Special value of the tangent. $\tan (π / 4) = 1$ : by Cofunction, supplementary, quarter-turn, and reflection identities for the six trigonometric functions, $\cos (π / 4) = \cos (π / 2 - π / 4) = \sin (π / 4)$ ; by Pi is the first positive zero of sine, $\sin (π / 4) > 0$ ; applying the half-angle identity of Half-angle identities with the sign determined by the quadrant at $x = π / 2$ , where $\sin (π / 2) = 1$ and $\cos (π / 2) = 0$ by Quarter-turn values and shifts by pi/2 and pi, gives $\sin (π / 4) = \sqrt{(1 - 0) / 2} = \sqrt{2} / 2 = \cos (π / 4)$ ; hence $\tan (π / 4) = \sin (π / 4) / \cos (π / 4) = 1$ by Tangent, cotangent, secant, and cosecant on their exact natural domains and the positivity of $\cos (π / 4)$ .

[F3] Rational order. For positive integers, $\frac{p}{q} < \frac{r}{s}$ iff $p s < r q$ , and $0 < \frac{1}{2} < 1$ ; if $0 < x$ and $x^{2} < 1$ then $x < 1$ .

1.1givenF1F2algebra

[First case: data and root] With $U = ℏ^{2} π^{2} / (16 m a^{2})$ one has $K = \sqrt{2 m U} / ℏ = π \sqrt{2} / (4 a)$ , hence $K^{2} = π^{2} / (8 a^{2})$ . Put $k = κ = π / (4 a)$ ; then $k^{2} + κ^{2} = 2 \cdot π^{2} / (16 a^{2}) = π^{2} / (8 a^{2}) = K^{2}$ , and $k \tan (k a) = κ \tan (π / 4) = κ$ by [F2], so the even condition of [F1] holds with $E = - ℏ^{2} κ^{2} / (2 m) = - ℏ^{2} π^{2} / (32 m a^{2}) = - U / 2$ . By [F1] this $E$ is a simple eigenvalue with an even eigenfunction.

1.2F1F3algebra

[Second case: three states] With $U = 25 ℏ^{2} π^{2} / (32 m a^{2})$ one has $K = \sqrt{2 m U} / ℏ = 5 π / (4 a)$ , so $2 a K / π = 5 / 2$ and $⌈ 5 / 2 ⌉ = 3$ . The admissible branches are those with left endpoint $n π / (2 a) < 5 π / (4 a)$ , i.e. $\frac{n}{2} < \frac{5}{4}$ ; by [F3] this holds exactly for $n = 0, 1, 2$ (for $n = 2$ , $1 < 5 / 4$ ; for $n = 3$ , $3 / 2 > 5 / 4$ ), so by [F1] there are exactly three negative eigenvalues, one in each of the branches $n = 0, 1, 2$ , with types even, odd, even.

2.1step 1.1F1F3algebra

[First case: count] The count parameter is $2 a K / π = 2 a π \sqrt{2} / (4 a) / π = \sqrt{2} / 2$ . Since $(\sqrt{2} / 2)^{2} = 1 / 2 < 1$ and $\sqrt{2} / 2 > 0$ , [F3] gives $\sqrt{2} / 2 < 1$ ; and $\sqrt{2} / 2 > 0$ . Hence $⌈ 2 a K / π ⌉ = 1$ by [F1]; the branch with $n = 0$ has left endpoint $0 < K$ , while the branch with $n = 1$ has left endpoint $π / (2 a)$ and $π / (2 a) > K = π \sqrt{2} / (4 a)$ because $\frac{1}{2} > \frac{\sqrt{2}}{4} = \frac{1}{2 \sqrt{2}}$ , equivalently $\sqrt{2} > 1$ , which holds since ${\sqrt{2}}^{2} = 2 > 1$ and $\sqrt{2} > 0$ . So the unique branch is $n = 0$ , the even branch, consistent with step 1.1.

2.2step 1.2F1F3algebra

[Thresholds and the ground state] For $K = π / (2 a)$ the count parameter is $2 a K / π = 1$ and the branch $n = 0$ is admissible while $n = 1$ has left endpoint $π / (2 a) = K$ , not strictly smaller, so exactly one bound state; for $K = π / a$ the count parameter is $2$ and the admissible branches are $n = 0, 1$ (left endpoints $0 < π / a$ and $π / (2 a) < π / a$ ), so exactly two. Since $⌈ x ⌉ \geq 1$ for every $x > 0$ and the branch $n = 0$ is always admissible, every well with $a, U > 0$ has at least one bound state.

3.1step 2.1step 1.2F1F3algebra∎

[Bracket and reading] The bracket $\frac{707}{1000} < \frac{\sqrt{2}}{2} < \frac{708}{1000}$ follows from [F3] because $(\frac{707}{1000})^{2} = \frac{499849}{1000000} < \frac{1}{2} < \frac{501264}{1000000} = (\frac{708}{1000})^{2}$ ; hence $\frac{707}{1000} < 2 a K / π < \frac{708}{1000}$ in case (i) and the count is one. No measured quantity is produced: the identities above are exact relations between the declared model data and the model's binding energies.

Remarks

Why the first case is exactly solvable. At the declared depth $K = π \sqrt{2} / (4 a)$ the radius circle of the even root condition passes through the point $k = κ = π / (4 a)$ of the first branch, where $\tan (k a) = 1$ , so the transcendental root condition is satisfied by an exact rational multiple of $1 / a$ and the signed binding energy is exactly $E = - U / 2$ (its positive magnitude is $U / 2$ ).
What the counts show and what they do not. The comparisons verify the branch criterion and the ceiling formula at declared depths. They are not a numerical solution of the transcendental equations at generic depths, do not compare with data and assert nothing about any physical well.

Finite square well: an exactly solvable bound state and exact bound-state counts

Example

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources