Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated
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 two-level dipole-drive model: identification, resonant first-order coefficient and its comparison with the exact Rabi probability

Physical scope

A conditional two-level instance of the declared dipole-drive model: Pauli matter data realized by explicit Coulomb and Cartesian-dipole compressions of two Gaussian functions, with a real dipole entry, a monochromatic spatially uniform prescribed field along one axis, with declared matter length L > 0 and wavevector k = 0 satisfying the phase tolerance, the identification with the declared linear two-level drive model, the resonant co-rotating first-order amplitude and its agreement at small times with the exact averaged Rabi probability of the driven-dynamics page. The example asserts no laboratory atom or field, no damping, no spontaneous emission, no measurement record and no empirical value.

Example

Adopt the prescribed dipole-drive model The declared prescribed dipole-drive model and its long-wavelength regime with the following realized two-level matter data. For any declared ω0>0 (s−1) and d>0 (C m), use the positive framework constant ε0 of The declared Coulomb and two-body hydrogen model: one-centre operator, relative problem, reduced mass and scope exclusions clause (d) and define q:=(82 π3/2ε0ℏω0d3)1/3,a:=2dq,μ:=9ℏ10ω0a2,κ:=q24πε0. These have units C, m, kg and J m, respectively. Declare the charged pair of Static finite-level electric-dipole coupling: compressed dipole of the declared two-body Coulomb model in a uniform field with m1=m2=2μ, charges −q,+q and relative-coordinate energy Hκ=−(ℏ2/(2μ))Δw−κ/∣x∣ on H2(R3;C); Δw is the sum of the three second weak coordinate derivatives. Its dipoles are Dj=−qQj, Qjf(x)=xjf(x) on D(Qj)={f∈L2:xjf∈L2}. Here L2=L2(R3;C) consists of Lebesgue square-integrable classes, and H2 consists of those classes whose weak coordinate derivatives through order two also belong to L2: Dαf is a weak derivative when ∫f ∂αφ=(−1)∣α∣∫Dαf φ for every smooth compactly supported test function φ:R3→C. Here α=(α1,α2,α3)∈N03, ∣α∣=α1+α2+α3 and ∂α denotes that sequence of classical coordinate derivatives. In this relative-coordinate space put ga(x):=(πa2)−3/4e−∣x∣2/(2a2),w↓:=ga,w↑:=−2x1aga,W:=span⁡{w↑,w↓}. The verification below proves that this is an orthonormal pair in D(Hκ)∩⋂j=13D(Qj) and that the actual compressions Ha=ΠWHκ∣W, DjW=ΠWDj∣W have the following matrices. Identify (w↑,w↓) with the coordinate basis (e↑,e↓) of C2, using the Pauli matrices (σx,σy,σz) of Finite spin matrices clause (e): Ha:=ℏω02σz,D1W:=d σx,D2W:=D3W:=0, where ω0,d are the arbitrary positive parameters fixed above. The two vectors are eigenvectors of the compression, not asserted to be Coulomb eigenfunctions; invariance of W under the uncompressed operators is unnecessary. Declare the field Eext(r):=E0cos⁡(ωr) e1,r∈I=[0,τ], with E0>0 in V m−1 and ω>0 in s−1, and τ>0 in seconds; declare L>0 in metres, x0=0∈R3, k=0∈R3 in inverse metres, and a dimensionless phase tolerance δph=1/10. Use the spatially uniform template Esp(x,r)=E0cos⁡(ωr)e1 of the dipole-drive definition (d), so ∣k∣L=0≤δph for every L. These are declared prescribed-field data, with no Maxwell dispersion relation; the temporal frequency ω>0 does not determine k in this model. Let v↑:=e↑, v↓:=e↓, so that E↑=ℏω0/2, E↓=−ℏω0/2 and Δ=E↑−E↓=ℏω0. Write δ:=ω0−ω for the detuning frequency, distinct from the energy Δ. Then:

(a) (identification) Hd(r)=ℏ2(ω0σz+Ω1cos⁡(ωr)σx) with Ω1=−2dE0ℏ, so the model is exactly the declared linear two-level drive model of clause (f) of The declared driven model: prescribed time-dependent energy families, propagator evolution and the two-level drive models with splitting frequency ω0 and transverse coupling Ω1;

