The base subgroup in Borisov's two-HNN model

This file identifies the subgroup generated by d₃,e₃ with the image of the original rank-two free base in Γ₃. It is the bridge needed to apply the two-stable-letter Britton lemma to the intersection input of Borisov's Lemma 4.

theorem Undecidability.BorisovBaseRange.baseEmbedding_eq_lift : BorisovHNNModel.of1.comp BorisovHNNModel.of0 = FreeGroup.lift ![BorisovHNNModel.d3, BorisovHNNModel.e3]

theorem Undecidability.BorisovBaseRange.DE3_eq_range_baseEmbedding : BorisovCStage.DE3 = (BorisovHNNModel.of1.comp BorisovHNNModel.of0).range

The displayed subgroup <d₃,e₃> is exactly the embedded original free-group base.

Borisov's Assertion IV

This file turns the four boundary computations into the full rank-five freeness statement. A signed displayed generator is expanded literally as a flat word in the two HNN stable letters; the coefficient at a boundary is exactly the coefficient studied in AssertionIVBoundary.lean.

@[reducible, inline]

abbrev Undecidability.BorisovAssertionIV.FlatSyllable : Type

A stable-letter syllable in the flattened two-HNN-extension model.

Equations

• Undecidability.BorisovAssertionIV.FlatSyllable = Undecidability.MultipleHNNFlat.Syllable

@[reducible, inline]

abbrev Undecidability.BorisovAssertionIV.FlatWord : Type

A reduced word in the flattened two-HNN-extension model.

Equations

• Undecidability.BorisovAssertionIV.FlatWord = Undecidability.MultipleHNNFlat.ReducedWord Undecidability.BorisovHNNModel.A0 Undecidability.BorisovHNNModel.B0

def Undecidability.BorisovAssertionIV.signedUnit : Bool → ℤˣ

Convert a Boolean orientation to the signed unit 1 or -1.

Equations

• Undecidability.BorisovAssertionIV.signedUnit true = 1
• Undecidability.BorisovAssertionIV.signedUnit false = -1

@[simp]

theorem Undecidability.BorisovAssertionIV.signedUnit_true : signedUnit true = 1

def Undecidability.BorisovAssertionIV.factorColors (rules : Fin 3 → List (Fin 2)) : BorisovIntersections.Basis × Bool → List (Fin 2)

The sequence of stable-letter colors in the expansion of a signed basis letter.

Equations

• Undecidability.BorisovAssertionIV.factorColors rules (Sum.inl beta, snd) = [beta]
• Undecidability.BorisovAssertionIV.factorColors rules (Sum.inr i, true) = rules i
• Undecidability.BorisovAssertionIV.factorColors rules (Sum.inr i, false) = (rules i).reverse

theorem Undecidability.BorisovAssertionIV.factorColors_ne_nil (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovIntersections.Basis × Bool) : factorColors rules x ≠ []

def Undecidability.BorisovAssertionIV.run (colors : List (Fin 2)) (hne : colors ≠ []) (u : ℤˣ) (lastCoeff : BorisovHNNModel.Base) : List FlatSyllable

The syllables in a run of same-sign stable letters, with the supplied final coefficient.

Equations

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

@[simp]

theorem Undecidability.BorisovAssertionIV.run_ne_nil (colors : List (Fin 2)) (hne : colors ≠ []) (u : ℤˣ) (lastCoeff : BorisovHNNModel.Base) : run colors hne u lastCoeff ≠ []

theorem Undecidability.BorisovAssertionIV.run_chain (colors : List (Fin 2)) (hne : colors ≠ []) (u : ℤˣ) (lastCoeff : BorisovHNNModel.Base) : List.IsChain (MultipleHNNFlat.Rel BorisovHNNModel.A0 BorisovHNNModel.B0) (run colors hne u lastCoeff)

@[simp]

theorem Undecidability.BorisovAssertionIV.run_getLast (colors : List (Fin 2)) (hne : colors ≠ []) (u : ℤˣ) (lastCoeff : BorisovHNNModel.Base) : (run colors hne u lastCoeff).getLast ⋯ = { color := colors.getLast hne, sign := u, coeff := lastCoeff }

@[simp]

theorem Undecidability.BorisovAssertionIV.run_head_color (colors : List (Fin 2)) (hne : colors ≠ []) (u : ℤˣ) (lastCoeff : BorisovHNNModel.Base) : ((run colors hne u lastCoeff).head ⋯).color = colors.head hne

