A genuine Φ ≠ id KahlerOnticSetup inhabitant (connectivity fix C1)

Category: 3-Local (A genuine Φ ≠ id KahlerOnticSetup inhabitant (connectivity fix C1)).

trivialKahlerOnticSetup (LF4/KahlerOnticSetup.lean) is the identity-flow witness (Φ = id, projectedFlow = id): the whole W-series Schrödinger chain, instantiated on it, collapses to exp(0) = 1. The 2026-07-07 connectivity audit (specs/connectivity-manifest.md, link L4) flagged this as the load-bearing gap — the only inhabitant of KahlerOnticSetup was trivial, so the Schrödinger pillar was never exercised on a non-trivial flow.

This module supplies a genuine one whose projected flow moves the rays.

• unitaryFlowSetup N U p₀ : for ANY one-parameter family of unitaries U : ℝ → unitaryGroup (Fin N) ℂ, the KahlerOnticSetup N with Σ = ℂℙ^{N-1}, π = id, flow t = projectedFlow t = (U t • ·), and Liouville measure the Fubini–Study measure. Measure-preservation is exactly the U(N)-invariance of μ_FS (fubiniStudyMeasure_smul_invariant); the descent equation projectable holds by rfl (π = id, flow = projectedFlow). Unlike kFlow (which translates a T² fibre and so acts trivially on rays), the projected flow here IS the unitary action on ℂℙ^{N-1}.

• rotationSetup p₀ : the concrete non-trivial witness at N = 2, with U t the real rotation R(t) = [[cos t, −sin t],[sin t, cos t]] (unitary, no matrix exponential needed). rotationSetup_projectedFlow_ne_id proves ∃ t, projectedFlow t ≠ id — at t = π/2 the flow sends the ray [e₀] to [e₁] ≠ [e₀]. This is the first KahlerOnticSetup inhabitant whose projected dynamics is genuinely ≠ id; it flips connectivity link L4.

Honest scope

This is a non-trivial instance, not the derivation of the sector. The flow is a posited measure-preserving unitary family (any U works); showing that the W-series recovers its Hermitian generator on this instance is the follow-on C2. The Kähler-geometry fields remain honest True placeholders (link L1).

Provenance

Foundational-triple only. Reuses KahlerOnticSetup, the projectivization unitary action, and fubiniStudyMeasure_smul_invariant; nothing is re-proved.

The general unitary-flow constructor

noncomputable def CSD.LF4.unitaryFlowSetup (N : ℕ) (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : KahlerOnticSetup N

A KahlerOnticSetup from any one-parameter unitary family. Σ = ℂℙ^{N-1}, π = id, flow t = projectedFlow t = (U t • ·), Liouville measure = μ_FS. Measure-preserving because μ_FS is U(N)-invariant.

The Kähler-geometry fields (concrete since the 2026-08-06 F-04 tightening; fix C5, connectivity link L1):

• liouville_isProbability — the formalizable core of "Liouville = Kähler volume": μ_FS is a normalized volume, i.e. a probability measure (∫ ω^n/n! = 1). Exposed by unitaryFlowSetup_liouville_isProbability.
• kahler_pointwise : IsFubiniStudyKahler N — the genuine formalizable core: the pointwise Fubini–Study Kähler compatibility on the tangent model (proved, isFubiniStudyKahler). Only the manifold closedness dω = 0 (no Mathlib API) stays the honestly-named residual.

Equations

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

@[simp]

theorem CSD.LF4.unitaryFlowSetup_projectedFlow (N : ℕ) (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : (unitaryFlowSetup N U p₀).projectedFlow t p = U t • p

The concrete rotation witness at N = 2

noncomputable def CSD.LF4.rotMat (t : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The real rotation matrix R(t) = [[cos t, −sin t],[sin t, cos t]] over ℂ.

Equations

• CSD.LF4.rotMat t = !![↑(Real.cos t), -↑(Real.sin t); ↑(Real.sin t), ↑(Real.cos t)]

theorem CSD.LF4.rotMat_mem_unitaryGroup (t : ℝ) : rotMat t ∈ Matrix.unitaryGroup (Fin 2) ℂ

R(t) is unitary: star R(t) * R(t) = 1, by sin² + cos² = 1.

noncomputable def CSD.LF4.rotU (t : ℝ) : ↥(Matrix.unitaryGroup (Fin 2) ℂ)

R(t) as a bundled unitary-group element.

Equations

• CSD.LF4.rotU t = ⟨CSD.LF4.rotMat t, ⋯⟩

noncomputable def CSD.LF4.rotationSetup (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin 2))) : KahlerOnticSetup 2

The concrete non-trivial KahlerOnticSetup 2: the rotation flow on ℂℙ¹. Its projected flow moves rays (rotationSetup_projectedFlow_ne_id).

Equations

• CSD.LF4.rotationSetup p₀ = CSD.LF4.unitaryFlowSetup 2 CSD.LF4.rotU p₀

theorem CSD.LF4.rotMat_pi_div_two_mulVec_e0 : (Matrix.toEuclideanLin (rotMat (Real.pi / 2))) (EuclideanSpace.single 0 1) = EuclideanSpace.single 1 1

R(π/2) = [[0, −1],[1, 0]], so it sends the first basis vector e₀ to the second e₁.

theorem CSD.LF4.rotationSetup_projectedFlow_ne_id (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin 2))) : ∃ (t : ℝ), (rotationSetup p₀).projectedFlow t ≠ id

C1 / connectivity link L4: the projected flow is genuinely ≠ id. For the rotation setup, projectedFlow (π/2) sends [e₀] to [e₁] ≠ [e₀], so it is not the identity map on rays. This is the first KahlerOnticSetup inhabitant with non-trivial projected dynamics.

Consuming the Kähler-volume field (connectivity fix C5, link L1)

theorem CSD.LF4.unitaryFlowSetup_liouville_isProbability (N : ℕ) (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : MeasureTheory.IsProbabilityMeasure (unitaryFlowSetup N U p₀).liouvilleMeasure

The liouville_isProbability field is load-bearing. It carries the formalizable core of the "Liouville = Kähler volume" posit — that the sector's typicality measure is a normalized volume (a probability measure) — and this theorem exposes it on the concrete instance. History: introduced at fix C5, when the field was the abstract IsLiouvilleKahlerVolume pair (inert before C5, made load-bearing by this consumer); since the 2026-08-06 F-04 tightening the field is the concrete IsProbabilityMeasure itself (and an instance), so this theorem is a thin projection kept for citation/pin stability.