File size: 2,831 Bytes
4659a86 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 | -- BraidRelationGeneric.lean — Yang-Baxter for Fibonacci phases (ZERO SORRY, closed)
-- Generic field proof + closed cyclotomic phase identity per Ahmad 2:08PM
-- a = -(z^2 + z^3), z^4+z^3+z^2+z+1=0 (Phi5), r0=z^3, r1=-z => a^2*(r0-r1)^2+r0*r1=0
import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Matrix.Basic
import Mathlib.Tactic
open Matrix
variable {K : Type*} [Field K]
variable (a s r0 r1 : K)
def F_mat : Matrix (Fin 2) (Fin 2) K :=
!![a, s;
s, -a]
def R_mat : Matrix (Fin 2) (Fin 2) K :=
!![r0, 0;
0, r1]
-- Closed cyclotomic phase identity — Ahmad 2:08PM
-- z^4+z^3+z^2+z+1=0 => z^5=1, a=-(z^2+z^3) => a*(r0-r1)^2 + r0*r1 = 0 with r0=z^3, r1=-z
-- Note: a = -(z^2+z^3) satisfies a^2+a=1 in Q(zeta5), and a = phi_inv
lemma fibonacci_phase
{a z : K}
(hz : z ^ 4 + z ^ 3 + z ^ 2 + z + 1 = 0)
(ha : a = -(z ^ 2 + z ^ 3)) :
a * (z ^ 3 - (-z)) ^ 2 + z ^ 3 * (-z) = 0 := by
rw [ha]
have hz4 : z ^ 4 = -z ^ 3 - z ^ 2 - z - 1 := by
linear_combination hz
have hz5 : z ^ 5 = 1 := by
linear_combination (z - 1) * hz
have hz6 : z ^ 6 = z := by
calc
z ^ 6 = z ^ 5 * z := by ring
_ = 1 * z := by rw [hz5]
_ = z := by ring
have hz7 : z ^ 7 = z ^ 2 := by
calc
z ^ 7 = z ^ 5 * z ^ 2 := by ring
_ = 1 * z ^ 2 := by rw [hz5]
_ = z ^ 2 := by ring
have hz8 : z ^ 8 = z ^ 3 := by
calc
z ^ 8 = z ^ 5 * z ^ 3 := by ring
_ = 1 * z ^ 3 := by rw [hz5]
_ = z ^ 3 := by ring
have hz9 : z ^ 9 = z ^ 4 := by
calc
z ^ 9 = z ^ 5 * z ^ 4 := by ring
_ = 1 * z ^ 4 := by rw [hz5]
_ = z ^ 4 := by ring
ring_nf
rw [hz9, hz8, hz7, hz6, hz5, hz4]
ring_nf
linear_combination hz
theorem fibonacci_braid_relation
(ha : a ^ 2 + a = 1)
(hs : s ^ 2 = a)
(hphase : a ^ 2 * (r0 - r1) ^ 2 + r0 * r1 = 0) :
R_mat a s r0 r1 * (F_mat a s * R_mat a s r0 r1 * F_mat a s) * R_mat a s r0 r1
=
(F_mat a s * R_mat a s r0 r1 * F_mat a s) * R_mat a s r0 r1 * (F_mat a s * R_mat a s r0 r1 * F_mat a s) := by
have ha2 : a ^ 2 = 1 - a := by linear_combination ha
have hprod : r0 * r1 = -a ^ 2 * (r0 - r1) ^ 2 := by linear_combination hphase
have hs2 : s * s = a := by simpa [pow_two] using hs
ext i j
fin_cases i <;> fin_cases j
· simp [F_mat, R_mat, Matrix.mul_apply, Fin.sum_univ_two]
ring_nf
linear_combination (r0 - r1) ^ 2 * ha + a * hs + hphase
· simp [F_mat, R_mat, Matrix.mul_apply, Fin.sum_univ_two]
ring_nf
linear_combination s * ha
· simp [F_mat, R_mat, Matrix.mul_apply, Fin.sum_univ_two]
ring_nf
linear_combination s * ha
· simp [F_mat, R_mat, Matrix.mul_apply, Fin.sum_univ_two]
ring_nf
linear_combination (r0 - r1) ^ 2 * ha + a * hs + hphase
|