Semantic inverse for the six compression eliminations

The compressed presentation need not be identified with the final HNN model in order to prove that the Borisov group survives the compression. It is enough to interpret the three surviving generators D,S,Z in the final HNN model. The six conjugation equations recover all nine old generators, and therefore give a homomorphism from the compressed presentation to that model. The resulting triangle with Compression.hom commutes. Its other side is the composite of three known injective maps, so Compression.hom is injective.

@[reducible, inline]

abbrev Undecidability.HostCompressionInjective.Z (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) : Type

The final host model after the two proper compression HNN extensions.

Equations

• Undecidability.HostCompressionInjective.Z datum theta zeta = Undecidability.HostZStage.ZStage datum theta zeta

noncomputable def Undecidability.HostCompressionInjective.gammaToZ (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) : HostYStage.Gamma datum →* Z datum theta zeta

The original Borisov model included through both proper HNN stages.

Equations

• Undecidability.HostCompressionInjective.gammaToZ datum theta zeta = (Undecidability.HostZStage.toZStage datum theta zeta).comp (Undecidability.HostYStage.toYStage datum theta)

noncomputable def Undecidability.HostCompressionInjective.oldValue (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) : Host.OldGen → Z datum theta zeta

Values of the nine generators immediately before the six eliminations.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.HostCompressionInjective.oldValue datum theta zeta Undecidability.Host.OldGen.z = Undecidability.HostZStage.zLetter datum theta zeta

noncomputable def Undecidability.HostCompressionInjective.hostValue (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) : Fin 3 → Z datum theta zeta

Values of the retained generators (D,S,Z).

Equations

• One or more equations did not get rendered due to their size.

