Documentation

MIPRE.Tailored.Sofic.AldousLyons

The Aldous–Lyons conjecture is false, from a halting reduction to tailored games #

Corollary I:2144 assembled: Main Theorem II (mainTheoremII, gap gapK) and Main Theorem I (Measure.aldous_lyons_false_of, through the ergodic value and its upper approximation by pseudo-subgroup polytopes) leave a halting reduction to tailored games as the only hypothesis.

source
theorem MIPRE.Tailored.Sofic.aldous_lyons_false (hred : TailoredGameValue.TailoredHaltingReduction) :
¬SubgroupTestValue.AldousLyons

The Aldous–Lyons conjecture is false (Corollary I:2144), from a halting reduction to tailored games.