Alphabeta Math
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.

Dimension bookkeeping for the quantities and laws of the framework

Physical scope

A worked application of the dimension and unit conventions of the framework to the quantities and displayed laws of this page: coordinates, wave function, position and momentum operators, the canonical commutator, the kinetic and potential terms of the Hamiltonian, the Schroedinger equation, the probability current and the candidate dimensionless exponent that could be used as a boost phase in a separately specified model. The item checks conventions only, asserts no frame-transformation law, and makes no empirical claim.

Example

Apply the dimension conventions of Dimensions, SI unit conventions and quantity types of the framework to the quantities of the framework: the time and space coordinates of an inertial frame of Inertial frames of the framework and the class of frame changes, a position wave function of the one-particle model, the position and momentum operators and their canonical commutator of Canonical commutation relations of position and momentum on the Schwartz core, the kinetic and potential terms of the Hamiltonian and the Schroedinger equation of Kinematics and massive-particle model postulate P5: Newtonian frames and one-particle operators and Autonomous dynamics postulate P4: self-adjoint generators and unitary evolution, the probability density and current of the continuity calculation, and the candidate phase exponent mv⋅x/ℏ if used in a separately specified boost model.

Facts & Assumptions

Given: The dimension symbols ℓ,τ,μ,ϑ with the product, quotient and derivative rules of Dimensions, SI unit conventions and quantity types of the framework; the readings [t]=τ, [xi]=ℓ, [ψ]=ℓ−3/2 for a position wave function in three spatial dimensions, [ℏ]=μℓ2τ−1, [m]=μ, [E]=μℓ2τ−2, [vi]=ℓτ−1 and [Rij]=1.

[L1]

Position and momentum acts: Qjf=xjf and Pkf=−iℏ Dkf for one component, with the Schwartz core and the canonical commutator (QjPk−PkQj)f=iℏδjkf (Kinematics and massive-particle model postulate P5: Newtonian frames and one-particle operators, Canonical commutation relations of position and momentum on the Schwartz core).

[L2]

Hamiltonian and evolution: for m,ℏ>0 and a real bounded measurable potential V in three spatial dimensions, Hop=−ℏ22mΔ+V(Q) on D(Hop)=W2,2(R3;C) componentwise. Its unitary evolution is ψ(t)=e−itHop/ℏψ(0) for every initial vector; the norm derivative and the equation iℏ ∂tψ=Hopψ are asserted exactly when ψ(0)∈D(Hop), in which case this domain is invariant under the evolution (Kinematics and massive-particle model postulate P5: Newtonian frames and one-particle operators, Autonomous dynamics postulate P4: self-adjoint generators and unitary evolution).

[L3]

Probability current of a smooth solution: j=ℏmIm⁡(ψ‾ ∇ψ) (Smooth local continuity equation and its integrated forms).

[L4]

Frame parameters: [b]=τ, [ai]=ℓ and [vi]=ℓτ−1; conditionally, if a separately specified model uses mv⋅x/ℏ as a phase exponent, these units make that exponent dimensionless (Inertial frames of the framework and the class of frame changes, Dimensions, SI unit conventions and quantity types of the framework).

Verification

technique · direct; evaluate the dimension rules on each displayed quantity and combine
1.1givenalgebra

The coordinates have [t]=τ and [xi]=ℓ, so a three-dimensional position wave function has [ψ]=ℓ−3/2, its squared modulus has [∣ψ∣2]=ℓ−3, and the product ∣ψ∣2d3x is dimensionless, as required of a probability density.

1.2givenL1algebra

For the operators of [L1], [Qjψ]=[xj][ψ]=ℓ⋅ℓ−3/2=ℓ−1/2=[ψ]⋅ℓ gives [Qj]=ℓ, and [Pkψ]=[ℏ]⋅[∂kψ]=μℓ2τ−1⋅ℓ−5/2=μℓ−1/2τ−1=[ψ]⋅μℓτ−1 gives [Pk]=μℓτ−1; the commutator identity is consistent, since [QjPk]=ℓ⋅μℓτ−1=μℓ2τ−1=[ℏ]=[iℏδjk].

1.3givenL2algebra

For the Hamiltonian of [L2], the kinetic term acts as [(−ℏ2/2m)Δψ]=μ2ℓ4τ−2μ−1ℓ−2ℓ−3/2=μℓ2τ−2ℓ−3/2=[E][ψ], and the potential term satisfies [Vψ]=[V][ψ] with [V]=μℓ2τ−2=[E]; both terms therefore carry the dimension of energy times wave function, as required for their sum to define an operator.

1.4givenL2algebra

The Schroedinger equation is dimensionally consistent: [iℏ∂tψ]=μℓ2τ−1⋅τ−1⋅ℓ−3/2=μℓ2τ−2ℓ−3/2=[Hopψ], and the phase Hopt/ℏ of the evolution operator is dimensionless because [E][t][ℏ]−1=1.

1.5givenL3algebra

The current of [L3] has [j]=[ℏ][m]−1[∣ψ∣2][∇ψ][ψ]−1=ℓ2τ−1⋅ℓ−3⋅ℓ−1=ℓ−2τ−1, which is ℓ1−dτ−1 for d=3: a probability flux per unit area and time, not a charge current.

2.1step 1.1step 1.2step 1.3step 1.4step 1.5L4algebra∎

The expression mv⋅x/ℏ in [L4] is dimensionless, [mv⋅x]/[ℏ]=μℓτ−1⋅ℓ⋅(μℓ2τ−1)−1=1. Thus it can serve as a dimensionless argument if a separately specified model assigns it as a phase; this dimensional calculation alone proves no frame-transformation or covariance law. Combining with steps 1.1-1.5, every quantity and displayed law checked here is dimensionally consistent under the stated conventions.

Remarks

Depends on

Dependency tree · 2 levels

Sources