Concrete one-rule cases of Borisov's pinch classifier

BorisovLemma4Pinch.PinchClassification asks for a classification of every coefficient of the form d^f Q e^r lying in one of the two rank-five subgroups. The central normal-form step shows that its unique rank-five preimage contains either no rule letter or exactly one rule letter.

This file proves the complete coefficient calculation in the latter case: if the coefficient is a positive stable prefix, followed by one displayed rule generator, followed by a positive stable suffix, then conjugating by the c-HNN equivalence performs exactly the corresponding Thue rewrite and again has the required d^f Q e^r shape.

Moving padding powers across positive stable words

theorem Undecidability.BorisovPinchCoefficientClassification.stable3_mul_d_zpow (beta : Fin 2) (n : ℤ) : BorisovCStage.stable3 beta * BorisovHNNModel.d3 ^ n = BorisovHNNModel.d3 ^ (4 * n) * BorisovCStage.stable3 beta

theorem Undecidability.BorisovPinchCoefficientClassification.e_zpow_mul_stable3 (beta : Fin 2) (n : ℤ) : BorisovHNNModel.e3 ^ n * BorisovCStage.stable3 beta = BorisovCStage.stable3 beta * BorisovHNNModel.e3 ^ (4 * n)

theorem Undecidability.BorisovPinchCoefficientClassification.positive3_mul_d_zpow (w : List (Fin 2)) (n : ℤ) : BorisovCStage.positive3 w * BorisovHNNModel.d3 ^ n = BorisovHNNModel.d3 ^ (4 ^ w.length * n) * BorisovCStage.positive3 w

theorem Undecidability.BorisovPinchCoefficientClassification.e_zpow_mul_positive3 (w : List (Fin 2)) (n : ℤ) : BorisovHNNModel.e3 ^ n * BorisovCStage.positive3 w = BorisovCStage.positive3 w * BorisovHNNModel.e3 ^ (4 ^ w.length * n)

theorem Undecidability.BorisovPinchCoefficientClassification.positive3_mul_d_pow (w : List (Fin 2)) (n : ℕ) : BorisovCStage.positive3 w * BorisovHNNModel.d3 ^ n = BorisovHNNModel.d3 ^ (4 ^ w.length * ↑n) * BorisovCStage.positive3 w

theorem Undecidability.BorisovPinchCoefficientClassification.e_pow_mul_positive3 (w : List (Fin 2)) (n : ℕ) : BorisovHNNModel.e3 ^ n * BorisovCStage.positive3 w = BorisovCStage.positive3 w * BorisovHNNModel.e3 ^ (4 ^ w.length * ↑n)

The displayed bases as elements of their range subgroups

noncomputable def Undecidability.BorisovPinchCoefficientClassification.sourceBasis (datum : Thue.StandingDatum) (q : BorisovCStage.RuleBasis) : ↥(BorisovCStage.U datum)

A generator of the source rewriting-rule subgroup, with its subgroup membership witness.

Equations

• Undecidability.BorisovPinchCoefficientClassification.sourceBasis datum q = ⟨Undecidability.BorisovCStage.uBasis datum q, ⋯⟩

noncomputable def Undecidability.BorisovPinchCoefficientClassification.targetBasis (datum : Thue.StandingDatum) (q : BorisovCStage.RuleBasis) : ↥(BorisovCStage.V datum)

The corresponding generator of the target rewriting-rule subgroup.

Equations

• Undecidability.BorisovPinchCoefficientClassification.targetBasis datum q = ⟨Undecidability.BorisovCStage.vBasis datum q, ⋯⟩

noncomputable def Undecidability.BorisovPinchCoefficientClassification.sourcePositive (datum : Thue.StandingDatum) (w : List (Fin 2)) : ↥(BorisovCStage.U datum)

Evaluate a positive stable-letter word inside the source rewriting-rule subgroup.

Equations

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

noncomputable def Undecidability.BorisovPinchCoefficientClassification.targetPositive (datum : Thue.StandingDatum) (w : List (Fin 2)) : ↥(BorisovCStage.V datum)

Evaluate a positive stable-letter word inside the target rewriting-rule subgroup.

Equations

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

@[simp]

theorem Undecidability.BorisovPinchCoefficientClassification.coe_sourceBasis (datum : Thue.StandingDatum) (q : BorisovCStage.RuleBasis) : ↑(sourceBasis datum q) = BorisovCStage.uBasis datum q

@[simp]

theorem Undecidability.BorisovPinchCoefficientClassification.coe_targetBasis (datum : Thue.StandingDatum) (q : BorisovCStage.RuleBasis) : ↑(targetBasis datum q) = BorisovCStage.vBasis datum q

@[simp]

theorem Undecidability.BorisovPinchCoefficientClassification.coe_sourcePositive (datum : Thue.StandingDatum) (w : List (Fin 2)) : ↑(sourcePositive datum w) = BorisovCStage.positive3 w

@[simp]

theorem Undecidability.BorisovPinchCoefficientClassification.coe_targetPositive (datum : Thue.StandingDatum) (w : List (Fin 2)) : ↑(targetPositive datum w) = BorisovCStage.positive3 w