@[simp]

theorem Undecidability.BorisovAssertionIV.run_head_sign (colors : List (Fin 2)) (hne : colors ≠ []) (u : ℤˣ) (lastCoeff : BorisovHNNModel.Base) : ((run colors hne u lastCoeff).head ⋯).sign = u

def Undecidability.BorisovAssertionIV.factorRun (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovIntersections.Basis × Bool) (lastCoeff : BorisovHNNModel.Base) : List FlatSyllable

The stable-letter run expanding one signed basis letter.

Equations

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

@[simp]

theorem Undecidability.BorisovAssertionIV.factorRun_ne_nil (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovIntersections.Basis × Bool) (lastCoeff : BorisovHNNModel.Base) : factorRun rules hne x lastCoeff ≠ []

theorem Undecidability.BorisovAssertionIV.factorRun_chain (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovIntersections.Basis × Bool) (lastCoeff : BorisovHNNModel.Base) : List.IsChain (MultipleHNNFlat.Rel BorisovHNNModel.A0 BorisovHNNModel.B0) (factorRun rules hne x lastCoeff)

theorem Undecidability.BorisovAssertionIV.factorColors_head (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovIntersections.Basis × Bool) : (factorColors rules x).head ⋯ = BorisovAssertionIVBoundary.firstStable rules hne x

theorem Undecidability.BorisovAssertionIV.factorColors_getLast (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovIntersections.Basis × Bool) : (factorColors rules x).getLast ⋯ = BorisovAssertionIVBoundary.lastStable rules hne x

theorem Undecidability.BorisovAssertionIV.factorRun_head_color (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovIntersections.Basis × Bool) (lastCoeff : BorisovHNNModel.Base) : ((factorRun rules hne x lastCoeff).head ⋯).color = BorisovAssertionIVBoundary.firstStable rules hne x

theorem Undecidability.BorisovAssertionIV.factorRun_head_sign (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovIntersections.Basis × Bool) (lastCoeff : BorisovHNNModel.Base) : ((factorRun rules hne x lastCoeff).head ⋯).sign = signedUnit x.2

theorem Undecidability.BorisovAssertionIV.factorRun_getLast_color (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovIntersections.Basis × Bool) (lastCoeff : BorisovHNNModel.Base) : ((factorRun rules hne x lastCoeff).getLast ⋯).color = BorisovAssertionIVBoundary.lastStable rules hne x

theorem Undecidability.BorisovAssertionIV.factorRun_getLast_sign (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovIntersections.Basis × Bool) (lastCoeff : BorisovHNNModel.Base) : ((factorRun rules hne x lastCoeff).getLast ⋯).sign = signedUnit x.2

theorem Undecidability.BorisovAssertionIV.factorRun_getLast_coeff (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovIntersections.Basis × Bool) (lastCoeff : BorisovHNNModel.Base) : ((factorRun rules hne x lastCoeff).getLast ⋯).coeff = lastCoeff

def Undecidability.BorisovAssertionIV.nextPrefix : List (BorisovIntersections.Basis × Bool) → BorisovHNNModel.Base

The initial coefficient contributed by the next signed basis letter, or the identity.

Equations

• Undecidability.BorisovAssertionIV.nextPrefix [] = 1
• Undecidability.BorisovAssertionIV.nextPrefix (y :: tail) = Undecidability.BorisovAssertionIVBoundary.factorPrefix y

def Undecidability.BorisovAssertionIV.expansionTail (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) : List (BorisovIntersections.Basis × Bool) → List FlatSyllable

The flattened tail obtained by expanding a list of signed basis letters.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.BorisovAssertionIV.expansionTail rules hne [] = []

def Undecidability.BorisovAssertionIV.expansionHead : List (BorisovIntersections.Basis × Bool) → BorisovHNNModel.Base

The initial coefficient of an expanded list of signed basis letters.

Equations

• Undecidability.BorisovAssertionIV.expansionHead [] = 1
• Undecidability.BorisovAssertionIV.expansionHead (y :: tail) = Undecidability.BorisovAssertionIVBoundary.factorPrefix y

