The phase group's generator is its multiplication operator

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #64(iii), and a correction to that row: it said it waits on Stone's theorem. It does not.

★★★ hasDerivAt_phaseGroup_apply — d/dt e^{−itκ} f = −i·κ·e^{−itκ} f in L², for every f with κ·f ∈ L². The group was already in hand explicitly and self-adjointness of the generator came from #64(i)+(ii); what was missing is only that the two are related, and that is this file:

• ★★★ hasDerivAt_phaseGroup_apply — the derivative, on the natural domain;
• ★★★ hasDerivAt_phaseGroup_freeSymbolOp — the Schrödinger equation for the free particle, i ∂_t ψ_t = H₀ ψ_t with H₀ the self-adjoint operator of #64(i), in the momentum representation, and ★★★ hasDerivAt_fourierGroup_freePositionOp the same in the position representation, where the generator is freePositionOp — transferred through #64(i)'s unitary conjugation rather than recomputed;
• ★ phaseGroup_mem_mulDomain — the group preserves the domain, which is what an interacting version would need next, and which is free here because a phase commutes with a multiplication.

Why this is not Stone's theorem

Stone's theorem is an existence statement: every self-adjoint operator generates a unitary group. Here the group is already explicit (phaseGroup, with its group law, unitarity and strong continuity all proved in SchrodingerGroup.lean), so nothing has to be constructed — the content is the identification of its derivative with a given operator. The corpus does have Stone's theorem in finite dimensions (Analysis/Matrix/StoneC1.lean, both the C¹ and the continuity-only forms); the infinite-dimensional existence theorem is still absent and is not needed by #64.

The proof in one line