(b) (resonance and first-order coefficient) at resonance ω=ω0 the co-rotating first-order amplitude of Stimulated dipole-drive transitions of the finite-level model: first-order amplitudes, equal emission and absorption coefficients, and the exact two-level identification clause (b) for the transition e↓→e↑ from time 0 to time τ has modulus ∣a+∣=∣⟨V0e↓,e↑⟩∣τ2ℏ=dE0τ2ℏ,V0=−dE0σx, and the co-rotating component coefficient is γ+=∣a+∣2=(dE0τ/(2ℏ))2; the counter-rotating term is bounded by ∣⟨V0e↓,e↑⟩∣/(Δ+ℏω)=dE0/(2ℏω) at resonance. The full first-order interaction-picture amplitude is A1=idE02ℏ[τ+e2iωτ−12iω],γ1:=∣A1∣2, including interference of both components; γ1 is an unnormalized first-order approximation, not a normalized-state Born law;

(c) (comparison with the exact averaged Rabi probability) by The linearly driven two-level model: rotating-wave approximation with an explicit finite-time error contract and the averaged Rabi populations clause (c) the averaged down-population of the initial up-state at resonance is p↓avg(τ)=sin⁡2(∣Ω1∣τ/4)=sin⁡2(dE0τ/(2ℏ)), whose small-τ expansion begins with (dE0τ/(2ℏ))2; the co-rotating coefficient γ+ of clause (b) is therefore the leading term of the exact averaged Rabi probability, and the rotating-wave error contract of the cited item bounds the difference between the exact linear-model population and this averaged probability by 2ε(τ) with ε(τ)=∣Ω1∣2ω[1+τ(∣δ∣2+3∣Ω1∣4)];

(d) (scope) the example is a conditional computation in the declared two-level drive model. The identification of a laboratory two-level atom, molecule or field with the declared data is a tested identification with uncertainty under P7; the model has no quantized field, no vacuum, no spontaneous emission, no damping, no measurement record and no empirical value, and the exact circular and linear families of the driven-dynamics page are models with their own scope.

Facts & Assumptions

Given: the explicit subspace W, the constructed parameters q,a,μ,κ, the declared two-level matter data Ha,DjW, the field Eext, the parameters ω0,d,E0,ω, the pair (e↑,e↓) and the cited suppliers.

[F1]

Identification supplier. The declared linear two-level drive model of clause (f) of The declared driven model: prescribed time-dependent energy families, propagator evolution and the two-level drive models has the family Hl(t)=ℏ2(ω0σz+Ω1cos⁡(ωt)σx) with splitting frequency ω0, transverse coupling Ω1 and drive frequency ω, read as the model's energy in the bounded norm-continuous class (The declared driven model: prescribed time-dependent energy families, propagator evolution and the two-level drive models clauses (b)(i),(f), Finite spin matrices).

[F2]

First-order supplier. Write V0 for the perturbation matrix called W in the supplier, keeping it distinct from the matter subspace. For a monochromatic field Eext(r)=E0cos⁡(ωr+ϑ) and V0=−∑jE0,jDjW, the first-order amplitude decomposes into co- and counter-rotating parts with ∣a+∣=∣⟨V0vi,vk⟩∣ ∣sin⁡((Δ−ℏω)τ/(2ℏ))∣/∣Δ−ℏω∣ for Δ≠ℏω and ∣a+∣=∣⟨V0vi,vk⟩∣τ/(2ℏ) at Δ=ℏω, while the counter-rotating part is bounded by ∣⟨V0vi,vk⟩∣/∣Δ+ℏω∣ when Δ+ℏω≠0 (Stimulated dipole-drive transitions of the finite-level model: first-order amplitudes, equal emission and absorption coefficients, and the exact two-level identification clause (b)).

[F3]

