NashEmbedding witness tests: realizable metrics + Theorem A

Concrete witness checks for NashEmbedding/Torus/RealizableMetrics.lean and NashEmbedding/Torus/Approximation/SmoothMetricApprox.lean:

• TN1 — closure under addition (realizable_sum).
• TN2 — closure under non-negative scaling (realizable_nonneg_smul).
• TN3 — injRealizable_posDef: injectively realizable ⟹ pos-def smooth.
• TN4 — convex_combination_approx invocation on the flat metric.