theorem Undecidability.BorisovPinchCoefficientClassification.cEquiv_sourceBasis (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (q : BorisovCStage.RuleBasis) : (BorisovCStage.cEquiv datum hfree) (sourceBasis datum q) = targetBasis datum q

theorem Undecidability.BorisovPinchCoefficientClassification.cEquiv_sourcePositive (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (w : List (Fin 2)) : (BorisovCStage.cEquiv datum hfree) (sourcePositive datum w) = targetPositive datum w

theorem Undecidability.BorisovPinchCoefficientClassification.cEquiv_symm_targetPositive (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (w : List (Fin 2)) : (BorisovCStage.cEquiv datum hfree).symm (targetPositive datum w) = sourcePositive datum w

theorem Undecidability.BorisovPinchCoefficientClassification.cEquiv_symm_targetBasis (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (q : BorisovCStage.RuleBasis) : (BorisovCStage.cEquiv datum hfree).symm (targetBasis datum q) = sourceBasis datum q

@[simp]

theorem Undecidability.BorisovPinchCoefficientClassification.positive3_append (u v : List (Fin 2)) : BorisovCStage.positive3 (u ++ v) = BorisovCStage.positive3 u * BorisovCStage.positive3 v

@[simp]

theorem Undecidability.BorisovPinchCoefficientClassification.positiveFree_append (u v : List (Fin 2)) : BorisovCStage.positiveFree (u ++ v) = BorisovCStage.positiveFree u * BorisovCStage.positiveFree v

Reading the middle positive word from a one-rule coefficient

theorem Undecidability.BorisovPinchCoefficientClassification.positive_word_eq_of_source_one_rule (datum : Thue.StandingDatum) (Q left right : List (Fin 2)) (f r : ℤ) (i : Fin 3) (hshape : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r = BorisovCStage.positive3 left * BorisovCStage.a3 datum i * BorisovCStage.positive3 right) : Q = left ++ datum.F i ++ right

theorem Undecidability.BorisovPinchCoefficientClassification.positive_word_eq_of_target_one_rule (datum : Thue.StandingDatum) (Q left right : List (Fin 2)) (f r : ℤ) (i : Fin 3) (hshape : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r = BorisovCStage.positive3 left * BorisovCStage.b3 datum i * BorisovCStage.positive3 right) : Q = left ++ datum.E i ++ right

Exact one-rule transport calculations

theorem Undecidability.BorisovPinchCoefficientClassification.source_one_rule_transport_value (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (left right : List (Fin 2)) (i : Fin 3) : ↑((BorisovCStage.cEquiv datum hfree) (sourcePositive datum left * sourceBasis datum (Sum.inr i) * sourcePositive datum right)) = BorisovHNNModel.d3 ^ (4 ^ left.length * (↑↑i + 1)) * BorisovCStage.positive3 (left ++ datum.E i ++ right) * BorisovHNNModel.e3 ^ (4 ^ right.length * (↑↑i + 1))

theorem Undecidability.BorisovPinchCoefficientClassification.target_one_rule_transport_value (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (left right : List (Fin 2)) (i : Fin 3) : ↑((BorisovCStage.cEquiv datum hfree).symm (targetPositive datum left * targetBasis datum (Sum.inr i) * targetPositive datum right)) = BorisovHNNModel.d3 ^ (4 ^ left.length * (↑↑i + 1)) * BorisovCStage.positive3 (left ++ datum.F i ++ right) * BorisovHNNModel.e3 ^ (4 ^ right.length * (↑↑i + 1))

Partial fields of PinchClassification

theorem Undecidability.BorisovPinchCoefficientClassification.source_classification_one_rule (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (Q : List (Fin 2)) (f r : ℤ) (left right : List (Fin 2)) (i : Fin 3) (hmem : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.U datum) (hshape : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r = BorisovCStage.positive3 left * BorisovCStage.a3 datum i * BorisovCStage.positive3 right) : ∃ (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'

The source field of PinchClassification for a coefficient whose rank-five normal form has one positive rule letter, with arbitrary positive stable-letter contexts on the two sides.

theorem Undecidability.BorisovPinchCoefficientClassification.target_classification_one_rule (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (Q : List (Fin 2)) (f r : ℤ) (left right : List (Fin 2)) (i : Fin 3) (hmem : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.V datum) (hshape : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r = BorisovCStage.positive3 left * BorisovCStage.b3 datum i * BorisovCStage.positive3 right) : ∃ (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'

The symmetric target field for a coefficient with one positive rule letter. It performs the reverse Thue rewrite E_i ↦ F_i.

The zero-rule shape and the exact classification interface

theorem Undecidability.BorisovPinchCoefficientClassification.source_classification_stable_shape (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (Q : List (Fin 2)) (f r : ℤ) (w : List (Fin 2)) (hmem : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.U datum) (hshape : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r = BorisovCStage.positive3 w) : ∃ (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'

theorem Undecidability.BorisovPinchCoefficientClassification.target_classification_stable_shape (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (Q : List (Fin 2)) (f r : ℤ) (w : List (Fin 2)) (hmem : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.V datum) (hshape : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r = BorisovCStage.positive3 w) : ∃ (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'

def Undecidability.BorisovPinchCoefficientClassification.SourceCoefficientShape (datum : Thue.StandingDatum) (Q : List (Fin 2)) (f r : ℤ) : Prop

The two coefficient shapes used by the Assertion-V normal-form classification.

Equations

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

def Undecidability.BorisovPinchCoefficientClassification.TargetCoefficientShape (datum : Thue.StandingDatum) (Q : List (Fin 2)) (f r : ℤ) : Prop

The classified shape of a coefficient after transport through the rewriting-rule isomorphism.

Equations

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

theorem Undecidability.BorisovPinchCoefficientClassification.pinchClassification_of_shapes (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hsource : ∀ (Q : List (Fin 2)) (f r : ℤ), BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.U datum → SourceCoefficientShape datum Q f r) (htarget : ∀ (Q : List (Fin 2)) (f r : ℤ), BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.V datum → TargetCoefficientShape datum Q f r) : BorisovLemma4Pinch.PinchClassification datum hfree

The two normal-form shape classifications yield the full coefficient classifier.