Finite-dimensional Stone's theorem (C¹ and continuity-only forms)

Category: 1-Mathlib (Finite-dimensional Stone's theorem).

Glossary: https://glossary.constraintsurfacedynamics.com/stone-theorem/ Plain-language, CSD-role and formal statements of Stone's theorem, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh. On upstreaming: this is a Category 1 file. Strip this Glossary block before any Mathlib or Physlib PR; a personal project link has no place in a canonical header.

A one-parameter unitary group of N x N complex matrices is t ↦ exp (t • A) for its skew-Hermitian generator A. This is the load-bearing content of Stone's theorem in finite dimensions: the group IS the exponential of its generator.

Mathlib has no Stone theorem (the Stone* names there are Stone-Weierstrass / Stone-Cech / Stone separation). This file supplies the forward direction, first under a smoothness hypothesis (stone_c1), then — the full-continuity strengthening (stone_continuous, 2026-07-23) — for a merely strongly continuous group, deriving the differentiability rather than assuming it (integral averaging + Fundamental Theorem of Calculus + invertibility of ∫₀ˢ U near 0). Together they close the CSD dynamics-spine residue W5-S2.

Main results

• Matrix.StoneC1.eq_exp_of_hasDeriv : ODE-uniqueness core. If U' t = U t * A and U 0 = 1, then U t = exp (t • A). This recovers the generator from the group.
• Matrix.StoneC1.exp_smul_unitary : skew-Hermitian A gives each exp (t • A) unitary ((exp (t • A))ᴴ * exp (t • A) = 1).
• Matrix.StoneC1.stone_c1 : the packaged C^1 Stone theorem. From star A = -A, ∀ t, HasDerivAt U (U t * A) t, U 0 = 1, conclude ∀ t, U t = exp (t • A) and each U t is unitary.
• Matrix.StoneC1.stone_continuous : the continuity-only Stone theorem. From continuity of U, U 0 = 1, the group law U (s+t) = U s * U t, and each U t unitary, conclude ∃ A skew-Hermitian with ∀ t, U t = exp (t • A) — no differentiability assumed.
• Matrix.StoneC1.trivial_group, Matrix.StoneC1.skew_witness : non-vacuity round-trips.

Implementation notes

NormedSpace.exp is field-independent in current Mathlib (a single-argument exp (x : 𝔸)), so it is written unqualified-by-field as NormedSpace.exp (t • A).

The route is ODE uniqueness (ODE_solution_unique_univ, Gronwall) against the reference solution t ↦ exp (t • A) whose derivative is hasDerivAt_exp_smul_const. No integral averaging, no continuity-to-differentiability step.

The matrix norm is the C^*-algebra L2-operator norm (open scoped Matrix.Norms.L2Operator), NOT the plain operator or Frobenius norm. This is load-bearing: hasDerivAt_exp_smul_const needs CompleteSpace (Matrix ...), and under the plain operator / Frobenius scopes the finite-dimensional completeness instance does not unify with the scoped NormedAddCommGroup (an instance diamond), so synthesis fails. The C^*-algebra norm carries completeness by definition, so CompleteSpace is automatic with no diamond, and norm_mul_le (submultiplicativity) still holds.

The scalar-action side conditions (0 • A = 0, t • (-A) = -(t • A)) are discharged with module, not the generic zero_smul / smul_neg rewrites: under the scoped matrix-norm the SMul ℝ (Matrix ...) instance path defeats those rewrites, while module normalises through the correct instance.

Declarations use dotted Matrix.StoneC1.* names at top level rather than a namespace ... end block (a namespace block can select a spurious SMul diamond).

Renamed CSD.StoneC1.* → Matrix.StoneC1.* 2026-08-06 (BACKLOG B6 readiness): this file and DuhamelBound.lean were the staged tree's only real CSD-namespace content, blocking upstreaming. AxiomAudit pins and all corpus consumers updated in the same commit.

theorem Matrix.StoneC1.eq_exp_of_hasDeriv {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (U : ℝ → Matrix (Fin N) (Fin N) ℂ) (hderiv : ∀ (t : ℝ), HasDerivAt U (U t * A) t) (hU0 : U 0 = 1) (t : ℝ) : U t = NormedSpace.exp (t • A)

ODE-uniqueness core. A C^1 curve solving Y' = Y * A with Y 0 = 1 is the matrix exponential t ↦ exp (t • A). Reuses ODE_solution_unique_univ (Gronwall) with the ‖A‖-Lipschitz linear field Y ↦ Y * A and hasDerivAt_exp_smul_const for the reference solution.

theorem Matrix.StoneC1.exp_smul_unitary {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (hA : star A = -A) (t : ℝ) : (NormedSpace.exp (t • A)).conjTranspose * NormedSpace.exp (t • A) = 1

For a skew-Hermitian generator A (star A = -A), each exp (t • A) is unitary. Reuses Matrix.exp_conjTranspose and Matrix.exp_add_of_commute.

theorem Matrix.StoneC1.stone_c1 {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (U : ℝ → Matrix (Fin N) (Fin N) ℂ) (hA : star A = -A) (hderiv : ∀ (t : ℝ), HasDerivAt U (U t * A) t) (hU0 : U 0 = 1) : (∀ (t : ℝ), U t = NormedSpace.exp (t • A)) ∧ ∀ (t : ℝ), (U t).conjTranspose * U t = 1

C^1 finite-dimensional Stone theorem. A differentiable one-parameter unitary group with skew-Hermitian generator A is t ↦ exp (t • A), and every U t is unitary. The generator is recovered from the group.

theorem Matrix.StoneC1.trivial_group (t : ℝ) : (fun (x : ℝ) => 1) t = NormedSpace.exp (t • 0)

Non-vacuity: the trivial group. A = 0 gives the constant unit curve, whose generator is recovered as 0 and U t = exp (t • 0) = 1.

theorem Matrix.StoneC1.skew_witness : star (Complex.I • 1) = -(Complex.I • 1) ∧ ∀ (t : ℝ), (NormedSpace.exp (t • Complex.I • 1)).conjTranspose * NormedSpace.exp (t • Complex.I • 1) = 1

Non-vacuity: a concrete skew-Hermitian generator A = I • 1 on Fin 2. The skew-Hermitian hypothesis holds, so exp (t • A) is a genuine unitary group.

theorem Matrix.StoneC1.apply_zero_eq_one {N : ℕ} (U : ℝ → Matrix (Fin N) (Fin N) ℂ) (hgroup : ∀ (s t : ℝ), U (s + t) = U s * U t) (hunit : ∀ (t : ℝ), (U t).conjTranspose * U t = 1) : U 0 = 1

★ A one-parameter unitary group is normalised at zero automatically.

U 0 = 1 follows from the group law and unitarity alone: U 0 = U 0 * U 0 by the group law at (0,0), and U 0 is left-invertible by unitarity, so cancelling gives 1.

Recorded as part of the CL-032 criterion-6 audit (2026-08-24), which is where the redundancy was noticed. stone_continuous still takes hU0 — see its docstring.

theorem Matrix.StoneC1.stone_continuous {N : ℕ} (U : ℝ → Matrix (Fin N) (Fin N) ℂ) (hcont : Continuous U) (hU0 : U 0 = 1) (hgroup : ∀ (s t : ℝ), U (s + t) = U s * U t) (hunit : ∀ (t : ℝ), (U t).conjTranspose * U t = 1) : ∃ (A : Matrix (Fin N) (Fin N) ℂ), star A = -A ∧ ∀ (t : ℝ), U t = NormedSpace.exp (t • A)

Continuity-only finite-dimensional Stone theorem. A strongly continuous one-parameter unitary group U : ℝ → Matrix N N ℂ is t ↦ exp (t • A) for a skew-Hermitian generator A. No differentiability is assumed — it is derived by the integral-averaging argument (FTC + invertibility of ∫₀ˢ U near 0) and fed to the C¹ core eq_exp_of_hasDeriv.

⚠️ hU0 is redundant — it is derivable from hgroup and hunit by Matrix.StoneC1.apply_zero_eq_one (found in the CL-032 criterion-6 audit, 2026-08-24). It is retained in the signature because it is free at every call site and makes the hypothesis list read as the standard four-part statement of the theorem. Anyone minimising hypotheses should drop it and call apply_zero_eq_one internally; nothing outside this file passes it.