[proofplan] We prove the $LDL^\top$ factorisation of a symmetric positive-definite matrix by first showing all leading principal minors are positive (so LU exists), then extracting the diagonal from $U$ and using symmetry to force $\tilde{U} = L^\top$. [/proofplan] [step:Show leading minors are positive and obtain the LU factorisation] For each $k$, the leading principal submatrix $A_k$ is symmetric positive-definite (restrict the quadratic form to vectors with last $n-k$ entries zero), so $\det(A_k) > 0$. By the [LU Existence Theorem](/theorems/497), $A = LU$ uniquely with $L$ unit lower triangular and $U$ upper triangular. [/step] [step:Extract the diagonal and use symmetry to identify $\tilde{U} = L^\top$] Let $D = \operatorname{diag}(U_{11}, \ldots, U_{nn})$ and $\tilde{U} = D^{-1}U$ (well-defined since $U_{kk} = \det(A_k)/\det(A_{k-1}) > 0$). Then $\tilde{U}$ is unit upper triangular and $A = LD\tilde{U}$. From $A = A^\top$: $LD\tilde{U} = \tilde{U}^\top D L^\top$. By uniqueness of LU factorisation, $L = \tilde{U}^\top$, i.e., $\tilde{U} = L^\top$. Therefore $A = LDL^\top$ with $D_{kk} > 0$. Uniqueness follows from the uniqueness of LU and the forced relation $\tilde{U} = L^\top$. [/step]