Base-group calculations used by the z compression stage

This file formalizes the part of Section 3.2 of the paper which takes place in the semantic Borisov tower. In the c-stage it defines B = ⟨d,e,c⟩ and B0 = ⟨d,e,c,s₂⟩, then proves the base exclusion P ∉ B0 needed by the nested normal-form calculation for the double-coset identity in the proof of Proposition 3.8.

@[reducible, inline]

abbrev Undecidability.HostZBaseIntersections.FreeInput (datum : Thue.StandingDatum) : BorisovCStage.RankFiveFree datum

The proved rank-five freeness witness for the concrete host model.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev Undecidability.HostZBaseIntersections.CStage (datum : Thue.StandingDatum) : Type

The semantic c-stage Gamma₂.

Equations

• Undecidability.HostZBaseIntersections.CStage datum = Undecidability.BorisovCStage.Gamma2 datum ⋯

noncomputable def Undecidability.HostZBaseIntersections.B (datum : Thue.StandingDatum) : Subgroup (CStage datum)

B = ⟨d,e,c⟩ ≤ Gamma₂.

Equations

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

noncomputable def Undecidability.HostZBaseIntersections.B0 (datum : Thue.StandingDatum) : Subgroup (CStage datum)

B₀ = ⟨d,e,c,s₂⟩ ≤ Gamma₂.

Equations

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

noncomputable def Undecidability.HostZBaseIntersections.Delta (datum : Thue.StandingDatum) : Subgroup (BorisovConverseCore.TStage datum ⋯)

Delta = ⟨c,e,p⟩, where p = P⁻¹tP.

Equations

• Undecidability.HostZBaseIntersections.Delta datum = Undecidability.BorisovConverseCore.KSubgroup datum ⋯

theorem Undecidability.HostZBaseIntersections.CE_le_B (datum : Thue.StandingDatum) : BorisovCStage.CE datum ⋯ ≤ B datum

theorem Undecidability.HostZBaseIntersections.CD_le_B (datum : Thue.StandingDatum) : BorisovCStage.CD datum ⋯ ≤ B datum

The larger base B0 = ⟨d,e,c,s₂⟩

def Undecidability.HostZBaseIntersections.firstExponentFree : FreeGroup (Fin 2) →* Multiplicative ℤ

Exponent sum of the first stable generator after projecting Gamma3 to the free group on s₁,s₂.

Equations

• Undecidability.HostZBaseIntersections.firstExponentFree = FreeGroup.lift fun (i : Fin 2) => if i = 0 then Multiplicative.ofAdd 1 else 1

noncomputable def Undecidability.HostZBaseIntersections.firstExponent3 : BorisovHNNModel.Gamma3 →* Multiplicative ℤ

The homomorphism recording the total exponent of the first stable generator.

Equations

• Undecidability.HostZBaseIntersections.firstExponent3 = Undecidability.HostZBaseIntersections.firstExponentFree.comp Undecidability.BorisovCStage.stableProjection3

@[simp]

theorem Undecidability.HostZBaseIntersections.firstExponentFree_of_zero : firstExponentFree (FreeGroup.of 0) = Multiplicative.ofAdd 1

@[simp]

theorem Undecidability.HostZBaseIntersections.firstExponentFree_of_one : firstExponentFree (FreeGroup.of 1) = 1

@[simp]

theorem Undecidability.HostZBaseIntersections.firstExponent3_d : firstExponent3 BorisovHNNModel.d3 = 1

@[simp]

theorem Undecidability.HostZBaseIntersections.firstExponent3_e : firstExponent3 BorisovHNNModel.e3 = 1

@[simp]

theorem Undecidability.HostZBaseIntersections.firstExponent3_s2 : firstExponent3 BorisovHNNModel.secondStableInStageThree = 1

theorem Undecidability.HostZBaseIntersections.firstExponent3_positive (w : List (Fin 2)) : Multiplicative.toAdd (firstExponent3 (BorisovCStage.positive3 w)) = ↑(List.count 0 w)

theorem Undecidability.HostZBaseIntersections.positive3_not_mem_J3_one (datum : Thue.StandingDatum) : BorisovCStage.positive3 datum.P ∉ BorisovInputsBridge.J3 1

theorem Undecidability.HostZBaseIntersections.positive2_not_mem_B0 (datum : Thue.StandingDatum) : BorisovCStage.positive2 datum ⋯ datum.P ∉ B0 datum

The stronger exclusion used in the proof of Proposition 3.8: P ∉ ⟨d,e,c,s₂⟩.

The nested double-coset calculation

noncomputable def Undecidability.HostZBaseIntersections.C0 (datum : Thue.StandingDatum) : Subgroup (CStage datum)

C₀ = ⟨c⟩ inside Gamma₂.

Equations

• Undecidability.HostZBaseIntersections.C0 datum = Subgroup.closure {Undecidability.BorisovCStage.c datum ⋯}

theorem Undecidability.HostZBaseIntersections.C0_le_iff (datum : Thue.StandingDatum) {S : Subgroup (CStage datum)} : C0 datum ≤ S ↔ BorisovCStage.c datum ⋯ ∈ S

noncomputable def Undecidability.HostZBaseIntersections.CT (datum : Thue.StandingDatum) : Subgroup (BorisovConverseCore.TStage datum ⋯)

L = ⟨c,t⟩ inside the t-stage.

Equations

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

noncomputable def Undecidability.HostZBaseIntersections.B0InT (datum : Thue.StandingDatum) : Subgroup (BorisovConverseCore.TStage datum ⋯)

The embedded copy of B₀ = ⟨d,e,c,s₂⟩ in the t-stage.

Equations

• Undecidability.HostZBaseIntersections.B0InT datum = Subgroup.map (Undecidability.BorisovConverseCore.toTStage datum ⋯) (Undecidability.HostZBaseIntersections.B0 datum)

noncomputable def Undecidability.HostZBaseIntersections.C0InT (datum : Thue.StandingDatum) : Subgroup (BorisovConverseCore.TStage datum ⋯)

The embedded copy of ⟨c⟩ in the t-stage.

Equations

• Undecidability.HostZBaseIntersections.C0InT datum = Subgroup.map (Undecidability.BorisovConverseCore.toTStage datum ⋯) (Undecidability.HostZBaseIntersections.C0 datum)

theorem Undecidability.HostZBaseIntersections.B_le_B0 (datum : Thue.StandingDatum) : B datum ≤ B0 datum

theorem Undecidability.HostZBaseIntersections.CE_le_B0 (datum : Thue.StandingDatum) : BorisovCStage.CE datum ⋯ ≤ B0 datum

theorem Undecidability.HostZBaseIntersections.CD_le_B0 (datum : Thue.StandingDatum) : BorisovCStage.CD datum ⋯ ≤ B0 datum

theorem Undecidability.HostZBaseIntersections.C0_le_CD (datum : Thue.StandingDatum) : C0 datum ≤ BorisovCStage.CD datum ⋯

theorem Undecidability.HostZBaseIntersections.CT_inter_deltaDoubleCoset_B0 (datum : Thue.StandingDatum) : ↑(CT datum) ∩ HNNLemmas.deltaDoubleCoset (Delta datum) (B0InT datum) = ↑(C0InT datum)

The double-coset identity in the proof of Proposition 3.8. Inside the t-stage, ⟨c,t⟩ ∩ (Delta · B₀ · Delta) = ⟨c⟩.