ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Critical, subcritical and supercritical Gaussian regimes for Hardy's theorem

Example

Assume countable choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), as Hardy's Gaussian uncertainty principle in $R^{n}$ and the Gaussian-transform interface do. Let $a, b > 0$ and put $C_{0} : = \max {1, a^{- n / 2}}$ . At the critical product $a b = 1$ the Gaussian $f (x) = e^{- π a ∣ x ∣^{2}}$ satisfies the two Hardy bounds $∣ f (x) ∣ \leq e^{- π a ∣ x ∣^{2}}$ and $∣ \hat{f} (ξ) ∣ \leq a^{- n / 2} e^{- π ∣ ξ ∣^{2} / a}$ of Hardy's Gaussian uncertainty principle in $R^{n}$ with the common constant $C_{0}$ , and the theorem returns a scalar multiple of the same Gaussian. In the subcritical regime $a b < 1$ , every $c$ with $a < c < 1 / b$ gives the Gaussian $e^{- π c ∣ x ∣^{2}}$ satisfying the two bounds with the common constant $C_{c} : = \max {1, c^{- n / 2}}$ , so no vanishing conclusion holds (Subcritical Gaussians show the Hardy threshold $a b = 1$ is sharp). In the supercritical regime $a b > 1$ the theorem forces $f = 0$ , and no Gaussian satisfies both bounds for any positive constants $C, C^{'}$ : $∣ e^{- π c ∣ x ∣^{2}} ∣ \leq C e^{- π a ∣ x ∣^{2}}$ forces $c \geq a$ , while $∣ \hat{f_{c}} ∣ \leq C^{'} e^{- π b ∣ ξ ∣^{2}}$ forces $c \leq 1 / b$ , and $a \leq 1 / b$ is exactly $a b \leq 1$ .

Facts & Assumptions

Given: Countable choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), an integer $n \geq 1$ , reals $a, b > 0$ , the common critical bound $C_{0} = \max {1, a^{- n / 2}}$ , and for $c > 0$ the Gaussian $f_{c} (x) : = e^{- π c ∣ x ∣^{2}}$ (Real powers for positive bases, with the zero-base positive-exponent convention for real powers).

[F1]

Countable choice is assumed; it is the hypothesis carried by the Gaussian transform identity and by the two cited theorems (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F2]

Gaussian transform: for every $t > 0$ , $f_{t} = e^{- π t ∣ x ∣^{2}}$ is absolutely integrable with $L^{1}$ transform $t^{- n / 2} e^{- π ∣ ξ ∣^{2} / t}$ (Euclidean Gaussian transform with the 2π normalization).

[F3]

Subcritical sharpness: if $a b < 1$ , then $(a, 1 / b)$ is a nonempty open interval and every $c$ with $a < c < 1 / b$ satisfies $∣ f_{c} (x) ∣ \leq e^{- π a ∣ x ∣^{2}}$ and $∣ \hat{f_{c}} (ξ) ∣ \leq c^{- n / 2} e^{- π b ∣ ξ ∣^{2}}$ (Subcritical Gaussians show the Hardy threshold $a b = 1$ is sharp).

[F4]

Hardy's theorem: if $a, b, C > 0$ and a measurable $g$ satisfies $∣ g (x) ∣ \leq C e^{- π a ∣ x ∣^{2}}$ almost everywhere and $∣ \hat{g} (ξ) ∣ \leq C e^{- π b ∣ ξ ∣^{2}}$ everywhere, then $g = 0$ almost everywhere when $a b > 1$ , and $g (x) = g^{\land} (0) a^{n / 2} e^{- π a ∣ x ∣^{2}}$ almost everywhere when $a b = 1$ (Hardy's Gaussian uncertainty principle in $R^{n}$ ).

[F5]

Every unit cube has Lebesgue measure $1$ under Countable Choice (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included). Hence a full-measure subset of $R^{n}$ is unbounded: if it were bounded, a unit cube outside a ball containing it would be contained in its null complement, a contradiction.