Averaged Rabi supplier. Under the stated hypotheses the linear model's exact down-population obeys ∣p↓(τ)−p↓avg(τ)∣≤2ε(τ) with ε(τ)=∣Ω1∣2∣ω∣[1+τ(∣δ∣2+3∣Ω1∣4)], and at resonance δ=0 the averaged probability is p↓avg(τ)=sin⁡2(∣Ω1∣τ/4) (The linearly driven two-level model: rotating-wave approximation with an explicit finite-time error contract and the averaged Rabi populations clauses (b),(c)).

[F4]

Pauli data and pairing. The Pauli matrices of Finite spin matrices clause (e) act on the declared orthonormal basis with σxe↓=e↑, so V0e↓=−E0dσxe↓=−dE0e↑ and ⟨−dE0e↑,e↑⟩=−dE0 with modulus dE0; the pairing is linear in the first argument (Real and complex inner product spaces, with the inner product linear in the first argument, Orthonormal families, complete orthonormal systems and Hilbert bases).

[F5]

Framework readings. Times, energies and field values are read in s, J and V m−1 as in Dimensions, SI unit conventions and quantity types of the framework, and the laboratory identification of a preparation or field with the declared data is a tested identification with uncertainty under P7 (Preparation and apparatus postulate P7: declared preparations, isolation and sampling assumptions, Assigned sharp observables and the outcome law of the framework).

[F6]

Coulomb realization and domains. The declared two-body model has reduced mass μ=m1m2/(m1+m2) and equal-charge coupling κ=q2/(4πε0); its relative energy has the stated weak differential action on H2 (The declared Coulomb and two-body hydrogen model: one-centre operator, relative problem, reduced mass and scope exclusions clauses (b),(d)). The finite-level postulate uses Dj=−qQj and the actual compressions on any declared finite-dimensional common-domain subspace (Static finite-level electric-dipole coupling: compressed dipole of the declared two-body Coulomb model in a uniform field clauses (ii)-(iv)). Classical derivatives of a C2 function are its weak derivatives (Classical derivatives agree with weak derivatives with k=2).

[F7]

Gaussian integration. For b>0, ∫Rne−b∣x∣2dx=(π/b)n/2, and all polynomial-Gaussian moments are absolutely integrable (Euclidean Gaussian transform with the 2π normalization, with zero Fourier argument and t=b/π). Nonnegative Gaussian product moments may be integrated successively by Tonelli's theorem for nonnegative measurable functions on a sigma-finite product on the sigma-finite Euclidean Lebesgue spaces. Polar integration in three dimensions is dx=r2dr dσ (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma). Integration by parts on a line is valid for C1 factors with integrable derivative products and vanishing boundary products (Complex integration by parts on intervals and decaying lines); all uses below have Gaussian decay.

Verification

technique · direct; realize the matter matrices on a common-domain Gaussian subspace, compute the matrix elements and the drive family in the declared basis, apply the supplier's first-order formula, and expand the supplier's exact averaged probability

Given: the explicit subspace W, the constructed parameters q,a,μ,κ, the declared two-level matter data Ha,DjW, the field Eext, the parameters ω0,d,E0,ω and the cited suppliers.

1.1givenF6F7algebra

[Common domain and normalization] Write ρ(x)=∣ga(x)∣2=(πa2)−3/2e−∣x∣2/a2. By [F7], ∫ρ=1; integrating (x1e−x12/a2)′ on the line gives ∫x12ρ=a2/2, so ∥w↑∥=∥w↓∥=1, and oddness in x1 gives their orthogonality. Every classical derivative of either vector through order two and every coordinate multiple is polynomial times a Gaussian and lies in L2 by [F7]. By [F6] those derivatives are weak derivatives, so both vectors lie in H2=D(Hκ) and every D(Qj). Thus the displayed W is a valid two-dimensional compression subspace.

2.1givenF6F7step 1.1algebra

