W5-S1: the projective-to-vector phase lift

Category: 3-Programme (CSD dynamics spine, W5 residual S1).

Glossary: https://glossary.constraintsurfacedynamics.com/schrodinger-from-records/ Plain-language, CSD-role and formal statements of Schrodinger dynamics from record statistics, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

This module discharges the S1 residual of W5 (ProjectedDynamics.lean): it makes the U(1) phase cocycle of the projected-flow unitary family a real object, proves it obeys the 2-cocycle law, and shows that a trivialising phase function (the coboundary datum) upgrades the ray-level projective representation to a GENUINE vector-level one-parameter unitary group realising the projected flow. Wired to the W5-S2 finite-dimensional Stone theorem (StoneC1.lean), this yields the full Schrödinger form: the projected flow is p ↦ exp(-itH) • p for a Hermitian generator H.

What is proved

• projectedFlow_phase_cocycle: the cocycle EXISTS. Given a unitary family realising a one-parameter projected flow, phase rigidity (Projectivization.exists_unit_smul_of_smul_eq_smul, the kernel of U(N) → PU(N) is the circle) extracts c : ℝ → ℝ → ℂ with ‖c s t‖ = 1 and U (s+t) = c s t • (U s * U t) at the matrix level. This names the obstruction: the family is a genuine group iff c can be killed.
• phase_cocycle_identity: any such c obeys the 2-cocycle law c s (t+u) * c t u = c (s+t) u * c s t (associativity, N ≠ 0).
• projectedFlow_phase_lift (the S1 theorem): a phase function b : ℝ → ℂ, ‖b t‖ = 1, trivialising the cocycle (c s t * b (s+t) = b s * b t, i.e. c = δb is a coboundary) rescales the family to phaseLiftFamily U b hb : ℝ → unitaryGroup which (i) realises the SAME projected flow (phases act trivially on rays), (ii) satisfies the vector-level group law V (s+t) = V s * V t on the nose, and (iii) has V 0 = 1. The projective phase freedom is killed.
• projectedFlow_schrodinger_form (the W5 capstone, S1 × S2): adding the C^1 datum (a skew-Hermitian A with V' t = V t * A), the S2 Stone theorem recovers the generator: there is a Hermitian H (namely i A) with d.projectedFlow t p = schrodingerUnitary hH t • p, i.e. the projected CSD flow IS exp(-itH)-conjugation on rays. This is the Schrödinger form of the W-series chain.

What is HYPOTHESIS (honest posture, load-bearing)

The coboundary datum b is the S1 physical/cohomological input, staged exactly as W3 staged its clopen datum: H²(ℝ, U(1)) does not vanish algebraically (antisymmetric bicharacters survive on ℝ as a ℚ-vector space), so the bare ray-level group law genuinely does NOT force a vector lift; killing c requires a regularity/cohomological input (Bargmann: for CONTINUOUS cocycles H²_cont(ℝ, U(1)) = 0; formalising that is a named follow-on, not claimed here). Likewise the C^1 datum in the capstone is the S2 smoothness posit. Both are surfaced as explicit hypotheses on an explicit family U / cocycle c — NOT extracted by choice inside the theorem — so a caller who owns concrete data can discharge them.

Non-vacuity

On trivialKahlerOnticSetup the whole chain fires end-to-end with the constant family U = 1, trivial cocycle c = 1, trivial phase b = 1, and zero generator: trivialKahlerOnticSetup_phase_lift (the lift) and trivialKahlerOnticSetup_schrodinger_form (the full Schrödinger form with H = 0). Genuine, not vacuous: every hypothesis is discharged concretely.

Provenance

Foundational-triple only (propext, Classical.choice, Quot.sound); no busch, no sorry, no native_decide, no new axioms. Reuses W5 (ProjectedDynamics), the phase-rigidity Mathlib layer (PhaseRigidity), and the W5-S2 Stone theorem (StoneC1); nothing is re-proved.

Part 1: the cocycle exists (the obstruction, named)

theorem CSD.LF4.projectedFlow_phase_cocycle {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) : ∃ (c : ℝ → ℝ → ℂ), (∀ (s t : ℝ), ‖c s t‖ = 1) ∧ ∀ (s t : ℝ), ↑(U (s + t)) = c s t • (↑(U s) * ↑(U t))

The U(1) phase cocycle exists. For a unitary family realising a one-parameter projected flow, each pair of times yields (by phase rigidity: the kernel of U(N) → PU(N) is the circle) a unit-modulus scalar c s t with U (s+t) = c s t • (U s * U t) at the matrix level. The family is a genuine vector-level group precisely when c can be trivialised; c is the named obstruction that residual S1 must kill.

theorem CSD.LF4.smul_unitary_cancel {N : ℕ} (hN : N ≠ 0) {x y : ℂ} (W : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (h : x • ↑W = y • ↑W) : x = y

Scalars acting on a fixed unitary are injective (N ≠ 0): cancel a common unitary factor in a scalar identity by multiplying with its star and evaluating a diagonal entry.

theorem CSD.LF4.phase_cocycle_identity {N : ℕ} (hN : N ≠ 0) (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (c : ℝ → ℝ → ℂ) (hc : ∀ (s t : ℝ), ↑(U (s + t)) = c s t • (↑(U s) * ↑(U t))) (s t u : ℝ) : c s (t + u) * c t u = c (s + t) u * c s t

The 2-cocycle law. Any unit-phase family c relating U (s+t) to U s * U t obeys c s (t+u) * c t u = c (s+t) u * c s t — associativity of the unitary family forces the cocycle identity. (For N = 0 the scalar is not pinned by the matrix equation, hence the N ≠ 0 hypothesis.)

Part 2: the phase lift (the S1 theorem)

noncomputable def CSD.LF4.phaseLiftFamily {N : ℕ} (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (b : ℝ → ℂ) (hb : ∀ (t : ℝ), ‖b t‖ = 1) (t : ℝ) : ↥(Matrix.unitaryGroup (Fin N) ℂ)

The rescaled family t ↦ b t • U t: the candidate vector-level group obtained by absorbing the phase function b into the unitary family.

Equations

• CSD.LF4.phaseLiftFamily U b hb t = ⟨b t • ↑(U t), ⋯⟩

@[simp]

theorem CSD.LF4.phaseLiftFamily_val {N : ℕ} (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (b : ℝ → ℂ) (hb : ∀ (t : ℝ), ‖b t‖ = 1) (t : ℝ) : ↑(phaseLiftFamily U b hb t) = b t • ↑(U t)

theorem CSD.LF4.cob_of_phaseLiftFamily_group {N : ℕ} [NeZero N] (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (c : ℝ → ℝ → ℂ) (hc : ∀ (s t : ℝ), ↑(U (s + t)) = c s t • (↑(U s) * ↑(U t))) (b : ℝ → ℂ) (hb : ∀ (t : ℝ), ‖b t‖ = 1) (hgroup : ∀ (s t : ℝ), phaseLiftFamily U b hb (s + t) = phaseLiftFamily U b hb s * phaseLiftFamily U b hb t) (s t : ℝ) : c s t * b (s + t) = b s * b t

★ The coboundary hypothesis is NECESSARY, not merely sufficient.

If the rescaled family t ↦ b t • U t is a genuine vector-level group, then b must trivialise the cocycle: c s t * b (s+t) = b s * b t. So projectedFlow_phase_lift's hcob is not a convenient sufficient condition that a cleverer proof might drop — it is equivalent to the conclusion it buys.

The argument is a cancellation: both sides are scalar multiples of the same invertible matrix U s * U t, and a unitary is nonzero, so the scalars agree.

Recorded as the CL-015 mutation study (2026-08-24). hb is load-bearing for a different and more basic reason: without ‖b t‖ = 1 the rescaled matrix is not unitary, so phaseLiftFamily cannot be formed at all and the conclusion cannot even be stated.

theorem CSD.LF4.projectedFlow_phase_lift {N : ℕ} (d : KahlerOnticSetup N) (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (hfam : ∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), d.projectedFlow t p = U t • p) (c : ℝ → ℝ → ℂ) (hc : ∀ (s t : ℝ), ↑(U (s + t)) = c s t • (↑(U s) * ↑(U t))) (b : ℝ → ℂ) (hb : ∀ (t : ℝ), ‖b t‖ = 1) (hcob : ∀ (s t : ℝ), c s t * b (s + t) = b s * b t) : (∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), d.projectedFlow t p = phaseLiftFamily U b hb t • p) ∧ (∀ (s t : ℝ), phaseLiftFamily U b hb (s + t) = phaseLiftFamily U b hb s * phaseLiftFamily U b hb t) ∧ phaseLiftFamily U b hb 0 = 1

The projective-to-vector phase lift (residual S1, discharged on the coboundary datum). If the phase cocycle c of the unitary family is a coboundary — trivialised by a unit-phase function b via c s t * b (s+t) = b s * b t — then the rescaled family V t = b t • U t is a GENUINE vector-level one-parameter unitary group (V (s+t) = V s * V t and V 0 = 1 as unitary-group identities, NOT merely up to phase) realising the same projected flow. The coboundary datum is the honest S1 residual input: H²(ℝ, U(1)) does not vanish algebraically, so some such input is genuinely required (see the module docstring).

Part 3: the W5 capstone (S1 × S2 ⇒ the Schrödinger form)

theorem CSD.LF4.projectedFlow_schrodinger_form {N : ℕ} (d : KahlerOnticSetup N) (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (hfam : ∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), d.projectedFlow t p = U t • p) (c : ℝ → ℝ → ℂ) (hc : ∀ (s t : ℝ), ↑(U (s + t)) = c s t • (↑(U s) * ↑(U t))) (b : ℝ → ℂ) (hb : ∀ (t : ℝ), ‖b t‖ = 1) (hcob : ∀ (s t : ℝ), c s t * b (s + t) = b s * b t) (A : Matrix (Fin N) (Fin N) ℂ) (hA : star A = -A) (hderiv : ∀ (t : ℝ), HasDerivAt (fun (τ : ℝ) => ↑(phaseLiftFamily U b hb τ)) (↑(phaseLiftFamily U b hb t) * A) t) : ∃ (H : Matrix (Fin N) (Fin N) ℂ) (hH : H.IsHermitian), ∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), d.projectedFlow t p = schrodingerUnitary hH t • p

The W5 capstone: projected CSD flow in Schrödinger form. Combining the S1 coboundary datum (b trivialises the phase cocycle c) with the S2 C^1 datum (the lifted family solves V' = V * A for a skew-Hermitian generator A), the finite-dimensional Stone theorem recovers the Hermitian generator: there is a Hermitian H (namely i A) with

`d.projectedFlow t p = schrodingerUnitary hH t • p`,

i.e. the projected flow IS conjugation by exp(-itH) on rays — the Schrödinger form of the W-series chain. Both data are explicit physical inputs (S1 cohomological, S2 smoothness), staged as hypotheses on an explicit family, exactly as W3 staged its clopen datum.

theorem CSD.LF4.projectedFlow_schrodinger_form_of_continuous {N : ℕ} (d : KahlerOnticSetup N) (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (hfam : ∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), d.projectedFlow t p = U t • p) (c : ℝ → ℝ → ℂ) (hc : ∀ (s t : ℝ), ↑(U (s + t)) = c s t • (↑(U s) * ↑(U t))) (b : ℝ → ℂ) (hb : ∀ (t : ℝ), ‖b t‖ = 1) (hcob : ∀ (s t : ℝ), c s t * b (s + t) = b s * b t) (hcont : Continuous fun (τ : ℝ) => ↑(phaseLiftFamily U b hb τ)) : ∃ (H : Matrix (Fin N) (Fin N) ℂ) (hH : H.IsHermitian), ∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), d.projectedFlow t p = schrodingerUnitary hH t • p

The Schrödinger form from a continuous projective flow (S2 discharged).

Same conclusion as projectedFlow_schrodinger_form, but the smoothness datum (A, hA, hderiv) is replaced by plain continuity of the lifted family. The finite-dimensional continuity-only Stone theorem (Matrix.StoneC1.stone_continuous, which derives smoothness by integral averaging) supplies the generator, so no C¹ input is posited.

This is the consumer stone_continuous was built for: before this, the theorem was proved and unused, and the capstones still took the derivative datum. Only the S1 coboundary datum (hcob) remains staged here.

theorem CSD.LF4.projectedFlow_schrodinger_form_of_continuous_flow {N : ℕ} (d : KahlerOnticSetup N) (hN : 0 < N) (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (hfam : ∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), d.projectedFlow t p = U t • p) (hUcont : Continuous fun (t : ℝ) => ↑(U t)) (c : ℝ → ℝ → ℂ) (hc : ∀ (s t : ℝ), ↑(U (s + t)) = c s t • (↑(U s) * ↑(U t))) : ∃ (H : Matrix (Fin N) (Fin N) ℂ) (hH : H.IsHermitian), ∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), d.projectedFlow t p = schrodingerUnitary hH t • p

★★ The Schrödinger form from continuity alone (S1 and S2 discharged).

The end of the W-series staging. Neither the coboundary datum (S1) nor the smoothness datum (S2) is posited: continuity of the projective flow supplies both.

• S1 dies by Matrix.ProjectiveLift.exists_continuous_phase_trivialisation — for a one-parameter group in finite dimensions the phase cocycle is automatically a coboundary (Λ²(ℝ) = 0; the proof is determinants + the circle covering lift, and needs no Bargmann theorem). Crucially it returns a continuous b.
• S2 then dies by Matrix.StoneC1.stone_continuous, whose missing hypothesis was exactly that continuity.

What remains conditional on the chain is hfam (that the projected flow IS conjugation by a unitary family) — the transition-probability-preservation input, not a cohomological or smoothness posit.

The Σ-level capstone: the ontic flow projects to Schrödinger evolution

The ray-level projectedFlow_schrodinger_form above is a statement about d.projectedFlow alone. This next theorem is the one that makes the sector substrate LOAD-BEARING: it consumes d.projectable (the descent equation pi (flow t x) = projectedFlow t (pi x)) together with the ontic flow d.flow and the projection d.pi to conclude that the DETERMINISTIC Σ-flow, pushed to ray space through π, is exp(-itH)-conjugation. This is the honest "Schrödinger dynamics from the posited ontic sector" statement — the whole point of packaging the dynamics as a KahlerOnticSetup.

theorem CSD.LF4.sigmaFlow_schrodinger_form {N : ℕ} (d : KahlerOnticSetup N) (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (hfam : ∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), d.projectedFlow t p = U t • p) (c : ℝ → ℝ → ℂ) (hc : ∀ (s t : ℝ), ↑(U (s + t)) = c s t • (↑(U s) * ↑(U t))) (b : ℝ → ℂ) (hb : ∀ (t : ℝ), ‖b t‖ = 1) (hcob : ∀ (s t : ℝ), c s t * b (s + t) = b s * b t) (A : Matrix (Fin N) (Fin N) ℂ) (hA : star A = -A) (hderiv : ∀ (t : ℝ), HasDerivAt (fun (τ : ℝ) => ↑(phaseLiftFamily U b hb τ)) (↑(phaseLiftFamily U b hb t) * A) t) : ∃ (H : Matrix (Fin N) (Fin N) ℂ) (hH : H.IsHermitian), ∀ (t : ℝ) (x : d.Sigma), d.pi (d.flow t x) = schrodingerUnitary hH t • d.pi x

The Σ-level Schrödinger capstone (PROVED; the substrate-consuming form). Under the same S1 (coboundary) + S2 (C¹) data as projectedFlow_schrodinger_form, the projection of the deterministic ontic flow is a one-parameter unitary (Schrödinger) evolution on rays:

`∀ t x, d.pi (d.flow t x) = exp(-i t H) • d.pi x`,

for a Hermitian generator H. Unlike the ray-level form, this GENUINELY consumes the sector fields d.projectable, d.flow, d.pi: it is the statement that the CSD ontic dynamics on Σ, viewed through the operational projection π, IS finite-dimensional Schrödinger evolution. It is the forward direction of the dynamics spine landed on the substrate, not merely on the already-projected map.

Non-vacuity on the trivialKahlerOnticSetup witness

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

The phase lift FIRES on the inhabitation witness: the constant family U = 1 realises the identity flow with trivial cocycle c = 1, trivialised by the trivial phase b = 1; the lifted family is a genuine vector-level one-parameter unitary group. Confirms the S1 hypotheses are jointly satisfiable and the conclusion genuine.

theorem CSD.LF4.trivialKahlerOnticSetup_schrodinger_form (N : ℕ) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : ∃ (H : Matrix (Fin N) (Fin N) ℂ) (hH : H.IsHermitian), ∀ (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), (trivialKahlerOnticSetup N p₀).projectedFlow t p = schrodingerUnitary hH t • p

The full Schrödinger form FIRES on the inhabitation witness: with the constant family, trivial cocycle/phase, and zero generator (A = 0, so H = i·0 = 0 Hermitian), the capstone concludes the identity flow is exp(-it·0) = 1 conjugation on rays. Confirms every capstone hypothesis (S1 coboundary + S2 C^1) is concretely dischargeable.

theorem CSD.LF4.trivialKahlerOnticSetup_sigmaFlow_schrodinger_form (N : ℕ) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : ∃ (H : Matrix (Fin N) (Fin N) ℂ) (hH : H.IsHermitian), ∀ (t : ℝ) (x : (trivialKahlerOnticSetup N p₀).Sigma), (trivialKahlerOnticSetup N p₀).pi ((trivialKahlerOnticSetup N p₀).flow t x) = schrodingerUnitary hH t • (trivialKahlerOnticSetup N p₀).pi x

The Σ-level capstone FIRES on the inhabitation witness: the identity ontic flow (flow t = id, pi = id, projectable by rfl) projects to the identity exp(-it·0) = 1 on rays. Confirms the substrate-consuming form's hypotheses are jointly dischargeable and the descent equation genuinely closes the loop (d.pi (d.flow t x) = x = 1 • x).