A syntactic endpoint for Borisov's coefficient-shape argument

This part of Assertion V compares the canonical rank-five preimage of a coefficient d^f Q e^r with its literal two-HNN normal form. This file isolates the exact output of that comparison: the canonical word has either only positive stable letters, or one positive rule letter between two positive stable contexts.

The resulting syntactic alternatives imply the semantic SourceCoefficientShape and TargetCoefficientShape consumed by the proof of Borisov's Lemma 4.

@[reducible, inline]

abbrev Undecidability.BorisovCoefficientShapes.Basis : Type

The indices of the two stable generators and the three rule generators.

Equations

• Undecidability.BorisovCoefficientShapes.Basis = Undecidability.BorisovCStage.RuleBasis

def Undecidability.BorisovCoefficientShapes.stableLetters (w : List (Fin 2)) : List (Basis × Bool)

The freely reduced word consisting of a positive stable word.

Equations

• Undecidability.BorisovCoefficientShapes.stableLetters w = List.map (fun (beta : Fin 2) => (Sum.inl beta, true)) w

def Undecidability.BorisovCoefficientShapes.oneRuleLetters (left right : List (Fin 2)) (i : Fin 3) : List (Basis × Bool)

A positive stable context, one positive rule letter, and another positive stable context.

Equations

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

def Undecidability.BorisovCoefficientShapes.AllPositive : List (Basis × Bool) → Prop

Every letter is positive. This recursive presentation is convenient for the normal-form parser, which consumes the canonical list from left to right.

Equations

• Undecidability.BorisovCoefficientShapes.AllPositive [] = True
• Undecidability.BorisovCoefficientShapes.AllPositive ((fst, sign) :: rest) = (sign = true ∧ Undecidability.BorisovCoefficientShapes.AllPositive rest)

def Undecidability.BorisovCoefficientShapes.ruleCount : List (Basis × Bool) → ℕ

Number of displayed rule letters, irrespective of sign.

Equations

• Undecidability.BorisovCoefficientShapes.ruleCount [] = 0
• Undecidability.BorisovCoefficientShapes.ruleCount ((Sum.inl val, snd) :: rest) = Undecidability.BorisovCoefficientShapes.ruleCount rest
• Undecidability.BorisovCoefficientShapes.ruleCount ((Sum.inr val, snd) :: rest) = Undecidability.BorisovCoefficientShapes.ruleCount rest + 1

theorem Undecidability.BorisovCoefficientShapes.eq_stableLetters_of_ruleCount_zero (letters : List (Basis × Bool)) (hpositive : AllPositive letters) (hzero : ruleCount letters = 0) : ∃ (stable : List (Fin 2)), letters = stableLetters stable

A positive list containing no rule letter is exactly a positive stable word.

theorem Undecidability.BorisovCoefficientShapes.letters_eq_stable_or_oneRule (letters : List (Basis × Bool)) (hpositive : AllPositive letters) (hsparse : ruleCount letters ≤ 1) : (∃ (stable : List (Fin 2)), letters = stableLetters stable) ∨ ∃ (left : List (Fin 2)) (right : List (Fin 2)) (i : Fin 3), letters = oneRuleLetters left right i

Pure list-theoretic form of Borisov's page-771 dichotomy: if all letters are positive and at most one is a rule letter, the word is either stable-only or has a unique rule letter in positive stable contexts.

@[simp]

theorem Undecidability.BorisovCoefficientShapes.uLift_mk_stableLetters (datum : Thue.StandingDatum) (w : List (Fin 2)) : (BorisovCStage.uLift datum) (FreeGroup.mk (stableLetters w)) = BorisovCStage.positive3 w

@[simp]

theorem Undecidability.BorisovCoefficientShapes.vLift_mk_stableLetters (datum : Thue.StandingDatum) (w : List (Fin 2)) : (BorisovCStage.vLift datum) (FreeGroup.mk (stableLetters w)) = BorisovCStage.positive3 w

@[simp]

theorem Undecidability.BorisovCoefficientShapes.uLift_mk_oneRuleLetters (datum : Thue.StandingDatum) (left right : List (Fin 2)) (i : Fin 3) : (BorisovCStage.uLift datum) (FreeGroup.mk (oneRuleLetters left right i)) = BorisovCStage.positive3 left * BorisovCStage.a3 datum i * BorisovCStage.positive3 right