The difference between the slope and the claimed derivative is multiplication by ω_h(x) = (e^{−ihκ(x)} − 1)/h + iκ(x), so its squared L² norm is the scalar integral ∫ ‖f x‖²·‖ω_h(x)‖². That integrand tends to 0 pointwise (the scalar exponential's derivative) and is dominated by 4‖κ(x)f(x)‖² — which is integrable precisely because f is in the domain. So the domain hypothesis is not a technical convenience: it is the dominating function.

Honest scope

⚠️ The interacting generator is not here. SchrodingerGroup.schrodinger already exists as a unitary propagator for a bounded potential (Dyson series, Duhamel, Trotter, in Semigroup/BoundedPerturbation.lean), and #64(ii) made H₀ + V self-adjoint, but differentiating the Duhamel integral — showing the mild solution is a classical one — needs more than the domain invariance proved here. That is #129.

⚠️ One derivative, not a flow statement. Nothing here says the orbit is the unique solution of the Cauchy problem; uniqueness for the free equation would follow from unitarity by the standard energy argument and is not stated.

References: SchrodingerGroup.lean (phaseGroup, fourierGroup, schrodinger), FreeHamiltonian.lean (#64(i)(ii), freeSymbolOp, freePositionOp), InnerProductSpace/LinearPMapConj.lean (the conjugation the position form rides on), Matrix/StoneC1.lean (finite-dimensional Stone); specs/BACKLOG.md #64, #129.

The squared norm as a scalar integral

theorem SchrodingerGroup.norm_sq_eq_integral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (u : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖u‖ ^ 2 = ∫ (x : E), ‖↑↑u x‖ ^ 2

The scalar phase, differentiated

theorem SchrodingerGroup.norm_phaseFun_sub_one_le {E : Type u_1} (κ : E → ℝ) (t : ℝ) (x : E) : ‖phaseFun κ t x - 1‖ ≤ |t| * |κ x|

The phase moves by at most |t|·|κ|, globally — the estimate that makes the dominating function the domain condition.

theorem SchrodingerGroup.hasDerivAt_phaseFun {E : Type u_1} (κ : E → ℝ) (x : E) (t : ℝ) : HasDerivAt (fun (h : ℝ) => phaseFun κ h x) (-Complex.I * ↑(κ x) * phaseFun κ t x) t

The scalar derivative at the identity: d/dh e^{−ihκ(x)} = −iκ(x).

The group's derivative

noncomputable def SchrodingerGroup.phaseDefect {E : Type u_1} (κ : E → ℝ) (h : ℝ) (x : E) : ℂ

The defect between the slope and the claimed derivative, as a scalar multiplier.

Equations

• SchrodingerGroup.phaseDefect κ h x = h⁻¹ • (SchrodingerGroup.phaseFun κ h x - 1) + Complex.I * ↑(κ x)

theorem SchrodingerGroup.norm_phaseDefect_le {E : Type u_1} {κ : E → ℝ} {h : ℝ} (hh : h ≠ 0) (x : E) : ‖phaseDefect κ h x‖ ≤ 2 * |κ x|

theorem SchrodingerGroup.measurable_phaseDefect {E : Type u_1} [MeasurableSpace E] {κ : E → ℝ} (hκ : Measurable κ) (h : ℝ) : Measurable (phaseDefect κ h)

theorem SchrodingerGroup.tendsto_phaseDefect {E : Type u_1} (κ : E → ℝ) (x : E) : Filter.Tendsto (fun (h : ℝ) => phaseDefect κ h x) (nhdsWithin 0 {0}ᶜ) (nhds 0)

The group's derivative on the domain

f is in the domain when κ·f is again in L², and that product is taken as data: the hypothesis hg says g is the product. The dominating function of the convergence below is 4‖g‖², so the domain hypothesis is not a convenience — it is what makes the dominated convergence available.

theorem SchrodingerGroup.coeFn_slope_phaseGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {κ : E → ℝ} (hκ : Measurable κ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (t s : ℝ) : ↑↑(slope (fun (r : ℝ) => (phaseGroup hκ r) f) t s) =ᵐ[MeasureTheory.volume] fun (x : E) => phaseFun κ t x * ↑↑f x * (s - t)⁻¹ • (phaseFun κ (s - t) x - 1)

The slope of the group, as multiplication by the defect.

theorem SchrodingerGroup.hasDerivAt_phaseGroup_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {κ : E → ℝ} (hκ : Measurable κ) (f g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hg : ↑↑g =ᵐ[MeasureTheory.volume] fun (x : E) => ↑(κ x) * ↑↑f x) (t : ℝ) : HasDerivAt (fun (s : ℝ) => (phaseGroup hκ s) f) (-Complex.I • (phaseGroup hκ t) g) t

★★★ The generator of the phase group is multiplication by its symbol: on the natural domain, d/dt e^{−itκ} f = −i·κ·e^{−itκ} f in L².

The group preserves the domain

A phase commutes with a multiplication, so this is free — and it is what an interacting version would need, since the Duhamel integrand has to stay in the domain.

theorem SchrodingerGroup.phaseGroup_mem_mulDomain {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {κ : E → ℝ} (hκ : Measurable κ) (f : ↥(MeasureTheory.L2.mulOp κ).domain) (t : ℝ) : (phaseGroup hκ t) ↑f ∈ (MeasureTheory.L2.mulOp κ).domain

The free Schrödinger equation, in both representations

The generator is the self-adjoint operator of #64(i), not a fresh object: these two theorems are what make "H₀ generates the free dynamics" a statement rather than a name.

theorem SchrodingerGroup.hasDerivAt_phaseGroup_freeSymbolOp (f : ↥freeSymbolOp.domain) (t : ℝ) : HasDerivAt (fun (s : ℝ) => (phaseGroup ⋯ s) ↑f) (-Complex.I • (phaseGroup ⋯ t) (↑freeSymbolOp f)) t

★★★ The free Schrödinger equation in the momentum representation: the phase group's derivative is −i times the free Hamiltonian, which is freeSymbolOp — self-adjoint by #64(i).

theorem SchrodingerGroup.freePositionOp_apply_fourierL2 (f : ↥freeSymbolOp.domain) (h : fourierL2.symm ↑f ∈ freePositionOp.domain) : ↑freePositionOp ⟨fourierL2.symm ↑f, h⟩ = fourierL2.symm (↑freeSymbolOp f)

The conjugated generator at an image point, in the vocabulary this file uses.

theorem SchrodingerGroup.hasDerivAt_fourierGroup_freePositionOp (f : ↥freeSymbolOp.domain) (h : fourierL2.symm ↑f ∈ freePositionOp.domain) (t : ℝ) : HasDerivAt (fun (s : ℝ) => (fourierGroup ⋯ s) (fourierL2.symm ↑f)) (-Complex.I • (fourierGroup ⋯ t) (↑freePositionOp ⟨fourierL2.symm ↑f, h⟩)) t

★★★ The free Schrödinger equation in the position representation, i ∂_t ψ = H₀ψ with H₀ the conjugated self-adjoint operator freePositionOp of #64(i). The proof applies the Fourier isometry to the momentum form — the conjugation does the work, nothing is recomputed.