Palindromic length in free groups through reflection length and noncrossing matchings

We express palindromic length in a finitely generated free group as the minimum of two reflection lengths in a universal Coxeter group. The identity converts optimal reflection factorizations into optimal palindromic factorizations. Combined with the classical cancellation-norm recurrence, it gives a concrete algorithm with \(O(L^3)\) arithmetic and symbol operations, \(O(L^2)\) table entries and \(O(L^2)\) written output for a reduced input of length \(L>0\). Qualitative computability already follows from Dahmani–Guirardel's theorem on twisted equations; the present construction supplies the explicit reduction and quantitative algorithm. The length identity, solver correctness and optimality, and explicit counting bounds are formalised in Lean 4.