W5: projected CSD dynamics = projective action of a one-parameter unitary family

Category: 3-Local (projected CSD dynamics = projective action of a one-parameter unitary family).

This module is the milestone of the CSD dynamics spine. It shows that the projected ontic flow of a Kähler ontic setup, once the W3 Wigner selection has placed every time-t map on the unitary branch, IS the projective action of a one-parameter unitary family {U_t}. This is the honest Lean-first reading of "projected CSD dynamics recovers finite-dimensional Schrödinger evolution".

What is proved (the achievable core)

• projectedFlow_eq_unitary_family (PROVED, the milestone): given the W3 selection output hU : ∀ t, ProjUnitary d t, the projected flow is the projective action of a one-parameter unitary family: ∃ U : ℝ → unitaryGroup, ∀ t p, d.projectedFlow t p = U t • p. Choice over the per-t existentials (Classical.choice, foundational-triple). The unitary family comes from hU / W3 (the Wigner selection), NOT from flow_preserves_volume: measure-preservation does not imply transition-probability preservation (measure ≠ metric, the §13.2 trap).

• unitaryFamily_projective_representation (PROVED, the ray-level group law): under the explicit ONE-PARAMETER-GROUP hypotheses on the projected flow (d.projectedFlow (s+t) = d.projectedFlow s ∘ d.projectedFlow t, d.projectedFlow 0 = id), the selected unitary family is a PROJECTIVE one-parameter representation: U (s+t) • p = (U s * U t) • p and U 0 • p = p for every p. This is the group law at the projective (ray) level, the level at which the projected flow lives. The group hypotheses are physical inputs, NOT carried by KahlerOnticSetup (its flow field has no one-parameter-group law, by design); they are surfaced as explicit hypotheses.

What is STAGED (the deeper residual, precisely named)

The vector-level U_t = exp(-i t H) for a Hermitian generator H (the Schrödinger form) is NOT claimed here. Two ingredients are missing and named (BOTH SINCE DISCHARGED downstream: S2 by Mathlib/Analysis/Matrix/StoneC1.lean (2026-07-05, C^1 form) and S1 by LF4/PhaseLift.lean (2026-07-07, on the coboundary datum), whose projectedFlow_schrodinger_form is the assembled capstone; this module's staging remarks describe the honest scope of THIS file):

(S1) The projective-to-vector phase lift. The ray-level representation U (s+t) • p = (U s * U t) • p only forces U (s+t) and U s * U t to agree UP TO A PHASE (they act identically on every ray). Promoting this to a genuine vector-level group U (s+t) = U s * U t requires killing the projective phase cocycle c(s,t) ∈ U(1), i.e. a section of U(N) → PU(N) that is a group homomorphism. That lift is a physical / cohomological input not carried by the setup.

(S2) Finite-dimensional Stone's theorem. Even with a genuine vector-level strongly-continuous one-parameter unitary group, recovering the self-adjoint generator H with U_t = exp(-i t H) is Stone's theorem. Mathlib (this toolchain) has Matrix.exp and exp_conjTranspose but NO Stone's theorem for one-parameter unitary groups (Stone* in Mathlib is Stone-Weierstrass / Stone-Cech / Stone-separation, all unrelated). So the generator-recovery direction is unavailable upstream.

The CONVERSE direction IS available and is recorded as a genuine realizability witness: expNegITH_unitary_group shows that for any Hermitian H, t ↦ exp(-i t H) is a genuine vector-level one-parameter unitary GROUP. This certifies the exp(-itH) target form is inhabited (the Schrödinger family is a real object), while making explicit that it is the converse of Stone, not Stone: it constructs U_t FROM H, it does not recover H from an abstract projected flow.

Provenance

Foundational-triple only (propext, Classical.choice, Quot.sound); no busch, no sorry, no native_decide, no new axioms. Reuses W2/W3 (KahlerOnticSetup, ProjUnitary, the Matrix.unitaryGroup action from Unitary.lean) and Mathlib's Matrix.exp; nothing is re-proved.

Part 1: the milestone (projective action of a one-parameter unitary family)

theorem CSD.LF4.projectedFlow_eq_unitary_family {N : ℕ} (d : KahlerOnticSetup N) (hU : ∀ (t : ℝ), ProjUnitary d t) : ∃ (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)), ∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), d.projectedFlow t p = U t • p

