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.

The Dirichlet box: exact spectrum, nodes, constant shift and gaps

Physical scope

Finite checks in the declared Dirichlet interval model of the pair: the free box eigenpairs, their explicit nodal points, the exact spectrum under a constant potential shift, the attainment of the min-max bound and the eigenvalue gaps. The example is an exact conditional computation in the declared confined model; it asserts no material wall, no measured spectrum and no empirical result.

Example

Work in the declared Dirichlet interval model The declared interval models with Dirichlet and Robin boundary conditions, and the declared zero-range (delta) model clause (b) with $0 < L < \infty$ , mass $m > 0$ , action constant $ℏ > 0$ , and energies in joules under Dimensions, SI unit conventions and quantity types of the framework. Then, as exact identities in the model:

(i) Free box. For $V = 0$ the eigenpairs of the assigned energy operator $H_{D, 0}$ are exactly $(E_{n}, e_{n}), E_{n} = \frac{ℏ^{2} π^{2} n^{2}}{2 m L^{2}}, e_{n} (x) = \sqrt{\frac{2}{L}} \sin ⁣ (\frac{n π x}{L}), n \geq 1,$ the family $(e_{n})_{n \geq 1}$ is a complete orthonormal family of $L^{2} (0, L; C)$ , each eigenvalue is simple, and $e_{n}$ has exactly $n - 1$ zeros in $(0, L)$ , namely the points $x_{k} = k L / n$ , $k = 1, \dots, n - 1$ .

(ii) Constant shift. If $V = c$ is the constant potential of value $c \in R$ (joules), then $H_{D, c}$ has exactly the same eigenfunctions $e_{n}$ and the eigenvalues $E_{n} + c$ ; consequently the min-max comparison bound of the interval theorem is attained with equality, $∣ E_{n} + c - E_{n} ∣ = ∣ c ∣ = ∥ V ∥_{\infty}$ for every $n$ .

(iii) Gaps. $E_{n + 1} - E_{n} = \frac{ℏ^{2} π^{2} (2 n + 1)}{2 m L^{2}} > 0$ , so the spectrum is strictly increasing.

The example is an exact conditional computation in the declared box model and asserts no measured transition energy.

Verification

Proof technique: direct; read the free-box clause of the interval theorem, evaluate the sine zeros explicitly, and shift the operator by a constant multiple of the identity to verify the exact spectrum under a constant potential.

Given: The declared Dirichlet interval model with $0 < L < \infty$ and $m, ℏ > 0$ ; the interval spectrum theorem Interval models: discrete spectra, complete eigenbases, min-max bounds and nodal counts; a real constant potential value $c$ .

[F1] Dirichlet box conclusions. For every $V \in C ([0, L]; R)$ the assigned operator $H_{D, V} = (ℏ^{2} / 2 m) (A_{D} + M_{\tilde{V}})$ with $\tilde{V} = (2 m / ℏ^{2}) V$ is an assigned sharp observable, self-adjoint with compact resolvent and a complete orthonormal eigenfamily, with strictly increasing simple eigenvalues $E_{n}$ and the nodal count: the eigenvector belonging to $E_{n}$ has exactly $n - 1$ zeros in $(0, L)$ ; the min-max comparison $∣ E_{n} - ℏ^{2} π^{2} n^{2} / (2 m L^{2}) ∣ \leq ∥ V ∥_{\infty}$ holds; and for $V = 0$ a complete orthonormal family of eigenpairs is $(ℏ^{2} π^{2} n^{2} / (2 m L^{2}), e_{n})$ with the displayed $e_{n}$ , a complete orthonormal family (Interval models: discrete spectra, complete eigenbases, min-max bounds and nodal counts clause (a)).

[F2] Sine zeros. For $n \geq 1$ and $x \in (0, L)$ , $\sin (n π x / L) = 0$ if and only if $n π x / L = k π$ for an integer $k$ , i.e. $x = k L / n$ ; among these only $k = 1, \dots, n - 1$ lie in $(0, L)$ (The zero sets of sine and cosine and the least positive common period 2 pi).

1.1givenF1algebra

[Free eigenpairs and completeness] For $V = 0$ the hypotheses of [F1] hold with $V = 0$ , and its free-box clause gives the complete orthonormal family of eigenpairs $(E_{n}, e_{n})$ with $E_{n} = ℏ^{2} π^{2} n^{2} / (2 m L^{2})$ and $e_{n} (x) = \sqrt{2 / L} \sin (n π x / L)$ , together with completeness of $(e_{n})$ and simplicity of the eigenvalues.

2.1step 1.1F1F2algebra

[Nodal points] By [F2] the zeros of $e_{n}$ in $(0, L)$ are exactly $x_{k} = k L / n$ , $k = 1, \dots, n - 1$ , so their number is $n - 1$ , in agreement with the nodal count of [F1].

2.2step 1.1F1algebra

[Constant shift] Let $c \in R$ and $V = c$ ; then $\tilde{V} = 2 m c / ℏ^{2}$ is constant and $H_{D, c} = (ℏ^{2} / 2 m) (A_{D} + M_{\tilde{V}}) = (ℏ^{2} / 2 m) A_{D} + c I$ on $D (A_{D})$ , because multiplication by the constant $\tilde{V}$ is the scalar $\tilde{V}$ times the identity and $(ℏ^{2} / 2 m) (2 m c / ℏ^{2}) = c$ . Applying this identity to an eigenvector $e_{n}$ of $A_{D}$ with eigenvalue $λ_{n} = (n π / L)^{2}$ gives $H_{D, c} e_{n} = (ℏ^{2} / 2 m) λ_{n} e_{n} + c e_{n} = (E_{n} + c) e_{n}$ ; by [F1] the eigenfamily $(e_{n})$ is complete and the eigenvalues simple, so the spectrum of $H_{D, c}$ is exactly ${E_{n} + c : n \geq 1}$ .

3.1step 2.2F1algebra

[Attainment of the min-max bound] For this constant potential the bound of [F1] reads $∣ E_{n} + c - E_{n} ∣ = ∣ c ∣$ , and $∥ V ∥_{\infty} = ∣ c ∣$ ; hence the inequality is an equality for every $n$ .

4.1step 3.1F1algebra∎

[Gaps and reading] Since $(n + 1)^{2} - n^{2} = 2 n + 1$ , the successive eigenvalue difference is $E_{n + 1} - E_{n} = ℏ^{2} π^{2} (2 n + 1) / (2 m L^{2}) > 0$ , consistent with strictness and simplicity in [F1]; every displayed number is an exact function of the declared data $m, ℏ, L$ and the declared shift $c$ , and no measured spectrum is asserted.

Remarks

Attainment is not generic. The equality in (ii) is a property of the constant potential, for which the perturbation commutes with the free box operator. For a nonconstant $V$ the min-max bound is an inequality and its attainment is not claimed.
What is not asserted. The example treats the free and constantly shifted Dirichlet box only. It does not treat Robin conditions, singular perturbations or a material wall, and it reports no data.

The Dirichlet box: exact spectrum, nodes, constant shift and gaps

Example

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources