[proofplan] The strategy is to extract the polar decomposition $JL = PS$ from the [Singular Value Decomposition](/theorems/3071) of $JL$ by regrouping factors. Writing $JL = U \Sigma V^\top$ with $U \in \mathbb{R}^{n\times n}$, $V \in \mathbb{R}^{m\times m}$ orthogonal and $\Sigma \in \mathbb{R}^{n\times m}$ rectangular diagonal with non-negative diagonal entries $\sigma_1 \ge \cdots \ge \sigma_m \ge 0$, we factor $\Sigma = J_{n,m} \tilde\Sigma$ where $J_{n,m} \in \mathbb{R}^{n\times m}$ is the standard isometric embedding (top block $I_m$, bottom block zero) and $\tilde\Sigma = \operatorname{diag}(\sigma_1, \dots, \sigma_m) \in \mathbb{R}^{m\times m}$. Defining $P := U J_{n,m} V^\top$ and $S := V \tilde\Sigma V^\top$ produces an isometric embedding and a symmetric positive semidefinite matrix whose product equals $JL$. Uniqueness of $S$ follows from $S^2 = JL^\top JL$ and uniqueness of the positive semidefinite square root, and $J_m L = \det S$ follows by combining $\det S = \prod_i \sigma_i$ with the [Jacobian as Product of Singular Values](/theorems/3072) identity. [/proofplan]

[step:Apply the SVD and split the rectangular diagonal matrix] Let $A := JL \in \mathbb{R}^{n \times m}$ with $m \le n$. By the [Singular Value Decomposition](/theorems/3071) (whose hypothesis $m \le n$ matches the hypothesis here), there exist orthogonal matrices $U \in \mathbb{R}^{n \times n}$ and $V \in \mathbb{R}^{m \times m}$ and a rectangular diagonal matrix $\Sigma \in \mathbb{R}^{n \times m}$ with diagonal entries $\sigma_1 \ge \sigma_2 \ge \cdots \ge \sigma_m \ge 0$ (the singular values of $L$) such that \begin{align*} A = U \Sigma V^\top. \end{align*} We split the rectangular diagonal $\Sigma$ as a product of an embedding and a square diagonal matrix. Define \begin{align*} J_{n,m} \in \mathbb{R}^{n \times m}, &\qquad (J_{n,m})_{ij} := \delta_{ij} \text{ for } i \in \{1, \dots, n\}, j \in \{1, \dots, m\}, \\ \tilde\Sigma &:= \operatorname{diag}(\sigma_1, \dots, \sigma_m) \in \mathbb{R}^{m \times m}, \end{align*} so $J_{n,m}$ has $I_m$ in its top $m$ rows and zeros in the bottom $n - m$ rows. A direct computation in coordinates verifies $\Sigma = J_{n,m} \tilde\Sigma$: for $i \in \{1, \dots, n\}$ and $j \in \{1, \dots, m\}$, \begin{align*} (J_{n,m} \tilde\Sigma)_{ij} = \sum_{k=1}^m (J_{n,m})_{ik} (\tilde\Sigma)_{kj} = \sum_{k=1}^m \delta_{ik} \sigma_k \delta_{kj}. \end{align*} The double Kronecker delta forces $i = k = j$, so the sum equals $\sigma_j$ when $i = j \le m$ and zero otherwise — which matches $\Sigma_{ij}$ exactly. Substituting, \begin{align*} A = U \Sigma V^\top = U J_{n,m} \tilde\Sigma V^\top. \end{align*} We also record the identity \begin{align*} (J_{n,m}^\top J_{n,m})_{jk} = \sum_{i=1}^n (J_{n,m})_{ij}(J_{n,m})_{ik} = \sum_{i=1}^n \delta_{ij}\delta_{ik} = \delta_{jk}, \qquad j,k \in \{1,\dots,m\}, \end{align*} i.e., $J_{n,m}^\top J_{n,m} = I_m$ — so $J_{n,m}$ is itself an isometric embedding $\mathbb{R}^m \hookrightarrow \mathbb{R}^n$. [/step]

[step:Define $P$ and $S$ and verify the polar identity $A = PS$] Define \begin{align*} P := U J_{n,m} V^\top \in \mathbb{R}^{n \times m}, \qquad S := V \tilde\Sigma V^\top \in \mathbb{R}^{m \times m}. \end{align*} We verify $A = PS$ by direct computation, using $V^\top V = I_m$ since $V$ is orthogonal: \begin{align*} PS = (U J_{n,m} V^\top)(V \tilde\Sigma V^\top) = U J_{n,m} (V^\top V) \tilde\Sigma V^\top = U J_{n,m} I_m \tilde\Sigma V^\top = U J_{n,m} \tilde\Sigma V^\top = A. \end{align*} [/step]