@[simp]

theorem Undecidability.BorisovCoefficientShapes.vLift_mk_oneRuleLetters (datum : Thue.StandingDatum) (left right : List (Fin 2)) (i : Fin 3) : (BorisovCStage.vLift datum) (FreeGroup.mk (oneRuleLetters left right i)) = BorisovCStage.positive3 left * BorisovCStage.b3 datum i * BorisovCStage.positive3 right

Canonical sparse coefficient words

def Undecidability.BorisovCoefficientShapes.CanonicalCoefficientWordShape (w : FreeGroup Basis) : Prop

The precise syntactic alternative established by the normal-form comparison for a canonical rank-five preimage.

Equations

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

theorem Undecidability.BorisovCoefficientShapes.canonicalCoefficientWordShape_of_positive_sparse (w : FreeGroup Basis) (hpositive : AllPositive w.toWord) (hsparse : ruleCount w.toWord ≤ 1) : CanonicalCoefficientWordShape w

theorem Undecidability.BorisovCoefficientShapes.sourceCoefficientShape_of_preimage (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) (hshape : CanonicalCoefficientWordShape w) : BorisovPinchCoefficientClassification.SourceCoefficientShape datum Q f r

A canonical source preimage of the stated syntactic form gives the exact semantic source shape.

theorem Undecidability.BorisovCoefficientShapes.targetCoefficientShape_of_preimage (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) (hshape : CanonicalCoefficientWordShape w) : BorisovPinchCoefficientClassification.TargetCoefficientShape datum Q f r

The target analogue of sourceCoefficientShape_of_preimage.

theorem Undecidability.BorisovCoefficientShapes.sourceCoefficientShape_of_parser (datum : Thue.StandingDatum) (hparse : ∀ (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup Basis), (BorisovCStage.uLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r → CanonicalCoefficientWordShape w) (Q : List (Fin 2)) (f r : ℤ) : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.U datum → BorisovPinchCoefficientClassification.SourceCoefficientShape datum Q f r

If the normal-form parser establishes the source syntactic alternative for every preimage, then the public source coefficient-shape theorem follows from subgroup membership.

theorem Undecidability.BorisovCoefficientShapes.targetCoefficientShape_of_parser (datum : Thue.StandingDatum) (hparse : ∀ (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup Basis), (BorisovCStage.vLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r → CanonicalCoefficientWordShape w) (Q : List (Fin 2)) (f r : ℤ) : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.V datum → BorisovPinchCoefficientClassification.TargetCoefficientShape datum Q f r

Target version of sourceCoefficientShape_of_parser.

theorem Undecidability.BorisovCoefficientShapes.sourceCoefficientShape_of_positive_sparse_parser (datum : Thue.StandingDatum) (hpositive : ∀ (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup Basis), (BorisovCStage.uLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r → AllPositive w.toWord) (hsparse : ∀ (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup Basis), (BorisovCStage.uLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r → ruleCount w.toWord ≤ 1) (Q : List (Fin 2)) (f r : ℤ) : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.U datum → BorisovPinchCoefficientClassification.SourceCoefficientShape datum Q f r

A local source interface for the Britton comparison. It is enough to prove that the canonical preimage has no negative letters and at most one displayed rule letter.

theorem Undecidability.BorisovCoefficientShapes.targetCoefficientShape_of_positive_sparse_parser (datum : Thue.StandingDatum) (hpositive : ∀ (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup Basis), (BorisovCStage.vLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r → AllPositive w.toWord) (hsparse : ∀ (Q : List (Fin 2)) (f r : ℤ) (w : FreeGroup Basis), (BorisovCStage.vLift datum) w = BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r → ruleCount w.toWord ≤ 1) (Q : List (Fin 2)) (f r : ℤ) : BorisovHNNModel.d3 ^ f * BorisovCStage.positive3 Q * BorisovHNNModel.e3 ^ r ∈ BorisovCStage.V datum → BorisovPinchCoefficientClassification.TargetCoefficientShape datum Q f r

Target counterpart of sourceCoefficientShape_of_positive_sparse_parser.