Borisov's simulation criterion

The forward implication is the relator calculation in Construction.lean. The converse is the complete normal-form argument, culminating in the mod-five free-product syllable comparison that bounds a coefficient preimage by one displayed rule letter.

theorem Undecidability.Borisov.criterion_converse (datum : Thue.StandingDatum) (Q : List (Fin 2)) : (presentation datum).wordProblem (testWord Q) → ThueEq (Thue.systemOf datum.F datum.E) Q datum.P

The deep normal-form direction in Borisov's simulation theorem.

theorem Undecidability.Borisov.criterion (datum : Thue.StandingDatum) (Q : List (Fin 2)) : ThueEq (Thue.systemOf datum.F datum.E) Q datum.P ↔ (presentation datum).wordProblem (testWord Q)

Borisov's simulation theorem, specialized to the standing datum.