The witnesses of the paper as corners of arrow matrices

Each witness inverse of the paper is minus the border corner of the inverse of an arrow matrix [[diag d, ω], [α, 0]] (ArrowMatrix), with entries in a division ring D:

• s⁻¹, s = u⁻² + v⁻² + w⁻² (Theorem 5.1): d = (u², v², w²), α = ω = 1;
• f_k⁻¹, f_k = u⁻² + w⁻² + Σ_{i=1}^{m} yⁱ u⁻² y⁻ⁱ, k = m + 2 (Theorems 7.1, 7.3);
• e_d = q_d⁻¹, q_d = w⁻¹ + Σ_{i=0}^{d-1} yⁱ u⁻¹ y⁻ⁱ (Corollary 7.10(a));
• φ_r⁻¹, φ_r = Σ_τ α_τ ℓ_{τ,1}⁻¹ ⋯ ℓ_{τ,r}⁻¹ ω_τ (equation (5.1), Remark 8.2), with d_τ = ℓ_{τ,r} ⋯ ℓ_{τ,1}; for the five chains of (5.1) the arrow matrix is 6 × 6.

Main results

• inv_eq_neg_corner: if x = Σ α d⁻¹ ω ≠ 0, the arrow matrix is a unit and x⁻¹ = −(arrowInv d α ω) (inr ()) (inr ()).
• s_inv_eq_neg_corner, f_inv_eq_neg_corner, e_inv_eq_neg_corner, phi_inv_eq_neg_corner: the four instances.

The statements hold in any division ring; in the paper D is the free field, where the nonvanishing hypotheses are true.

theorem ThreeAxes.ArrowInstances.inv_eq_neg_corner {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (d α ω : ι → D) (hd : ∀ (τ : ι), d τ ≠ 0) (hx : ArrowMatrix.arrowSum d α ω ≠ 0) : IsUnit (ArrowMatrix.arrow d α ω) ∧ (ArrowMatrix.arrowSum d α ω)⁻¹ = -ArrowMatrix.arrowInv d α ω (Sum.inr ()) (Sum.inr ())

x⁻¹ is minus the border corner of the inverse of the arrow matrix, which is a unit.

s = u⁻² + v⁻² + w⁻²

theorem ThreeAxes.ArrowInstances.arrowSum_s {D : Type u_1} [DivisionRing D] (u v w : D) : ArrowMatrix.arrowSum ![u ^ 2, v ^ 2, w ^ 2] 1 1 = (u ^ 2)⁻¹ + (v ^ 2)⁻¹ + (w ^ 2)⁻¹

theorem ThreeAxes.ArrowInstances.s_inv_eq_neg_corner {D : Type u_1} [DivisionRing D] (u v w : D) (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0) (hs : (u ^ 2)⁻¹ + (v ^ 2)⁻¹ + (w ^ 2)⁻¹ ≠ 0) : IsUnit (ArrowMatrix.arrow ![u ^ 2, v ^ 2, w ^ 2] 1 1) ∧ ((u ^ 2)⁻¹ + (v ^ 2)⁻¹ + (w ^ 2)⁻¹)⁻¹ = -ArrowMatrix.arrowInv ![u ^ 2, v ^ 2, w ^ 2] 1 1 (Sum.inr ()) (Sum.inr ())

f_k = u⁻² + w⁻² + Σ_{i=1}^{m} yⁱ u⁻² y⁻ⁱ

def ThreeAxes.ArrowInstances.fDiag {D : Type u_1} [DivisionRing D] (u w : D) (m : ℕ) : Fin 2 ⊕ Fin m → D

Diagonal of the arrow matrix of f_k: u², w², then m copies of u².

Equations

• ThreeAxes.ArrowInstances.fDiag u w m = Sum.elim ![u ^ 2, w ^ 2] fun (x : Fin m) => u ^ 2

def ThreeAxes.ArrowInstances.fLeft {D : Type u_1} [DivisionRing D] (y : D) (m : ℕ) : Fin 2 ⊕ Fin m → D

Left border: 1, 1, y, …, y^m.

Equations

• ThreeAxes.ArrowInstances.fLeft y m = Sum.elim 1 fun (i : Fin m) => y ^ (↑i + 1)

def ThreeAxes.ArrowInstances.fRight {D : Type u_1} [DivisionRing D] (y : D) (m : ℕ) : Fin 2 ⊕ Fin m → D

Right border: 1, 1, y⁻¹, …, y⁻ᵐ.

Equations

• ThreeAxes.ArrowInstances.fRight y m = Sum.elim 1 fun (i : Fin m) => (y ^ (↑i + 1))⁻¹

theorem ThreeAxes.ArrowInstances.arrowSum_f {D : Type u_1} [DivisionRing D] (u w y : D) (m : ℕ) : ArrowMatrix.arrowSum (fDiag u w m) (fLeft y m) (fRight y m) = (u ^ 2)⁻¹ + (w ^ 2)⁻¹ + ∑ i : Fin m, y ^ (↑i + 1) * (u ^ 2)⁻¹ * (y ^ (↑i + 1))⁻¹

theorem ThreeAxes.ArrowInstances.f_inv_eq_neg_corner {D : Type u_1} [DivisionRing D] (u w y : D) (m : ℕ) (hu : u ≠ 0) (hw : w ≠ 0) (hf : (u ^ 2)⁻¹ + (w ^ 2)⁻¹ + ∑ i : Fin m, y ^ (↑i + 1) * (u ^ 2)⁻¹ * (y ^ (↑i + 1))⁻¹ ≠ 0) : IsUnit (ArrowMatrix.arrow (fDiag u w m) (fLeft y m) (fRight y m)) ∧ ((u ^ 2)⁻¹ + (w ^ 2)⁻¹ + ∑ i : Fin m, y ^ (↑i + 1) * (u ^ 2)⁻¹ * (y ^ (↑i + 1))⁻¹)⁻¹ = -ArrowMatrix.arrowInv (fDiag u w m) (fLeft y m) (fRight y m) (Sum.inr ()) (Sum.inr ())

q_d = w⁻¹ + Σ_{i=0}^{d-1} yⁱ u⁻¹ y⁻ⁱ

def ThreeAxes.ArrowInstances.qDiag {D : Type u_1} (u w : D) (d : ℕ) : Option (Fin d) → D

Diagonal of the arrow matrix of q_d: w, then d copies of u.

Equations

• ThreeAxes.ArrowInstances.qDiag u w d τ = τ.elim w fun (x : Fin d) => u

def ThreeAxes.ArrowInstances.qLeft {D : Type u_1} [DivisionRing D] (y : D) (d : ℕ) : Option (Fin d) → D

Left border: 1, 1, y, …, y^{d-1}.

Equations

• ThreeAxes.ArrowInstances.qLeft y d τ = τ.elim 1 fun (i : Fin d) => y ^ ↑i

def ThreeAxes.ArrowInstances.qRight {D : Type u_1} [DivisionRing D] (y : D) (d : ℕ) : Option (Fin d) → D

Right border: 1, 1, y⁻¹, …, y^{-(d-1)}.

Equations

• ThreeAxes.ArrowInstances.qRight y d τ = τ.elim 1 fun (i : Fin d) => (y ^ ↑i)⁻¹

theorem ThreeAxes.ArrowInstances.arrowSum_q {D : Type u_1} [DivisionRing D] (u w y : D) (d : ℕ) : ArrowMatrix.arrowSum (qDiag u w d) (qLeft y d) (qRight y d) = w⁻¹ + ∑ i : Fin d, y ^ ↑i * u⁻¹ * (y ^ ↑i)⁻¹

theorem ThreeAxes.ArrowInstances.e_inv_eq_neg_corner {D : Type u_1} [DivisionRing D] (u w y : D) (d : ℕ) (hu : u ≠ 0) (hw : w ≠ 0) (hq : w⁻¹ + ∑ i : Fin d, y ^ ↑i * u⁻¹ * (y ^ ↑i)⁻¹ ≠ 0) : IsUnit (ArrowMatrix.arrow (qDiag u w d) (qLeft y d) (qRight y d)) ∧ (w⁻¹ + ∑ i : Fin d, y ^ ↑i * u⁻¹ * (y ^ ↑i)⁻¹)⁻¹ = -ArrowMatrix.arrowInv (qDiag u w d) (qLeft y d) (qRight y d) (Sum.inr ()) (Sum.inr ())

φ_r = Σ_τ α_τ ℓ_{τ,1}⁻¹ ⋯ ℓ_{τ,r}⁻¹ ω_τ

def ThreeAxes.ArrowInstances.chainDiag {D : Type u_1} [DivisionRing D] {ι : Type u_2} {r : ℕ} (ℓ : ι → Fin r → D) : ι → D

d_τ = ℓ_{τ,r} ⋯ ℓ_{τ,1}, so that d_τ⁻¹ = ℓ_{τ,1}⁻¹ ⋯ ℓ_{τ,r}⁻¹.

Equations

• ThreeAxes.ArrowInstances.chainDiag ℓ τ = (List.ofFn (ℓ τ)).reverse.prod

theorem ThreeAxes.ArrowInstances.prod_reverse_inv {D : Type u_1} [DivisionRing D] (L : List D) : L.reverse.prod⁻¹ = (List.map (fun (x : D) => x⁻¹) L).prod

(a_n ⋯ a_1)⁻¹ = a_1⁻¹ ⋯ a_n⁻¹ in a division ring (List.prod_inv_reverse is for groups).

theorem ThreeAxes.ArrowInstances.chainDiag_inv {D : Type u_1} [DivisionRing D] {ι : Type u_2} {r : ℕ} (ℓ : ι → Fin r → D) (τ : ι) : (chainDiag ℓ τ)⁻¹ = (List.ofFn fun (j : Fin r) => (ℓ τ j)⁻¹).prod

theorem ThreeAxes.ArrowInstances.arrowSum_phi {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] {r : ℕ} (ℓ : ι → Fin r → D) (α ω : ι → D) : ArrowMatrix.arrowSum (chainDiag ℓ) α ω = ∑ τ : ι, α τ * (List.ofFn fun (j : Fin r) => (ℓ τ j)⁻¹).prod * ω τ

theorem ThreeAxes.ArrowInstances.phi_inv_eq_neg_corner {D : Type u_1} [DivisionRing D] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {r : ℕ} (ℓ : ι → Fin r → D) (α ω : ι → D) (hℓ : ∀ (τ : ι) (j : Fin r), ℓ τ j ≠ 0) (hφ : ∑ τ : ι, α τ * (List.ofFn fun (j : Fin r) => (ℓ τ j)⁻¹).prod * ω τ ≠ 0) : IsUnit (ArrowMatrix.arrow (chainDiag ℓ) α ω) ∧ (∑ τ : ι, α τ * (List.ofFn fun (j : Fin r) => (ℓ τ j)⁻¹).prod * ω τ)⁻¹ = -ArrowMatrix.arrowInv (chainDiag ℓ) α ω (Sum.inr ()) (Sum.inr ())