English
There exists a computable truncation of a swap-factorization exposing a finite witness that every permutation is a product of transpositions.
Русский
Существуют вычислимые трUNC-версии разложения на транспозиции, показывающие конечное доказательство того, что любая перестановка является произведением транспозиций.
LaTeX
$$$ \\mathrm{truncSwapFactors} [Fintype\\ α] (f : Perm\\ α) : Trunc { l : List (Perm α) // l.prod = f ∧ ∀ g ∈ l, g.isSwap } $$$
Lean4
/-- This computably represents the fact that any permutation can be represented as the product of
a list of transpositions. -/
def truncSwapFactors [Fintype α] (f : Perm α) : Trunc { l : List (Perm α) // l.prod = f ∧ ∀ g ∈ l, IsSwap g } :=
Quotient.recOnSubsingleton (@univ α _).1 (fun l h => Trunc.mk (swapFactorsAux l f (h _)))
(show ∀ x, f x ≠ x → x ∈ (@univ α _).1 from fun _ _ => mem_univ _)
