Evaluating positive rank-five words in the mod-five quotient

This file connects the displayed u- and v-basis lifts in Borisov's two-HNN group with the explicit evaluator in GroupUndecidability.Borisov.Mod5.BaseWords. For a positive freely reduced word, inverses do not occur, so evaluation is just the product of the corresponding quotient basis elements.

@[reducible, inline]

abbrev Undecidability.BorisovModFiveEvalBridge.Basis : Type

The indices of the stable and rewriting-rule basis elements.

Equations

• Undecidability.BorisovModFiveEvalBridge.Basis = Undecidability.BorisovCStage.RuleBasis

@[simp]

theorem Undecidability.BorisovModFiveEvalBridge.gamma3ToQuotient_stable3 (beta : Fin 2) : BorisovModFiveQuotient.gamma3ToQuotient (BorisovCStage.stable3 beta) = BorisovModFiveQuotient.quotientStable

@[simp]

theorem Undecidability.BorisovModFiveEvalBridge.gamma3ToQuotient_positive3 (word : List (Fin 2)) : BorisovModFiveQuotient.gamma3ToQuotient (BorisovCStage.positive3 word) = BorisovModFiveQuotient.quotientStable ^ word.length

@[simp]

theorem Undecidability.BorisovModFiveEvalBridge.gamma3ToQuotient_uBasis (datum : Thue.StandingDatum) (q : Basis) : BorisovModFiveQuotient.gamma3ToQuotient (BorisovCStage.uBasis datum q) = BorisovModFiveBaseWords.quotientBasis datum.F q

@[simp]

theorem Undecidability.BorisovModFiveEvalBridge.gamma3ToQuotient_vBasis (datum : Thue.StandingDatum) (q : Basis) : BorisovModFiveQuotient.gamma3ToQuotient (BorisovCStage.vBasis datum q) = BorisovModFiveBaseWords.quotientBasis datum.E q

theorem Undecidability.BorisovModFiveEvalBridge.gamma3ToQuotient_uLift_of_allPositive (datum : Thue.StandingDatum) (w : FreeGroup Basis) (hpositive : BorisovCoefficientShapes.AllPositive w.toWord) : BorisovModFiveQuotient.gamma3ToQuotient ((BorisovCStage.uLift datum) w) = BorisovModFiveBaseWords.quotientEval datum.F (List.map Prod.fst w.toWord)

A positive source-basis word is evaluated by the explicit mod-five quotient evaluator after forgetting its (necessarily positive) signs.

theorem Undecidability.BorisovModFiveEvalBridge.gamma3ToQuotient_vLift_of_allPositive (datum : Thue.StandingDatum) (w : FreeGroup Basis) (hpositive : BorisovCoefficientShapes.AllPositive w.toWord) : BorisovModFiveQuotient.gamma3ToQuotient ((BorisovCStage.vLift datum) w) = BorisovModFiveBaseWords.quotientEval datum.E (List.map Prod.fst w.toWord)

Target-basis counterpart of gamma3ToQuotient_uLift_of_allPositive.

Rule sparsity from the mod-five Borisov quotient

In the quotient (C₅ * C₅) ⋊ ℤ, both stable letters act by factorwise inversion. A positive displayed rule contributes two alternating nonzero free-product syllables. The padded coefficient d^f Q e^r, on the other hand, has at most one syllable in each free factor. Equality therefore forces the displayed rank-five word to contain at most one rule letter.

@[reducible, inline]

abbrev Undecidability.BorisovModFiveSparsity.Basis : Type

The indices of the stable and rewriting-rule basis elements.

Equations

• Undecidability.BorisovModFiveSparsity.Basis = Undecidability.BorisovCStage.RuleBasis

@[simp]

theorem Undecidability.BorisovModFiveSparsity.basisRuleCount_map_fst (letters : List (Basis × Bool)) : BorisovModFiveBaseWords.basisRuleCount (List.map Prod.fst letters) = BorisovCoefficientShapes.ruleCount letters

@[simp]

theorem Undecidability.BorisovModFiveSparsity.quotientBase_zpow_left (x : BorisovModFiveQuotient.ModFiveBase) (n : ℤ) : (BorisovModFiveQuotient.quotientBase x ^ n).left = x ^ n

@[simp]

theorem Undecidability.BorisovModFiveSparsity.quotientBase_zpow_right (x : BorisovModFiveQuotient.ModFiveBase) (n : ℤ) : (BorisovModFiveQuotient.quotientBase x ^ n).right = 1

theorem Undecidability.BorisovModFiveSparsity.quotient_coefficient_left (Q : List (Fin 2)) (f r : ℤ) : (BorisovModFiveQuotient.gamma3ToQuotient (BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r)).left = BorisovModFiveQuotient.modD ^ f * (BorisovModFiveQuotient.invertFactors ^ Q.length) (BorisovModFiveQuotient.modE ^ r)

theorem Undecidability.BorisovModFiveSparsity.modD_zpow_as_letter (f : ℤ) : BorisovModFiveQuotient.modD ^ f = Monoid.CoprodI.of (BorisovModFiveQuotient.c5Generator ^ f)

theorem Undecidability.BorisovModFiveSparsity.twisted_modE_zpow_as_letter (n : ℕ) (r : ℤ) : (BorisovModFiveQuotient.invertFactors ^ n) (BorisovModFiveQuotient.modE ^ r) = Monoid.CoprodI.of ((BorisovModFiveBaseWords.invertC5 ^ n) (BorisovModFiveQuotient.c5Generator ^ r))

theorem Undecidability.BorisovModFiveSparsity.coefficient_normalForm_length_le_two (Q : List (Fin 2)) (f r : ℤ) : (Monoid.CoprodI.Word.equiv (BorisovModFiveQuotient.modD ^ f * (BorisovModFiveQuotient.invertFactors ^ Q.length) (BorisovModFiveQuotient.modE ^ r))).toList.length ≤ 2

The source and target parsers

theorem Undecidability.BorisovModFiveSparsity.u_ruleCount_le_one (datum : Thue.StandingDatum) (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup Basis) (heval : (BorisovCStage.uLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r) : BorisovCoefficientShapes.ruleCount w.toWord ≤ 1

The source-basis word representing a padded positive coefficient contains at most one displayed Thue-rule letter.

theorem Undecidability.BorisovModFiveSparsity.v_ruleCount_le_one (datum : Thue.StandingDatum) (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup Basis) (heval : (BorisovCStage.vLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r) : BorisovCoefficientShapes.ruleCount w.toWord ≤ 1

Target-basis counterpart of u_ruleCount_le_one.

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

Borisov's converse criterion obtained from the mod-five free-product rule-count bound.