Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

Heisenberg uncertainty and Gaussian equality

Statement

Assume countable choice and let n≥1. For f∈S(Rn) and a,b∈Rn, ∥∣x−a∣f∥2∥∣ξ−b∣f^∥2≥n4π∥f∥22. For nonzero f, equality holds exactly for f(x)=cexp⁡(−λ∣x−a∣2/2)exp⁡(2πib⋅x),c∈C∖{0},λ>0. The zero function also gives equality.

Facts & Assumptions

Given: An integer n≥1 and The Axiom of Countable Choice (ACω).

[F1]

Schwartz Parseval preserves norms (Parseval pairing on Schwartz space).

[F2]

Fourier transforms derivatives to multiplication by 2πiξ (Fourier transform acts continuously on Schwartz space).

[F3]

Translation and modulation have the stated Fourier covariance laws (Translation, modulation, linear dilation and reflection laws).

[F4]

Complex finite-tuple Cauchy–Schwarz has equality exactly for one common scalar multiple when the second tuple is nonzero (Complex completeness, density, and inner product: the consumer interface).

[F5]

Complex line integration by parts and interval FTC hold (Complex integration by parts on intervals and decaying lines).

[F6]

The basic operations preserve Schwartz space (Basic operations are continuous on Schwartz space), and weighted derivatives are integrable in all required exponents (Schwartz derivatives are integrable).

[F7]

Absolute-integrable product functions admit Fubini (Fubini's theorem for L1 functions on a sigma-finite product).

[F8]

Positive-parameter Gaussians are Schwartz (Polynomial Gaussians are Schwartz).

Proof

technique · direct
1.1F3F6given

Put g(y)=e−2πib⋅(y+a)f(y+a). By [F6] it is Schwartz, and [F3] gives g^(η)=e2πia⋅ηf^(η+b). Translation substitution and unit modulus therefore identify ∥g∥2=∥f∥2, ∥∣y∣g∥2=∥∣x−a∣f∥2, and ∥∣η∣g^∥2=∥∣ξ−b∣f^∥2. It suffices to prove the zero-centre assertion for g.

2.1step 1.1F1F2F4F5F6F7

For each coordinate j, apply [F5] along that line to u=xjg and v=g‾. The endpoint product xj∣g∣2 tends to zero at both ends by rapid decay, and both differentiated products are line-integrable. Their full-space integrability follows from [F6] and [F4], so [F7] permits integrating the identity in the other coordinates. It yields ∥g∥22=−2Re⁡∫xjg∂jg‾. Sum over j and define tuples A=(xjg)j, B=(∂jg)j. Then n∥g∥22=−2Re⁡⟨A,B⟩≤2∣⟨A,B⟩∣≤2∥A∥∥B∥. By [F1] and [F2], ∥B∥2=4π2∫∣ξ∣2∣g^(ξ)∣2 dξ, while ∥A∥=∥∣x∣g∥2. This proves the inequality with the claimed constant.

3.1step 1.1step 2.1F4F5

Suppose g≠0 and equality holds. Step 2.1 gives n∥g∥22>0, so both tuple norms are nonzero. Equality in [F4] makes B=dA for one complex scalar d. Equality in the real-part bound, together with ⟨A,B⟩=d‾∥A∥2, forces d to be a negative real number. Write d=−λ, λ>0. The identities ∂jg=−λxjg hold a.e., hence everywhere by continuity and the positive measure of nondegenerate boxes. Thus every partial derivative of G(x)=eλ∣x∣2/2g(x) is zero. Applying the interval FTC [F5] along successive coordinate segments shows G(x)=G(0)=c, so g(x)=ce−λ∣x∣2/2. Nonzero g forces c≠0. Undoing step 1.1 gives exactly the displayed form for f.

4.1step 1.1step 2.1F8given∎

Conversely let g(x)=ce−λ∣x∣2/2 with λ>0, c≠0. By [F8] it is Schwartz, and direct differentiation gives B=−λA. Thus both inequalities in step 2.1 are equalities, giving equality in the uncertainty inequality. By step 1.1 the translated and modulated functions have the same equality property. If f=0, both sides are zero directly. The common scalar across all coordinates is essential to the radial equality assertion proved here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources