Preserving orthonormality along a linear ODE: use uniqueness on the Gram matrix

For frames e_i' = Σ_j K_ij e_j with K(t) skew, do not compute the energy Σ(⟪e_i,e_j⟫ - δ_ij)². Instead, the Gram matrix G : ℝ → ι → ι → ℝ solves the linear ODE G' = KG + GKᵀ, and the constant identity matrix solves it too, because K + Kᵀ = 0. Uniqueness for linear ODEs then gives G = δ. Lean details: build the matrix field as LinearMap.toContinuousLinearMap of an explicit →ₗ on ι → ι → ℝ. Continuity in t comes from continuous_clm_apply (the domain is finite-dimensional) with continuous_pi. Assemble HasDerivAt for G with hasDerivAt_pi twice (import Mathlib.Analysis.Calculus.Deriv.Prod) and HasDerivAt.inner. The state space ι → E is not finite-dimensional, so build its CLM as Σ_i Σ_j K_ij • (pi of if i' = i then proj j else 0); continuity is then a finite sum of continuous.smul continuous_const. Deprecations in v4.35: ContinuousLinearMap.coe_sum' → FunLike.coe_sum, continuous_finset_sum → continuous_finsetSum.