The Schrödinger flow on ℂℙⁿ is Hamiltonian, with Hamiltonian -2 ⟨H⟩

TERM-SCOPE(Kahler) TERM-SCOPE(Hamiltonian) TERM-SCOPE(MomentMap) — this module uses the restricted senses of these words; specs/TERMS.md records what is backed and what is not.

Category: 1-Mathlib (1-Mathlib-staging in its mathematics; it consumes the corpus's). Matrix.schrodingerUnitary (the unitary exp(-itH)) and its derivative Matrix.schrodingerUnitary_hasDerivAt as the flow whose generator it identifies.

Brick G13 of specs/generator-layer-scoping.md (with the G2, G3, G4, G16 and G19 corollaries): the U(n+1) moment map. For a Hermitian H, the unitary flow p ↦ exp(-itH) • p on ℂℙⁿ — the corpus's projected Schrödinger flow — is Hamiltonian for the Fubini–Study form, and its Hamiltonian is -2 ⟨H⟩, the expectation value ⟪z, Hz⟫ / ‖z‖² up to the form's convention. Brick G6 (the torus) is the diagonal case.

• expectation H p = ⟪z, Hz⟫.re / ‖z‖² — the expectation value on rays (expectation_mk, continuous_expectation); schrodingerHamiltonian H = -2 • expectation H;
• insertZeroCLM i — the tangent lift of the affine chart (0 in slot i), an ℝ-linear map; insertOne i w = insertOne i 0 + insertZeroCLM i w, so hasFDerivAt_insertOne; and the lift preserves the inner products the model form is written in (inner_insertZeroCLM_insertZeroCLM, inner_insertZeroCLM_insertOne, norm_sq_insertOne_toLpCLM);
• schrodingerChartField H i w — the velocity in chart i, -i ((Hv)_{sⱼ} - (Hv)_i wⱼ) for v = insertOne i w; ★ hasDerivAt_chartFun_schrodingerUnitary — it is the velocity of the flow: the t-derivative at 0 of t ↦ chartFun i (exp(-itH) • chartInv i w);
• schrodingerChartHam, hasFDerivAt_schrodingerChartHam — the chart Hamiltonian -2 ⟪v, Hv⟫.re / ‖v‖² and its derivative, through HasFDerivAt.inner along the affine lift;
• ★★ fsModelForm_schrodingerChartField — the chart identity ω_w (X_w, u) = dH_w u, proved in the ambient inner product: the lifted velocity is -i (Hv - (Hv)_i v), the (Hv)_i terms cancel, and what remains is the symmetry of H and Im (i z) = Re z;
• ★★★ schrodingerField_isHamiltonianVectorField — IsHamiltonianVectorField fsForm (schrodingerField H) (schrodingerHamiltonian H): the Schrödinger flow on ℂℙⁿ is Hamiltonian for the Fubini–Study form, with -2 ⟨H⟩ as its Hamiltonian;
• schrodingerChartField_neg_diagonal, schrodingerHamiltonian_neg_diagonal — for H = -diag θ the field and the Hamiltonian are G6's torusChartField and torusHamiltonian: the torus is the diagonal case;
• torusField_eq_hamiltonianVectorField, schrodingerField_eq_hamiltonianVectorField — both fields are the Hamiltonian vector fields (ω♭)⁻¹ dH of their Hamiltonians for the symplectic form fsForm (G2's existence-and-uniqueness construction, IsSymplectic.hamiltonianVectorField);
• contDiff_schrodingerChartHam, ★ contMDiff_schrodingerHamiltonian, ★ contMDiff_torusHamiltonian (both Hamiltonians are C^m on ℂℙⁿ for every order m, so C^∞ and real-analytic at once — one statement each since 2026-09-16), and ★★ contMDiff_schrodingerField, ★★ contMDiff_torusField — both fields are C^∞ vector fields, C^∞ sections of the tangent bundle, by G2's identification and G3's smoothness theorem;
• exists_isMIntegralCurveAt_schrodingerField, isMIntegralCurve_schrodingerField_eq, ★★ expectation_eq_of_isMIntegralCurve_schrodingerField (⟨H⟩ is conserved along every integral curve of the field), ★★★ isMIntegralCurve_schrodingerUnitary_smul — the Schrödinger flow t ↦ exp(-itH) • p is the integral curve of its field, for every p — and ★★ expectation_schrodingerUnitary_smul (⟨H⟩ is conserved by the flow), all G4;
• G16 (2026-09-10). Given ★★★ isMIntegralCurve_torusUnitary_smul — the torus orbit t ↦ diag(e^{itθ}) • p is the integral curve of torusField θ — which lives with the field in ProjectiveSpaceMomentMap.lean since 2026-09-16 (it uses only the moment-map module's own hasDerivAt_chartFun_torusUnitary and group law torusUnitary_add_smul): isMIntegralCurve_torusField_eq, ★★ eq_torusUnitary_smul_of_isMIntegralCurve (every integral curve through p at 0 IS the orbit); ★★ torusHamiltonian_eq_of_isMIntegralCurve_torusField and ★★ torusHamiltonian_torusUnitary_smul (2 ∑ θₖ μₖ is conserved along the curves and by the flow);
• G19 (2026-09-10). ★★ contMDiff_omega_schrodingerField, ★★ contMDiff_omega_torusField — both fields are analytic vector fields, C^ω sections of the tangent bundle: the Hamiltonian vector fields of C^ω energies for the C^ω form fsFormAnalytic (G12), by G19's contMDiff_omega_hamiltonianVectorField;
• Q29(e) (2026-09-12). ★★ hamiltonianFlow_schrodingerHamiltonian, ★★ hamiltonianFlow_torusHamiltonian — the Schrödinger flow and the torus flow ARE the Hamiltonian flows IsSymplectic.hamiltonianFlow (HamiltonianFlowVolume.lean) of -2⟨H⟩ and of 2 ∑ θₖ μₖ: the manifold flow of the Hamiltonian vector field is p ↦ exp(-itH) • p, by uniqueness of integral curves (integralFlow_eq_of_isMIntegralCurve); hence ★★ fsVolume_map_schrodingerUnitary_smul, fsVolumeNormalized_map_schrodingerUnitary_smul — Liouville for the Schrödinger flow from the Hamiltonian, a corollary of the manifold-level theorem fsVolume_map_hamiltonianFlow (Q29(d′)), not of unitary invariance.

Honest scope

⚠️ The sign and the factor are conventions. fsChartForm carries the -4 of its potential, which makes the generator of the torus 2 · momentMap (G6); the corpus's Schrödinger flow is exp(-itH), so its Hamiltonian is -2 ⟨H⟩. Nothing here rescales either; the statement shows both.

⚠️ The flow is consumed, not built. Matrix.schrodingerUnitary and its derivative come from Analysis/Matrix/SchrodingerUnitary.lean, under the L2Operator matrix norm (the one under which hasDerivAt_exp_smul_const synthesises); this module opens that scope and adds nothing to it.

⚠️ Two routes to Liouville, both in the corpus. fsVolume_map_torusUnitary_smul (G10) and fsVolume_map_smul (W1 on the sectors) are unitary invariance; fsVolume_map_schrodingerUnitary_smul here is the manifold-level flow theorem (Q29, formerly G5) applied through the identification of the flows. They prove the same equation by independent arguments; the second is the one that generalises to a non-unitary Hamiltonian flow.

⚠️ Posits untouched. Posit 1 asserts that the dynamics generates the pointer torus; this module says which Hamiltonian a given unitary flow has, for every Hermitian H, and does not touch what generates it.

References: specs/generator-layer-scoping.md (G13, G6); Instances/ProjectiveSpaceMomentMap.lean (torusChartField, torusHamiltonian, torusField_isHamiltonianVectorField); Geometry/Manifold/HamiltonianVectorField.lean (G1); Instances/ProjectiveSpaceFubiniStudyMass.lean (fsModelForm_apply, toLpCLM_apply); Instances/ProjectiveSpaceUnitaryAction.lean (chartFun_smul_chartInv); Analysis/Matrix/SchrodingerUnitary.lean (schrodingerUnitary, expNegITH_unitary_group, schrodingerUnitary_hasDerivAt); specs/TERMS.md (Hamiltonian, moment map); specs/POSITS.md (Posit 1); specs/future-work.md.

The expectation value, on rays

noncomputable def Projectivization.expectation {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (p : Projectivization ℂ (Ambient n)) : ℝ

⟨H⟩ at a ray: ⟪z, Hz⟫.re / ‖z‖², on any representative.

Equations

• Projectivization.expectation H p = (inner ℂ p.rep ((Matrix.toEuclideanLin H) p.rep)).re / ‖p.rep‖ ^ 2

theorem Projectivization.expectation_ratio_smul {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (c : ℂ) (hc : c ≠ 0) (v : Ambient n) : (inner ℂ (c • v) ((Matrix.toEuclideanLin H) (c • v))).re / ‖c • v‖ ^ 2 = (inner ℂ v ((Matrix.toEuclideanLin H) v)).re / ‖v‖ ^ 2

theorem Projectivization.expectation_mk {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (ψ : Ambient n) (hψ : ψ ≠ 0) : expectation H (mk ℂ ψ hψ) = (inner ℂ ψ ((Matrix.toEuclideanLin H) ψ)).re / ‖ψ‖ ^ 2

The expectation value at a representative.

theorem Projectivization.continuous_expectation {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) : Continuous (expectation H)

noncomputable def Projectivization.schrodingerHamiltonian {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (p : Projectivization ℂ (Ambient n)) : ℝ

The Hamiltonian of the Schrödinger flow exp(-itH): -2 ⟨H⟩.

Equations

• Projectivization.schrodingerHamiltonian H p = -2 * Projectivization.expectation H p

theorem Projectivization.continuous_schrodingerHamiltonian {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) : Continuous (schrodingerHamiltonian H)

The tangent lift of the affine chart

noncomputable def Projectivization.insertZeroCLM {n : ℕ} (i : Fin (n + 1)) : (Fin n → ℂ) →L[ℝ] Ambient n

Insert 0 in slot i, as an ℝ-linear map: the lift of chart tangent vectors.

Equations

• Projectivization.insertZeroCLM i = LinearMap.toContinuousLinearMap { toFun := fun (u : Fin n → ℂ) => WithLp.toLp 2 (i.insertNth 0 u), map_add' := ⋯, map_smul' := ⋯ }

theorem Projectivization.insertZeroCLM_apply {n : ℕ} (i : Fin (n + 1)) (u : Fin n → ℂ) : (insertZeroCLM i) u = WithLp.toLp 2 (i.insertNth 0 u)

@[simp]

theorem Projectivization.insertZeroCLM_apply_same {n : ℕ} (i : Fin (n + 1)) (u : Fin n → ℂ) : ((insertZeroCLM i) u).ofLp i = 0

@[simp]

theorem Projectivization.insertZeroCLM_apply_succAbove {n : ℕ} (i : Fin (n + 1)) (u : Fin n → ℂ) (j : Fin n) : ((insertZeroCLM i) u).ofLp (i.succAbove j) = u j

theorem Projectivization.insertOne_eq_add {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : insertOne i w = insertOne i 0 + (insertZeroCLM i) w

theorem Projectivization.hasFDerivAt_insertOne {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : HasFDerivAt (insertOne i) (insertZeroCLM i) w

theorem Projectivization.inner_insertZeroCLM_insertZeroCLM {n : ℕ} (i : Fin (n + 1)) (u u' : Fin n → ℂ) : inner ℂ ((insertZeroCLM i) u) ((insertZeroCLM i) u') = inner ℂ (toLpCLM u) (toLpCLM u')

theorem Projectivization.inner_insertZeroCLM_insertOne {n : ℕ} (i : Fin (n + 1)) (u w : Fin n → ℂ) : inner ℂ ((insertZeroCLM i) u) (insertOne i w) = inner ℂ (toLpCLM u) (toLpCLM w)

theorem Projectivization.inner_insertOne_insertZeroCLM {n : ℕ} (i : Fin (n + 1)) (w u : Fin n → ℂ) : inner ℂ (insertOne i w) ((insertZeroCLM i) u) = inner ℂ (toLpCLM w) (toLpCLM u)

theorem Projectivization.norm_sq_insertOne_toLpCLM {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : ‖insertOne i w‖ ^ 2 = 1 + ‖toLpCLM w‖ ^ 2

The velocity and the Hamiltonian in the chart

noncomputable def Projectivization.schrodingerChartField {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (i : Fin (n + 1)) (w : Fin n → ℂ) : Fin n → ℂ

The velocity of t ↦ exp(-itH) • p in chart i: -i ((Hv)_{sⱼ} - (Hv)_i wⱼ), v = insertOne i w.

Equations

• Projectivization.schrodingerChartField H i w j = -Complex.I * (H.mulVec (Projectivization.insertOne i w).ofLp (i.succAbove j) - H.mulVec (Projectivization.insertOne i w).ofLp i * w j)

theorem Projectivization.insertZeroCLM_schrodingerChartField {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (i : Fin (n + 1)) (w : Fin n → ℂ) : (insertZeroCLM i) (schrodingerChartField H i w) = -Complex.I • ((Matrix.toEuclideanLin H) (insertOne i w) - H.mulVec (insertOne i w).ofLp i • insertOne i w)

The lift of the chart velocity to the ambient space: -i (Hv - (Hv)_i v).

noncomputable def Projectivization.schrodingerChartHam {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (i : Fin (n + 1)) (w : Fin n → ℂ) : ℝ

The chart Hamiltonian -2 ⟪v, Hv⟫.re / ‖v‖².

Equations

• One or more equations did not get rendered due to their size.

theorem Projectivization.schrodingerHamiltonian_chartInv {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (i : Fin (n + 1)) (w : Fin n → ℂ) : schrodingerHamiltonian H (chartInv i w) = schrodingerChartHam H i w

theorem Projectivization.norm_sq_insertOne_pos {n : ℕ} (i : Fin (n + 1)) (w : Fin n → ℂ) : 0 < ‖insertOne i w‖ ^ 2

noncomputable def Projectivization.schrodingerChartHamDeriv {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (i : Fin (n + 1)) (w : Fin n → ℂ) : (Fin n → ℂ) →L[ℝ] ℝ

The derivative of the chart Hamiltonian, by the product and inverse rules from HasFDerivAt.inner along the affine lift.

Equations

• One or more equations did not get rendered due to their size.

theorem Projectivization.hasFDerivAt_schrodingerChartHam {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (i : Fin (n + 1)) (w : Fin n → ℂ) : HasFDerivAt (schrodingerChartHam H i) (schrodingerChartHamDeriv H i w) w

theorem Projectivization.schrodingerChartHamDeriv_apply {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (i : Fin (n + 1)) (w u : Fin n → ℂ) : (schrodingerChartHamDeriv H i w) u = -2 * ((inner ℂ (insertOne i w) ((Matrix.toEuclideanLin H) (insertOne i w))).re * (-((‖insertOne i w‖ ^ 2) ^ 2)⁻¹ * (inner ℂ (insertOne i w) ((insertZeroCLM i) u) + inner ℂ ((insertZeroCLM i) u) (insertOne i w)).re) + (‖insertOne i w‖ ^ 2)⁻¹ * (inner ℂ (insertOne i w) ((Matrix.toEuclideanLin H) ((insertZeroCLM i) u)) + inner ℂ ((insertZeroCLM i) u) ((Matrix.toEuclideanLin H) (insertOne i w))).re)

The chart identity ι_X ω = dH, in the ambient inner product

theorem Projectivization.fsModelForm_schrodingerChartField {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) (i : Fin (n + 1)) (w u : Fin n → ℂ) : (fsModelForm w) ![schrodingerChartField H i w, u] = (schrodingerChartHamDeriv H i w) u

★★ The chart identity: the Fubini–Study model form pairs the Schrödinger velocity with u exactly as the derivative of the chart Hamiltonian does. Lifted to the ambient space, the velocity is -i (Hv - (Hv)_i v); the (Hv)_i terms cancel, and what remains is Im (i z) = Re z together with the symmetry of H.

The manifold statement

noncomputable def Projectivization.schrodingerField {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (x : Projectivization ℂ (Ambient n)) : TangentSpace (modelWithCornersSelf ℝ (Fin n → ℂ)) x

The velocity field of the Schrödinger flow p ↦ exp(-itH) • p on ℂℙⁿ, read in the chart at each point.

Equations

• Projectivization.schrodingerField H x = Projectivization.schrodingerChartField H x.idx (Projectivization.chartFun x.idx x)

theorem Projectivization.hasMFDerivAt_schrodingerHamiltonian {n : ℕ} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (x : Projectivization ℂ (Ambient n)) : HasMFDerivAt% (schrodingerHamiltonian H) x (schrodingerChartHamDeriv H x.idx (chartFun x.idx x))

theorem Projectivization.schrodingerField_isHamiltonianVectorField {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) : DifferentialForm.IsHamiltonianVectorField (fun (x : Projectivization ℂ (Ambient n)) => fsForm x) (schrodingerField H) (schrodingerHamiltonian H)

★★★ The Schrödinger flow on ℂℙⁿ is Hamiltonian for the Fubini–Study form, with -2 ⟨H⟩ as its Hamiltonian: ι_X ω_FS = dH on the manifold, for every Hermitian H.

The field is the velocity of the flow

noncomputable def Projectivization.mulVecEntryCLM {n : ℕ} (v : Fin (n + 1) → ℂ) (k : Fin (n + 1)) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ →L[ℝ] ℂ

The entry k of M *ᵥ v, as an ℝ-linear functional of the matrix.

Equations

• One or more equations did not get rendered due to their size.

theorem Projectivization.mulVecEntryCLM_apply {n : ℕ} (v : Fin (n + 1) → ℂ) (k : Fin (n + 1)) (M : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) : (mulVecEntryCLM v k) M = M.mulVec v k

theorem Projectivization.schrodingerUnitary_zero_val {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) : ↑(Matrix.schrodingerUnitary hH 0) = 1

theorem Projectivization.schrodingerUnitary_zero_val' {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) : Matrix.schrodingerUnitary hH 0 = 1

theorem Projectivization.hasDerivAt_chartFun_schrodingerUnitary {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) (i : Fin (n + 1)) (w : Fin n → ℂ) : HasDerivAt (fun (t : ℝ) => chartFun i (Matrix.schrodingerUnitary hH t • chartInv i w)) (schrodingerChartField H i w) 0

★ The field is the velocity of the flow: at every chart point, schrodingerChartField is the t-derivative at 0 of t ↦ exp(-itH) • p, read in the chart.

The torus is the diagonal case (G6)

theorem Projectivization.schrodingerChartField_neg_diagonal {n : ℕ} (θ : Fin (n + 1) → ℝ) (i : Fin (n + 1)) (w : Fin n → ℂ) : schrodingerChartField (-Matrix.diagonal fun (k : Fin (n + 1)) => ↑(θ k)) i w = torusChartField i θ w

theorem Projectivization.schrodingerHamiltonian_neg_diagonal {n : ℕ} (θ : Fin (n + 1) → ℝ) : schrodingerHamiltonian (-Matrix.diagonal fun (k : Fin (n + 1)) => ↑(θ k)) = torusHamiltonian θ

Both fields are THE Hamiltonian vector fields of their Hamiltonians (G2)

theorem Projectivization.torusField_eq_hamiltonianVectorField {n : ℕ} (θ : Fin (n + 1) → ℝ) : torusField θ = ⋯.hamiltonianVectorField (torusHamiltonian θ)

The torus field is the Hamiltonian vector field (ω♭)⁻¹ dH of torusHamiltonian θ for the symplectic form fsForm (G2 + G6).

theorem Projectivization.schrodingerField_eq_hamiltonianVectorField {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) : schrodingerField H = ⋯.hamiltonianVectorField (schrodingerHamiltonian H)

The Schrödinger field is the Hamiltonian vector field (ω♭)⁻¹ dH of -2 ⟨H⟩ for the symplectic form fsForm (G2 + G13).

The Hamiltonians are C^m for every order m (so C^∞ and C^ω), and both fields are

C^∞ vector fields (G3)

theorem Projectivization.contDiff_schrodingerChartHam {n : ℕ} {m : WithTop ℕ∞} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) (i : Fin (n + 1)) : ContDiff ℝ m (schrodingerChartHam H i)

The chart Hamiltonian is C^m for every order m (∞ and ω included): inner-product calculus along the affine lift, every step generic in the order.

theorem Projectivization.contMDiff_schrodingerHamiltonian {n : ℕ} {m : WithTop ℕ∞} (H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ) : ContMDiff (modelWithCornersSelf ℝ (Fin n → ℂ)) (modelWithCornersSelf ℝ ℝ) m (schrodingerHamiltonian H)

★ The Hamiltonian of the Schrödinger flow is C^m on ℂℙⁿ for every order m (C^∞ and real-analytic in particular).

theorem Projectivization.contMDiff_torusHamiltonian {n : ℕ} {m : WithTop ℕ∞} (θ : Fin (n + 1) → ℝ) : ContMDiff (modelWithCornersSelf ℝ (Fin n → ℂ)) (modelWithCornersSelf ℝ ℝ) m (torusHamiltonian θ)

★ The Hamiltonian of the torus action is C^m on ℂℙⁿ for every order m (the diagonal case).

theorem Projectivization.contMDiff_schrodingerField_of_le {n : ℕ} {m : WithTop ℕ∞} (hm : m + 1 ≤ m) {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) : ContMDiff (modelWithCornersSelf ℝ (Fin n → ℂ)) ((modelWithCornersSelf ℝ (Fin n → ℂ)).prod (modelWithCornersSelf ℝ (Fin n → ℂ))) m fun (x : Projectivization ℂ (Ambient n)) => ⟨x, schrodingerField H x⟩

★★ The Schrödinger vector field on ℂℙⁿ is a C^m vector field for every infinite order m (∞ and ω): it is the Hamiltonian vector field of a C^m energy for the C^ω form fsForm (G2), and those are C^m (G3, contMDiff_hamiltonianVectorField_of_contMDiff).

theorem Projectivization.contMDiff_schrodingerField {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) : ContMDiff (modelWithCornersSelf ℝ (Fin n → ℂ)) ((modelWithCornersSelf ℝ (Fin n → ℂ)).prod (modelWithCornersSelf ℝ (Fin n → ℂ))) ↑⊤ fun (x : Projectivization ℂ (Ambient n)) => ⟨x, schrodingerField H x⟩

★★ The Schrödinger vector field on ℂℙⁿ is a C^∞ vector field (a C^∞ section of the tangent bundle).

theorem Projectivization.contMDiff_torusField_of_le {n : ℕ} {m : WithTop ℕ∞} (hm : m + 1 ≤ m) (θ : Fin (n + 1) → ℝ) : ContMDiff (modelWithCornersSelf ℝ (Fin n → ℂ)) ((modelWithCornersSelf ℝ (Fin n → ℂ)).prod (modelWithCornersSelf ℝ (Fin n → ℂ))) m fun (x : Projectivization ℂ (Ambient n)) => ⟨x, torusField θ x⟩

★★ The torus vector field on ℂℙⁿ is a C^m vector field for every infinite order m.

theorem Projectivization.contMDiff_torusField {n : ℕ} (θ : Fin (n + 1) → ℝ) : ContMDiff (modelWithCornersSelf ℝ (Fin n → ℂ)) ((modelWithCornersSelf ℝ (Fin n → ℂ)).prod (modelWithCornersSelf ℝ (Fin n → ℂ))) ↑⊤ fun (x : Projectivization ℂ (Ambient n)) => ⟨x, torusField θ x⟩

★★ The torus vector field on ℂℙⁿ is a C^∞ vector field.

Integral curves on ℂℙⁿ: the Schrödinger flow is one, and ⟨H⟩ is conserved (G4)

theorem Projectivization.exists_isMIntegralCurveAt_schrodingerField {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) (x₀ : Projectivization ℂ (Ambient n)) (t₀ : ℝ) : ∃ (γ : ℝ → Projectivization ℂ (Ambient n)), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ (schrodingerField H) t₀

Local existence of integral curves of the Schrödinger field, through every point.

theorem Projectivization.isMIntegralCurve_schrodingerField_eq {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) {γ γ' : ℝ → Projectivization ℂ (Ambient n)} (hγ : IsMIntegralCurve γ (schrodingerField H)) (hγ' : IsMIntegralCurve γ' (schrodingerField H)) {t₀ : ℝ} (h : γ t₀ = γ' t₀) : γ = γ'

Uniqueness of global integral curves of the Schrödinger field.

theorem Projectivization.expectation_eq_of_isMIntegralCurve_schrodingerField {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) {γ : ℝ → Projectivization ℂ (Ambient n)} (hγ : IsMIntegralCurve γ (schrodingerField H)) (t s : ℝ) : expectation H (γ t) = expectation H (γ s)

★★ ⟨H⟩ is conserved along every integral curve of the Schrödinger field.

theorem Projectivization.isMIntegralCurve_schrodingerUnitary_smul {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) (p : Projectivization ℂ (Ambient n)) : IsMIntegralCurve (fun (t : ℝ) => Matrix.schrodingerUnitary hH t • p) (schrodingerField H)

★★★ The Schrödinger flow is the integral curve of its field: t ↦ exp(-itH) • p is a global integral curve of schrodingerField H, for every p. In the chart at exp(-itH) • p the curve is s ↦ chartFun (exp(-i(s-t)H) • q), whose derivative at s = t is the chart velocity (hasDerivAt_chartFun_schrodingerUnitary, shifted by the group law expNegITH_unitary_group).

theorem Projectivization.expectation_schrodingerUnitary_smul {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) (p : Projectivization ℂ (Ambient n)) (t : ℝ) : expectation H (Matrix.schrodingerUnitary hH t • p) = expectation H p

★★ ⟨H⟩ is conserved by the Schrödinger flow: ⟨H⟩_{exp(-itH) • p} = ⟨H⟩_p.

The torus orbits are integral curves of the torus field (G16)

continuous_torusUnitary_smul and isMIntegralCurve_torusUnitary_smul moved to ProjectiveSpaceMomentMap.lean on 2026-09-16 (they use nothing from this file, and the moment-map module's docstring cites them); the uniqueness corollaries stay here.

theorem Projectivization.isMIntegralCurve_torusField_eq {n : ℕ} (θ : Fin (n + 1) → ℝ) {γ γ' : ℝ → Projectivization ℂ (Ambient n)} (hγ : IsMIntegralCurve γ (torusField θ)) (hγ' : IsMIntegralCurve γ' (torusField θ)) {t₀ : ℝ} (h : γ t₀ = γ' t₀) : γ = γ'

Uniqueness of global integral curves of the torus field.

theorem Projectivization.eq_torusUnitary_smul_of_isMIntegralCurve {n : ℕ} (θ : Fin (n + 1) → ℝ) {γ : ℝ → Projectivization ℂ (Ambient n)} (hγ : IsMIntegralCurve γ (torusField θ)) {p : Projectivization ℂ (Ambient n)} (h0 : γ 0 = p) : γ = fun (t : ℝ) => torusUnitary (t • θ) • p

★★ The torus orbit is THE integral curve: every global integral curve of the torus field through p at time 0 is t ↦ diag(e^{itθ}) • p.

theorem Projectivization.torusHamiltonian_eq_of_isMIntegralCurve_torusField {n : ℕ} (θ : Fin (n + 1) → ℝ) {γ : ℝ → Projectivization ℂ (Ambient n)} (hγ : IsMIntegralCurve γ (torusField θ)) (t s : ℝ) : torusHamiltonian θ (γ t) = torusHamiltonian θ (γ s)

★★ The torus Hamiltonian 2 ∑ θₖ μₖ is conserved along every integral curve of the torus field.

theorem Projectivization.torusHamiltonian_torusUnitary_smul {n : ℕ} (θ : Fin (n + 1) → ℝ) (p : Projectivization ℂ (Ambient n)) (t : ℝ) : torusHamiltonian θ (torusUnitary (t • θ) • p) = torusHamiltonian θ p

★★ The torus Hamiltonian is conserved by the torus flow: 2 ∑ θₖ μₖ (diag(e^{itθ}) • p) = 2 ∑ θₖ μₖ (p).

Both fields are analytic (G19)

The ω case of contMDiff_schrodingerField_of_le / contMDiff_torusField_of_le: one proof with the C^∞ case since 2026-09-17.

theorem Projectivization.contMDiff_omega_schrodingerField {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) : ContMDiff (modelWithCornersSelf ℝ (Fin n → ℂ)) ((modelWithCornersSelf ℝ (Fin n → ℂ)).prod (modelWithCornersSelf ℝ (Fin n → ℂ))) ⊤ fun (x : Projectivization ℂ (Ambient n)) => ⟨x, schrodingerField H x⟩

★★ The Schrödinger vector field on ℂℙⁿ is an analytic vector field.

theorem Projectivization.contMDiff_omega_torusField {n : ℕ} (θ : Fin (n + 1) → ℝ) : ContMDiff (modelWithCornersSelf ℝ (Fin n → ℂ)) ((modelWithCornersSelf ℝ (Fin n → ℂ)).prod (modelWithCornersSelf ℝ (Fin n → ℂ))) ⊤ fun (x : Projectivization ℂ (Ambient n)) => ⟨x, torusField θ x⟩

★★ The torus vector field on ℂℙⁿ is an analytic vector field.

The flows are the Hamiltonian flows, and Liouville from the Hamiltonian (Q29(e))

theorem Projectivization.hamiltonianFlow_schrodingerHamiltonian {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) (t : ℝ) (p : Projectivization ℂ (Ambient n)) : ⋯.hamiltonianFlow ⋯ t p = Matrix.schrodingerUnitary hH t • p

★★ The Schrödinger flow IS the Hamiltonian flow of -2⟨H⟩: for Hermitian H, the manifold flow of the Hamiltonian vector field of schrodingerHamiltonian H is p ↦ exp(-itH) • p, by uniqueness of integral curves.

theorem Projectivization.hamiltonianFlow_torusHamiltonian {n : ℕ} (θ : Fin (n + 1) → ℝ) (t : ℝ) (p : Projectivization ℂ (Ambient n)) : ⋯.hamiltonianFlow ⋯ t p = torusUnitary (t • θ) • p

★★ The torus flow IS the Hamiltonian flow of 2 ∑ θₖ μₖ: the manifold flow of the Hamiltonian vector field of torusHamiltonian θ is p ↦ diag(e^{itθ}) • p.

theorem Projectivization.fsVolume_map_schrodingerUnitary_smul {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) (t : ℝ) : MeasureTheory.Measure.map (fun (p : Projectivization ℂ (Ambient n)) => Matrix.schrodingerUnitary hH t • p) (fsVolume n) = fsVolume n

★★ Liouville for the Schrödinger flow, from the Hamiltonian: p ↦ exp(-itH) • p preserves the Fubini–Study volume because it is the Hamiltonian flow of -2⟨H⟩ (fsVolume_map_hamiltonianFlow), not because it is unitary (fsVolume_map_smul).

theorem Projectivization.fsVolumeNormalized_map_schrodingerUnitary_smul {n : ℕ} {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℂ} (hH : H.IsHermitian) (t : ℝ) : MeasureTheory.Measure.map (fun (p : Projectivization ℂ (Ambient n)) => Matrix.schrodingerUnitary hH t • p) (fsVolumeNormalized n) = fsVolumeNormalized n

The same for the normalised volume, fsMeasure p₀.