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.

A finite-level static Stark model: vanishing first-order shift, exact splitting with leading quadratic shift and a finite check of the remainder bound

Physical scope

A conditional finite-level computation in the declared two-body Coulomb model with the adopted static finite-level dipole coupling: the compressed two-state Stark family built from the model's 1s-like and 2p-like relative states, the vanishing diagonal dipole matrix elements by the angular selection rule, the exact closed-form eigenvalues of the two-state family, the vanishing first-order shift and the exact second derivative at zero from the page's non-degenerate theorem, and a finite numeric check of the cubic remainder bound. The example identifies no laboratory atom, asserts no measured Stark shift or polarizability value, and states no transition or lifetime; the uncompressed linear-potential model is explicitly outside its scope.

Example

Adopt P1, P2 and P4 for the declared two-body Coulomb model of The declared Coulomb and two-body hydrogen model: one-centre operator, relative problem, reduced mass and scope exclusions clause (d), in the relative-coordinate factor $L^{2} (R^{3}; C)$ with the dipole operator $D_{j} = - q Q_{j}$ and the compressed finite-level coupling of Static finite-level electric-dipole coupling: compressed dipole of the declared two-body Coulomb model in a uniform field. Use the Coulomb mass parameter $m = μ : = m_{1} m_{2} / (m_{1} + m_{2})$ and $a_{μ} : = ℏ^{2} / (μ κ) > 0$ . Choose as the finite-level subspace the declared two-dimensional subspace $W : = span {ψ_{1}, ψ_{2}} \subseteq L^{2} (R^{3}; C),$ where $ψ_{1}$ and $ψ_{2}$ are normalized bound states of the model with angular labels $(n, l, m) = (1, 0, 0)$ and $(2, 1, 0)$ supplied by The one-centre Coulomb model: bound energies, n^2-degeneracy, completeness of the bound states in the negative spectral subspace and the continuum, so that $H_{κ} ψ_{1} = E_{1} ψ_{1}$ , $H_{κ} ψ_{2} = E_{2} ψ_{2}$ with $E_{1} = - \frac{m κ^{2}}{2 ℏ^{2}}, E_{2} = - \frac{m κ^{2}}{8 ℏ^{2}}, Δ : = E_{2} - E_{1} = \frac{3 m κ^{2}}{8 ℏ^{2}} > 0.$ Choose the external field along the third axis of the declared frame, $E_{e x t} = (0, 0, E)$ with $E > 0$ in $V m^{- 1}$ , and use the dimensionless coupling $λ : = \frac{E}{1 V m^{- 1}}, V : = - (1 V m^{- 1}) D_{3}^{W},$ so that the Stark model of the postulate reads $H_{S} (E) = H_{0} + λ V, H_{0} : = Π_{W} H_{κ} ∣_{W} = (\begin{array}{cc} E_{1} & 0 \\ 0 & E_{2} \end{array})$ in the declared orthonormal basis. Then:

(a) the compression of the dipole matrix has the form $D_{1}^{W} = D_{2}^{W} = 0, D_{3}^{W} = D_{r e l} (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array}), D_{r e l} : = ∣ ⟨ ψ_{2}, D_{3} ψ_{1} ⟩ ∣ > 0,$ with unit $C m$ , where the phase of $ψ_{2}$ is chosen to make the off-diagonal entry positive. The local computation below gives $D_{r e l} = 128 \sqrt{2} q a_{μ} / 243 > 0$ from the declared model parameters; this is an exact model identity, with no measured value of any parameter. The diagonal entries vanish by angular degree selection, and only $Q_{0}$ can contribute between the chosen $m = 0$ states; nonvanishing is proved by explicit radial and angular integration;

(b) $v = ∥ V ∥ = D_{r e l} (1 V m^{- 1})$ in joules and the family $H_{S}$ has the exact eigenvalues $F_{\pm} (E) = \frac{E_{1} + E_{2}}{2} \pm \sqrt{(\frac{Δ}{2})^{2} + (D_{r e l} E)^{2}},$ the lower branch $F_{-}$ being the model's followed label for dimensionless couplings $0 \leq λ < R : = Δ / (8 v)$ , equivalently $0 \leq E < Δ / (8 D_{r e l})$ , with $Δ$ playing the role of the gap $g$ ;

