LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Laplace uniqueness identifies two exponentially bounded semigroups

Statement

Assume Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain) and the Hahn-Banach extension principle HB (The real dominated-extension principle as an additional hypothesis over ZF). Let $(S (t))_{t \geq 0}$ and $(T (t))_{t \geq 0}$ be strongly continuous semigroups on a Banach space $X$ with generators $A$ and $B$ and resolvents $R_{A}, R_{B}$ (Resolvent and spectrum of a closed operator on a Banach space), and suppose there are $M \geq 1$ , $ω \in R$ with $∥ S (t) ∥, ∥ T (t) ∥ \leq M e^{ω t}$ for all $t \geq 0$ . If $R_{A} (λ) = R_{B} (λ)$ for every real $λ > ω$ , then $S (t) = T (t)$ for every $t \geq 0$ . In particular two strongly continuous semigroups with the same generator coincide.

Facts & Assumptions

Given: Dependent Choice; The Hahn-Banach extension principle HB (The real dominated-extension principle as an additional hypothesis over ZF); strongly continuous semigroups $(S (t))_{t \geq 0}$ , $(T (t))_{t \geq 0}$ on a Banach space $X$ with generators $A, B$ and resolvents $R_{A}, R_{B}$ (Strongly continuous semigroup, Resolvent and spectrum of a closed operator on a Banach space); $M \geq 1$ , $ω \in R$ with $∥ S (t) ∥, ∥ T (t) ∥ \leq M e^{ω t}$ (Exponential bound for a C0-semigroup); and $R_{A} (λ) = R_{B} (λ)$ for every real $λ > ω$ .

[F1]

Laplace formula: for real $λ > ω$ , $λ$ lies in the resolvent sets of both generators and $R_{A} (λ) x = \int_{0}^{\infty} e^{- λ t} S (t) x d t$ , $R_{B} (λ) x = \int_{0}^{\infty} e^{- λ t} T (t) x d t$ (Laplace transform formula for the resolvent).

[F2]

Bounded linear functionals and, more generally, bounded linear maps commute with Bochner integrals: $x^{*} (\int h) = \int x^{*} \circ h$ (Bounded linear maps commute with Bochner integration, Bochner-integrable function).

[F3]

Scalar Laplace uniqueness: a continuous scalar function $φ$ with $∣ φ (t) ∣ \leq C e^{σ t}$ whose Laplace transform vanishes for every real $λ > σ$ is identically zero (Uniqueness of the scalar Laplace transform in the exponential-growth class).

[F4]

Point separation and norming under HB: for every $x \neq 0$ there is $x^{*} \in X^{*}$ with $∥ x^{*} ∥ = 1$ and $x^{*} (x) = ∥ x ∥$ , so the dual separates points (Relative dual norming, point separation, and recovery of the norm).

Proof

technique · direct: scalarise the difference of the two semigroups by a functional and apply scalar Laplace uniqueness

1.1given

Put $D (t) : = S (t) - T (t)$ for $t \geq 0$ . For fixed $x \in X$ and $x^{*} \in X^{*}$ the scalar function $φ (t) : = x^{*} (D (t) x)$ is continuous and satisfies $∣ φ (t) ∣ \leq 2 M e^{ω t} ∥ x^{*} ∥ ∥ x ∥$ , because $S, T$ are strongly continuous and exponentially bounded.

2.1F1F2step 1.1

For real $λ > ω$ , [F1] and [F2] give $\int_{0}^{\infty} e^{- λ t} φ (t) d t = x^{*} (\int_{0}^{\infty} e^{- λ t} D (t) x d t) = x^{*} [(R_{A} (λ) - R_{B} (λ)) x] = 0$ .

3.1F3step 1.1step 2.1

By scalar Laplace uniqueness [F3] applied with $σ : = ω$ and $C : = 2 M ∥ x^{*} ∥ ∥ x ∥$ , the continuous function $φ$ vanishes identically: $x^{*} (S (t) x) = x^{*} (T (t) x)$ for every $t \geq 0$ .

4.1F4step 3.1

Since $x^{*} \in X^{*}$ was arbitrary, the dual separates points of $X$ (using HB, [F4]), so $S (t) x = T (t) x$ for every $x$ and every $t \geq 0$ ; that is, $S (t) = T (t)$ for all $t$ .

5.1F1step 4.1∎

If moreover $A = B$ , then both semigroups have exponential bounds and, taking a common pair $M, ω$ for the two bounds (for instance the maxima of the respective constants), their resolvents agree on $(ω, \infty)$ because both are given by the Laplace formula for the same operator; [step 4.1] then gives $S = T$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

55 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

Klaus-Jochen Engel and Rainer Nagel, One-Parameter Semigroups for Linear Evolution Equations, Graduate Texts in Mathematics 194 (complete author-hosted monograph) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)
Mathew A. Johnson, Math 951 Lecture Notes, Chapter 6: Introduction to Semigroup Methods, University of Kansas (complete 37-page chapter) (standard reference, not scraped)