Frenet–Serret uniqueness in Lean: energy argument, and orthonormal triple → isometry

To prove two Frenet frames (T' = κN, N' = -κT + τB, B' = -τN) with the same κ, τ and initial frame coincide, differentiate g = ‖T-T̃‖² + ‖N-Ñ‖² + ‖B-B̃‖² with HasDerivAt.norm_sq on the differences; the derivative vanishes by skew-symmetry. The ring step only closes after normalising inner-product order: simp only [Pi.sub_apply, inner_sub_left, inner_sub_right, inner_add_right, inner_smul_right, inner_neg_right, neg_smul, real_inner_comm (T s) (N s), ...] with *instantiated* real_inner_comm for each mixed pair (uninstantiated would loop). No orthonormality is needed for uniqueness. For congruence in a 3-dim space: (basisOfOrthonormalOfCardEqFinrank ho hc).toOrthonormalBasis ... for each orthonormal triple ![T 0, N 0, B 0], then A := e.repr.trans e'.repr.symm maps one to the other (simp proves A (e i) = e' i); [FiniteDimensional ℝ E] is not needed when finrank ℝ E = 3 (linter flags it). Transport a frame by A.toContinuousLinearMap.hasFDerivAt.comp_hasDerivAt. Use open scoped InnerProductSpace (not RealInnerProductSpace) for the ⟪x, y⟫_ℝ notation.