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 assumed: the unitary class is a posit

ProjUnitary enters as a hypothesis, and this module proves an implication, not the antecedent. projectedFlow_eq_unitary_family is literally choose U hU'; exact ⟨U, hU'⟩: it selects the family from hU and establishes nothing about why the flow should be unitary. With projectedFlow_schrodinger_form_of_continuous_flow (ledger CL-063) the corpus therefore proves "unitary ⇒ Schrödinger" and posits "unitary" — registered as Posit 6 in specs/POSITS.md (the external review's Part II numbers it Posit 4).

The posit is motivated, not arbitrary. Nonlinear projective evolution, combined with tensor structure and local Born statistics, permits superluminal signalling (Gisin 1990), which no-signalling forbids. So the unitary class is the one compatible with a constraint the corpus independently respects. ⚠️ That is a reason to believe the posit, not a derivation of it: no such derivation is in the corpus. One is available if wanted (Gisin's argument run in reverse), queued as an optional upgrade in specs/cr-queue.md; until it lands, "Schrödinger evolution is derived" should be read as "derived from the unitary class", never unqualified.

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).

The generator -(it)H, the bundled unitary exp(-itH) and its one-parameter group law moved to the Category-1 module Mathlib/Analysis/Matrix/SchrodingerUnitary.lean on 2026-09-16 (Matrix.schrodingerGen, Matrix.schrodingerUnitary, Matrix.expNegITH_unitary_group), so that the manifold-level Schrödinger flow on ℂℙⁿ is Category 1 by closure. The names are re-exported here; every consumer reads as before.

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.