Documentation

CsdLean4.LF4.ManyToOneSchrodingerDerived

General-N Schrödinger pillar, DERIVED (not by rfl) #

Category: 3-Local (General-N Schrödinger pillar, DERIVED (not by rfl)).

manyToOneSchrodingerSetup_schrodinger_form (in ManyToOnePillars) delivers the Schrödinger pillar π (Φ_t x) = exp(-itH) • π x by rfl — true, but only because the flow was built as exp(-itH). That form does not, on its own, exhibit that the finite-dimensional Stone/Wigner derivation machinery actually FIRES on the real object: prior to this module the C¹-Stone core (Matrix.StoneC1.eq_exp_of_hasDeriv, via PhaseLift.sigmaFlow_schrodinger_form) was only ever exercised on the trivial A = 0 witness (trivialKahlerOnticSetup_sigmaFlow_schrodinger_form).

This module closes that gap at general N with an arbitrary Hermitian generator. It EXHIBITS the genuine skew-Hermitian generator A = -i H, DISCHARGES (proves, does not assume) the C¹ smoothness datum U' t = U t * A for the real family U t = exp(-itH), runs the finite-dimensional Stone theorem on it to recover U t = exp(t • A), and delivers the pillar — so the Schrödinger form is now backed by an exercised derivation, not standing alone on rfl.

The CompleteSpace (Matrix ...) obstruction that stalled an earlier attempt is avoided exactly as in StoneC1: the C^*-algebra L2-operator norm (open scoped Matrix.Norms.L2Operator) carries completeness with no instance diamond, so hasDerivAt_exp_smul_const synthesises. Under the plain operator / Frobenius scopes the finite-dimensional completeness instance does not unify and synthesis fails.

Main results #

References: LF4/PhaseLift.lean (sigmaFlow_schrodinger_form, S1), Mathlib/Analysis/Matrix/StoneC1.lean (eq_exp_of_hasDeriv, S2), LF4/ProjectedDynamics.lean (schrodingerUnitary, expNegITH_unitary_group), LF4/ManyToOnePillars.lean (manyToOneSchrodingerSetup_schrodinger_form, the rfl-form this backs). See specs/future-work.md (W5-S2) and specs/reconstruction-status.md (L3/L8, the Schrödinger pillar).

The three lemmas that discharge the C¹ datum — schrodingerGen_neg_i_smul_skew, schrodingerGen_eq_real_smul and schrodingerUnitary_hasDerivAt — moved to the Category-1 module Mathlib/Analysis/Matrix/SchrodingerUnitary.lean on 2026-09-16 (namespace Matrix), so that the manifold-level Schrödinger flow on ℂℙⁿ is Category 1 by closure. Re-exported here.

source
theorem CSD.LF4.manyToOneSchrodingerSetup_schrodinger_derived {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : CPN (M + 1)) :
∃ (A : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ), star A = -A ∧ (∀ (t : ℝ), HasDerivAt (fun (τ : ℝ) => ↑(schrodingerUnitary hH τ)) (↑(schrodingerUnitary hH t) * A) t) ∧ (∀ (t : ℝ), ↑(schrodingerUnitary hH t) = NormedSpace.exp (t • A)) ∧ ∀ (t : ℝ) (x : (manyToOneSchrodingerSetup H hH p₀).Sigma), (manyToOneSchrodingerSetup H hH p₀).pi ((manyToOneSchrodingerSetup H hH p₀).flow t x) = schrodingerUnitary hH t • (manyToOneSchrodingerSetup H hH p₀).pi x

General-N Schrödinger pillar, DERIVED. For the real Kähler ontic instance manyToOneSchrodingerSetup H hH p₀ (arbitrary Hermitian H, general N), there is a genuine skew-Hermitian generator A = -iH such that:

  • star A = -A — the generator is skew-Hermitian;
  • ∀ t, HasDerivAt U (U t * A) t — the C¹ smoothness datum is DISCHARGED for the real family U t = exp(-itH) (not assumed, not the A = 0 witness);
  • ∀ t, U t = exp (t • A) — the finite-dimensional Stone theorem (Matrix.StoneC1.eq_exp_of_hasDeriv) recovers the family from its generator;
  • ∀ t x, π (Φ_t x) = exp(-itH) • π x — the projected-flow Schrödinger pillar.

This EXERCISES the Wigner/Stone derivation on the real nonzero-generator object at general N, so manyToOneSchrodingerSetup_schrodinger_form (the rfl-form) is backed by an actual derivation. It is the FORWARD direction (consumes the posited sector); it does not derive the sector from the dynamics (L7/SO-1, untouched).