C2: the Schrödinger form on the non-trivial rotation flow

Category: 3-Local (the Schrödinger form on the non-trivial rotation flow).

Connectivity fix C2 (specs/connectivity-manifest.md, link L3): fire the full W-series Schrödinger capstone sigmaFlow_schrodinger_form on the genuine Φ ≠ id instance rotationSetup (fix C1), NOT just the trivial H = 0 witness.

The rotation flow R(t) = [[cos t, −sin t],[sin t, cos t]] on ℂℙ¹ is a genuine one-parameter unitary GROUP (R(s+t) = R(s)R(t), so the phase cocycle is trivial: c = 1, b = 1) with skew-Hermitian generator J = [[0,−1],[1,0]] (R(τ) = cos τ · I + sin τ · J, whence R'(τ) = R(τ)·J). The capstone therefore recovers the Hermitian generator H = iJ = σ_y (Pauli-Y), landing

`rotationSetup.pi (rotationSetup.flow t x) = exp(-it·σ_y) • rotationSetup.pi x`,

i.e. the deterministic rotation flow, projected, IS Schrödinger evolution exp(-it H) for H = σ_y ≠ 0. This is the first fully-instantiated, H ≠ 0 Schrödinger statement of the corpus — the connectivity gap the audit flagged (Schrödinger only on the trivial witness) closed for rotationSetup.

Honest scope

This discharges the FS-isometry (via the unitary flow), coboundary (b = 1), and C¹ (R' = R·J) data of sigmaFlow_schrodinger_form on a concrete non-trivial flow. It is a witness that the chain fires genuinely, not a derivation of the sector. Born-side connectivity (manifest L5/L6/L7) is untouched.

Provenance

Foundational-triple only. Reuses sigmaFlow_schrodinger_form (S1×S2 capstone), rotationSetup/rotU (C1), and standard trig derivatives; nothing re-proved.

def CSD.LF4.rotGen : Matrix (Fin 2) (Fin 2) ℂ

The generator J = [[0, −1],[1, 0]] of the ℂℙ¹ rotation flow: real skew-symmetric, so skew-Hermitian. iJ = σ_y is the recovered Hamiltonian.

Equations

• CSD.LF4.rotGen = !![0, -1; 1, 0]

theorem CSD.LF4.rotGen_star : star rotGen = -rotGen

J is skew-Hermitian: star J = −J.

theorem CSD.LF4.rotMat_add (s t : ℝ) : rotMat (s + t) = rotMat s * rotMat t

Rotation addition: R(s+t) = R(s) · R(t). So the rotation family is a genuine one-parameter unitary group and its phase cocycle is trivial.

theorem CSD.LF4.rotMat_eq_smul (t : ℝ) : rotMat t = Real.cos t • 1 + Real.sin t • rotGen

R(τ) = cos τ · I + sin τ · J (real scalar multiples). The decomposition that gives the derivative.

theorem CSD.LF4.rotMat_smulDeriv (t : ℝ) : -Real.sin t • 1 + Real.cos t • rotGen = rotMat t * rotGen

(−sin t) · I + (cos t) · J = R(t) · J: the target derivative in matrix form.

theorem CSD.LF4.rotMat_hasDerivAt (t : ℝ) : HasDerivAt (fun (τ : ℝ) => rotMat τ) (rotMat t * rotGen) t

The C¹ datum: R'(τ) = R(τ) · J. From R = cos · I + sin · J and the scalar derivatives of cos, sin, via HasDerivAt.smul_const.

The capstone on the rotation flow

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

C2 / connectivity link L3 (off the trivial witness): Schrödinger form on the rotation flow. The projected deterministic rotation flow of rotationSetup is exp(-itH)-conjugation on rays for the Hermitian generator H = iJ = σ_y:

`rotationSetup.pi (rotationSetup.flow t x) = exp(-it·σ_y) • rotationSetup.pi x`.

This is the W-series Schrödinger capstone fired on a genuine Φ ≠ id flow with H ≠ 0 — the connectivity gap (Schrödinger only on the identity witness) closed for rotationSetup.

theorem CSD.LF4.rotationSetup_generator_ne_zero (_p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin 2))) : Complex.I • rotGen ≠ 0

The recovered generator is non-trivial: H = iJ = σ_y ≠ 0, so this is a genuine (H ≠ 0) Schrödinger evolution, not the trivial exp(0) = 1.