(c) the page's perturbation theorem applies with nondegenerate label $E_{1}$ (gap $Δ$ ), and gives the vanishing first-order shift $E^{'} (0) = 0$ and the exact second derivative at zero $E^{''} (0) = - \frac{2 D_{r e l}^{2} (1 V m^{- 1})^{2}}{Δ},$ equivalently the quadratic Stark shift $F_{-} (E) = E_{1} - \frac{D_{r e l}^{2} E^{2}}{Δ} + O (E^{4});$

(d) the finite remainder check at half the perturbation radius $λ = R / 2$ , equivalently $E = Δ / (16 D_{r e l})$ , gives the exact remainder $∣ F_{-} + \frac{Δ}{256} - E_{1} ∣ = Δ \frac{129 - 16 \sqrt{65}}{256} = \frac{Δ}{256 (129 + 16 \sqrt{65})} < \frac{Δ}{32768} < \frac{Δ}{32},$ so the page's cubic bound is satisfied at this coupling with a wide margin;

(e) scope: the computation is conditional on the declared truncated two-state model and the adopted coupling; it identifies no laboratory atom, reports no measured shift and no polarizability value, asserts no transition rate, and does not treat the uncompressed linear potential $- E_{e x t} \cdot D$ . The postulate excludes that model and proves its common-test-domain expectations unbounded below for every nonzero uniform field; no full energy-form domain is used here.

Verification

Given: the declared two-body Coulomb model with charges $\mp q$ , coupling $κ > 0$ , relative-coordinate states $ψ_{1}, ψ_{2}$ of angular labels $(1, 0, 0)$ , $(2, 1, 0)$ and energies $E_{1}, E_{2}$ ; the finite-level subspace $W = span {ψ_{1}, ψ_{2}}$ ; the dipole operators $D_{j} = - q Q_{j}$ of the postulate with $m = μ$ and $a_{μ} = ℏ^{2} / (μ κ)$ ; the field $E_{e x t} = (0, 0, E)$ ; the coupling $λ$ , matrix $V$ and family $H_{S}$ of the Example; the Axiom of Countable Choice and the Axiom of Choice as the choice hypotheses of the cited suppliers.

[L1] Spectrum and eigenstates. For the one-centre Coulomb model $H_{κ}$ , the normalized bound states $ψ_{n l m}$ satisfy $H_{κ} ψ_{n l m} = E_{n} ψ_{n l m}$ with $E_{n} = - m κ^{2} / (2 ℏ^{2} n^{2})$ , so in particular $E_{1} = - m κ^{2} / (2 ℏ^{2})$ and $E_{2} = - m κ^{2} / (8 ℏ^{2})$ and $Δ = 3 m κ^{2} / (8 ℏ^{2}) > 0$ ; states with different labels are orthogonal (The one-centre Coulomb model: bound energies, n^2-degeneracy, completeness of the bound states in the negative spectral subspace and the continuum).