Verification

technique · direct

1.1F2F4given

Critical regime. For $g = f_{a}$ we have $∣ g (x) ∣ = e^{- π a ∣ x ∣^{2}} \leq C_{0} e^{- π a ∣ x ∣^{2}}$ and, by [F2] with $t = a$ , $∣ \hat{g} (ξ) ∣ = a^{- n / 2} e^{- π ∣ ξ ∣^{2} / a} \leq C_{0} e^{- π b ∣ ξ ∣^{2}}$ since $b = 1 / a$ . Thus $g$ meets both Hardy bounds with one common constant $C_{0}$ . Since $a b = 1$ , [F4] returns $g (x) = \hat{g} (0) a^{n / 2} e^{- π a ∣ x ∣^{2}}$ almost everywhere, with $\hat{g} (0) = \int g = a^{- n / 2}$ ; that is the same Gaussian, so the classification is attained, not merely bounded.

1.2F3given

Subcritical regime. Suppose $a b < 1$ , equivalently $a < 1 / b$ . By [F3] the interval $(a, 1 / b)$ is nonempty and every $c \in (a, 1 / b)$ produces a nonzero Gaussian $f_{c}$ satisfying $∣ f_{c} ∣ \leq e^{- π a ∣ x ∣^{2}}$ and $∣ \hat{f_{c}} ∣ \leq c^{- n / 2} e^{- π b ∣ ξ ∣^{2}}$ . With $C_{c} = \max {1, c^{- n / 2}}$ both bounds hold with a single constant, so the Hardy hypotheses admit a nonzero function and no vanishing conclusion can be drawn.

1.3F1F2F4F5given

Supercritical regime. Suppose $a b > 1$ , equivalently $a > 1 / b$ . If $c > 0$ and constants $C, C^{'} > 0$ satisfied $e^{- π c ∣ x ∣^{2}} \leq C e^{- π a ∣ x ∣^{2}}$ almost everywhere, then $e^{π (a - c) ∣ x ∣^{2}} \leq C$ would hold on a set of full measure, and a set of full measure is unbounded by [F5]; were $c < a$ , the left side would tend to $+ \infty$ along that unbounded set, which is impossible for a finite constant, so $c \geq a$ . Similarly, by [F2], $∣ \hat{f_{c}} (ξ) ∣ = c^{- n / 2} e^{- π ∣ ξ ∣^{2} / c} \leq C^{'} e^{- π b ∣ ξ ∣^{2}}$ for every $ξ$ would give $e^{π (b - 1 / c) ∣ ξ ∣^{2}} \leq C^{'} c^{n / 2}$ for every $ξ$ ; if $b > 1 / c$ , the left side diverges as $∣ ξ ∣ \to \infty$ , contradicting the finite bound; thus $1 / c \geq b$ , that is $c \leq 1 / b$ . Both requirements together would give $a \leq c \leq 1 / b$ , hence $a b \leq 1$ , contrary to the hypothesis; so no Gaussian meets the two bounds, and by [F4] the only function satisfying them is $0$ almost everywhere.

2.1step 1.1step 1.2step 1.3∎

Tabulation. Steps 1.1–1.3 separate the three parameter regions: at $a b = 1$ the Gaussian $e^{- π a ∣ x ∣^{2}}$ is a nonzero solution classified as itself, for $a b < 1$ nonzero Gaussian solutions exist with rate $c \in (a, 1 / b)$ , and for $a b > 1$ no Gaussian solution exists and every solution vanishes almost everywhere.

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

Aingeru Fernández-Bertolín and Eugenia Malinnikova, Dynamical Versions of Hardy's Uncertainty Principle: A Survey (arXiv:2210.03369) (standard reference, not scraped)
Calder Sheagren, Uncertainty Principles with Fourier Analysis (University of Chicago REU 2017, author PDF) (standard reference, not scraped)