The Lean 4 theorem `timeEvoU_one` in the `?` chapter of the timepiece formalization

import Theorems.Thm_BookProof_ChapterConservative_timeEvo_mem_unitaryGroup

import Theorems.Thm_BookProof_ChapterConservative_timeEvo_add


import Theorems.Thm_BookProof_ChapterConservative_timeEvo_zero

import Definitions.Def_ChapterConservative
import Mathlib


/-!
# Chapter "Wave-function parametrization of a probability measure", §7 —
# Symmetries and unitary representations

This file formalizes the self-contained core of the book's section
*"7. Symmetries and unitary representations"* (`book.tex` line ~1857), of the
main-conclusion chapter *"Wave-function parametrization of a probability
measure"*.

The book states: *"When a subset of canonical transformations forms a group,
such subset is always a linear unitary representation of a group which is then
called symmetry group"*, and (in §8) that *"any unitary automorphism can be
defined as a time-evolution"*. The concrete self-contained instance is the
one-parameter **time-translation group**: the family `U(t) = e^{iHt}`
(`ChapterConservative.timeEvo`) generated by a self-adjoint Hamiltonian `H` is a
group homomorphism from the additive real line `(ℝ, +)` into the unitary group,
i.e. a **unitary representation of the one-parameter symmetry group `ℝ`**.

We package this as a `MonoidHom` from `Multiplicative ℝ` (the additive reals
viewed multiplicatively) into `Matrix.unitaryGroup n ℂ`:

* `timeEvoU` — the time-evolution as a bundled element of the unitary group;
* `timeEvoU_one` / `timeEvoU_mul` — it sends `0 ↦ 1` and `s + t ↦ U(s)·U(t)`;
* `timeEvoRep` — the one-parameter unitary representation
  `ℝ → unitaryGroup n ℂ`, `t ↦ e^{iHt}`, as a group homomorphism;
* `timeEvoRep_apply` — its underlying matrix is `timeEvo H t`.

Everything is `sorry`-free and `axiom`-free (only `propext`, `Classical.choice`,
`Quot.sound`).
-/

open scoped Matrix

namespace BookProof.ChapterSymmetryRep

open BookProof.ChapterConservative

variable {n : Type*} [Fintype n] [DecidableEq n]

/-- The time-evolution `U(t) = e^{iHt}` as a bundled element of the unitary
group, for a self-adjoint Hamiltonian `H`. -/
noncomputable def timeEvoU (H : Matrix n n ℂ) (hH : H.IsHermitian) (t : ℝ) :
    Matrix.unitaryGroup n ℂ :=
  ⟨timeEvo H t, timeEvo_mem_unitaryGroup H hH t⟩

/-- The time-evolution at `t = 0` is the identity of the unitary group. -/
theorem timeEvoU_one (H : Matrix n n ℂ) (hH : H.IsHermitian) :
    timeEvoU H hH 0 = 1 := by
  ext; simp [timeEvoU, timeEvo_zero]

/-- The one-parameter group law inside the unitary group. -/
theorem timeEvoU_mul (H : Matrix n n ℂ) (hH : H.IsHermitian) (s t : ℝ) :
    timeEvoU H hH (s + t) = timeEvoU H hH s * timeEvoU H hH t := by
  exact Subtype.ext ( timeEvo_add H s t |> Eq.symm )

/-- The one-parameter **unitary representation** of the additive symmetry group
`ℝ` generated by a self-adjoint Hamiltonian `H`: `t ↦ e^{iHt}`, a group
homomorphism from `(ℝ, +)` (viewed multiplicatively) into `unitaryGroup n ℂ`. -/
noncomputable def timeEvoRep (H : Matrix n n ℂ) (hH : H.IsHermitian) :
    Multiplicative ℝ →* Matrix.unitaryGroup n ℂ where
  toFun t := timeEvoU H hH (Multiplicative.toAdd t)
  map_one' := timeEvoU_one H hH
  map_mul' s t := timeEvoU_mul H hH (Multiplicative.toAdd s) (Multiplicative.toAdd t)



end BookProof.ChapterSymmetryRep