[L2] Dipole domain and angular selection rule. Each $Q_{j}$ is self-adjoint on its maximal domain $D (Q_{j}) = {ψ : ξ_{j} ψ \in L^{2}}$ and all bound states lie in $D (Q_{j})$ ; for the spherical components $Q_{0} = x_{3}$ , $Q_{\pm} = (x_{1} \pm i x_{2}) / \sqrt{2}$ the angular matrix element $⟨ Y_{l^{'} m^{'}}, Q_{q} ∣_{S^{2}} Y_{l m} ⟩$ can be nonzero only if $l^{'} = l + 1, m^{'} = m + q$ or $l \geq 1, l^{'} = l - 1, m^{'} = m + q$ (Atomic dipole matrix-element domain clauses (a), (b), Dipole angular selection rules). In particular with $l = l^{'} = 0$ or $l = l^{'} = 1$ the angular factor vanishes, and with $m = m^{'} = 0$ only $q = 0$ can contribute; for the pair $(l, m) = (0, 0)$ and $(l^{'}, m^{'}) = (1, 0)$ the rule allows $l^{'} = l + 1$ , $m^{'} = m + 0$ .

[L3] The model's theorem. Under the model's hypotheses with a simple label, for every real $∣ λ ∣ < R = g / (8 v)$ the followed label is the unique spectral value in $∣ z - E ∣ < g / 2$ , and the coefficients and remainder bound of Nondegenerate stationary perturbation of a simple gapped label: first- and second-order coefficients and an explicit cubic remainder hold (Nondegenerate stationary perturbation of a simple gapped label: first- and second-order coefficients and an explicit cubic remainder, The declared perturbed-family model: bounded self-adjoint perturbation, isolated gapped label and followed spectral cluster).

[L4] Elementary algebra. For real $u$ , $\sqrt{u^{2}} = ∣ u ∣$ ; and $\sqrt{1 + t} = 1 + \frac{1}{2} t - \frac{1}{8} t^{2} + O (t^{3})$ as the analytic square root near $t = 0$ . Also $129^{2} - (16 \sqrt{65})^{2} = 1$ , so $129 - 16 \sqrt{65} = 1 / (129 + 16 \sqrt{65}) > 0$ .

[L5] Explicit local integral data. With $a = a_{μ}$ , the Kummer regular solutions for $(n, l) = (1, 0), (2, 1)$ have $j = n - l - 1 = 0$ , $L_{0}^{(1)} = L_{0}^{(3)} = 1$ , decay rates $1 / a, 1 / (2 a)$ , and normalized positive radial representatives $u_{10} = 2 a^{- 3 / 2} r e^{- r / a}$ , $u_{21} = (2 \sqrt{6})^{- 1} a^{- 5 / 2} r^{2} e^{- r / (2 a)}$ (Kummer recurrence and termination clauses (c)-(e)). Their normalizations follow locally from $\int_{0}^{\infty} r^{k} e^{- b r} d r = k! / b^{k + 1}$ (Moments of the exponential law on the half-line). The sphere family is orthonormal with the positive real representatives $Y_{00} = 1 / \sqrt{4 π}$ , $Y_{10} = \sqrt{3 / (4 π)} Ω_{3}$ , obtained from $P_{0} = 1$ , $P_{1} = t$ and the normalizing integral (Associated Legendre function normalization clauses (c), (e), Sphere ONB); sphere integration is $d σ = \sin θ d θ d φ$ (Sphere integrals in angle coordinates). No nonzero radial assertion is inferred from the necessary selection rule.

Proof technique: direct; evaluate the compressed dipole matrix by the angular selection rule and the explicit nonzero radial/angular integral, diagonalize the resulting Hermitian two-by-two family exactly, read off the page's coefficients, and compare the exact closed form with the second-order truncation at the test coupling.

Given: the data of the Example and [L1]-[L5].

1.1L1L2L5givenalgebra

[The compressed matrices and their nonzero entry] Write $a = a_{μ}$ . From [L5], $∥ u_{10} ∥_{2}^{2} = 4 a^{- 3} 2! / (2 / a)^{3} = 1$ and $∥ u_{21} ∥_{2}^{2} = (24 a^{5})^{- 1} 4! / (1 / a)^{5} = 1$ ; the explicit Kummer solutions therefore give the normalized bound states with the stated labels. For their positive real representatives, $\int_{S^{2}} Y_{10} Ω_{3} Y_{00} d σ = (\sqrt{3} / (4 π)) 2 π \int_{- 1}^{1} t^{2} d t = 1 / \sqrt{3}$ . Their radial dipole integral is $\int_{0}^{\infty} r u_{21} u_{10} d r = (1 / \sqrt{6}) a^{- 4} 4! / (3 / (2 a))^{5} = 256 a / (81 \sqrt{6}) > 0$ . The absolutely convergent factorization [L2] yields $⟨ ψ_{210}, Q_{3} ψ_{100} ⟩ = 128 \sqrt{2} a / 243 > 0$ . Since $D_{3} = - q Q_{3}$ , its matrix element is $- 128 \sqrt{2} q a / 243$ before rephasing. Set $ψ_{1} = ψ_{100}$ and $ψ_{2} = - ψ_{210}$ to obtain the positive off-diagonal value $D_{r e l} = 128 \sqrt{2} q a / 243$ without changing energies, labels or normalization. By [L2], bound states lie in all coordinate domains; all diagonal entries vanish by degree selection, and the off-diagonal $Q_{\pm}$ entries vanish by weight selection. Thus $D_{1}^{W} = D_{2}^{W} = 0$ and $D_{3}^{W} = D_{r e l} σ_{1}$ with $D_{r e l} > 0$ , proving (a).

1.2L1givenalgebra

[The two-state family] In the orthonormal basis $(ψ_{1}, ψ_{2})$ one has $Π_{W} H_{κ} ∣_{W} = diag (E_{1}, E_{2})$ by [L1] and orthogonality of distinct eigenstates; with $v : = D_{r e l} (1 V m^{- 1})$ in joules one has $V = - v σ_{1}$ and $H_{S} = (\begin{array}{cc} E_{1} & - v λ \\ - v λ & E_{2} \end{array}) .$ Since $σ_{1}$ is Hermitian with $∥ σ_{1} ∥ = 1$ , $V$ is bounded self-adjoint with norm $v$ ; the exact eigenvalues of a matrix $(\begin{array}{cc} a & w \\ w & b \end{array})$ with real $w$ are $\frac{a + b}{2} \pm \sqrt{(\frac{a - b}{2})^{2} + w^{2}}$ , because its characteristic polynomial is $(a - z) (b - z) - w^{2}$ ; here $a \neq b$ , so the two displayed roots are distinct, each has a nonzero kernel vector, and their eigenvectors are independent and span the two-dimensional space; substituting $a = E_{1}, b = E_{2}$ gives clause (b).

2.1L3L4step 1.2algebra

[Coefficients] The label $E = E_{1}$ is simple with gap $Δ$ (the second level is $E_{2} = E_{1} + Δ$ and there are no further levels in the two-dimensional model); the perturbation $V$ is bounded self-adjoint with norm $v$ ; hence [L3] applies for $∣ λ ∣ v < Δ / 8$ . Since $V$ has vanishing diagonal, $E^{'} (0) = ⟨ V ψ_{1}, ψ_{1} ⟩ = 0$ . The reduced inverse on $Q_{0} W = C ψ_{2}$ is $S = Δ^{- 1} ∣ ψ_{2} ⟩ ⟨ ψ_{2} ∣$ , so $S V ψ_{1} = - (v / Δ) ψ_{2}$ and $V S V ψ_{1} = (v^{2} / Δ) ψ_{1}$ , giving $E^{''} (0) = - 2 v^{2} / Δ$ ; substituting $v = D_{r e l} (1 V m^{- 1})$ and expanding the closed form of clause (b) by [L4] gives the displayed quadratic Stark shift. This is clause (c).

3.1L3L4step 2.1algebra

[The finite remainder check at the true half radius] At $E = Δ / (16 D_{r e l})$ , $λ v = D_{r e l} E = Δ / 16$ and hence $λ = R / 2$ for $R = Δ / (8 v)$ . The page's bound is $R v (1 / 2)^{3} / (1 - 1 / 2) = R v / 4 = Δ / 32$ . The exact lower branch satisfies $F_{-} = E_{1} + Δ / 2 - \sqrt{Δ^{2} / 4 + Δ^{2} / 256} = E_{1} + Δ (8 - \sqrt{65}) / 16$ , whereas its quadratic truncation is $E_{1} - (λ v)^{2} / Δ = E_{1} - Δ / 256$ . Therefore $∣ F_{-} - E_{1} + Δ / 256 ∣ = Δ (129 - 16 \sqrt{65}) / 256 = Δ / [256 (129 + 16 \sqrt{65})]$ by [L4]. Since $129 + 16 \sqrt{65} > 128$ , this remainder is strictly less than $Δ / 32768$ , and consequently less than $Δ / 32$ . This proves (d) without a decimal approximation.

4.1step 1.1step 2.1step 3.1given∎

[Scope] The argument used the declared two-state truncation, the adopted coupling, the model's exact spectrum and the page's theorem; no laboratory atom, measured shift, polarizability, transition rate or uncompressed linear potential entered. The exclusion of the uncompressed static perturbation is the postulate's scope clause; clause (e) holds.

Remarks

Why the first-order shift vanishes. The two declared states have angular degrees $0$ and $1$ ; the coordinate multiplier changes the degree by exactly one, so the diagonal matrix elements of $D_{j}$ vanish and the leading shift is quadratic, exactly as in the textbook quadratic Stark effect. The nonzero dipole modulus is computed locally as $D_{r e l} = 128 \sqrt{2} q a_{μ} / 243$ from the model's parameters; no measured charge, length or dipole value is supplied.
Shared two-by-two identity. The eigenvalue formula for $(\begin{array}{cc} a & w \\ w & b \end{array})$ used in step 1.2 was verified directly on this page in A two-level finite-gap model: exact eigenvalues, the second-order correction and a finite check of the cubic remainder bound; the present example re-derives it by the same substitution, so no dependency on the sibling example is claimed.
Relation to the linear Stark effect. A degenerate truncation (for instance the four states with $n = 2$ ) would instead be governed by Degenerate stationary perturbation: the perturbed eigenvalues stay within 4 lambda^2 v^2/g of the first-order shifts, and no branch relaxation is asserted and could produce a first-order shift; the present two-state nondegenerate truncation produces the quadratic shift, and no statement about a laboratory line is made in either case.

A finite-level static Stark model: vanishing first-order shift, exact splitting with leading quadratic shift and a finite check of the remainder bound

Example

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources