Gordon's printed condition (2.1)

This file separates Gordon's original torsion hypothesis from the proof-oriented data used by the presentation construction. Repeated order values are removed by choosing one representative of each value. The remaining partial degree assignment is extended injectively by assigning all unselected generators values above the sum of the selected orders.

structure Undecidability.Gordon.Condition21 {n m : ℕ} (P : FP n m) : Type

Gordon's condition (2.1), before passing to a minimal witness.

The selected generators are distinct, but their abelianized orders q need not be distinct.

• p : ℕ

  The number of generators selected for the torsion condition.

• selected : Fin self.p ↪ Fin n

  The distinct generator indices selected for the torsion condition.

• q : Fin self.p → ℕ

  The prescribed orders of the selected generators in the abelianization.

• q_pos (i : Fin self.p) : 0 < self.q i
• gcd_q : Finset.univ.gcd self.q = 1
• exactOrder (i : Fin self.p) : orderOf (Abelianization.of (PresentedGroup.of (self.selected i))) = self.q i

def Undecidability.Gordon.Condition21.orderValues {n m : ℕ} {P : FP n m} (condition : Condition21 P) : Finset ℕ

The finite set of distinct abelianized orders appearing in a witness to condition (2.1).

Equations

• condition.orderValues = Finset.image condition.q Finset.univ

noncomputable def Undecidability.Gordon.Condition21.valueEquiv {n m : ℕ} {P : FP n m} (condition : Condition21 P) : Fin condition.orderValues.card ≃ ↥condition.orderValues

Enumerate the distinct order values by a finite ordinal.

Equations

• condition.valueEquiv = condition.orderValues.equivFin.symm

noncomputable def Undecidability.Gordon.Condition21.representative {n m : ℕ} {P : FP n m} (condition : Condition21 P) (q : ↥condition.orderValues) : Fin condition.p

Choose one original selected generator for each distinct order value.

Equations

• condition.representative q = Classical.choose ⋯

theorem Undecidability.Gordon.Condition21.q_representative {n m : ℕ} {P : FP n m} (condition : Condition21 P) (q : ↥condition.orderValues) : condition.q (condition.representative q) = ↑q

noncomputable def Undecidability.Gordon.Condition21.representativeEmbedding {n m : ℕ} {P : FP n m} (condition : Condition21 P) : ↥condition.orderValues ↪ Fin condition.p

Distinct order values have distinct chosen representatives.

Equations

• condition.representativeEmbedding = { toFun := condition.representative, inj' := ⋯ }

noncomputable def Undecidability.Gordon.Condition21.normalizedSelected {n m : ℕ} {P : FP n m} (condition : Condition21 P) : Fin condition.orderValues.card ↪ Fin n

The duplicate-free selection of host generators.

Equations

• condition.normalizedSelected = (condition.valueEquiv.toEmbedding.trans condition.representativeEmbedding).trans condition.selected

noncomputable def Undecidability.Gordon.Condition21.normalizedQ {n m : ℕ} {P : FP n m} (condition : Condition21 P) : Fin condition.orderValues.card → ℕ

The duplicate-free list of exact abelianized orders.

Equations

• condition.normalizedQ i = ↑(condition.valueEquiv i)

theorem Undecidability.Gordon.Condition21.normalizedQ_injective {n m : ℕ} {P : FP n m} (condition : Condition21 P) : Function.Injective condition.normalizedQ

theorem Undecidability.Gordon.Condition21.normalizedQ_pos {n m : ℕ} {P : FP n m} (condition : Condition21 P) (i : Fin condition.orderValues.card) : 0 < condition.normalizedQ i

theorem Undecidability.Gordon.Condition21.normalized_exactOrder {n m : ℕ} {P : FP n m} (condition : Condition21 P) (i : Fin condition.orderValues.card) : orderOf (Abelianization.of (PresentedGroup.of (condition.normalizedSelected i))) = condition.normalizedQ i

theorem Undecidability.Gordon.Condition21.normalized_gcd {n m : ℕ} {P : FP n m} (condition : Condition21 P) : Finset.univ.gcd condition.normalizedQ = 1

noncomputable def Undecidability.Gordon.Condition21.degreeBound {n m : ℕ} {P : FP n m} (condition : Condition21 P) : ℕ

A bound above every duplicate-free selected order.

Equations

• condition.degreeBound = Finset.univ.sum condition.normalizedQ

theorem Undecidability.Gordon.Condition21.normalizedQ_le_degreeBound {n m : ℕ} {P : FP n m} (condition : Condition21 P) (i : Fin condition.orderValues.card) : condition.normalizedQ i ≤ condition.degreeBound

def Undecidability.Gordon.Condition21.IsNormalizedSelected {n m : ℕ} {P : FP n m} (condition : Condition21 P) (j : Fin n) : Prop

A generator belongs to the duplicate-free selected family.

Equations

• condition.IsNormalizedSelected j = ∃ (i : Fin condition.orderValues.card), condition.normalizedSelected i = j

noncomputable def Undecidability.Gordon.Condition21.normalizedPreimage {n m : ℕ} {P : FP n m} (condition : Condition21 P) (j : Fin n) (hj : condition.IsNormalizedSelected j) : Fin condition.orderValues.card

Recover the unique selected index of a selected generator.

Equations

• condition.normalizedPreimage j hj = Classical.choose hj

theorem Undecidability.Gordon.Condition21.normalizedSelected_preimage {n m : ℕ} {P : FP n m} (condition : Condition21 P) (j : Fin n) (hj : condition.IsNormalizedSelected j) : condition.normalizedSelected (condition.normalizedPreimage j hj) = j

noncomputable def Undecidability.Gordon.Condition21.extendedDegree {n m : ℕ} {P : FP n m} (condition : Condition21 P) (j : Fin n) : ℕ

Extend the selected order values to a positive injective degree assignment on all host generators. Unselected generators receive values strictly above the sum of the selected orders.

Equations

• condition.extendedDegree j = if hj : condition.IsNormalizedSelected j then condition.normalizedQ (condition.normalizedPreimage j hj) else condition.degreeBound + ↑j + 1

theorem Undecidability.Gordon.Condition21.extendedDegree_selected {n m : ℕ} {P : FP n m} (condition : Condition21 P) (i : Fin condition.orderValues.card) : condition.extendedDegree (condition.normalizedSelected i) = condition.normalizedQ i

theorem Undecidability.Gordon.Condition21.extendedDegree_pos {n m : ℕ} {P : FP n m} (condition : Condition21 P) (j : Fin n) : 0 < condition.extendedDegree j

theorem Undecidability.Gordon.Condition21.extendedDegree_injective {n m : ℕ} {P : FP n m} (condition : Condition21 P) : Function.Injective condition.extendedDegree

noncomputable def Undecidability.Gordon.Condition21.toTorsionData {n m : ℕ} {P : FP n m} (condition : Condition21 P) : TorsionData P

Normalize Gordon's printed condition (2.1) to the data required by the one-extra-relator construction.

Equations

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