Two explicit Adian--Rabin constructions

This file is the statement-level interface for the two constructions formalized in this project. The Miller--Tancer construction is generic in the number of generators and relators, subject to the normal-weight-one hypothesis. Gordon's Lemma 2.1 is generic in the host presentation and its abelian-order data.

theorem Undecidability.AdianRabin.exists_miller_tancer_family {n m : ℕ} (P : FP n m) (k : Fin n) (hP : ¬ComputablePred P.wordProblem) (hk : P.NormallyGenerates (Word.generator k)) : ∃ (A : ℕ → FP (n + 1) (m + 2)), FP.IsAdianRabinFamily A

The compressed Miller--Tancer construction produces an Adian--Rabin family with one additional generator and two additional relators when the normal generator is a displayed presentation generator.

theorem Undecidability.AdianRabin.exists_gordon_family {n m : ℕ} (P : FP n m) (condition : Gordon.Condition21 P) (hP : ¬ComputablePred P.wordProblem) : ∃ (A : ℕ → FP 2 (m + 1)), FP.IsAdianRabinFamily A

Gordon's Lemma 2.1 produces a two-generator Adian--Rabin family with one more relator than the host presentation.