[step:Verify that $P$ is an isometric embedding] We show $P^\top P = I_m$. Using $U^\top U = I_n$ (since $U$ is orthogonal), $J_{n,m}^\top J_{n,m} = I_m$ (computed above), and $V V^\top = I_m$ (since $V$ is orthogonal), \begin{align*} P^\top P &= (U J_{n,m} V^\top)^\top (U J_{n,m} V^\top) \\ &= V J_{n,m}^\top U^\top U J_{n,m} V^\top \\ &= V J_{n,m}^\top J_{n,m} V^\top \\ &= V I_m V^\top \\ &= V V^\top \\ &= I_m. \end{align*} Hence $P$ satisfies the defining identity $P^\top P = I_m$ of an isometric embedding. In particular, $|Pw|^2 = (Pw)^\top(Pw) = w^\top P^\top P w = |w|^2$ for every $w \in \mathbb{R}^m$, so $P$ preserves Euclidean norms. [/step]

[step:Verify that $S$ is symmetric positive semidefinite] **Symmetry**: since $\tilde\Sigma$ is diagonal hence symmetric, \begin{align*} S^\top = (V \tilde\Sigma V^\top)^\top = V \tilde\Sigma^\top V^\top = V \tilde\Sigma V^\top = S. \end{align*} **Positive semidefiniteness**: for any $w \in \mathbb{R}^m$, set $z := V^\top w \in \mathbb{R}^m$ (so $w = V z$ since $V$ is orthogonal). Then \begin{align*} w^\top S w = w^\top V \tilde\Sigma V^\top w = z^\top \tilde\Sigma z = \sum_{i=1}^m \sigma_i z_i^2 \ge 0, \end{align*} using $\sigma_i \ge 0$ and $z_i^2 \ge 0$ for every $i$. Hence $S$ is symmetric positive semidefinite. [/step]

[step:Identify $S = (A^\top A)^{1/2}$ and deduce uniqueness] Compute $S^2$ using $V^\top V = I_m$: \begin{align*} S^2 = (V \tilde\Sigma V^\top)(V \tilde\Sigma V^\top) = V \tilde\Sigma (V^\top V) \tilde\Sigma V^\top = V \tilde\Sigma^2 V^\top. \end{align*} On the other hand, using $A = PS$, $S^\top = S$, and $P^\top P = I_m$: \begin{align*} A^\top A = (PS)^\top(PS) = S^\top P^\top P S = S \cdot I_m \cdot S = S^2. \end{align*} Hence $S^2 = A^\top A$. Combined with the symmetry and positive semidefiniteness of $S$ established above, $S$ is a positive semidefinite square root of $A^\top A$. We now invoke uniqueness of the positive semidefinite square root: any symmetric positive semidefinite matrix $M \in \mathbb{R}^{m \times m}$ has a unique symmetric positive semidefinite square root. To verify this in our setting: suppose $T \in \mathbb{R}^{m \times m}$ is symmetric positive semidefinite with $T^2 = A^\top A$. By the Spectral Theorem, $T = W \operatorname{diag}(\mu_1, \dots, \mu_m) W^\top$ for some orthogonal $W$ and $\mu_i \ge 0$. Then \begin{align*} A^\top A = T^2 = W \operatorname{diag}(\mu_1^2, \dots, \mu_m^2) W^\top. \end{align*} This is an orthogonal diagonalisation of $A^\top A$, so the multiset $\{\mu_i^2\}$ equals the multiset of eigenvalues of $A^\top A$ (which depend only on $A^\top A$, as the roots of its characteristic polynomial). Since $\mu_i \ge 0$, taking square roots determines the $\mu_i$ uniquely as a multiset. Furthermore, on each eigenspace of $A^\top A$ the action of $T$ is multiplication by the corresponding $\mu$, which is the same operator regardless of the choice of orthonormal basis $W$. Hence $T$ is uniquely determined by $A^\top A$. We may therefore write $S = (A^\top A)^{1/2}$ unambiguously. [/step]

[step:Compute $J_m L = \det S$] By the [Jacobian as Product of Singular Values](/theorems/3072), $J_m L = \sigma_1 \sigma_2 \cdots \sigma_m$. We compute $\det S$ using $S = V \tilde\Sigma V^\top$ and the multiplicativity of the determinant: \begin{align*} \det S = \det(V) \det(\tilde\Sigma) \det(V^\top) = \det(V)^2 \det(\tilde\Sigma) = \det(\tilde\Sigma) = \prod_{i=1}^m \sigma_i, \end{align*} using $\det(V) \in \{+1, -1\}$ (so $\det(V)^2 = 1$) since $V$ is orthogonal, and the determinant of a diagonal matrix is the product of its diagonal entries. Therefore $J_m L = \prod_{i=1}^m \sigma_i = \det S$, completing the proof of all the assertions of the theorem. [/step]