The exact arc for the three-axes problem

Finite identities behind the proof that s⁻¹, s = u⁻² + v⁻² + w⁻², does not lie in the first layer generated by inverses of binomials, stated in general form.

Main results

• sq_eq_neg_det_of_trace_zero: a 2×2 matrix over a commutative ring with trace 0 squares to −det • 1. exactArc_sq: U = !![i t², −t; i² t³ − η, −i t²] satisfies U * U = (t η) • 1; exactArc_sq_pow: with η = t^k, U * U = t^(k+1) • 1.
• prod_scalar_interleave: in an R-algebra, a₀ (c b₁) (c b₂) ⋯ (c b_r) with c a scalar equals c^r • (a₀ b₁ ⋯ b_r) (evaluation of 𝒥^r where every u_j² is the scalar c). H0_eval: if u², v², w² all equal s • 1, then [[u²+v², u²],[u², u²+w²]] = s • [[2,1],[1,2]]; H_eval_pow: the same for H_{3,2r}, with s^r.
• inv_add_inv: for units a, b, a⁻¹ + b⁻¹ = a⁻¹ (a + b) b⁻¹; inv_add_inv_inverse: if a + b is a unit e, then b e⁻¹ a is a two-sided inverse of a⁻¹ + b⁻¹.
• one_add_pow_char: in characteristic p, (1 + x)^p = 1 + x^p; inv_sq_char: if 1 + x^p is a unit e, then (1+x)^(p−2) e⁻¹ is a two-sided inverse of (1+x)² (so the non-membership result fails in characteristic p).

Related

Three statements are restated here under the names the paper cites, with one-line proofs from existing lemmas: sq_eq_neg_det_of_trace_zero is the trace-zero case of the 2×2 Cayley–Hamilton identity Matrix.mul_self_eq_trace_smul_sub_det_smul_fin_two (in Formalizations.LinearAlgebra.Matrix.FinTwo); inv_add_inv is Mathlib's invOf_add_invOf for the Invertible instance of a unit; one_add_pow_char is Mathlib's add_pow_char_of_commute with Commute.one_left.

T1: trace-zero 2×2 matrices have scalar square; the exact arc

theorem ThreeAxes.ExactArc.sq_eq_neg_det_of_trace_zero {R : Type u_1} [CommRing R] (M : Matrix (Fin 2) (Fin 2) R) (h : M.trace = 0) : M * M = -M.det • 1

A traceless 2×2 matrix squares to −det • 1 (the trace-zero case of Matrix.mul_self_eq_trace_smul_sub_det_smul_fin_two).

def ThreeAxes.ExactArc.exactArc {R : Type u_1} [CommRing R] (i t η : R) : Matrix (Fin 2) (Fin 2) R

The exact arc: one matrix per index i, perturbation η (take η = t^k).

Equations

• ThreeAxes.ExactArc.exactArc i t η = !![i * t ^ 2, -t; i ^ 2 * t ^ 3 - η, -(i * t ^ 2)]

theorem ThreeAxes.ExactArc.exactArc_trace {R : Type u_1} [CommRing R] (i t η : R) : (exactArc i t η).trace = 0

theorem ThreeAxes.ExactArc.exactArc_det {R : Type u_1} [CommRing R] (i t η : R) : (exactArc i t η).det = -(t * η)

theorem ThreeAxes.ExactArc.exactArc_sq {R : Type u_1} [CommRing R] (i t η : R) : exactArc i t η * exactArc i t η = (t * η) • 1

theorem ThreeAxes.ExactArc.exactArc_sq_pow {R : Type u_1} [CommRing R] (i t : R) (k : ℕ) : exactArc i t (t ^ k) * exactArc i t (t ^ k) = t ^ (k + 1) • 1

T2: scalar evaluation

theorem ThreeAxes.ExactArc.prod_scalar_interleave {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] (c : R) (a : S) (l : List S) : a * (List.map (fun (b : S) => (algebraMap R S) c * b) l).prod = c ^ l.length • (a * l.prod)

theorem ThreeAxes.ExactArc.H0_eval {R : Type u_1} {n : Type u_2} [CommRing R] [Fintype n] [DecidableEq n] (s : R) (u v w : Matrix n n R) (hu : u * u = s • 1) (hv : v * v = s • 1) (hw : w * w = s • 1) : Matrix.fromBlocks (u * u + v * v) (u * u) (u * u) (u * u + w * w) = s • Matrix.fromBlocks (1 + 1) 1 1 (1 + 1)

theorem ThreeAxes.ExactArc.H_eval_pow {R : Type u_1} {n : Type u_2} [CommRing R] [Fintype n] [DecidableEq n] (s : R) (u v w : Matrix n n R) (hu : u * u = s • 1) (hv : v * v = s • 1) (hw : w * w = s • 1) (r : ℕ) : Matrix.fromBlocks (u ^ (2 * r) + v ^ (2 * r)) (u ^ (2 * r)) (u ^ (2 * r)) (u ^ (2 * r) + w ^ (2 * r)) = s ^ r • Matrix.fromBlocks (1 + 1) 1 1 (1 + 1)

Lemma 4.2(2) for every r: if u², v², w² all equal s • 1, then H_{3,2r} = [[u^{2r}+v^{2r}, u^{2r}],[u^{2r}, u^{2r}+w^{2r}]] = s^r • [[2,1],[1,2]].

T3: two axes

theorem ThreeAxes.ExactArc.inv_add_inv {R : Type u_1} [Ring R] (a b : Rˣ) : ↑a⁻¹ + ↑b⁻¹ = ↑a⁻¹ * (↑a + ↑b) * ↑b⁻¹

a⁻¹ + b⁻¹ = a⁻¹ (a + b) b⁻¹ for units. This is Mathlib's invOf_add_invOf, restated for Rˣ under the name the paper cites.

theorem ThreeAxes.ExactArc.inv_add_inv_inverse {R : Type u_1} [Ring R] (a b e : Rˣ) (he : ↑e = ↑a + ↑b) : ↑b * ↑e⁻¹ * ↑a * (↑a⁻¹ + ↑b⁻¹) = 1 ∧ (↑a⁻¹ + ↑b⁻¹) * (↑b * ↑e⁻¹ * ↑a) = 1

T4: characteristic p

theorem ThreeAxes.ExactArc.one_add_pow_char {R : Type u_1} [Ring R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (x : R) : (1 + x) ^ p = 1 + x ^ p

(1 + x)^p = 1 + x^p in characteristic p: Mathlib's add_pow_char_of_commute with Commute.one_left, restated under the name the paper cites.

theorem ThreeAxes.ExactArc.inv_sq_char {R : Type u_1} [Ring R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] (x : R) (e : Rˣ) (he : ↑e = 1 + x ^ p) : (1 + x) ^ 2 * ((1 + x) ^ (p - 2) * ↑e⁻¹) = 1 ∧ (1 + x) ^ (p - 2) * ↑e⁻¹ * (1 + x) ^ 2 = 1