[Exact Coulomb and dipole compressions] All off-diagonal energy entries vanish by oddness in x1, since the Laplacian and radial Coulomb multiplier preserve that parity. The derivative identity ∂jga=−xjga/a2, integration by parts from [F7], and the Gaussian moments give ∫∣∇w↓∣2=3/(2a2) and ∫∣∇w↑∣2=5/(2a2). Explicitly ∂jw↑=−(2/a)(δj1−x1xj/a2)ga; the line recurrence obtained by integrating (x12n−1e−x12/a2)′ gives ∫x14ρ=3a4/4, while product integration gives ∫x12x22ρ=∫x12x32ρ=a4/4, which yields the second gradient value. Polar integration gives ∫ρ/∣x∣=2/(πa) and ∫∣w↑∣2/∣x∣=4/(3πa): spherical symmetry assigns one third of ∫∣x∣ρ=2a/π to ∫x12ρ/∣x∣, and the radial integrals follow by substituting u=r2/a2. Therefore ⟨Hκw↓,w↓⟩=3ℏ2/(4μa2)−2κ/(πa) and ⟨Hκw↑,w↑⟩=5ℏ2/(4μa2)−4κ/(3πa). The declared parameters satisfy a=3πℏ2/(5μκ), so these values are −9ℏ2/(20μa2)=−ℏω0/2 and +9ℏ2/(20μa2)=+ℏω0/2. Every diagonal dipole entry vanishes by coordinate parity, and ⟨D1w↓,w↑⟩=(q2/a)∫x12ρ=qa/2=d; its reverse equals it by real symmetry. The cross entries for D2,D3 are zero by oddness in x2,x3. Thus the actual compressions are exactly Ha=(ℏω0/2)σz, D1W=dσx, D2W=D3W=0.

3.1F1step 2.1algebra

[Identification] Since D2W=D3W=0 and Eext(r)=E0cos⁡(ωr)e1, the interaction term is −∑jEext,j(r)DjW=−E0cos⁡(ωr)dσx, so Hd(r)=ℏω02σz−dE0cos⁡(ωr)σx=ℏ2(ω0σz+Ω1cos⁡(ωr)σx) with Ω1=−2dE0/ℏ; this is the linear family of [F1].

4.1F2F4step 3.1algebra

[Resonant first-order amplitude] At resonance ω=ω0 one has Δ=ℏω, so the co-rotating quotient is τ and ∣a+∣=∣⟨V0e↓,e↑⟩∣τ/(2ℏ); by [F4] this is dE0τ/(2ℏ), so the co-rotating coefficient is γ+=(dE0τ/(2ℏ))2. Integrating the full interaction-picture entry gives A1=(idE0/(2ℏ))[τ+(e2iωτ−1)/(2iω)], which contains both components and their interference. The quotient tends to τ+O(τ2) at small τ, so γ1=(dE0τ/ℏ)2+O(τ3), with leading coefficient four times that of γ+; the counter-rotating bound of [F2] at Δ+ℏω=2ℏω is dE0/(2ℏω).

5.1F3step 4.1algebra

[Exact averaged comparison] By [F3] at δ=ω0−ω=0 the averaged down-population is sin⁡2(∣Ω1∣τ/4)=sin⁡2(dE0τ/(2ℏ)), whose power series begins with (dE0τ/(2ℏ))2, the co-rotating coefficient of step 4.1; the difference between the exact linear-model population and this averaged probability is at most 2ε(τ) with the displayed ε.

6.1F5step 3.1step 4.1step 5.1∎

[Scope] The computation used only the declared two-level data, the prescribed field and the cited driven-dynamics results; no quantized field, vacuum, spontaneous emission, damping or record entered, and the laboratory identifications are P7-tested by [F5]. This is clause (d).

Remarks

  • First order versus exact. The co-rotating component coefficient of clause (b) is the leading term of the exact averaged Rabi oscillation of clause (c) only at small τ; the full linear-drive first-order coefficient is γ1=∣a++a−∣2 and has four times that leading small-time coefficient, so no averaging of the full model is silently assumed; the exact linear model differs from the averaged model by the rotating-wave error, and the exact circular model of the driven-dynamics page is a different declared family, not an approximation proved here.
  • No spontaneous emission. The example is stimulated: the field is prescribed and unaffected by the transition, and the model contains no vacuum. Spontaneous emission is treated only in the quantized cutoff dipole model of this pair, under the additional vacuum-preparation assumption of the postulate item.

Depends on

Dependency tree · 2 levels

Sources