The W5 milestone (PROVED). Given the W3 Wigner-selection output hU : ∀ t, ProjUnitary d t (every time-t projected map is on the unitary branch), the projected flow is the projective action of a single one-parameter unitary family {U_t}:

`∃ U : ℝ → unitaryGroup (Fin N) ℂ, ∀ t p, d.projectedFlow t p = U t • p`.

This is choice over the per-t existentials packaged in ProjUnitary (Classical.choice, foundational-triple). The unitary family is supplied by hU / the Wigner selection, NOT by flow_preserves_volume: the projected flow being measure-preserving does not make it transition-probability preserving (measure ≠ metric), so the unitary structure genuinely enters through the W3 FS-isometry posit, not the Liouville field.

Part 2: the ray-level one-parameter projective representation

theorem CSD.LF4.unitaryFamily_projective_representation {N : ℕ} (d : KahlerOnticSetup N) (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (hfam : ∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), d.projectedFlow t p = U t • p) (hgrp : ∀ (s t : ℝ), d.projectedFlow (s + t) = d.projectedFlow s ∘ d.projectedFlow t) (h0 : d.projectedFlow 0 = id) : (∀ (s t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), U (s + t) • p = (U s * U t) • p) ∧ ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), U 0 • p = p

The ray-level group law (PROVED). Under the explicit one-parameter-group hypotheses on the projected flow (hgrp composition, h0 identity), any unitary family U realising the projected flow (hfam) is a PROJECTIVE one-parameter representation:

`U (s + t) • p = (U s * U t) • p`   and   `U 0 • p = p`   for all `p`.

The equalities hold at the RAY level (as maps on ℙ ℂ (EuclideanSpace ℂ (Fin N))); they do NOT assert the vector-level identities U (s+t) = U s * U t, U 0 = 1, which would additionally require killing the projective phase cocycle (residual S1, see the module docstring). The group hypotheses are physical inputs not carried by KahlerOnticSetup; they are surfaced here as explicit arguments.

theorem CSD.LF4.projectedFlow_projective_one_parameter_representation {N : ℕ} (d : KahlerOnticSetup N) (hU : ∀ (t : ℝ), ProjUnitary d t) (hgrp : ∀ (s t : ℝ), d.projectedFlow (s + t) = d.projectedFlow s ∘ d.projectedFlow t) (h0 : d.projectedFlow 0 = id) : ∃ (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)), (∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), d.projectedFlow t p = U t • p) ∧ (∀ (s t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), U (s + t) • p = (U s * U t) • p) ∧ ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), U 0 • p = p

The projected flow, packaged directly as a projective one-parameter representation from the W3 selection plus the group hypotheses: the milestone family and the ray-level group law together.

Part 3 (STAGED): the exp(-itH) converse realizability witness

The Stone direction (recover a Hermitian H with U_t = exp(-i t H) from an abstract projected flow) is unavailable: it needs the phase lift S1 and finite-dim Stone S2, neither in this toolchain. The CONVERSE direction is available and recorded here as a genuine realizability witness: for any Hermitian H, t ↦ exp(-i t H) is a genuine vector-level one-parameter unitary group. This certifies the Schrödinger target form is inhabited, and makes explicit that it is the converse of Stone (it builds U_t from H, it does not recover H).

noncomputable def CSD.LF4.schrodingerGen {N : ℕ} (H : Matrix (Fin N) (Fin N) ℂ) (t : ℝ) : Matrix (Fin N) (Fin N) ℂ

The candidate Schrödinger generator matrix -(i t) H for a time t and a matrix H. When H is Hermitian and t real this is skew-Hermitian, so its matrix exponential is unitary.

