The simulator-specific statement is a classification of one base-group coefficient. Notice that it mentions neither c, nor t, nor either of the final HNN extensions.

@[reducible, inline]

abbrev Undecidability.BorisovLemma4Pinch.ChainRel (datum : Thue.StandingDatum) (_hfree : BorisovCStage.RankFiveFree datum) (a b : ℤˣ × BorisovHNNModel.Gamma3) : Prop

The reducedness condition relating consecutive stable-letter syllables.

Equations

• Undecidability.BorisovLemma4Pinch.ChainRel datum _hfree a b = (a.2 ∈ HNNExtension.toSubgroup (Undecidability.BorisovCStage.U datum) (Undecidability.BorisovCStage.V datum) a.1 → a.1 = b.1)

theorem Undecidability.BorisovLemma4Pinch.lemma4_boundary_pinch (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (P Q : List (Fin 2)) (L : BorisovCStage.LeftContext datum hfree) (R : BorisovCStage.RightContext datum hfree) (heq : BorisovCStage.Lemma4Equation datum hfree P Q L R) (hpositive : BorisovCStage.contextComplexity datum hfree L R ≠ 0) : ∃ (pre : List (ℤˣ × BorisovHNNModel.Gamma3)) (u : ℤˣ) (a : BorisovHNNModel.Gamma3) (v : ℤˣ) (b : BorisovHNNModel.Gamma3) (tail : List (ℤˣ × BorisovHNNModel.Gamma3)), L.word.toList = pre ++ [(u, a)] ∧ R.word.toList = (v, b) :: tail ∧ a * BorisovCStage.positive3 Q * R.word.head ∈ HNNExtension.toSubgroup (BorisovCStage.U datum) (BorisovCStage.V datum) u ∧ v = -u

The first genuinely group-theoretic step in Borisov's positive-c induction. If P⁻¹ L Q R = 1 and at least one c occurs, then both contexts contain a stable letter and the coefficient across their boundary is a Britton pinch.

theorem Undecidability.BorisovLemma4Pinch.lemma4_boundary_pinch_power_form (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (P Q : List (Fin 2)) (L : BorisovCStage.LeftContext datum hfree) (R : BorisovCStage.RightContext datum hfree) (heq : BorisovCStage.Lemma4Equation datum hfree P Q L R) (hpositive : BorisovCStage.contextComplexity datum hfree L R ≠ 0) : ∃ (f : ℤ) (r : ℤ) (pre : List (ℤˣ × BorisovHNNModel.Gamma3)) (b : BorisovHNNModel.Gamma3) (tail : List (ℤˣ × BorisovHNNModel.Gamma3)), L.word.toList = pre ++ [(1, BorisovHNNModel.d3 ^ f)] ∧ R.word.toList = (-1, b) :: tail ∧ R.word.head = BorisovHNNModel.e3 ^ r ∧ BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.U datum ∨ L.word.toList = pre ++ [(-1, BorisovHNNModel.d3 ^ f)] ∧ R.word.toList = (1, b) :: tail ∧ R.word.head = BorisovHNNModel.e3 ^ r ∧ BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.V datum

The boundary pinch with the cyclic context coefficients written as integer powers. These are the two cases to which Borisov's Assertion V is applied: an A-pinch rewrites an F_i, and a B-pinch rewrites an E_i.

noncomputable def Undecidability.BorisovLemma4Pinch.listValue (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (l : List (ℤˣ × BorisovHNNModel.Gamma3)) : BorisovCStage.Gamma2 datum hfree

The group value of a list of signed stable-letter syllables.

Equations

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

noncomputable def Undecidability.BorisovLemma4Pinch.prefixValue (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (head : BorisovHNNModel.Gamma3) (l : List (ℤˣ × BorisovHNNModel.Gamma3)) : BorisovCStage.Gamma2 datum hfree

The group value of an initial base coefficient followed by the supplied syllables.

Equations

• Undecidability.BorisovLemma4Pinch.prefixValue datum hfree head l = (Undecidability.BorisovCStage.of3 datum hfree) head * Undecidability.BorisovLemma4Pinch.listValue datum hfree l

structure Undecidability.BorisovLemma4Pinch.PinchClassification (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Prop

Borisov's Assertion V in the exact coefficient form consumed by Lemma 4. An U-coefficient is transported by cEquiv; a V-coefficient is transported by its inverse. In both cases the positive middle word changes by finitely many (in the published proof, at most one) Thue steps.

• source (Q : List (Fin 2)) (f r : ℤ) (hmem : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.U datum) : ∃ (Q' : List (Fin 2)) (f' : ℤ) (r' : ℤ), ThueEq (Thue.systemOf datum.F datum.E) Q Q' ∧ ↑((BorisovCStage.cEquiv datum hfree) ⟨BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r, hmem⟩) = BorisovHNNModel.d3 ^ f' * BorisovCStage.positive3 Q' * BorisovHNNModel.e3 ^ r'
• target (Q : List (Fin 2)) (f r : ℤ) (hmem : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.V datum) : ∃ (Q' : List (Fin 2)) (f' : ℤ) (r' : ℤ), ThueEq (Thue.systemOf datum.F datum.E) Q Q' ∧ ↑((BorisovCStage.cEquiv datum hfree).symm ⟨BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r, hmem⟩) = BorisovHNNModel.d3 ^ f' * BorisovCStage.positive3 Q' * BorisovHNNModel.e3 ^ r'

theorem Undecidability.BorisovLemma4Pinch.pinchReduction_of_classification (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hclass : PinchClassification datum hfree) : BorisovCStage.PinchReduction datum hfree

All HNN manipulation in the positive-c induction follows formally from the base-group coefficient classification.

theorem Undecidability.BorisovLemma4Pinch.borisovLemma4_of_classification (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hclass : PinchClassification datum hfree) : BorisovCStage.BorisovLemma4 datum hfree

Borisov's Lemma 4 derived from PinchClassification.