theorem Undecidability.BorisovAssertionIV.expansionTail_chain (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (letters : List (BorisovIntersections.Basis × Bool)) (hreduced : List.IsChain (fun (x y : BorisovIntersections.Basis × Bool) => x.1 = y.1 → x.2 = y.2) letters) : List.IsChain (MultipleHNNFlat.Rel BorisovHNNModel.A0 BorisovHNNModel.B0) (expansionTail rules hne letters)

noncomputable def Undecidability.BorisovAssertionIV.stableProduct (colors : List (Fin 2)) (u : ℤˣ) : MultipleHNN.Extension BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0

The product of the indicated same-sign stable letters in the two-HNN-extension group.

Equations

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

@[simp]

theorem Undecidability.BorisovAssertionIV.flat_baseEmbedding (g : BorisovHNNModel.Base) : (MultipleHNN.baseEmbedding BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0) g = BorisovG0HNN.baseToG0HNN g

theorem Undecidability.BorisovAssertionIV.flat_baseEmbedding_one : (MultipleHNN.baseEmbedding BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0) 1 = 1

@[simp]

theorem Undecidability.BorisovAssertionIV.baseToG0HNN_d : BorisovG0HNN.baseToG0HNN BorisovHNNModel.d = BorisovG0HNN.hnnD

@[simp]

theorem Undecidability.BorisovAssertionIV.baseToG0HNN_e : BorisovG0HNN.baseToG0HNN BorisovHNNModel.e = BorisovG0HNN.hnnE

theorem Undecidability.BorisovAssertionIV.flat_d_rulePower (i : Fin 3) : (MultipleHNN.baseEmbedding BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0) (BorisovHNNModel.d ^ BorisovAssertionIVBoundary.rulePower i) = BorisovG0HNN.hnnD ^ (↑i + 1)

theorem Undecidability.BorisovAssertionIV.flat_e_rulePower (i : Fin 3) : (MultipleHNN.baseEmbedding BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0) (BorisovHNNModel.e ^ BorisovAssertionIVBoundary.rulePower i) = BorisovG0HNN.hnnE ^ (↑i + 1)

theorem Undecidability.BorisovAssertionIV.run_eval (colors : List (Fin 2)) (hne : colors ≠ []) (u : ℤˣ) (lastCoeff : BorisovHNNModel.Base) : (List.map (fun (s : FlatSyllable) => MultipleHNNFlat.stableLetter BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 s.color ^ ↑s.sign * (MultipleHNN.baseEmbedding BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0) s.coeff) (run colors hne u lastCoeff)).prod = stableProduct colors u * (MultipleHNN.baseEmbedding BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0) lastCoeff

theorem Undecidability.BorisovAssertionIV.stableProduct_one (colors : List (Fin 2)) : stableProduct colors 1 = BorisovG0NormalForm.modelPositive colors

theorem Undecidability.BorisovAssertionIV.stableProduct_reverse_neg_one (colors : List (Fin 2)) : stableProduct colors.reverse (-1) = (stableProduct colors 1)⁻¹

theorem Undecidability.BorisovAssertionIV.stableProduct_singleton_one (color : Fin 2) : stableProduct [color] 1 = MultipleHNNFlat.stableLetter BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 color

theorem Undecidability.BorisovAssertionIV.stableProduct_singleton_neg_one (color : Fin 2) : stableProduct [color] (-1) = (MultipleHNNFlat.stableLetter BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 color)⁻¹

theorem Undecidability.BorisovAssertionIV.toHNN_stable_flat (beta : Fin 2) : BorisovG0HNN.toHNN (BorisovIntersections.stable beta) = MultipleHNNFlat.stableLetter BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 beta

noncomputable def Undecidability.BorisovAssertionIV.factorModel (rules : Fin 3 → List (Fin 2)) (x : BorisovIntersections.Basis × Bool) : MultipleHNN.Extension BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0

The group element represented by the expansion of one signed basis letter.

Equations

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

theorem Undecidability.BorisovAssertionIV.factorModel_positive_u (datum : Thue.StandingDatum) (q : BorisovIntersections.Basis) : factorModel datum.F (q, true) = BorisovG0HNN.toHNN (BorisovIntersections.uBasis datum q)

theorem Undecidability.BorisovAssertionIV.factorModel_positive_v (datum : Thue.StandingDatum) (q : BorisovIntersections.Basis) : factorModel datum.E (q, true) = BorisovG0HNN.toHNN (BorisovIntersections.vBasis datum q)

theorem Undecidability.BorisovAssertionIV.factorModel_negative (rules : Fin 3 → List (Fin 2)) (q : BorisovIntersections.Basis) : factorModel rules (q, false) = (factorModel rules (q, true))⁻¹

theorem Undecidability.BorisovAssertionIV.factorModel_u (datum : Thue.StandingDatum) (x : BorisovIntersections.Basis × Bool) : factorModel datum.F x = if x.2 = true then BorisovG0HNN.toHNN (BorisovIntersections.uBasis datum x.1) else (BorisovG0HNN.toHNN (BorisovIntersections.uBasis datum x.1))⁻¹

theorem Undecidability.BorisovAssertionIV.factorModel_v (datum : Thue.StandingDatum) (x : BorisovIntersections.Basis × Bool) : factorModel datum.E x = if x.2 = true then BorisovG0HNN.toHNN (BorisovIntersections.vBasis datum x.1) else (BorisovG0HNN.toHNN (BorisovIntersections.vBasis datum x.1))⁻¹

theorem Undecidability.BorisovAssertionIV.factorRun_eval (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovIntersections.Basis × Bool) (lastCoeff : BorisovHNNModel.Base) : (List.map (fun (s : FlatSyllable) => MultipleHNNFlat.stableLetter BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 s.color ^ ↑s.sign * (MultipleHNN.baseEmbedding BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0) s.coeff) (factorRun rules hne x lastCoeff)).prod = stableProduct (factorColors rules x) (signedUnit x.2) * (MultipleHNN.baseEmbedding BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0) lastCoeff

theorem Undecidability.BorisovAssertionIV.expansion_eval (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (letters : List (BorisovIntersections.Basis × Bool)) : (MultipleHNN.baseEmbedding BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0) (expansionHead letters) * (List.map (fun (s : FlatSyllable) => MultipleHNNFlat.stableLetter BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 s.color ^ ↑s.sign * (MultipleHNN.baseEmbedding BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0) s.coeff) (expansionTail rules hne letters)).prod = (List.map (factorModel rules) letters).prod

The literal expansion evaluates to the product of its signed displayed factors. This is independent of reducedness.

theorem Undecidability.BorisovAssertionIV.expansionTail_ne_nil (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (letters : List (BorisovIntersections.Basis × Bool)) (hletters : letters ≠ []) : expansionTail rules hne letters ≠ []

def Undecidability.BorisovAssertionIV.expansionWord (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (letters : List (BorisovIntersections.Basis × Bool)) (hreduced : List.IsChain (fun (x y : BorisovIntersections.Basis × Bool) => x.1 = y.1 → x.2 = y.2) letters) : FlatWord

The flattened reduced-word expansion associated with the supplied rewriting rules.

Equations

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

theorem Undecidability.BorisovAssertionIV.expansionWord_eval (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (letters : List (BorisovIntersections.Basis × Bool)) (hreduced : List.IsChain (fun (x y : BorisovIntersections.Basis × Bool) => x.1 = y.1 → x.2 = y.2) letters) : MultipleHNNFlat.eval BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 (expansionWord rules hne letters hreduced) = (List.map (factorModel rules) letters).prod

theorem Undecidability.BorisovAssertionIV.factorProduct_u (datum : Thue.StandingDatum) (letters : List (BorisovIntersections.Basis × Bool)) : (List.map (factorModel datum.F) letters).prod = BorisovG0HNN.toHNN ((FreeGroup.lift (BorisovIntersections.uBasis datum)) (FreeGroup.mk letters))

theorem Undecidability.BorisovAssertionIV.factorProduct_v (datum : Thue.StandingDatum) (letters : List (BorisovIntersections.Basis × Bool)) : (List.map (factorModel datum.E) letters).prod = BorisovG0HNN.toHNN ((FreeGroup.lift (BorisovIntersections.vBasis datum)) (FreeGroup.mk letters))

def Undecidability.BorisovAssertionIV.uExpansion (datum : Thue.StandingDatum) (w : FreeGroup BorisovIntersections.Basis) : FlatWord

The flattened expansion of a word in the left-rule basis.

Equations

• Undecidability.BorisovAssertionIV.uExpansion datum w = Undecidability.BorisovAssertionIV.expansionWord datum.F ⋯ w.toWord ⋯

def Undecidability.BorisovAssertionIV.vExpansion (datum : Thue.StandingDatum) (w : FreeGroup BorisovIntersections.Basis) : FlatWord

The flattened expansion of a word in the right-rule basis.

Equations

• Undecidability.BorisovAssertionIV.vExpansion datum w = Undecidability.BorisovAssertionIV.expansionWord datum.E ⋯ w.toWord ⋯

theorem Undecidability.BorisovAssertionIV.uExpansion_eval (datum : Thue.StandingDatum) (w : FreeGroup BorisovIntersections.Basis) : MultipleHNNFlat.eval BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 (uExpansion datum w) = BorisovG0HNN.toHNN ((FreeGroup.lift (BorisovIntersections.uBasis datum)) w)

theorem Undecidability.BorisovAssertionIV.vExpansion_eval (datum : Thue.StandingDatum) (w : FreeGroup BorisovIntersections.Basis) : MultipleHNNFlat.eval BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 (vExpansion datum w) = BorisovG0HNN.toHNN ((FreeGroup.lift (BorisovIntersections.vBasis datum)) w)

theorem Undecidability.BorisovAssertionIV.uExpansion_toList_ne_nil (datum : Thue.StandingDatum) {w : FreeGroup BorisovIntersections.Basis} (hw : w ≠ 1) : (uExpansion datum w).toList ≠ []

theorem Undecidability.BorisovAssertionIV.vExpansion_toList_ne_nil (datum : Thue.StandingDatum) {w : FreeGroup BorisovIntersections.Basis} (hw : w ≠ 1) : (vExpansion datum w).toList ≠ []

theorem Undecidability.BorisovAssertionIV.uLift_ne_one (datum : Thue.StandingDatum) {w : FreeGroup BorisovIntersections.Basis} (hw : w ≠ 1) : (FreeGroup.lift (BorisovIntersections.uBasis datum)) w ≠ 1

A nontrivial free word has nontrivial image under the displayed A-basis lift.

theorem Undecidability.BorisovAssertionIV.vLift_ne_one (datum : Thue.StandingDatum) {w : FreeGroup BorisovIntersections.Basis} (hw : w ≠ 1) : (FreeGroup.lift (BorisovIntersections.vBasis datum)) w ≠ 1

The corresponding nontriviality theorem for the displayed B-basis.

theorem Undecidability.BorisovAssertionIV.uLift_injective (datum : Thue.StandingDatum) : Function.Injective ⇑(FreeGroup.lift (BorisovIntersections.uBasis datum))

Borisov's first rank-five freeness assertion.

theorem Undecidability.BorisovAssertionIV.vLift_injective (datum : Thue.StandingDatum) : Function.Injective ⇑(FreeGroup.lift (BorisovIntersections.vBasis datum))

Borisov's second rank-five freeness assertion.

theorem Undecidability.BorisovAssertionIV.uLift_not_mem_DE3_of_ne_one (datum : Thue.StandingDatum) {w : FreeGroup BorisovIntersections.Basis} (hw : w ≠ 1) : BorisovG0HNN.toHNN ((FreeGroup.lift (BorisovIntersections.uBasis datum)) w) ∉ BorisovCStage.DE3

A nontrivial A-basis word does not land in the embedded base subgroup <d₃,e₃>.

theorem Undecidability.BorisovAssertionIV.vLift_not_mem_DE3_of_ne_one (datum : Thue.StandingDatum) {w : FreeGroup BorisovIntersections.Basis} (hw : w ≠ 1) : BorisovG0HNN.toHNN ((FreeGroup.lift (BorisovIntersections.vBasis datum)) w) ∉ BorisovCStage.DE3

A nontrivial B-basis word does not land in the embedded base subgroup <d₃,e₃>.

theorem Undecidability.BorisovAssertionIV.Uc_eq_uLift_range (datum : Thue.StandingDatum) : BorisovIntersections.Uc datum = (FreeGroup.lift (BorisovIntersections.uBasis datum)).range

theorem Undecidability.BorisovAssertionIV.Vc_eq_vLift_range (datum : Thue.StandingDatum) : BorisovIntersections.Vc datum = (FreeGroup.lift (BorisovIntersections.vBasis datum)).range

theorem Undecidability.BorisovAssertionIV.assertionIV (datum : Thue.StandingDatum) : BorisovIntersections.AssertionIV datum

The complete Assertion IV package, including the letterwise correspondence between the two free rank-five subgroups.