LF4 plan B, Part 1 (step): unitary norm-preservation on ℂ^N

Category: 3-Local (unitary norm-preservation on ℂ^N).

Toward discharging fs_moment_pushforward_uniform via the Gaussian route (specs/plan-b-detail.md Part 1). This file lands the matrix-analytic core that L3 (Gaussian unitary-invariance) needs: a unitary matrix's toEuclideanLin action preserves the Euclidean norm.

Blocker note (RESOLVED). Building the U(2) action as a ≃ₗᵢ[ℝ] for stdGaussian_map via (unitaryIsomC U).restrictScalars ℝ hit an instance-resolution ambiguity (LinearMap.CompatibleSMul … ℝ ℂ / IsScalarTower ℝ ℂ … failing inside the full LF4 import chain). This was resolved by taking the ℝ-isometry route (plan §Part 1 option (a)): conjRN / coordsN in GaussianCPN.lean realise the real-scalar route in a genuine real space, sidestepping the ℝ-over-ℂ instances, and the Gaussian → Fubini–Study identification gaussianCPN_eq_fubiniStudy is proved there. The qubit DH fact fs_moment_pushforward_uniform is consequently a theorem (MomentUniform.lean), not an axiom.

theorem CSD.LF4.unitary_norm_preserving {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (v : EuclideanSpace ℂ (Fin N)) : ‖(Matrix.toEuclideanLin ↑U) v‖ = ‖v‖

A unitary matrix's toEuclideanLin action preserves the Euclidean norm (‖U v‖ = ‖v‖), from Uᴴ U = 1.

noncomputable def CSD.LF4.unitaryIsomC (U : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) : EuclideanSpace ℂ (Fin 2) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin 2)

The unitary action on ℂ² as a complex linear isometry equiv (the real form, needed for stdGaussian_map, is blocked on the restrictScalars instance issue — see the module docstring).

Equations

• CSD.LF4.unitaryIsomC U = { toLinearEquiv := Matrix.UnitaryGroup.toEuclideanLinearEquiv U, norm_map' := ⋯ }