Friedman and Stanley asked whether an invariant Borel class of countable structures must be Borel complete whenever every countable level of their tree-isomorphism hierarchy Borel-reduces to it.

The authors build a single invariant Borel class in one fixed countable language, parameterized by closed subgroups of S_∞ × S_∞, using ultrahomogeneous structures whose automorphism groups are the given subgroups. They show that coset relations of Polishable subgroups are cofinal in the Friedman–Stanley hierarchy, using a layered coding with finite contexts and Boolean matrices, and then show that graph isomorphism does not reduce to the class. The structural theorem and four supporting statements are formalized in Lean 4.30.0 against a pinned Mathlib revision.

The paper gives a negative answer to the Friedman–Stanley question: there is an L_{ω1ω} sentence to which every countable Friedman–Stanley level reduces, while graph isomorphism does not reduce to it. The Lean proof uses only standard axioms and contains no unfinished placeholders. The López–Escobar step and the Appendix A arguments are not formalized.