The J_beta intersections in the semantic Gamma3 model

theorem Undecidability.BorisovInputsBridge.g0Equiv_stable (beta : Fin 2) : BorisovG0HNN.g0Equiv (BorisovIntersections.stable beta) = BorisovCStage.stable3 beta

theorem Undecidability.BorisovInputsBridge.g0Equiv_uBasis (datum : Thue.StandingDatum) (q : BorisovIntersections.Basis) : BorisovG0HNN.g0Equiv (BorisovIntersections.uBasis datum q) = BorisovCStage.uBasis datum q

theorem Undecidability.BorisovInputsBridge.g0Equiv_vBasis (datum : Thue.StandingDatum) (q : BorisovIntersections.Basis) : BorisovG0HNN.g0Equiv (BorisovIntersections.vBasis datum q) = BorisovCStage.vBasis datum q

theorem Undecidability.BorisovInputsBridge.g0Equiv_uLift (datum : Thue.StandingDatum) (w : FreeGroup BorisovIntersections.Basis) : BorisovG0HNN.g0Equiv ((FreeGroup.lift (BorisovIntersections.uBasis datum)) w) = (BorisovCStage.uLift datum) w

Transporting the displayed source-basis lift through g0Equiv gives the semantic source-basis lift.

theorem Undecidability.BorisovInputsBridge.g0Equiv_vLift (datum : Thue.StandingDatum) (w : FreeGroup BorisovIntersections.Basis) : BorisovG0HNN.g0Equiv ((FreeGroup.lift (BorisovIntersections.vBasis datum)) w) = (BorisovCStage.vLift datum) w

Transporting the displayed target-basis lift through g0Equiv gives the semantic target-basis lift.

theorem Undecidability.BorisovInputsBridge.rankFiveFree_of_assertionIV (datum : Thue.StandingDatum) (hIV : BorisovIntersections.AssertionIV datum) : BorisovCStage.RankFiveFree datum

Assertion IV in the four-generator presentation supplies exactly the freeness input used to construct the semantic c-HNN extension.

theorem Undecidability.BorisovInputsBridge.rankFiveFree (datum : Thue.StandingDatum) : BorisovCStage.RankFiveFree datum

Borisov's Assertion IV, transported from the four-generator presentation to the concrete iterated-HNN model used by the later stages.

theorem Undecidability.BorisovInputsBridge.baseIntersections (datum : Thue.StandingDatum) : BorisovContextNormalForm.BaseIntersections datum

The base-intersection input needed after the c-stage follows directly from the strengthened, base-exclusion form of Assertion IV. This bypasses the weaker presentation-level AssertionV interface: a nontrivial word in either displayed rank-five basis has a nonempty flat reduced expansion and therefore cannot lie in the embedded <d,e> base.

noncomputable def Undecidability.BorisovInputsBridge.J3 (beta : Fin 2) : Subgroup BorisovHNNModel.Gamma3

The semantic copy of J_beta = <d,e,s_beta> inside the concrete iterated-HNN model Gamma3.

Equations

• Undecidability.BorisovInputsBridge.J3 beta = Subgroup.closure {Undecidability.BorisovHNNModel.d3, Undecidability.BorisovHNNModel.e3, Undecidability.BorisovCStage.stable3 beta}

noncomputable def Undecidability.BorisovInputsBridge.stableCyclic3 (beta : Fin 2) : Subgroup BorisovHNNModel.Gamma3

The semantic cyclic subgroup <s_beta> inside Gamma3.

Equations

• Undecidability.BorisovInputsBridge.stableCyclic3 beta = Subgroup.closure {Undecidability.BorisovCStage.stable3 beta}

theorem Undecidability.BorisovInputsBridge.g0Equiv_d : BorisovG0HNN.g0Equiv BorisovIntersections.d = BorisovHNNModel.d3

theorem Undecidability.BorisovInputsBridge.g0Equiv_e : BorisovG0HNN.g0Equiv BorisovIntersections.e = BorisovHNNModel.e3

theorem Undecidability.BorisovInputsBridge.stableCyclic3_le_U (datum : Thue.StandingDatum) (beta : Fin 2) : stableCyclic3 beta ≤ BorisovCStage.U datum

theorem Undecidability.BorisovInputsBridge.stableCyclic3_le_V (datum : Thue.StandingDatum) (beta : Fin 2) : stableCyclic3 beta ≤ BorisovCStage.V datum

theorem Undecidability.BorisovInputsBridge.stableCyclic3_le_J3 (beta : Fin 2) : stableCyclic3 beta ≤ J3 beta

theorem Undecidability.BorisovInputsBridge.U_inf_J3 (datum : Thue.StandingDatum) (beta : Fin 2) : BorisovCStage.U datum ⊓ J3 beta = stableCyclic3 beta

The U_c ∩ J_beta statement in Lemma 3.5 of the paper, transported to the concrete semantic model Gamma3.

theorem Undecidability.BorisovInputsBridge.V_inf_J3 (datum : Thue.StandingDatum) (beta : Fin 2) : BorisovCStage.V datum ⊓ J3 beta = stableCyclic3 beta

The V_c ∩ J_beta statement in Lemma 3.5 of the paper, transported to the concrete semantic model Gamma3.

noncomputable def Undecidability.BorisovInputsBridge.uStable (datum : Thue.StandingDatum) (beta : Fin 2) : ↥(BorisovCStage.U datum)

The canonical copy of s_beta in the source associated subgroup U.

Equations

• Undecidability.BorisovInputsBridge.uStable datum beta = ⟨Undecidability.BorisovCStage.stable3 beta, ⋯⟩

@[simp]

theorem Undecidability.BorisovInputsBridge.cEquiv_uStable (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (beta : Fin 2) : ↑((BorisovCStage.cEquiv datum hfree) (uStable datum beta)) = BorisovCStage.stable3 beta

theorem Undecidability.BorisovInputsBridge.cEquiv_mem_J3_iff (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (beta : Fin 2) (a : ↥(BorisovCStage.U datum)) : ↑a ∈ J3 beta ↔ ↑((BorisovCStage.cEquiv datum hfree) a) ∈ J3 beta

The associated isomorphism for the c-HNN stage preserves membership in J_beta. This is the compatibility hypothesis consumed by the restricted-HNN embedding over J_beta.