Equations

• CSD.LF4.schrodingerGen H t = (-↑t * Complex.I) • H

theorem CSD.LF4.schrodingerGen_star {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (t : ℝ) : (schrodingerGen H t).conjTranspose = -schrodingerGen H t

For Hermitian H, the generator -(i t) H is skew-Hermitian: (schrodingerGen H t)ᴴ = - schrodingerGen H t.

theorem CSD.LF4.schrodingerGen_exp_mem_unitaryGroup {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (t : ℝ) : NormedSpace.exp (schrodingerGen H t) ∈ Matrix.unitaryGroup (Fin N) ℂ

exp(-itH) is unitary (PROVED). For Hermitian H and real t, the matrix exponential exp(schrodingerGen H t) = exp(-i t H) lies in unitaryGroup (Fin N) ℂ: the generator is skew-Hermitian, so (exp A)ᴴ = exp (Aᴴ) = exp (-A) and exp A * exp (-A) = exp 0 = 1.

noncomputable def CSD.LF4.schrodingerUnitary {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (t : ℝ) : ↥(Matrix.unitaryGroup (Fin N) ℂ)

The unitary exp(-i t H) ∈ unitaryGroup as a bundled group element.

Equations

• CSD.LF4.schrodingerUnitary hH t = ⟨NormedSpace.exp (CSD.LF4.schrodingerGen H t), ⋯⟩

theorem CSD.LF4.expNegITH_unitary_group {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) : (∀ (s t : ℝ), schrodingerUnitary hH (s + t) = schrodingerUnitary hH s * schrodingerUnitary hH t) ∧ schrodingerUnitary hH 0 = 1

The exp(-itH) family is a vector-level one-parameter unitary GROUP (PROVED, the converse realizability witness). For Hermitian H, the family U t = exp(-i t H) satisfies U (s + t) = U s * U t and U 0 = 1 as genuine matrix / unitary-group identities (NOT merely up to phase). This certifies the Schrödinger target form exp(-itH) is inhabited.

Honest scope: this is the CONVERSE of Stone (it constructs U_t FROM H); it does NOT recover H from an abstract projected flow. The projected-flow → generator direction remains staged on the phase lift (S1) and finite-dim Stone (S2); see the module docstring.

Non-vacuity on the trivialKahlerOnticSetup witness

theorem CSD.LF4.trivialKahlerOnticSetup_eq_unitary_family (N : ℕ) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : ∃ (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)), ∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), (trivialKahlerOnticSetup N p₀).projectedFlow t p = U t • p

The milestone fires on the inhabitation witness: hU holds (the identity flow is ProjUnitary via 1), so the projected flow is the projective action of the constant unitary family U t = 1. Genuine (id = (1 : _) • ·), not vacuous.

theorem CSD.LF4.trivialKahlerOnticSetup_projective_representation (N : ℕ) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : ∃ (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)), (∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), (trivialKahlerOnticSetup N p₀).projectedFlow t p = U t • p) ∧ (∀ (s t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), U (s + t) • p = (U s * U t) • p) ∧ ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), U 0 • p = p

The full projective one-parameter representation fires on the inhabitation witness: the identity flow IS a one-parameter group (projectedFlow t = id for all t, so composition and identity hold on the nose), so the milestone family U t = 1 is a genuine trivial one-parameter representation.

theorem CSD.LF4.expNegITH_unitary_group_zero (N : ℕ) : (∀ (s t : ℝ), schrodingerUnitary ⋯ (s + t) = schrodingerUnitary ⋯ s * schrodingerUnitary ⋯ t) ∧ schrodingerUnitary ⋯ 0 = 1

The exp(-itH) realizability witness is non-vacuous: the zero generator H = 0 (Hermitian) gives the constant unitary family exp(0) = 1, a genuine one-parameter unitary group. Confirms expNegITH_unitary_group's hypotheses are satisfiable.