theorem Undecidability.HostCompressionInjective.eval_tau (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (g : Host.OldGen) : Word.eval (hostValue datum theta zeta) (Host.tau g) = oldValue datum theta zeta g

Each ordered substitution word evaluates back to the old generator it eliminated.

Evaluation of words in the nine-generator alphabet

noncomputable def Undecidability.HostCompressionInjective.evalOld (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (w : Host.OldWord) : Z datum theta zeta

Semantic evaluation of a word in the old, nine-generator alphabet.

Equations

• Undecidability.HostCompressionInjective.evalOld datum theta zeta w = (FreeGroup.lift (Undecidability.HostCompressionInjective.oldValue datum theta zeta)) (FreeGroup.mk w)

@[simp]

theorem Undecidability.HostCompressionInjective.evalOld_generator (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (g : Host.OldGen) : evalOld datum theta zeta (Host.OldWord.generator g) = oldValue datum theta zeta g

@[simp]

theorem Undecidability.HostCompressionInjective.evalOld_mul (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (u v : Host.OldWord) : evalOld datum theta zeta (u.mul v) = evalOld datum theta zeta u * evalOld datum theta zeta v

@[simp]

theorem Undecidability.HostCompressionInjective.evalOld_inverse (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (u : Host.OldWord) : evalOld datum theta zeta u.inverse = (evalOld datum theta zeta u)⁻¹

@[simp]

theorem Undecidability.HostCompressionInjective.evalOld_product (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (us : List Host.OldWord) : evalOld datum theta zeta (Host.OldWord.product us) = (List.map (evalOld datum theta zeta) us).prod

@[simp]

theorem Undecidability.HostCompressionInjective.evalOld_pow (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (u : Host.OldWord) (n : ℕ) : evalOld datum theta zeta (u.pow n) = evalOld datum theta zeta u ^ n

theorem Undecidability.HostCompressionInjective.evalOld_positive (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (w : List (Fin 2)) : evalOld datum theta zeta (Host.OldWord.positive w) = (List.map (fun (i : Fin 2) => if i = 0 then oldValue datum theta zeta Host.OldGen.s1 else oldValue datum theta zeta Host.OldGen.s2) w).prod

@[simp]

theorem Undecidability.HostCompressionInjective.evalOld_relation (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (u v : Host.OldWord) : evalOld datum theta zeta (u.relation v) = evalOld datum theta zeta u * (evalOld datum theta zeta v)⁻¹

@[simp]

theorem Undecidability.HostCompressionInjective.evalOld_commutator (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (u v : Host.OldWord) : evalOld datum theta zeta (u.commutator v) = (evalOld datum theta zeta u)⁻¹ * (evalOld datum theta zeta v)⁻¹ * evalOld datum theta zeta u * evalOld datum theta zeta v

theorem Undecidability.HostCompressionInjective.eval_evaluate (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (w : Host.OldWord) : Word.eval (hostValue datum theta zeta) (Host.OldWord.evaluate Host.tau w) = evalOld datum theta zeta w

Evaluation commutes with substitution of the six eliminated generators.

The nine surviving relations in the semantic model

noncomputable def Undecidability.HostCompressionInjective.borisovValue (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) : Fin 7 → Z datum theta zeta

Borisov's seven generators, included in the final z-stage.

Equations

• One or more equations did not get rendered due to their size.

theorem Undecidability.HostCompressionInjective.borisovValue_eq_oldGenerator (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (i : Fin 7) : borisovValue datum theta zeta i = oldValue datum theta zeta (Host.Compression.oldGenerator i)

theorem Undecidability.HostCompressionInjective.borisov_relator_eq_one (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (i : Fin 14) : Word.eval (borisovValue datum theta zeta) ((Borisov.presentation datum).relator i) = 1

Every Borisov relator remains valid after the two proper HNN extensions.

theorem Undecidability.HostCompressionInjective.surviving_relator_eq_one (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (i : Fin 9) : evalOld datum theta zeta (Host.oldSurvivingRelator datum.F datum.E datum.P i) = 1

The eight inherited Borisov relations and the last y-relation all hold before syntactic elimination.

The decompression homomorphism

theorem Undecidability.HostCompressionInjective.host_relator_eq_one (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (i : Fin 9) : Word.eval (hostValue datum theta zeta) ((Host.presentationOf datum).relator i) = 1

noncomputable def Undecidability.HostCompressionInjective.fromHost (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) : (Host.presentationOf datum).Group →* Z datum theta zeta

Interpret the compressed three-generator presentation in the final HNN model. This is the one-sided semantic inverse needed for injectivity.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Undecidability.HostCompressionInjective.fromHost_of (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (i : Fin 3) : (fromHost datum theta zeta) (PresentedGroup.of i) = hostValue datum theta zeta i

theorem Undecidability.HostCompressionInjective.fromHost_evalWord (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) (w : Host.HostWord) : (fromHost datum theta zeta) ((Host.presentationOf datum).evalWord w) = Word.eval (hostValue datum theta zeta) w

noncomputable def Undecidability.HostCompressionInjective.borisovToZ (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) : (Borisov.presentation datum).Group →* Z datum theta zeta

The injective route from Borisov's presentation through its semantic model and the two proper HNN extensions.

Equations

• One or more equations did not get rendered due to their size.

theorem Undecidability.HostCompressionInjective.borisovToZ_injective (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) : Function.Injective ⇑(borisovToZ datum theta zeta)

theorem Undecidability.HostCompressionInjective.fromHost_comp_compression (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) : (fromHost datum theta zeta).comp (Host.Compression.hom datum) = borisovToZ datum theta zeta

The six eliminations commute with the semantic inclusions.

theorem Undecidability.HostCompressionInjective.compression_injective_of (datum : Thue.StandingDatum) (theta : HostYStage.ThetaData datum) (zeta : HostZStage.ZetaData datum theta) : Host.Compression.Injective datum

The subgroup equivalences constructed in Section 3 of the paper imply injectivity of the compression homomorphism.

theorem Undecidability.Host.compression_injective (datum : Thue.StandingDatum) : Compression.Injective datum

The canonical data from Section 3 of the paper give compression injectivity for the concrete simulator.