refactor: Rename deltas in ACC conditions
This commit is contained in:
jstoobysmith
parent
d26f010cb2
commit
6f83f5a623
8 changed files with 367 additions and 355 deletions
|
|
@ -127,7 +127,7 @@ lemma pureU1_last {n : ℕ} (S : (PureU1 n.succ).LinSols) :
|
|||
rw [Fin.sum_univ_castSucc] at hS
|
||||
linear_combination hS
|
||||
|
||||
/-- Two solutions to the Linear ACCs for `n.succ` areq equal if their first `n` charges are
|
||||
/-- Two solutions to the Linear ACCs for `n.succ` areq equal if their first `n` charges are
|
||||
equal. -/
|
||||
lemma pureU1_anomalyFree_ext {n : ℕ} {S T : (PureU1 n.succ).LinSols}
|
||||
(h : ∀ (i : Fin n), S.val i.castSucc = T.val i.castSucc) : S = T := by
|
||||
|
|
|
|||
|
|
@ -28,53 +28,53 @@ namespace VectorLikeEvenPlane
|
|||
lemma n_cond₂ (n : ℕ) : 1 + ((n + n) + 1) = 2 * n.succ := by
|
||||
linarith
|
||||
|
||||
section theδs
|
||||
|
||||
/-- The inclusion of `Fin n.succ` into `Fin (n.succ + n.succ)` via the first `n.succ`,
|
||||
casted into `Fin (2 * n.succ)`. -/
|
||||
def δ₁ (j : Fin n.succ) : Fin (2 * n.succ) := Fin.cast (split_equal n.succ) (Fin.castAdd n.succ j)
|
||||
def evenFst (j : Fin n.succ) : Fin (2 * n.succ) :=
|
||||
Fin.cast (split_equal n.succ) (Fin.castAdd n.succ j)
|
||||
|
||||
/-- The inclusion of `Fin n.succ` into `Fin (n.succ + n.succ)` via the second `n.succ`,
|
||||
casted into `Fin (2 * n.succ)`. -/
|
||||
def δ₂ (j : Fin n.succ) : Fin (2 * n.succ) := Fin.cast (split_equal n.succ) (Fin.natAdd n.succ j)
|
||||
def evenSnd (j : Fin n.succ) : Fin (2 * n.succ) :=
|
||||
Fin.cast (split_equal n.succ) (Fin.natAdd n.succ j)
|
||||
|
||||
/-- The inclusion of `Fin n` into `Fin (1 + (n + n + 1))` via the first `n`,
|
||||
casted into `Fin (2 * n.succ)`. -/
|
||||
def δ!₁ (j : Fin n) : Fin (2 * n.succ) := Fin.cast (n_cond₂ n)
|
||||
def evenShiftFst (j : Fin n) : Fin (2 * n.succ) := Fin.cast (n_cond₂ n)
|
||||
(Fin.natAdd 1 (Fin.castAdd 1 (Fin.castAdd n j)))
|
||||
|
||||
/-- The inclusion of `Fin n` into `Fin (1 + (n + n + 1))` via the second `n`,
|
||||
casted into `Fin (2 * n.succ)`. -/
|
||||
def δ!₂ (j : Fin n) : Fin (2 * n.succ) := Fin.cast (n_cond₂ n)
|
||||
def evenShiftSnd (j : Fin n) : Fin (2 * n.succ) := Fin.cast (n_cond₂ n)
|
||||
(Fin.natAdd 1 (Fin.castAdd 1 (Fin.natAdd n j)))
|
||||
|
||||
/-- The element of `Fin (1 + (n + n + 1))` corresponding to the first `1`,
|
||||
casted into `Fin (2 * n.succ)`. -/
|
||||
def δ!₃ : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.castAdd ((n + n) + 1) 0))
|
||||
def evenShiftZero : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.castAdd ((n + n) + 1) 0))
|
||||
|
||||
/-- The element of `Fin (1 + (n + n + 1))` corresponding to the second `1`,
|
||||
casted into `Fin (2 * n.succ)`. -/
|
||||
def δ!₄ : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.natAdd 1 (Fin.natAdd (n + n) 0)))
|
||||
def evenShiftLast : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.natAdd 1 (Fin.natAdd (n + n) 0)))
|
||||
|
||||
lemma ext_δ (S T : Fin (2 * n.succ) → ℚ) (h1 : ∀ i, S (δ₁ i) = T (δ₁ i))
|
||||
(h2 : ∀ i, S (δ₂ i) = T (δ₂ i)) : S = T := by
|
||||
lemma ext_even (S T : Fin (2 * n.succ) → ℚ) (h1 : ∀ i, S (evenFst i) = T (evenFst i))
|
||||
(h2 : ∀ i, S (evenSnd i) = T (evenSnd i)) : S = T := by
|
||||
funext i
|
||||
by_cases hi : i.val < n.succ
|
||||
· let j : Fin n.succ := ⟨i, hi⟩
|
||||
have h2 := h1 j
|
||||
have h3 : δ₁ j = i := rfl
|
||||
have h3 : evenFst j = i := rfl
|
||||
rw [h3] at h2
|
||||
exact h2
|
||||
· let j : Fin n.succ := ⟨i - n.succ, by omega⟩
|
||||
have h2 := h2 j
|
||||
have h3 : δ₂ j = i := by
|
||||
simp only [succ_eq_add_one, δ₂, Fin.ext_iff, Fin.coe_cast, Fin.coe_natAdd]
|
||||
have h3 : evenSnd j = i := by
|
||||
simp only [succ_eq_add_one, evenSnd, Fin.ext_iff, Fin.coe_cast, Fin.coe_natAdd]
|
||||
omega
|
||||
rw [h3] at h2
|
||||
exact h2
|
||||
|
||||
lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) :
|
||||
∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
|
||||
lemma sum_even (S : Fin (2 * n.succ) → ℚ) :
|
||||
∑ i, S i = ∑ i : Fin n.succ, ((S ∘ evenFst) i + (S ∘ evenSnd) i) := by
|
||||
have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by
|
||||
rw [Finset.sum_equiv (Fin.castOrderIso (split_equal n.succ)).symm.toEquiv]
|
||||
· intro i
|
||||
|
|
@ -83,18 +83,9 @@ lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) :
|
|||
rw [h1, Fin.sum_univ_add, Finset.sum_add_distrib]
|
||||
rfl
|
||||
|
||||
lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) :
|
||||
∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
|
||||
have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by
|
||||
rw [Finset.sum_equiv (Fin.castOrderIso (split_equal n.succ)).symm.toEquiv]
|
||||
· intro i
|
||||
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
|
||||
· exact fun _ _ => rfl
|
||||
rw [h1, Fin.sum_univ_add, Finset.sum_add_distrib]
|
||||
rfl
|
||||
|
||||
lemma sum_δ!₁_δ!₂ (S : Fin (2 * n.succ) → ℚ) :
|
||||
∑ i, S i = S δ!₃ + S δ!₄ + ∑ i : Fin n, ((S ∘ δ!₁) i + (S ∘ δ!₂) i) := by
|
||||
lemma sum_evenShift (S : Fin (2 * n.succ) → ℚ) :
|
||||
∑ i, S i = S evenShiftZero + S evenShiftLast +
|
||||
∑ i : Fin n, ((S ∘ evenShiftFst) i + (S ∘ evenShiftSnd) i) := by
|
||||
have h1 : ∑ i, S i = ∑ i : Fin (1 + ((n + n) + 1)), S (Fin.cast (n_cond₂ n) i) := by
|
||||
rw [Finset.sum_equiv (Fin.castOrderIso (n_cond₂ n)).symm.toEquiv]
|
||||
· intro i
|
||||
|
|
@ -112,35 +103,33 @@ lemma sum_δ!₁_δ!₂ (S : Fin (2 * n.succ) → ℚ) :
|
|||
nth_rewrite 2 [Rat.add_comm]
|
||||
rfl
|
||||
|
||||
lemma δ!₃_δ₁0 : @δ!₃ n = δ₁ 0 := rfl
|
||||
lemma evenShiftZero_eq_evenFst_zero : @evenShiftZero n = evenFst 0 := rfl
|
||||
|
||||
lemma δ!₄_δ₂Last: @δ!₄ n = δ₂ (Fin.last n) := by
|
||||
lemma evenShiftLast_eq_evenSnd_last: @evenShiftLast n = evenSnd (Fin.last n) := by
|
||||
rw [Fin.ext_iff]
|
||||
simp only [succ_eq_add_one, δ!₄, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd, Fin.val_eq_zero,
|
||||
add_zero, δ₂, Fin.natAdd_last, Fin.val_last]
|
||||
simp only [succ_eq_add_one, evenShiftLast, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd,
|
||||
Fin.val_eq_zero, add_zero, evenSnd, Fin.natAdd_last, Fin.val_last]
|
||||
omega
|
||||
|
||||
lemma δ!₁_δ₁ (j : Fin n) : δ!₁ j = δ₁ j.succ := by
|
||||
rw [Fin.ext_iff, δ₁, δ!₁]
|
||||
lemma evenShiftFst_eq_evenFst_succ (j : Fin n) : evenShiftFst j = evenFst j.succ := by
|
||||
rw [Fin.ext_iff, evenFst, evenShiftFst]
|
||||
simp only [Fin.coe_cast, Fin.coe_natAdd, Fin.coe_castAdd, Fin.val_succ]
|
||||
ring
|
||||
|
||||
lemma δ!₂_δ₂ (j : Fin n) : δ!₂ j = δ₂ j.castSucc := by
|
||||
rw [Fin.ext_iff, δ₂, δ!₂]
|
||||
lemma evenShiftSnd_eq_evenSnd_castSucc (j : Fin n) : evenShiftSnd j = evenSnd j.castSucc := by
|
||||
rw [Fin.ext_iff, evenSnd, evenShiftSnd]
|
||||
simp only [Fin.coe_cast, Fin.coe_natAdd, Fin.coe_castAdd, Fin.coe_castSucc]
|
||||
ring_nf
|
||||
rw [Nat.succ_eq_add_one]
|
||||
ring
|
||||
|
||||
end theδs
|
||||
|
||||
/-- The first part of the basis as charges. -/
|
||||
def basisAsCharges (j : Fin n.succ) : (PureU1 (2 * n.succ)).Charges :=
|
||||
fun i =>
|
||||
if i = δ₁ j then
|
||||
if i = evenFst j then
|
||||
1
|
||||
else
|
||||
if i = δ₂ j then
|
||||
if i = evenSnd j then
|
||||
- 1
|
||||
else
|
||||
0
|
||||
|
|
@ -148,23 +137,23 @@ def basisAsCharges (j : Fin n.succ) : (PureU1 (2 * n.succ)).Charges :=
|
|||
/-- The second part of the basis as charges. -/
|
||||
def basis!AsCharges (j : Fin n) : (PureU1 (2 * n.succ)).Charges :=
|
||||
fun i =>
|
||||
if i = δ!₁ j then
|
||||
if i = evenShiftFst j then
|
||||
1
|
||||
else
|
||||
if i = δ!₂ j then
|
||||
if i = evenShiftSnd j then
|
||||
- 1
|
||||
else
|
||||
0
|
||||
|
||||
lemma basis_on_δ₁_self (j : Fin n.succ) : basisAsCharges j (δ₁ j) = 1 := by
|
||||
lemma basis_on_evenFst_self (j : Fin n.succ) : basisAsCharges j (evenFst j) = 1 := by
|
||||
simp [basisAsCharges]
|
||||
|
||||
lemma basis!_on_δ!₁_self (j : Fin n) : basis!AsCharges j (δ!₁ j) = 1 := by
|
||||
lemma basis!_on_evenShiftFst_self (j : Fin n) : basis!AsCharges j (evenShiftFst j) = 1 := by
|
||||
simp [basis!AsCharges]
|
||||
|
||||
lemma basis_on_δ₁_other {k j : Fin n.succ} (h : k ≠ j) :
|
||||
basisAsCharges k (δ₁ j) = 0 := by
|
||||
simp only [basisAsCharges, succ_eq_add_one, PureU1_numberCharges, δ₁, succ_eq_add_one, δ₂]
|
||||
lemma basis_on_evenFst_other {k j : Fin n.succ} (h : k ≠ j) :
|
||||
basisAsCharges k (evenFst j) = 0 := by
|
||||
simp only [basisAsCharges, succ_eq_add_one, PureU1_numberCharges, evenFst, evenSnd]
|
||||
split
|
||||
· rename_i h1
|
||||
rw [Fin.ext_iff] at h1
|
||||
|
|
@ -179,20 +168,20 @@ lemma basis_on_δ₁_other {k j : Fin n.succ} (h : k ≠ j) :
|
|||
omega
|
||||
· rfl
|
||||
|
||||
lemma basis_on_other {k : Fin n.succ} {j : Fin (2 * n.succ)} (h1 : j ≠ δ₁ k) (h2 : j ≠ δ₂ k) :
|
||||
basisAsCharges k j = 0 := by
|
||||
lemma basis_on_other {k : Fin n.succ} {j : Fin (2 * n.succ)} (h1 : j ≠ evenFst k)
|
||||
(h2 : j ≠ evenSnd k) : basisAsCharges k j = 0 := by
|
||||
simp only [basisAsCharges, succ_eq_add_one, PureU1_numberCharges]
|
||||
simp_all only [ne_eq, ↓reduceIte]
|
||||
|
||||
lemma basis!_on_other {k : Fin n} {j : Fin (2 * n.succ)} (h1 : j ≠ δ!₁ k) (h2 : j ≠ δ!₂ k) :
|
||||
basis!AsCharges k j = 0 := by
|
||||
lemma basis!_on_other {k : Fin n} {j : Fin (2 * n.succ)} (h1 : j ≠ evenShiftFst k)
|
||||
(h2 : j ≠ evenShiftSnd k) : basis!AsCharges k j = 0 := by
|
||||
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges]
|
||||
simp_all only [ne_eq, ↓reduceIte]
|
||||
|
||||
lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
|
||||
basis!AsCharges k (δ!₁ j) = 0 := by
|
||||
lemma basis!_on_evenShiftFst_other {k j : Fin n} (h : k ≠ j) :
|
||||
basis!AsCharges k (evenShiftFst j) = 0 := by
|
||||
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges]
|
||||
simp only [δ!₁, succ_eq_add_one, δ!₂]
|
||||
simp only [evenShiftFst, succ_eq_add_one, evenShiftSnd]
|
||||
split
|
||||
· rename_i h1
|
||||
rw [Fin.ext_iff] at h1
|
||||
|
|
@ -207,9 +196,9 @@ lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
|
|||
omega
|
||||
· rfl
|
||||
|
||||
lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n.succ) :
|
||||
basisAsCharges j (δ₂ i) = - basisAsCharges j (δ₁ i) := by
|
||||
simp only [basisAsCharges, succ_eq_add_one, PureU1_numberCharges, δ₂, δ₁]
|
||||
lemma basis_evenSnd_eq_neg_evenFst (j i : Fin n.succ) :
|
||||
basisAsCharges j (evenSnd i) = - basisAsCharges j (evenFst i) := by
|
||||
simp only [basisAsCharges, succ_eq_add_one, PureU1_numberCharges, evenSnd, evenFst]
|
||||
split <;> split
|
||||
any_goals split
|
||||
any_goals rfl
|
||||
|
|
@ -225,9 +214,9 @@ lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n.succ) :
|
|||
simp_all
|
||||
all_goals omega
|
||||
|
||||
lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
|
||||
basis!AsCharges j (δ!₂ i) = - basis!AsCharges j (δ!₁ i) := by
|
||||
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges, δ!₂, δ!₁]
|
||||
lemma basis!_evenShftSnd_eq_neg_evenShiftFst (j i : Fin n) :
|
||||
basis!AsCharges j (evenShiftSnd i) = - basis!AsCharges j (evenShiftFst i) := by
|
||||
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges, evenShiftSnd, evenShiftFst]
|
||||
split <;> split
|
||||
any_goals split
|
||||
any_goals split
|
||||
|
|
@ -242,75 +231,76 @@ lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
|
|||
all_goals simp_all
|
||||
all_goals omega
|
||||
|
||||
lemma basis_on_δ₂_self (j : Fin n.succ) : basisAsCharges j (δ₂ j) = - 1 := by
|
||||
rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_self]
|
||||
lemma basis_on_evenSnd_self (j : Fin n.succ) : basisAsCharges j (evenSnd j) = - 1 := by
|
||||
rw [basis_evenSnd_eq_neg_evenFst, basis_on_evenFst_self]
|
||||
|
||||
lemma basis!_on_δ!₂_self (j : Fin n) : basis!AsCharges j (δ!₂ j) = - 1 := by
|
||||
rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_self]
|
||||
lemma basis!_on_evenShiftSnd_self (j : Fin n) : basis!AsCharges j (evenShiftSnd j) = - 1 := by
|
||||
rw [basis!_evenShftSnd_eq_neg_evenShiftFst, basis!_on_evenShiftFst_self]
|
||||
|
||||
lemma basis_on_δ₂_other {k j : Fin n.succ} (h : k ≠ j) : basisAsCharges k (δ₂ j) = 0 := by
|
||||
rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_other h]
|
||||
lemma basis_on_evenSnd_other {k j : Fin n.succ} (h : k ≠ j) : basisAsCharges k (evenSnd j) = 0 := by
|
||||
rw [basis_evenSnd_eq_neg_evenFst, basis_on_evenFst_other h]
|
||||
rfl
|
||||
|
||||
lemma basis!_on_δ!₂_other {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (δ!₂ j) = 0 := by
|
||||
rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_other h]
|
||||
lemma basis!_on_evenShiftSnd_other {k j : Fin n} (h : k ≠ j) :
|
||||
basis!AsCharges k (evenShiftSnd j) = 0 := by
|
||||
rw [basis!_evenShftSnd_eq_neg_evenShiftFst, basis!_on_evenShiftFst_other h]
|
||||
rfl
|
||||
|
||||
lemma basis!_on_δ!₃ (j : Fin n) : basis!AsCharges j δ!₃ = 0 := by
|
||||
lemma basis!_on_evenShiftZero (j : Fin n) : basis!AsCharges j evenShiftZero = 0 := by
|
||||
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges]
|
||||
split<;> rename_i h
|
||||
· simp only [δ!₃, succ_eq_add_one, Fin.isValue, δ!₁, Fin.ext_iff, Fin.coe_cast, Fin.coe_castAdd,
|
||||
Fin.val_eq_zero, Fin.coe_natAdd] at h
|
||||
· simp only [evenShiftZero, succ_eq_add_one, Fin.isValue, evenShiftFst, Fin.ext_iff,
|
||||
Fin.coe_cast, Fin.coe_castAdd, Fin.val_eq_zero, Fin.coe_natAdd] at h
|
||||
omega
|
||||
· split <;> rename_i h2
|
||||
· simp only [δ!₃, succ_eq_add_one, Fin.isValue, δ!₂, Fin.ext_iff, Fin.coe_cast,
|
||||
Fin.coe_castAdd, Fin.val_eq_zero, Fin.coe_natAdd] at h2
|
||||
· simp only [evenShiftZero, succ_eq_add_one, Fin.isValue, evenShiftSnd, Fin.ext_iff,
|
||||
Fin.coe_cast, Fin.coe_castAdd, Fin.val_eq_zero, Fin.coe_natAdd] at h2
|
||||
omega
|
||||
· rfl
|
||||
|
||||
lemma basis!_on_δ!₄ (j : Fin n) : basis!AsCharges j δ!₄ = 0 := by
|
||||
lemma basis!_on_evenShiftLast (j : Fin n) : basis!AsCharges j evenShiftLast = 0 := by
|
||||
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges]
|
||||
split <;> rename_i h
|
||||
· rw [Fin.ext_iff] at h
|
||||
simp only [succ_eq_add_one, δ!₄, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd, Fin.val_eq_zero,
|
||||
add_zero, δ!₁, Fin.coe_castAdd, add_right_inj] at h
|
||||
simp only [succ_eq_add_one, evenShiftLast, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd,
|
||||
Fin.val_eq_zero, add_zero, evenShiftFst, Fin.coe_castAdd, add_right_inj] at h
|
||||
omega
|
||||
· split <;> rename_i h2
|
||||
· rw [Fin.ext_iff] at h2
|
||||
simp only [succ_eq_add_one, δ!₄, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd, Fin.val_eq_zero,
|
||||
add_zero, δ!₂, Fin.coe_castAdd, add_right_inj] at h2
|
||||
simp only [succ_eq_add_one, evenShiftLast, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd,
|
||||
Fin.val_eq_zero, add_zero, evenShiftSnd, Fin.coe_castAdd, add_right_inj] at h2
|
||||
omega
|
||||
· rfl
|
||||
|
||||
lemma basis_linearACC (j : Fin n.succ) : (accGrav (2 * n.succ)) (basisAsCharges j) = 0 := by
|
||||
rw [accGrav]
|
||||
simp only [LinearMap.coe_mk, AddHom.coe_mk]
|
||||
rw [sum_δ₁_δ₂]
|
||||
simp [basis_δ₂_eq_minus_δ₁]
|
||||
rw [sum_even]
|
||||
simp [basis_evenSnd_eq_neg_evenFst]
|
||||
|
||||
lemma basis!_linearACC (j : Fin n) : (accGrav (2 * n.succ)) (basis!AsCharges j) = 0 := by
|
||||
rw [accGrav]
|
||||
simp only [LinearMap.coe_mk, AddHom.coe_mk]
|
||||
rw [sum_δ!₁_δ!₂, basis!_on_δ!₃, basis!_on_δ!₄]
|
||||
simp [basis!_δ!₂_eq_minus_δ!₁]
|
||||
rw [sum_evenShift, basis!_on_evenShiftZero, basis!_on_evenShiftLast]
|
||||
simp [basis!_evenShftSnd_eq_neg_evenShiftFst]
|
||||
|
||||
lemma basis_accCube (j : Fin n.succ) :
|
||||
accCube (2 * n.succ) (basisAsCharges j) = 0 := by
|
||||
rw [accCube_explicit, sum_δ₁_δ₂]
|
||||
rw [accCube_explicit, sum_even]
|
||||
apply Finset.sum_eq_zero
|
||||
intro i _
|
||||
simp only [succ_eq_add_one, Function.comp_apply, basis_δ₂_eq_minus_δ₁]
|
||||
simp only [succ_eq_add_one, Function.comp_apply, basis_evenSnd_eq_neg_evenFst]
|
||||
ring
|
||||
|
||||
lemma basis!_accCube (j : Fin n) :
|
||||
accCube (2 * n.succ) (basis!AsCharges j) = 0 := by
|
||||
rw [accCube_explicit, sum_δ!₁_δ!₂]
|
||||
rw [basis!_on_δ!₄, basis!_on_δ!₃]
|
||||
rw [accCube_explicit, sum_evenShift]
|
||||
rw [basis!_on_evenShiftLast, basis!_on_evenShiftZero]
|
||||
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero, Function.comp_apply,
|
||||
zero_add]
|
||||
apply Finset.sum_eq_zero
|
||||
intro i _
|
||||
simp only [basis!_δ!₂_eq_minus_δ!₁]
|
||||
simp only [basis!_evenShftSnd_eq_neg_evenShiftFst]
|
||||
ring
|
||||
|
||||
/-- The first part of the basis as `LinSols`. -/
|
||||
|
|
@ -339,22 +329,23 @@ def basisa : (Fin n.succ) ⊕ (Fin n) → (PureU1 (2 * n.succ)).LinSols := fun i
|
|||
| .inl i => basis i
|
||||
| .inr i => basis! i
|
||||
|
||||
/-- Swapping the elements δ!₁ j and δ!₂ j is equivalent to adding a vector basis!AsCharges j. -/
|
||||
/-- Swapping the elements evenShiftFst j and evenShiftSnd j is equivalent to
|
||||
adding a vector basis!AsCharges j. -/
|
||||
lemma swap!_as_add {S S' : (PureU1 (2 * n.succ)).LinSols} (j : Fin n)
|
||||
(hS : ((FamilyPermutations (2 * n.succ)).linSolRep
|
||||
(pairSwap (δ!₁ j) (δ!₂ j))) S = S') :
|
||||
S'.val = S.val + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j := by
|
||||
(pairSwap (evenShiftFst j) (evenShiftSnd j))) S = S') :
|
||||
S'.val = S.val + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j := by
|
||||
funext i
|
||||
rw [← hS, FamilyPermutations_anomalyFreeLinear_apply]
|
||||
by_cases hi : i = δ!₁ j
|
||||
by_cases hi : i = evenShiftFst j
|
||||
· subst hi
|
||||
simp [HSMul.hSMul, basis!_on_δ!₁_self, pairSwap_inv_fst]
|
||||
· by_cases hi2 : i = δ!₂ j
|
||||
· simp [HSMul.hSMul, hi2, basis!_on_δ!₂_self, pairSwap_inv_snd]
|
||||
simp [HSMul.hSMul, basis!_on_evenShiftFst_self, pairSwap_inv_fst]
|
||||
· by_cases hi2 : i = evenShiftSnd j
|
||||
· simp [HSMul.hSMul, hi2, basis!_on_evenShiftSnd_self, pairSwap_inv_snd]
|
||||
· simp only [succ_eq_add_one, Equiv.invFun_as_coe, HSMul.hSMul,
|
||||
ACCSystemCharges.chargesAddCommMonoid_add, ACCSystemCharges.chargesModule_smul]
|
||||
rw [basis!_on_other hi hi2]
|
||||
change S.val ((pairSwap (δ!₁ j) (δ!₂ j)).invFun i) =_
|
||||
change S.val ((pairSwap (evenShiftFst j) (evenShiftSnd j)).invFun i) =_
|
||||
erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)]
|
||||
simp
|
||||
|
||||
|
|
@ -367,106 +358,107 @@ def P! (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).Charges := ∑ i, f i • bas
|
|||
/-- A point in the span of the basis as a charge. -/
|
||||
def Pa (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n.succ)).Charges := P f + P! g
|
||||
|
||||
lemma P_δ₁ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₁ j) = f j := by
|
||||
lemma P_evenFst (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (evenFst j) = f j := by
|
||||
rw [P, sum_of_charges]
|
||||
simp only [succ_eq_add_one, HSMul.hSMul, SMul.smul]
|
||||
rw [Finset.sum_eq_single j]
|
||||
· rw [basis_on_δ₁_self]
|
||||
· rw [basis_on_evenFst_self]
|
||||
exact Rat.mul_one (f j)
|
||||
· intro k _ hkj
|
||||
rw [basis_on_δ₁_other hkj]
|
||||
rw [basis_on_evenFst_other hkj]
|
||||
exact Rat.mul_zero (f k)
|
||||
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
|
||||
|
||||
lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
|
||||
lemma P!_evenShiftFst (f : Fin n → ℚ) (j : Fin n) : P! f (evenShiftFst j) = f j := by
|
||||
rw [P!, sum_of_charges]
|
||||
simp only [HSMul.hSMul, SMul.smul]
|
||||
rw [Finset.sum_eq_single j]
|
||||
· rw [basis!_on_δ!₁_self]
|
||||
· rw [basis!_on_evenShiftFst_self]
|
||||
exact Rat.mul_one (f j)
|
||||
· intro k _ hkj
|
||||
rw [basis!_on_δ!₁_other hkj]
|
||||
rw [basis!_on_evenShiftFst_other hkj]
|
||||
exact Rat.mul_zero (f k)
|
||||
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
|
||||
|
||||
lemma Pa_δ!₁ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
|
||||
Pa f g (δ!₁ j) = f j.succ + g j := by
|
||||
lemma Pa_evenShiftFst (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
|
||||
Pa f g (evenShiftFst j) = f j.succ + g j := by
|
||||
rw [Pa]
|
||||
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
|
||||
rw [P!_δ!₁, δ!₁_δ₁, P_δ₁]
|
||||
rw [P!_evenShiftFst, evenShiftFst_eq_evenFst_succ, P_evenFst]
|
||||
|
||||
lemma P_δ₂ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₂ j) = - f j := by
|
||||
lemma P_evenSnd (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (evenSnd j) = - f j := by
|
||||
rw [P, sum_of_charges]
|
||||
simp only [succ_eq_add_one, HSMul.hSMul, SMul.smul]
|
||||
rw [Finset.sum_eq_single j]
|
||||
· simp only [basis_on_δ₂_self, mul_neg, mul_one]
|
||||
· simp only [basis_on_evenSnd_self, mul_neg, mul_one]
|
||||
· intro k _ hkj
|
||||
simp only [basis_on_δ₂_other hkj, mul_zero]
|
||||
simp only [basis_on_evenSnd_other hkj, mul_zero]
|
||||
· simp
|
||||
|
||||
lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
|
||||
lemma P!_evenShiftSnd (f : Fin n → ℚ) (j : Fin n) : P! f (evenShiftSnd j) = - f j := by
|
||||
rw [P!, sum_of_charges]
|
||||
simp only [HSMul.hSMul, SMul.smul]
|
||||
rw [Finset.sum_eq_single j]
|
||||
· rw [basis!_on_δ!₂_self]
|
||||
· rw [basis!_on_evenShiftSnd_self]
|
||||
exact mul_neg_one (f j)
|
||||
· intro k _ hkj
|
||||
rw [basis!_on_δ!₂_other hkj]
|
||||
rw [basis!_on_evenShiftSnd_other hkj]
|
||||
exact Rat.mul_zero (f k)
|
||||
· simp
|
||||
|
||||
lemma Pa_δ!₂ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
|
||||
Pa f g (δ!₂ j) = - f j.castSucc - g j := by
|
||||
lemma Pa_evenShiftSnd (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
|
||||
Pa f g (evenShiftSnd j) = - f j.castSucc - g j := by
|
||||
rw [Pa]
|
||||
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
|
||||
rw [P!_δ!₂, δ!₂_δ₂, P_δ₂]
|
||||
rw [P!_evenShiftSnd, evenShiftSnd_eq_evenSnd_castSucc, P_evenSnd]
|
||||
ring
|
||||
|
||||
lemma P!_δ!₃ (f : Fin n → ℚ) : P! f (δ!₃) = 0 := by
|
||||
lemma P!_evenShiftZero (f : Fin n → ℚ) : P! f (evenShiftZero) = 0 := by
|
||||
rw [P!, sum_of_charges]
|
||||
simp [HSMul.hSMul, SMul.smul, basis!_on_δ!₃]
|
||||
simp [HSMul.hSMul, SMul.smul, basis!_on_evenShiftZero]
|
||||
|
||||
lemma Pa_δ!₃ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g (δ!₃) = f 0 := by
|
||||
lemma Pa_evenShitZero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g (evenShiftZero) = f 0 := by
|
||||
rw [Pa]
|
||||
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
|
||||
rw [P!_δ!₃, δ!₃_δ₁0, P_δ₁]
|
||||
rw [P!_evenShiftZero, evenShiftZero_eq_evenFst_zero, P_evenFst]
|
||||
exact Rat.add_zero (f 0)
|
||||
|
||||
lemma P!_δ!₄ (f : Fin n → ℚ) : P! f (δ!₄) = 0 := by
|
||||
lemma P!_evenShiftLast (f : Fin n → ℚ) : P! f (evenShiftLast) = 0 := by
|
||||
rw [P!, sum_of_charges]
|
||||
simp [HSMul.hSMul, SMul.smul, basis!_on_δ!₄]
|
||||
simp [HSMul.hSMul, SMul.smul, basis!_on_evenShiftLast]
|
||||
|
||||
lemma Pa_δ!₄ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g (δ!₄) = - f (Fin.last n) := by
|
||||
lemma Pa_evenShiftLast (f : Fin n.succ → ℚ) (g : Fin n → ℚ) :
|
||||
Pa f g (evenShiftLast) = - f (Fin.last n) := by
|
||||
rw [Pa]
|
||||
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
|
||||
rw [P!_δ!₄, δ!₄_δ₂Last, P_δ₂]
|
||||
rw [P!_evenShiftLast, evenShiftLast_eq_evenSnd_last, P_evenSnd]
|
||||
exact Rat.add_zero (-f (Fin.last n))
|
||||
|
||||
lemma P_δ₁_δ₂ (f : Fin n.succ → ℚ) : P f ∘ δ₂ = - P f ∘ δ₁ := by
|
||||
lemma P_evenSnd_evenFst (f : Fin n.succ → ℚ) : P f ∘ evenSnd = - P f ∘ evenFst := by
|
||||
funext j
|
||||
simp only [PureU1_numberCharges, Function.comp_apply, Pi.neg_apply]
|
||||
rw [P_δ₁, P_δ₂]
|
||||
rw [P_evenFst, P_evenSnd]
|
||||
|
||||
lemma P_linearACC (f : Fin n.succ → ℚ) : (accGrav (2 * n.succ)) (P f) = 0 := by
|
||||
rw [accGrav]
|
||||
simp only [LinearMap.coe_mk, AddHom.coe_mk]
|
||||
rw [sum_δ₁_δ₂]
|
||||
simp [P_δ₂, P_δ₁]
|
||||
rw [sum_even]
|
||||
simp [P_evenSnd, P_evenFst]
|
||||
|
||||
lemma P_accCube (f : Fin n.succ → ℚ) : accCube (2 * n.succ) (P f) = 0 := by
|
||||
rw [accCube_explicit, sum_δ₁_δ₂]
|
||||
rw [accCube_explicit, sum_even]
|
||||
apply Finset.sum_eq_zero
|
||||
intro i _
|
||||
simp only [succ_eq_add_one, Function.comp_apply, P_δ₁, P_δ₂]
|
||||
simp only [succ_eq_add_one, Function.comp_apply, P_evenFst, P_evenSnd]
|
||||
ring
|
||||
|
||||
lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n.succ) (P! f) = 0 := by
|
||||
rw [accCube_explicit, sum_δ!₁_δ!₂, P!_δ!₃, P!_δ!₄]
|
||||
rw [accCube_explicit, sum_evenShift, P!_evenShiftZero, P!_evenShiftLast]
|
||||
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero, Function.comp_apply,
|
||||
zero_add]
|
||||
apply Finset.sum_eq_zero
|
||||
intro i _
|
||||
simp only [P!_δ!₁, P!_δ!₂]
|
||||
simp only [P!_evenShiftFst, P!_evenShiftSnd]
|
||||
ring
|
||||
|
||||
lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) :
|
||||
|
|
@ -474,47 +466,47 @@ lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) :
|
|||
= g (j.succ) ^ 2 - g (j.castSucc) ^ 2 := by
|
||||
simp only [succ_eq_add_one, accCubeTriLinSymm, PureU1Charges_numberCharges,
|
||||
TriLinearSymm.mk₃_toFun_apply_apply]
|
||||
rw [sum_δ!₁_δ!₂, basis!_on_δ!₃, basis!_on_δ!₄]
|
||||
rw [sum_evenShift, basis!_on_evenShiftZero, basis!_on_evenShiftLast]
|
||||
simp only [mul_zero, add_zero, Function.comp_apply, zero_add]
|
||||
rw [Finset.sum_eq_single j, basis!_on_δ!₁_self, basis!_on_δ!₂_self]
|
||||
· simp only [δ!₁_δ₁, mul_one, δ!₂_δ₂, mul_neg]
|
||||
rw [P_δ₁, P_δ₂]
|
||||
rw [Finset.sum_eq_single j, basis!_on_evenShiftFst_self, basis!_on_evenShiftSnd_self]
|
||||
· simp only [evenShiftFst_eq_evenFst_succ, mul_one, evenShiftSnd_eq_evenSnd_castSucc, mul_neg]
|
||||
rw [P_evenFst, P_evenSnd]
|
||||
ring
|
||||
· intro k _ hkj
|
||||
erw [basis!_on_δ!₁_other hkj.symm, basis!_on_δ!₂_other hkj.symm]
|
||||
erw [basis!_on_evenShiftFst_other hkj.symm, basis!_on_evenShiftSnd_other hkj.symm]
|
||||
simp only [mul_zero, add_zero]
|
||||
· simp
|
||||
|
||||
lemma P_P!_P!_accCube (g : Fin n → ℚ) (j : Fin n.succ) :
|
||||
accCubeTriLinSymm (P! g) (P! g) (basisAsCharges j)
|
||||
= (P! g (δ₁ j))^2 - (P! g (δ₂ j))^2 := by
|
||||
= (P! g (evenFst j))^2 - (P! g (evenSnd j))^2 := by
|
||||
simp only [succ_eq_add_one, accCubeTriLinSymm, PureU1Charges_numberCharges,
|
||||
TriLinearSymm.mk₃_toFun_apply_apply]
|
||||
rw [sum_δ₁_δ₂]
|
||||
rw [sum_even]
|
||||
simp only [Function.comp_apply]
|
||||
rw [Finset.sum_eq_single j, basis_on_δ₁_self, basis_on_δ₂_self]
|
||||
rw [Finset.sum_eq_single j, basis_on_evenFst_self, basis_on_evenSnd_self]
|
||||
· simp only [mul_one, mul_neg]
|
||||
ring
|
||||
· intro k _ hkj
|
||||
erw [basis_on_δ₁_other hkj.symm, basis_on_δ₂_other hkj.symm]
|
||||
erw [basis_on_evenFst_other hkj.symm, basis_on_evenSnd_other hkj.symm]
|
||||
simp only [mul_zero, add_zero]
|
||||
· simp
|
||||
|
||||
lemma P_zero (f : Fin n.succ → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by
|
||||
intro i
|
||||
erw [← P_δ₁ f]
|
||||
erw [← P_evenFst f]
|
||||
rw [h]
|
||||
rfl
|
||||
|
||||
lemma P!_zero (f : Fin n → ℚ) (h : P! f = 0) : ∀ i, f i = 0 := by
|
||||
intro i
|
||||
rw [← P!_δ!₁ f]
|
||||
rw [← P!_evenShiftFst f]
|
||||
rw [h]
|
||||
rfl
|
||||
|
||||
lemma Pa_zero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) :
|
||||
∀ i, f i = 0 := by
|
||||
have h₃ := Pa_δ!₃ f g
|
||||
have h₃ := Pa_evenShitZero f g
|
||||
rw [h] at h₃
|
||||
change 0 = f 0 at h₃
|
||||
intro i
|
||||
|
|
@ -524,8 +516,8 @@ lemma Pa_zero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) :
|
|||
rename_i iv hi
|
||||
have hivi : iv < n.succ := lt_of_succ_lt hiv
|
||||
have hi2 := hi hivi
|
||||
have h1 := Pa_δ!₁ f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
|
||||
have h2 := Pa_δ!₂ f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
|
||||
have h1 := Pa_evenShiftFst f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
|
||||
have h2 := Pa_evenShiftSnd f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
|
||||
rw [h] at h1 h2
|
||||
simp only [Fin.succ_mk, succ_eq_add_one, Fin.castSucc_mk] at h1 h2
|
||||
erw [hi2] at h2
|
||||
|
|
@ -685,7 +677,7 @@ lemma P!_in_span (f : Fin n → ℚ) : P! f ∈ Submodule.span ℚ (Set.range ba
|
|||
rfl
|
||||
|
||||
lemma smul_basis!AsCharges_in_span (S : (PureU1 (2 * n.succ)).LinSols) (j : Fin n) :
|
||||
(S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∈
|
||||
(S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∈
|
||||
Submodule.span ℚ (Set.range basis!AsCharges) := by
|
||||
apply Submodule.smul_mem
|
||||
apply SetLike.mem_of_subset
|
||||
|
|
@ -694,11 +686,11 @@ lemma smul_basis!AsCharges_in_span (S : (PureU1 (2 * n.succ)).LinSols) (j : Fin
|
|||
|
||||
lemma span_basis_swap! {S : (PureU1 (2 * n.succ)).LinSols} (j : Fin n)
|
||||
(hS : ((FamilyPermutations (2 * n.succ)).linSolRep
|
||||
(pairSwap (δ!₁ j) (δ!₂ j))) S = S') (g : Fin n.succ → ℚ) (f : Fin n → ℚ)
|
||||
(pairSwap (evenShiftFst j) (evenShiftSnd j))) S = S') (g : Fin n.succ → ℚ) (f : Fin n → ℚ)
|
||||
(h : S.val = P g + P! f) : ∃ (g' : Fin n.succ → ℚ) (f' : Fin n → ℚ),
|
||||
S'.val = P g' + P! f' ∧ P! f' = P! f +
|
||||
(S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∧ g' = g := by
|
||||
let X := P! f + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j
|
||||
(S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = g := by
|
||||
let X := P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j
|
||||
have hX : X ∈ Submodule.span ℚ (Set.range (basis!AsCharges)) := by
|
||||
apply Submodule.add_mem
|
||||
exact (P!_in_span f)
|
||||
|
|
@ -721,20 +713,20 @@ lemma vectorLikeEven_in_span (S : (PureU1 (2 * n.succ)).LinSols)
|
|||
use (Tuple.sort S.val).symm
|
||||
change sortAFL S ∈ Submodule.span ℚ (Set.range basis)
|
||||
rw [mem_span_range_iff_exists_fun ℚ]
|
||||
let f : Fin n.succ → ℚ := fun i => (sortAFL S).val (δ₁ i)
|
||||
let f : Fin n.succ → ℚ := fun i => (sortAFL S).val (evenFst i)
|
||||
use f
|
||||
apply ACCSystemLinear.LinSols.ext
|
||||
rw [sortAFL_val]
|
||||
erw [P'_val]
|
||||
apply ext_δ
|
||||
apply ext_even
|
||||
· intro i
|
||||
rw [P_δ₁]
|
||||
rw [P_evenFst]
|
||||
rfl
|
||||
· intro i
|
||||
rw [P_δ₂]
|
||||
rw [P_evenSnd]
|
||||
have ht := hS i
|
||||
change sort S.val (δ₁ i) = - sort S.val (δ₂ i) at ht
|
||||
have h : sort S.val (δ₂ i) = - sort S.val (δ₁ i) := by
|
||||
change sort S.val (evenFst i) = - sort S.val (evenSnd i) at ht
|
||||
have h : sort S.val (evenSnd i) = - sort S.val (evenFst i) := by
|
||||
rw [ht]
|
||||
ring
|
||||
rw [h]
|
||||
|
|
|
|||
|
|
@ -91,15 +91,18 @@ lemma lineInCubicPerm_permute {S : (PureU1 (2 * n.succ)).LinSols}
|
|||
lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ)).LinSols}
|
||||
(LIC : LineInCubicPerm S) :
|
||||
∀ (j : Fin n) (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f),
|
||||
(S.val (δ!₂ j) - S.val (δ!₁ j))
|
||||
(S.val (evenShiftSnd j) - S.val (evenShiftFst j))
|
||||
* accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := by
|
||||
intro j g f h
|
||||
let S' := (FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (δ!₁ j) (δ!₂ j)) S
|
||||
have hSS' : ((FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (δ!₁ j) (δ!₂ j))) S = S' := rfl
|
||||
let S' := (FamilyPermutations (2 * n.succ)).linSolRep
|
||||
(pairSwap (evenShiftFst j) (evenShiftSnd j)) S
|
||||
have hSS' : ((FamilyPermutations (2 * n.succ)).linSolRep
|
||||
(pairSwap (evenShiftFst j) (evenShiftSnd j))) S = S' := rfl
|
||||
obtain ⟨g', f', hall⟩ := span_basis_swap! j hSS' g f h
|
||||
have h1 := line_in_cubic_P_P_P! (lineInCubicPerm_self LIC) g f h
|
||||
have h2 := line_in_cubic_P_P_P!
|
||||
(lineInCubicPerm_self (lineInCubicPerm_permute LIC (pairSwap (δ!₁ j) (δ!₂ j)))) g' f' hall.1
|
||||
(lineInCubicPerm_self (lineInCubicPerm_permute LIC
|
||||
(pairSwap (evenShiftFst j) (evenShiftSnd j)))) g' f' hall.1
|
||||
rw [hall.2.1, hall.2.2] at h2
|
||||
rw [accCubeTriLinSymm.map_add₃, h1, accCubeTriLinSymm.map_smul₃] at h2
|
||||
simpa using h2
|
||||
|
|
@ -107,20 +110,22 @@ lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ)).LinSols}
|
|||
lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ)).LinSols}
|
||||
(f : Fin n.succ.succ → ℚ) (g : Fin n.succ → ℚ) (hS : S.val = Pa f g) :
|
||||
accCubeTriLinSymm (P f) (P f) (basis!AsCharges (Fin.last n)) =
|
||||
- (S.val (δ!₂ (Fin.last n)) + S.val (δ!₁ (Fin.last n))) * (2 * S.val δ!₄ +
|
||||
S.val (δ!₂ (Fin.last n)) + S.val (δ!₁ (Fin.last n))) := by
|
||||
- (S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n))) *
|
||||
(2 * S.val evenShiftLast +
|
||||
S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n))) := by
|
||||
rw [P_P_P!_accCube f (Fin.last n)]
|
||||
have h1 := Pa_δ!₄ f g
|
||||
have h2 := Pa_δ!₁ f g (Fin.last n)
|
||||
have h3 := Pa_δ!₂ f g (Fin.last n)
|
||||
have h1 := Pa_evenShiftLast f g
|
||||
have h2 := Pa_evenShiftFst f g (Fin.last n)
|
||||
have h3 := Pa_evenShiftSnd f g (Fin.last n)
|
||||
simp only [Fin.succ_last, Nat.succ_eq_add_one] at h1 h2 h3
|
||||
have hl : f (Fin.succ (Fin.last n)) = - Pa f g δ!₄ := by
|
||||
have hl : f (Fin.succ (Fin.last n)) = - Pa f g evenShiftLast := by
|
||||
simp_all only [Fin.succ_last, neg_neg]
|
||||
erw [hl] at h2
|
||||
have hg : g (Fin.last n) = Pa f g (δ!₁ (Fin.last n)) + Pa f g δ!₄ := by
|
||||
have hg : g (Fin.last n) = Pa f g (evenShiftFst (Fin.last n)) + Pa f g evenShiftLast := by
|
||||
linear_combination -(1 * h2)
|
||||
have hll : f (Fin.castSucc (Fin.last n)) =
|
||||
- (Pa f g (δ!₂ (Fin.last n)) + Pa f g (δ!₁ (Fin.last n)) + Pa f g δ!₄) := by
|
||||
- (Pa f g (evenShiftSnd (Fin.last n)) + Pa f g (evenShiftFst (Fin.last n))
|
||||
+ Pa f g evenShiftLast) := by
|
||||
linear_combination h3 - 1 * hg
|
||||
rw [← hS] at hl hll
|
||||
rw [hl, hll]
|
||||
|
|
@ -129,7 +134,8 @@ lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ)).LinSols}
|
|||
lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}
|
||||
(LIC : LineInCubicPerm S) :
|
||||
LineInPlaneProp
|
||||
((S.val (δ!₂ (Fin.last n))), ((S.val (δ!₁ (Fin.last n))), (S.val δ!₄))) := by
|
||||
((S.val (evenShiftSnd (Fin.last n))), ((S.val (evenShiftFst (Fin.last n))),
|
||||
(S.val evenShiftLast))) := by
|
||||
obtain ⟨g, f, hfg⟩ := span_basis S
|
||||
have h1 := lineInCubicPerm_swap LIC (Fin.last n) g f hfg
|
||||
rw [P_P_P!_accCube' g f hfg] at h1
|
||||
|
|
@ -144,12 +150,14 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}
|
|||
|
||||
lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ)).LinSols}
|
||||
(LIC : LineInCubicPerm S) : LineInPlaneCond S := by
|
||||
refine @Prop_three (2 * n.succ.succ) LineInPlaneProp S (δ!₂ (Fin.last n)) (δ!₁ (Fin.last n))
|
||||
δ!₄ ?_ ?_ ?_ ?_
|
||||
· simp [Fin.ext_iff, δ!₂, δ!₁]
|
||||
· simp [Fin.ext_iff, δ!₂, δ!₄]
|
||||
· simp only [Nat.succ_eq_add_one, δ!₁, δ!₄, Fin.isValue, ne_eq, Fin.ext_iff, Fin.coe_cast,
|
||||
Fin.coe_natAdd, Fin.coe_castAdd, Fin.val_last, Fin.val_eq_zero, add_zero, add_right_inj]
|
||||
refine @Prop_three (2 * n.succ.succ) LineInPlaneProp S
|
||||
(evenShiftSnd (Fin.last n)) (evenShiftFst (Fin.last n))
|
||||
evenShiftLast ?_ ?_ ?_ ?_
|
||||
· simp [Fin.ext_iff, evenShiftSnd, evenShiftFst]
|
||||
· simp [Fin.ext_iff, evenShiftSnd, evenShiftLast]
|
||||
· simp only [Nat.succ_eq_add_one, evenShiftFst, evenShiftLast, Fin.isValue, ne_eq, Fin.ext_iff,
|
||||
Fin.coe_cast, Fin.coe_natAdd, Fin.coe_castAdd, Fin.val_last, Fin.val_eq_zero, add_zero,
|
||||
add_right_inj]
|
||||
omega
|
||||
· exact fun M => lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M)
|
||||
|
||||
|
|
|
|||
|
|
@ -25,22 +25,22 @@ variable {n : ℕ}
|
|||
|
||||
namespace VectorLikeOddPlane
|
||||
|
||||
lemma split_odd! (n : ℕ) : (1 + n) + n = 2 * n +1 := by
|
||||
lemma odd_shift_eq (n : ℕ) : (1 + n) + n = 2 * n +1 := by
|
||||
omega
|
||||
|
||||
lemma split_adda (n : ℕ) : ((1+n)+1) + n.succ = 2 * n.succ + 1 := by
|
||||
lemma odd_shift_shift_eq (n : ℕ) : ((1+n)+1) + n.succ = 2 * n.succ + 1 := by
|
||||
omega
|
||||
|
||||
section theDeltas
|
||||
|
||||
/-- The inclusion of `Fin n` into `Fin ((n + 1) + n)` via the first `n`.
|
||||
This is then casted to `Fin (2 * n + 1)`. -/
|
||||
def oddFstEmbed (j : Fin n) : Fin (2 * n + 1) :=
|
||||
def oddFst (j : Fin n) : Fin (2 * n + 1) :=
|
||||
Fin.cast (split_odd n) (Fin.castAdd n (Fin.castAdd 1 j))
|
||||
|
||||
/-- The inclusion of `Fin n` into `Fin ((n + 1) + n)` via the second `n`.
|
||||
This is then casted to `Fin (2 * n + 1)`. -/
|
||||
def oddSndEmbed (j : Fin n) : Fin (2 * n + 1) :=
|
||||
def oddSnd (j : Fin n) : Fin (2 * n + 1) :=
|
||||
Fin.cast (split_odd n) (Fin.natAdd (n+1) j)
|
||||
|
||||
/-- The element representing `1` in `Fin ((n + 1) + n)`.
|
||||
|
|
@ -50,76 +50,80 @@ def oddMid : Fin (2 * n + 1) :=
|
|||
|
||||
/-- The inclusion of `Fin n` into `Fin (1 + n + n)` via the first `n`.
|
||||
This is then casted to `Fin (2 * n + 1)`. -/
|
||||
def oddShiftFstEmbed (j : Fin n) : Fin (2 * n + 1) :=
|
||||
Fin.cast (split_odd! n) (Fin.castAdd n (Fin.natAdd 1 j))
|
||||
def oddShiftFst (j : Fin n) : Fin (2 * n + 1) :=
|
||||
Fin.cast (odd_shift_eq n) (Fin.castAdd n (Fin.natAdd 1 j))
|
||||
|
||||
/-- The inclusion of `Fin n` into `Fin (1 + n + n)` via the second `n`.
|
||||
This is then casted to `Fin (2 * n + 1)`. -/
|
||||
def oddShiftSndEmbed (j : Fin n) : Fin (2 * n + 1) :=
|
||||
Fin.cast (split_odd! n) (Fin.natAdd (1 + n) j)
|
||||
def oddShiftSnd (j : Fin n) : Fin (2 * n + 1) :=
|
||||
Fin.cast (odd_shift_eq n) (Fin.natAdd (1 + n) j)
|
||||
|
||||
/-- The element representing the `1` in `Fin (1 + n + n)`.
|
||||
This is then casted to `Fin (2 * n + 1)`. -/
|
||||
def oddShiftZero : Fin (2 * n + 1) :=
|
||||
Fin.cast (split_odd! n) (Fin.castAdd n (Fin.castAdd n 1))
|
||||
Fin.cast (odd_shift_eq n) (Fin.castAdd n (Fin.castAdd n 1))
|
||||
|
||||
/-- The element representing the first `1` in `Fin (1 + n + 1 + n.succ)` casted
|
||||
to `Fin (2 * n.succ + 1)`. -/
|
||||
def δa₁ : Fin (2 * n.succ + 1) :=
|
||||
Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.castAdd n 1)))
|
||||
def oddShiftShiftZero : Fin (2 * n.succ + 1) :=
|
||||
Fin.cast (odd_shift_shift_eq n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.castAdd n 1)))
|
||||
|
||||
/-- The inclusion of `Fin n` into `Fin (1 + n + 1 + n.succ)` via the first `n` and casted
|
||||
to `Fin (2 * n.succ + 1)`. -/
|
||||
def δa₂ (j : Fin n) : Fin (2 * n.succ + 1) :=
|
||||
Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.natAdd 1 j)))
|
||||
def oddShiftShiftFst (j : Fin n) : Fin (2 * n.succ + 1) :=
|
||||
Fin.cast (odd_shift_shift_eq n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.natAdd 1 j)))
|
||||
|
||||
/-- The element representing the second `1` in `Fin (1 + n + 1 + n.succ)` casted
|
||||
to `2 * n.succ + 1`. -/
|
||||
def δa₃ : Fin (2 * n.succ + 1) :=
|
||||
Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.natAdd (1+n) 1))
|
||||
def oddShiftShiftMid : Fin (2 * n.succ + 1) :=
|
||||
Fin.cast (odd_shift_shift_eq n) (Fin.castAdd n.succ (Fin.natAdd (1+n) 1))
|
||||
|
||||
/-- The inclusion of `Fin n.succ` into `Fin (1 + n + 1 + n.succ)` via the `n.succ` and casted
|
||||
to `Fin (2 * n.succ + 1)`. -/
|
||||
def δa₄ (j : Fin n.succ) : Fin (2 * n.succ + 1) :=
|
||||
Fin.cast (split_adda n) (Fin.natAdd ((1+n)+1) j)
|
||||
def oddShiftShiftSnd (j : Fin n.succ) : Fin (2 * n.succ + 1) :=
|
||||
Fin.cast (odd_shift_shift_eq n) (Fin.natAdd ((1+n)+1) j)
|
||||
|
||||
lemma δa₁_δ₁ : @δa₁ n = oddFstEmbed 0 := Fin.rev_inj.mp rfl
|
||||
lemma oddShiftShiftZero_eq_oddFst_zero : @oddShiftShiftZero n = oddFst 0 :=
|
||||
Fin.rev_inj.mp rfl
|
||||
|
||||
lemma δa₁_δ!₃ : @δa₁ n = oddShiftZero := rfl
|
||||
lemma oddShiftShiftZero_eq_oddShiftZero : @oddShiftShiftZero n = oddShiftZero := rfl
|
||||
|
||||
lemma δa₂_δ₁ (j : Fin n) : δa₂ j = oddFstEmbed j.succ := by
|
||||
lemma oddShiftShiftFst_eq_oddFst_succ (j : Fin n) :
|
||||
oddShiftShiftFst j = oddFst j.succ := by
|
||||
rw [Fin.ext_iff]
|
||||
simp only [succ_eq_add_one, δa₂, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd, oddFstEmbed, Fin.val_succ]
|
||||
simp only [succ_eq_add_one, oddShiftShiftFst, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd,
|
||||
oddFst, Fin.val_succ]
|
||||
exact Nat.add_comm 1 ↑j
|
||||
|
||||
lemma δa₂_δ!₁ (j : Fin n) : δa₂ j = oddShiftFstEmbed j.castSucc := by
|
||||
lemma oddShiftShiftFst_eq_oddShiftFst_castSucc (j : Fin n) :
|
||||
oddShiftShiftFst j = oddShiftFst j.castSucc := by
|
||||
rfl
|
||||
|
||||
lemma δa₃_δ₃ : @δa₃ n = oddMid := by
|
||||
lemma oddShiftShiftMid_eq_oddMid : @oddShiftShiftMid n = oddMid := by
|
||||
rw [Fin.ext_iff]
|
||||
simp only [succ_eq_add_one, δa₃, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd,
|
||||
Fin.val_eq_zero, add_zero, oddMid]
|
||||
simp only [succ_eq_add_one, oddShiftShiftMid, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd,
|
||||
Fin.coe_natAdd, Fin.val_eq_zero, add_zero, oddMid]
|
||||
exact Nat.add_comm 1 n
|
||||
|
||||
lemma δa₃_δ!₁ : δa₃ = oddShiftFstEmbed (Fin.last n) := by
|
||||
lemma oddShiftShiftMid_eq_oddShiftFst_last : oddShiftShiftMid = oddShiftFst (Fin.last n) := by
|
||||
rfl
|
||||
|
||||
lemma δa₄_δ₂ (j : Fin n.succ) : δa₄ j = oddSndEmbed j := by
|
||||
lemma oddShiftShiftSnd_eq_oddSnd (j : Fin n.succ) : oddShiftShiftSnd j = oddSnd j := by
|
||||
rw [Fin.ext_iff]
|
||||
simp only [succ_eq_add_one, δa₄, Fin.coe_cast, Fin.coe_natAdd, oddSndEmbed, add_left_inj]
|
||||
simp only [succ_eq_add_one, oddShiftShiftSnd, Fin.coe_cast, Fin.coe_natAdd, oddSnd, add_left_inj]
|
||||
exact Nat.add_comm 1 n
|
||||
|
||||
lemma δa₄_δ!₂ (j : Fin n.succ) : δa₄ j = oddShiftSndEmbed j := by
|
||||
lemma oddShiftShiftSnd_eq_oddShiftSnd (j : Fin n.succ) : oddShiftShiftSnd j = oddShiftSnd j := by
|
||||
rw [Fin.ext_iff]
|
||||
rfl
|
||||
|
||||
lemma δ₂_δ!₂ (j : Fin n) : oddSndEmbed j = oddShiftSndEmbed j := by
|
||||
lemma oddSnd_eq_oddShiftSnd (j : Fin n) : oddSnd j = oddShiftSnd j := by
|
||||
rw [Fin.ext_iff]
|
||||
simp only [oddSndEmbed, Fin.coe_cast, Fin.coe_natAdd, oddShiftSndEmbed, add_left_inj]
|
||||
simp only [oddSnd, Fin.coe_cast, Fin.coe_natAdd, oddShiftSnd, add_left_inj]
|
||||
exact Nat.add_comm n 1
|
||||
|
||||
lemma sum_δ (S : Fin (2 * n + 1) → ℚ) :
|
||||
∑ i, S i = S oddMid + ∑ i : Fin n, ((S ∘ oddFstEmbed) i + (S ∘ oddSndEmbed) i) := by
|
||||
lemma sum_odd (S : Fin (2 * n + 1) → ℚ) :
|
||||
∑ i, S i = S oddMid + ∑ i : Fin n, ((S ∘ oddFst) i + (S ∘ oddSnd) i) := by
|
||||
have h1 : ∑ i, S i = ∑ i : Fin (n + 1 + n), S (Fin.cast (split_odd n) i) := by
|
||||
rw [Finset.sum_equiv (Fin.castOrderIso (split_odd n)).symm.toEquiv]
|
||||
· intro i
|
||||
|
|
@ -133,10 +137,10 @@ lemma sum_δ (S : Fin (2 * n + 1) → ℚ) :
|
|||
rw [Finset.sum_add_distrib]
|
||||
rfl
|
||||
|
||||
lemma sum_δ! (S : Fin (2 * n + 1) → ℚ) :
|
||||
∑ i, S i = S oddShiftZero + ∑ i : Fin n, ((S ∘ oddShiftFstEmbed) i + (S ∘ oddShiftSndEmbed) i) := by
|
||||
have h1 : ∑ i, S i = ∑ i : Fin ((1+n)+n), S (Fin.cast (split_odd! n) i) := by
|
||||
rw [Finset.sum_equiv (Fin.castOrderIso (split_odd! n)).symm.toEquiv]
|
||||
lemma sum_oddShift (S : Fin (2 * n + 1) → ℚ) :
|
||||
∑ i, S i = S oddShiftZero + ∑ i : Fin n, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i) := by
|
||||
have h1 : ∑ i, S i = ∑ i : Fin ((1+n)+n), S (Fin.cast (odd_shift_eq n) i) := by
|
||||
rw [Finset.sum_equiv (Fin.castOrderIso (odd_shift_eq n)).symm.toEquiv]
|
||||
· intro i
|
||||
simp only [mem_univ, Fin.castOrderIso, RelIso.coe_fn_toEquiv]
|
||||
· exact fun _ _ => rfl
|
||||
|
|
@ -152,10 +156,10 @@ section theBasisVectors
|
|||
/-- The first part of the basis as charge assignments. -/
|
||||
def basisAsCharges (j : Fin n) : (PureU1 (2 * n + 1)).Charges :=
|
||||
fun i =>
|
||||
if i = oddFstEmbed j then
|
||||
if i = oddFst j then
|
||||
1
|
||||
else
|
||||
if i = oddSndEmbed j then
|
||||
if i = oddSnd j then
|
||||
- 1
|
||||
else
|
||||
0
|
||||
|
|
@ -163,24 +167,24 @@ def basisAsCharges (j : Fin n) : (PureU1 (2 * n + 1)).Charges :=
|
|||
/-- The second part of the basis as charge assignments. -/
|
||||
def basis!AsCharges (j : Fin n) : (PureU1 (2 * n + 1)).Charges :=
|
||||
fun i =>
|
||||
if i = oddShiftFstEmbed j then
|
||||
if i = oddShiftFst j then
|
||||
1
|
||||
else
|
||||
if i = oddShiftSndEmbed j then
|
||||
if i = oddShiftSnd j then
|
||||
- 1
|
||||
else
|
||||
0
|
||||
|
||||
lemma basis_on_δ₁_self (j : Fin n) : basisAsCharges j (oddFstEmbed j) = 1 := by
|
||||
lemma basis_on_oddFst_self (j : Fin n) : basisAsCharges j (oddFst j) = 1 := by
|
||||
simp [basisAsCharges]
|
||||
|
||||
lemma basis!_on_δ!₁_self (j : Fin n) : basis!AsCharges j (oddShiftFstEmbed j) = 1 := by
|
||||
lemma basis!_on_oddShiftFst_self (j : Fin n) : basis!AsCharges j (oddShiftFst j) = 1 := by
|
||||
simp [basis!AsCharges]
|
||||
|
||||
lemma basis_on_δ₁_other {k j : Fin n} (h : k ≠ j) :
|
||||
basisAsCharges k (oddFstEmbed j) = 0 := by
|
||||
lemma basis_on_oddFst_other {k j : Fin n} (h : k ≠ j) :
|
||||
basisAsCharges k (oddFst j) = 0 := by
|
||||
simp only [basisAsCharges, PureU1_numberCharges]
|
||||
simp only [oddFstEmbed, oddSndEmbed]
|
||||
simp only [oddFst, oddSnd]
|
||||
split
|
||||
· rename_i h1
|
||||
rw [Fin.ext_iff] at h1
|
||||
|
|
@ -195,10 +199,10 @@ lemma basis_on_δ₁_other {k j : Fin n} (h : k ≠ j) :
|
|||
omega
|
||||
· rfl
|
||||
|
||||
lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
|
||||
basis!AsCharges k (oddShiftFstEmbed j) = 0 := by
|
||||
lemma basis!_on_oddShiftFst_other {k j : Fin n} (h : k ≠ j) :
|
||||
basis!AsCharges k (oddShiftFst j) = 0 := by
|
||||
simp only [basis!AsCharges, PureU1_numberCharges]
|
||||
simp only [oddShiftFstEmbed, oddShiftSndEmbed]
|
||||
simp only [oddShiftFst, oddShiftSnd]
|
||||
split
|
||||
· rename_i h1
|
||||
rw [Fin.ext_iff] at h1
|
||||
|
|
@ -213,19 +217,20 @@ lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
|
|||
omega
|
||||
rfl
|
||||
|
||||
lemma basis_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ oddFstEmbed k) (h2 : j ≠ oddSndEmbed k) :
|
||||
lemma basis_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ oddFst k) (h2 : j ≠ oddSnd k) :
|
||||
basisAsCharges k j = 0 := by
|
||||
simp only [basisAsCharges, PureU1_numberCharges]
|
||||
simp_all only [ne_eq, ↓reduceIte]
|
||||
|
||||
lemma basis!_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ oddShiftFstEmbed k) (h2 : j ≠ oddShiftSndEmbed k) :
|
||||
lemma basis!_on_other {k : Fin n} {j : Fin (2 * n + 1)}
|
||||
(h1 : j ≠ oddShiftFst k) (h2 : j ≠ oddShiftSnd k) :
|
||||
basis!AsCharges k j = 0 := by
|
||||
simp only [basis!AsCharges, PureU1_numberCharges]
|
||||
simp_all only [ne_eq, ↓reduceIte]
|
||||
|
||||
lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n) :
|
||||
basisAsCharges j (oddSndEmbed i) = - basisAsCharges j (oddFstEmbed i) := by
|
||||
simp only [basisAsCharges, PureU1_numberCharges, oddSndEmbed, oddFstEmbed]
|
||||
lemma basis_oddSnd_eq_minus_oddFst (j i : Fin n) :
|
||||
basisAsCharges j (oddSnd i) = - basisAsCharges j (oddFst i) := by
|
||||
simp only [basisAsCharges, PureU1_numberCharges, oddSnd, oddFst]
|
||||
split <;> split
|
||||
any_goals split
|
||||
any_goals split
|
||||
|
|
@ -238,9 +243,9 @@ lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n) :
|
|||
all_goals simp_all
|
||||
all_goals omega
|
||||
|
||||
lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
|
||||
basis!AsCharges j (oddShiftSndEmbed i) = - basis!AsCharges j (oddShiftFstEmbed i) := by
|
||||
simp only [basis!AsCharges, PureU1_numberCharges, oddShiftSndEmbed, oddShiftFstEmbed]
|
||||
lemma basis!_oddShiftSnd_eq_minus_oddShiftFst (j i : Fin n) :
|
||||
basis!AsCharges j (oddShiftSnd i) = - basis!AsCharges j (oddShiftFst i) := by
|
||||
simp only [basis!AsCharges, PureU1_numberCharges, oddShiftSnd, oddShiftFst]
|
||||
split <;> split
|
||||
any_goals split
|
||||
any_goals split
|
||||
|
|
@ -255,59 +260,60 @@ lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
|
|||
all_goals simp_all
|
||||
all_goals omega
|
||||
|
||||
lemma basis_on_δ₂_self (j : Fin n) : basisAsCharges j (oddSndEmbed j) = - 1 := by
|
||||
rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_self]
|
||||
lemma basis_on_oddSnd_self (j : Fin n) : basisAsCharges j (oddSnd j) = - 1 := by
|
||||
rw [basis_oddSnd_eq_minus_oddFst, basis_on_oddFst_self]
|
||||
|
||||
lemma basis!_on_δ!₂_self (j : Fin n) : basis!AsCharges j (oddShiftSndEmbed j) = - 1 := by
|
||||
rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_self]
|
||||
lemma basis!_on_oddShiftSnd_self (j : Fin n) : basis!AsCharges j (oddShiftSnd j) = - 1 := by
|
||||
rw [basis!_oddShiftSnd_eq_minus_oddShiftFst, basis!_on_oddShiftFst_self]
|
||||
|
||||
lemma basis_on_δ₂_other {k j : Fin n} (h : k ≠ j) : basisAsCharges k (oddSndEmbed j) = 0 := by
|
||||
rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_other h]
|
||||
lemma basis_on_oddSnd_other {k j : Fin n} (h : k ≠ j) : basisAsCharges k (oddSnd j) = 0 := by
|
||||
rw [basis_oddSnd_eq_minus_oddFst, basis_on_oddFst_other h]
|
||||
rfl
|
||||
|
||||
lemma basis!_on_δ!₂_other {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (oddShiftSndEmbed j) = 0 := by
|
||||
rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_other h]
|
||||
lemma basis!_on_oddShiftSnd_other {k j : Fin n} (h : k ≠ j) :
|
||||
basis!AsCharges k (oddShiftSnd j) = 0 := by
|
||||
rw [basis!_oddShiftSnd_eq_minus_oddShiftFst, basis!_on_oddShiftFst_other h]
|
||||
rfl
|
||||
|
||||
lemma basis_on_δ₃ (j : Fin n) : basisAsCharges j oddMid = 0 := by
|
||||
lemma basis_on_oddMid (j : Fin n) : basisAsCharges j oddMid = 0 := by
|
||||
simp only [basisAsCharges, PureU1_numberCharges]
|
||||
split <;> rename_i h
|
||||
· rw [Fin.ext_iff] at h
|
||||
simp only [oddMid, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd, Fin.val_eq_zero,
|
||||
add_zero, oddFstEmbed] at h
|
||||
add_zero, oddFst] at h
|
||||
omega
|
||||
· split <;> rename_i h2
|
||||
· rw [Fin.ext_iff] at h2
|
||||
simp only [oddMid, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd, Fin.val_eq_zero,
|
||||
add_zero, oddSndEmbed] at h2
|
||||
simp only [oddMid, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd,
|
||||
Fin.val_eq_zero, add_zero, oddSnd] at h2
|
||||
omega
|
||||
· rfl
|
||||
|
||||
lemma basis!_on_δ!₃ (j : Fin n) : basis!AsCharges j oddShiftZero = 0 := by
|
||||
lemma basis!_on_oddShiftZero (j : Fin n) : basis!AsCharges j oddShiftZero = 0 := by
|
||||
simp only [basis!AsCharges, PureU1_numberCharges]
|
||||
split <;> rename_i h
|
||||
· rw [Fin.ext_iff] at h
|
||||
simp only [oddShiftZero, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.val_eq_zero, oddShiftFstEmbed,
|
||||
Fin.coe_natAdd] at h
|
||||
simp only [oddShiftZero, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.val_eq_zero,
|
||||
oddShiftFst, Fin.coe_natAdd] at h
|
||||
omega
|
||||
· split <;> rename_i h2
|
||||
· rw [Fin.ext_iff] at h2
|
||||
simp only [oddShiftZero, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.val_eq_zero, oddShiftSndEmbed,
|
||||
Fin.coe_natAdd] at h2
|
||||
simp only [oddShiftZero, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.val_eq_zero,
|
||||
oddShiftSnd, Fin.coe_natAdd] at h2
|
||||
omega
|
||||
· rfl
|
||||
|
||||
lemma basis_linearACC (j : Fin n) : (accGrav (2 * n + 1)) (basisAsCharges j) = 0 := by
|
||||
rw [accGrav]
|
||||
simp only [LinearMap.coe_mk, AddHom.coe_mk]
|
||||
erw [sum_δ]
|
||||
simp [basis_δ₂_eq_minus_δ₁, basis_on_δ₃]
|
||||
erw [sum_odd]
|
||||
simp [basis_oddSnd_eq_minus_oddFst, basis_on_oddMid]
|
||||
|
||||
lemma basis!_linearACC (j : Fin n) : (accGrav (2 * n + 1)) (basis!AsCharges j) = 0 := by
|
||||
rw [accGrav]
|
||||
simp only [LinearMap.coe_mk, AddHom.coe_mk]
|
||||
rw [sum_δ!, basis!_on_δ!₃]
|
||||
simp [basis!_δ!₂_eq_minus_δ!₁]
|
||||
rw [sum_oddShift, basis!_on_oddShiftZero]
|
||||
simp [basis!_oddShiftSnd_eq_minus_oddShiftFst]
|
||||
|
||||
/-- The first part of the basis as `LinSols`. -/
|
||||
@[simps!]
|
||||
|
|
@ -337,23 +343,24 @@ def basisa : Fin n ⊕ Fin n → (PureU1 (2 * n + 1)).LinSols := fun i =>
|
|||
|
||||
end theBasisVectors
|
||||
|
||||
/-- Swapping the elements δ!₁ j and δ!₂ j is equivalent to adding a vector basis!AsCharges j. -/
|
||||
/-- Swapping the elements oddShiftFst j and oddShiftSnd j is equivalent to adding a vector
|
||||
basis!AsCharges j. -/
|
||||
lemma swap!_as_add {S S' : (PureU1 (2 * n + 1)).LinSols} (j : Fin n)
|
||||
(hS : ((FamilyPermutations (2 * n + 1)).linSolRep
|
||||
(pairSwap (oddShiftFstEmbed j) (oddShiftSndEmbed j))) S = S') :
|
||||
S'.val = S.val + (S.val (oddShiftSndEmbed j) - S.val (oddShiftFstEmbed j)) • basis!AsCharges j := by
|
||||
(pairSwap (oddShiftFst j) (oddShiftSnd j))) S = S') :
|
||||
S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j := by
|
||||
funext i
|
||||
rw [← hS, FamilyPermutations_anomalyFreeLinear_apply]
|
||||
by_cases hi : i = oddShiftFstEmbed j
|
||||
by_cases hi : i = oddShiftFst j
|
||||
· subst hi
|
||||
simp [HSMul.hSMul, basis!_on_δ!₁_self, pairSwap_inv_fst]
|
||||
· by_cases hi2 : i = oddShiftSndEmbed j
|
||||
simp [HSMul.hSMul, basis!_on_oddShiftFst_self, pairSwap_inv_fst]
|
||||
· by_cases hi2 : i = oddShiftSnd j
|
||||
· subst hi2
|
||||
simp [HSMul.hSMul,basis!_on_δ!₂_self, pairSwap_inv_snd]
|
||||
simp [HSMul.hSMul,basis!_on_oddShiftSnd_self, pairSwap_inv_snd]
|
||||
· simp only [Equiv.invFun_as_coe, HSMul.hSMul, ACCSystemCharges.chargesAddCommMonoid_add,
|
||||
ACCSystemCharges.chargesModule_smul]
|
||||
rw [basis!_on_other hi hi2]
|
||||
change S.val ((pairSwap (oddShiftFstEmbed j) (oddShiftSndEmbed j)).invFun i) =_
|
||||
change S.val ((pairSwap (oddShiftFst j) (oddShiftSnd j)).invFun i) =_
|
||||
erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)]
|
||||
simp
|
||||
|
||||
|
|
@ -366,146 +373,148 @@ def P! (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := ∑ i, f i • basi
|
|||
/-- A point in the span of the basis as a charge. -/
|
||||
def Pa (f : Fin n → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := P f + P! g
|
||||
|
||||
lemma P_δ₁ (f : Fin n → ℚ) (j : Fin n) : P f (oddFstEmbed j) = f j := by
|
||||
lemma P_oddFst (f : Fin n → ℚ) (j : Fin n) : P f (oddFst j) = f j := by
|
||||
rw [P, sum_of_charges]
|
||||
simp only [HSMul.hSMul, SMul.smul]
|
||||
rw [Finset.sum_eq_single j]
|
||||
· rw [basis_on_δ₁_self]
|
||||
· rw [basis_on_oddFst_self]
|
||||
exact Rat.mul_one (f j)
|
||||
· intro k _ hkj
|
||||
rw [basis_on_δ₁_other hkj]
|
||||
rw [basis_on_oddFst_other hkj]
|
||||
exact Rat.mul_zero (f k)
|
||||
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
|
||||
|
||||
lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (oddShiftFstEmbed j) = f j := by
|
||||
lemma P!_oddShiftFst (f : Fin n → ℚ) (j : Fin n) : P! f (oddShiftFst j) = f j := by
|
||||
rw [P!, sum_of_charges]
|
||||
simp only [HSMul.hSMul, SMul.smul]
|
||||
rw [Finset.sum_eq_single j]
|
||||
· rw [basis!_on_δ!₁_self]
|
||||
· rw [basis!_on_oddShiftFst_self]
|
||||
exact Rat.mul_one (f j)
|
||||
· intro k _ hkj
|
||||
rw [basis!_on_δ!₁_other hkj]
|
||||
rw [basis!_on_oddShiftFst_other hkj]
|
||||
exact Rat.mul_zero (f k)
|
||||
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
|
||||
|
||||
lemma P_δ₂ (f : Fin n → ℚ) (j : Fin n) : P f (oddSndEmbed j) = - f j := by
|
||||
lemma P_oddSnd (f : Fin n → ℚ) (j : Fin n) : P f (oddSnd j) = - f j := by
|
||||
rw [P, sum_of_charges]
|
||||
simp only [HSMul.hSMul, SMul.smul]
|
||||
rw [Finset.sum_eq_single j]
|
||||
· rw [basis_on_δ₂_self]
|
||||
· rw [basis_on_oddSnd_self]
|
||||
exact mul_neg_one (f j)
|
||||
· intro k _ hkj
|
||||
rw [basis_on_δ₂_other hkj]
|
||||
rw [basis_on_oddSnd_other hkj]
|
||||
exact Rat.mul_zero (f k)
|
||||
· simp
|
||||
|
||||
lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (oddShiftSndEmbed j) = - f j := by
|
||||
lemma P!_oddShiftSnd (f : Fin n → ℚ) (j : Fin n) : P! f (oddShiftSnd j) = - f j := by
|
||||
rw [P!, sum_of_charges]
|
||||
simp only [HSMul.hSMul, SMul.smul]
|
||||
rw [Finset.sum_eq_single j]
|
||||
· rw [basis!_on_δ!₂_self]
|
||||
· rw [basis!_on_oddShiftSnd_self]
|
||||
exact mul_neg_one (f j)
|
||||
· intro k _ hkj
|
||||
rw [basis!_on_δ!₂_other hkj]
|
||||
rw [basis!_on_oddShiftSnd_other hkj]
|
||||
exact Rat.mul_zero (f k)
|
||||
· simp
|
||||
|
||||
lemma P_δ₃ (f : Fin n → ℚ) : P f (oddMid) = 0 := by
|
||||
lemma P_oddMid (f : Fin n → ℚ) : P f (oddMid) = 0 := by
|
||||
rw [P, sum_of_charges]
|
||||
simp [HSMul.hSMul, SMul.smul, basis_on_δ₃]
|
||||
simp [HSMul.hSMul, SMul.smul, basis_on_oddMid]
|
||||
|
||||
lemma P!_δ!₃ (f : Fin n → ℚ) : P! f (oddShiftZero) = 0 := by
|
||||
lemma P!_oddShiftZero (f : Fin n → ℚ) : P! f (oddShiftZero) = 0 := by
|
||||
rw [P!, sum_of_charges]
|
||||
simp [HSMul.hSMul, SMul.smul, basis!_on_δ!₃]
|
||||
simp [HSMul.hSMul, SMul.smul, basis!_on_oddShiftZero]
|
||||
|
||||
lemma Pa_δa₁ (f g : Fin n.succ → ℚ) : Pa f g δa₁ = f 0 := by
|
||||
lemma Pa_oddShiftShiftZero (f g : Fin n.succ → ℚ) : Pa f g oddShiftShiftZero = f 0 := by
|
||||
rw [Pa]
|
||||
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
|
||||
nth_rewrite 1 [δa₁_δ₁]
|
||||
rw [δa₁_δ!₃]
|
||||
rw [P_δ₁, P!_δ!₃]
|
||||
nth_rewrite 1 [oddShiftShiftZero_eq_oddFst_zero]
|
||||
rw [oddShiftShiftZero_eq_oddShiftZero]
|
||||
rw [P_oddFst, P!_oddShiftZero]
|
||||
exact Rat.add_zero (f 0)
|
||||
|
||||
lemma Pa_δa₂ (f g : Fin n.succ → ℚ) (j : Fin n) : Pa f g (δa₂ j) = f j.succ + g j.castSucc := by
|
||||
lemma Pa_oddShiftShiftFst (f g : Fin n.succ → ℚ) (j : Fin n) :
|
||||
Pa f g (oddShiftShiftFst j) = f j.succ + g j.castSucc := by
|
||||
rw [Pa]
|
||||
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
|
||||
nth_rewrite 1 [δa₂_δ₁]
|
||||
rw [δa₂_δ!₁]
|
||||
rw [P_δ₁, P!_δ!₁]
|
||||
nth_rewrite 1 [oddShiftShiftFst_eq_oddFst_succ]
|
||||
rw [oddShiftShiftFst_eq_oddShiftFst_castSucc]
|
||||
rw [P_oddFst, P!_oddShiftFst]
|
||||
|
||||
lemma Pa_δa₃ (f g : Fin n.succ → ℚ) : Pa f g (δa₃) = g (Fin.last n) := by
|
||||
lemma Pa_oddShiftShiftMid (f g : Fin n.succ → ℚ) : Pa f g (oddShiftShiftMid) = g (Fin.last n) := by
|
||||
rw [Pa]
|
||||
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
|
||||
nth_rewrite 1 [δa₃_δ₃]
|
||||
rw [δa₃_δ!₁]
|
||||
rw [P_δ₃, P!_δ!₁]
|
||||
nth_rewrite 1 [oddShiftShiftMid_eq_oddMid]
|
||||
rw [oddShiftShiftMid_eq_oddShiftFst_last]
|
||||
rw [P_oddMid, P!_oddShiftFst]
|
||||
exact Rat.zero_add (g (Fin.last n))
|
||||
|
||||
lemma Pa_δa₄ (f g : Fin n.succ → ℚ) (j : Fin n.succ) : Pa f g (δa₄ j) = - f j - g j := by
|
||||
lemma Pa_oddShiftShiftSnd (f g : Fin n.succ → ℚ) (j : Fin n.succ) :
|
||||
Pa f g (oddShiftShiftSnd j) = - f j - g j := by
|
||||
rw [Pa]
|
||||
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
|
||||
nth_rewrite 1 [δa₄_δ₂]
|
||||
rw [δa₄_δ!₂]
|
||||
rw [P_δ₂, P!_δ!₂]
|
||||
nth_rewrite 1 [oddShiftShiftSnd_eq_oddSnd]
|
||||
rw [oddShiftShiftSnd_eq_oddShiftSnd]
|
||||
rw [P_oddSnd, P!_oddShiftSnd]
|
||||
ring
|
||||
|
||||
lemma P_linearACC (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (P f) = 0 := by
|
||||
rw [accGrav]
|
||||
simp only [LinearMap.coe_mk, AddHom.coe_mk]
|
||||
rw [sum_δ]
|
||||
simp [P_δ₂, P_δ₁, P_δ₃]
|
||||
rw [sum_odd]
|
||||
simp [P_oddSnd, P_oddFst, P_oddMid]
|
||||
|
||||
lemma P!_linearACC (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (P! f) = 0 := by
|
||||
rw [accGrav]
|
||||
simp only [LinearMap.coe_mk, AddHom.coe_mk]
|
||||
rw [sum_δ!]
|
||||
simp [P!_δ!₂, P!_δ!₁, P!_δ!₃]
|
||||
rw [sum_oddShift]
|
||||
simp [P!_oddShiftSnd, P!_oddShiftFst, P!_oddShiftZero]
|
||||
|
||||
lemma P_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P f) = 0 := by
|
||||
rw [accCube_explicit, sum_δ, P_δ₃]
|
||||
rw [accCube_explicit, sum_odd, P_oddMid]
|
||||
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, Function.comp_apply, zero_add]
|
||||
apply Finset.sum_eq_zero
|
||||
intro i _
|
||||
simp only [P_δ₁, P_δ₂]
|
||||
simp only [P_oddFst, P_oddSnd]
|
||||
ring
|
||||
|
||||
lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P! f) = 0 := by
|
||||
rw [accCube_explicit, sum_δ!, P!_δ!₃]
|
||||
rw [accCube_explicit, sum_oddShift, P!_oddShiftZero]
|
||||
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, Function.comp_apply, zero_add]
|
||||
apply Finset.sum_eq_zero
|
||||
intro i _
|
||||
simp only [P!_δ!₁, P!_δ!₂]
|
||||
simp only [P!_oddShiftFst, P!_oddShiftSnd]
|
||||
ring
|
||||
|
||||
lemma P_P_P!_accCube (g : Fin n → ℚ) (j : Fin n) :
|
||||
accCubeTriLinSymm (P g) (P g) (basis!AsCharges j)
|
||||
= (P g (oddShiftFstEmbed j))^2 - (g j)^2 := by
|
||||
= (P g (oddShiftFst j))^2 - (g j)^2 := by
|
||||
simp only [accCubeTriLinSymm, PureU1Charges_numberCharges, TriLinearSymm.mk₃_toFun_apply_apply]
|
||||
rw [sum_δ!, basis!_on_δ!₃]
|
||||
rw [sum_oddShift, basis!_on_oddShiftZero]
|
||||
simp only [mul_zero, Function.comp_apply, zero_add]
|
||||
rw [Finset.sum_eq_single j, basis!_on_δ!₁_self, basis!_on_δ!₂_self]
|
||||
· rw [← δ₂_δ!₂, P_δ₂]
|
||||
rw [Finset.sum_eq_single j, basis!_on_oddShiftFst_self, basis!_on_oddShiftSnd_self]
|
||||
· rw [← oddSnd_eq_oddShiftSnd, P_oddSnd]
|
||||
ring
|
||||
· intro k _ hkj
|
||||
erw [basis!_on_δ!₁_other hkj.symm, basis!_on_δ!₂_other hkj.symm]
|
||||
erw [basis!_on_oddShiftFst_other hkj.symm, basis!_on_oddShiftSnd_other hkj.symm]
|
||||
simp only [mul_zero, add_zero]
|
||||
· simp
|
||||
|
||||
lemma P_zero (f : Fin n → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by
|
||||
intro i
|
||||
erw [← P_δ₁ f]
|
||||
erw [← P_oddFst f]
|
||||
rw [h]
|
||||
rfl
|
||||
|
||||
lemma P!_zero (f : Fin n → ℚ) (h : P! f = 0) : ∀ i, f i = 0 := by
|
||||
intro i
|
||||
rw [← P!_δ!₁ f]
|
||||
rw [← P!_oddShiftFst f]
|
||||
rw [h]
|
||||
rfl
|
||||
|
||||
lemma Pa_zero (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :
|
||||
∀ i, f i = 0 := by
|
||||
have h₃ := Pa_δa₁ f g
|
||||
have h₃ := Pa_oddShiftShiftZero f g
|
||||
rw [h] at h₃
|
||||
change 0 = _ at h₃
|
||||
simp only at h₃
|
||||
|
|
@ -516,11 +525,11 @@ lemma Pa_zero (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :
|
|||
rename_i iv hi
|
||||
have hivi : iv < n.succ := lt_of_succ_lt hiv
|
||||
have hi2 := hi hivi
|
||||
have h1 := Pa_δa₄ f g ⟨iv, hivi⟩
|
||||
have h1 := Pa_oddShiftShiftSnd f g ⟨iv, hivi⟩
|
||||
rw [h, hi2] at h1
|
||||
change 0 = _ at h1
|
||||
simp only [neg_zero, succ_eq_add_one, zero_sub, zero_eq_neg] at h1
|
||||
have h2 := Pa_δa₂ f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
|
||||
have h2 := Pa_oddShiftShiftFst f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
|
||||
simp only [succ_eq_add_one, h, Fin.succ_mk, Fin.castSucc_mk, h1, add_zero] at h2
|
||||
exact h2.symm
|
||||
exact hinduc i.val i.prop
|
||||
|
|
@ -676,16 +685,16 @@ lemma span_basis (S : (PureU1 (2 * n.succ + 1)).LinSols) :
|
|||
|
||||
lemma span_basis_swap! {S : (PureU1 (2 * n.succ + 1)).LinSols} (j : Fin n.succ)
|
||||
(hS : ((FamilyPermutations (2 * n.succ + 1)).linSolRep
|
||||
(pairSwap (oddShiftFstEmbed j) (oddShiftSndEmbed j))) S = S') (g f : Fin n.succ → ℚ) (hS1 : S.val = P g + P! f) :
|
||||
∃ (g' f' : Fin n.succ → ℚ),
|
||||
(pairSwap (oddShiftFst j) (oddShiftSnd j))) S = S') (g f : Fin n.succ → ℚ)
|
||||
(hS1 : S.val = P g + P! f) : ∃ (g' f' : Fin n.succ → ℚ),
|
||||
S'.val = P g' + P! f' ∧ P! f' = P! f +
|
||||
(S.val (oddShiftSndEmbed j) - S.val (oddShiftFstEmbed j)) • basis!AsCharges j ∧ g' = g := by
|
||||
let X := P! f + (S.val (oddShiftSndEmbed j) - S.val (oddShiftFstEmbed j)) • basis!AsCharges j
|
||||
(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = g := by
|
||||
let X := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j
|
||||
have hf : P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges) := by
|
||||
rw [(mem_span_range_iff_exists_fun ℚ)]
|
||||
use f
|
||||
rfl
|
||||
have hP : (S.val (oddShiftSndEmbed j) - S.val (oddShiftFstEmbed j)) • basis!AsCharges j ∈
|
||||
have hP : (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈
|
||||
Submodule.span ℚ (Set.range basis!AsCharges) := by
|
||||
apply Submodule.smul_mem
|
||||
apply SetLike.mem_of_subset
|
||||
|
|
|
|||
|
|
@ -82,17 +82,17 @@ lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols}
|
|||
lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
|
||||
(LIC : LineInCubicPerm S) :
|
||||
∀ (j : Fin n.succ) (g f : Fin n.succ → ℚ) (_ : S.val = Pa g f),
|
||||
(S.val (oddShiftSndEmbed j) - S.val (oddShiftFstEmbed j))
|
||||
(S.val (oddShiftSnd j) - S.val (oddShiftFst j))
|
||||
* accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := by
|
||||
intro j g f h
|
||||
let S' := (FamilyPermutations (2 * n.succ + 1)).linSolRep
|
||||
(pairSwap (oddShiftFstEmbed j) (oddShiftSndEmbed j)) S
|
||||
(pairSwap (oddShiftFst j) (oddShiftSnd j)) S
|
||||
have hSS' : ((FamilyPermutations (2 * n.succ + 1)).linSolRep
|
||||
(pairSwap (oddShiftFstEmbed j) (oddShiftSndEmbed j))) S = S' := rfl
|
||||
(pairSwap (oddShiftFst j) (oddShiftSnd j))) S = S' := rfl
|
||||
obtain ⟨g', f', hall⟩ := span_basis_swap! j hSS' g f h
|
||||
have h1 := line_in_cubic_P_P_P! (lineInCubicPerm_self LIC) g f h
|
||||
have h2 := line_in_cubic_P_P_P!
|
||||
(lineInCubicPerm_self (lineInCubicPerm_permute LIC (pairSwap (oddShiftFstEmbed j) (δ!₂ j)))) g' f' hall.1
|
||||
have h2 := line_in_cubic_P_P_P! (lineInCubicPerm_self (lineInCubicPerm_permute LIC
|
||||
(pairSwap (oddShiftFst j) (oddShiftSnd j)))) g' f' hall.1
|
||||
rw [hall.2.1, hall.2.2] at h2
|
||||
rw [accCubeTriLinSymm.map_add₃, h1, accCubeTriLinSymm.map_smul₃] at h2
|
||||
simpa using h2
|
||||
|
|
@ -100,26 +100,30 @@ lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
|
|||
lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
|
||||
(f g : Fin n.succ.succ → ℚ) (hS : S.val = Pa f g) :
|
||||
accCubeTriLinSymm (P f) (P f) (basis!AsCharges 0) =
|
||||
(S.val (oddShiftFstEmbed 0) + S.val (oddShiftSndEmbed 0)) * (2 * S.val oddShiftZero + S.val (oddShiftFstEmbed 0) + S.val (oddShiftSndEmbed 0)) := by
|
||||
(S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
|
||||
(2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) := by
|
||||
rw [P_P_P!_accCube f 0]
|
||||
rw [← Pa_δa₁ f g]
|
||||
rw [← Pa_oddShiftShiftZero f g]
|
||||
rw [← hS]
|
||||
have ht : oddShiftFstEmbed (0 : Fin n.succ.succ) = oddFstEmbed 1 := rfl
|
||||
have ht : oddShiftFst (0 : Fin n.succ.succ) = oddFst 1 := rfl
|
||||
nth_rewrite 1 [ht]
|
||||
rw [P_δ₁]
|
||||
have h1 := Pa_δa₁ f g
|
||||
have h4 := Pa_δa₄ f g 0
|
||||
have h2 := Pa_δa₂ f g 0
|
||||
rw [P_oddFst]
|
||||
have h1 := Pa_oddShiftShiftZero f g
|
||||
have h4 := Pa_oddShiftShiftSnd f g 0
|
||||
have h2 := Pa_oddShiftShiftFst f g 0
|
||||
rw [← hS] at h1 h2 h4
|
||||
simp only [Nat.succ_eq_add_one, Fin.succ_zero_eq_one, Fin.castSucc_zero] at h2
|
||||
have h5 : f 1 = S.val (δa₂ 0) + S.val δa₁ + S.val (δa₄ 0) := by
|
||||
have h5 : f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero +
|
||||
S.val (oddShiftShiftSnd 0) := by
|
||||
linear_combination -(1 * h1) - 1 * h4 - 1 * h2
|
||||
rw [h5, δa₄_δ!₂, show (δa₂ (0 : Fin n.succ)) = δ!₁ 0 from rfl, δa₁_δ!₃]
|
||||
rw [h5, oddShiftShiftSnd_eq_oddShiftSnd,
|
||||
show (oddShiftShiftFst (0 : Fin n.succ)) = oddShiftFst 0 from rfl,
|
||||
oddShiftShiftZero_eq_oddShiftZero]
|
||||
ring
|
||||
|
||||
lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols}
|
||||
(LIC : LineInCubicPerm S) :
|
||||
LineInPlaneProp ((S.val (oddShiftSndEmbed 0)), ((S.val (oddShiftFstEmbed 0)), (S.val oddShiftZero))) := by
|
||||
LineInPlaneProp ((S.val (oddShiftSnd 0)), ((S.val (oddShiftFst 0)), (S.val oddShiftZero))) := by
|
||||
obtain ⟨g, f, hfg⟩ := span_basis S
|
||||
have h1 := lineInCubicPerm_swap LIC 0 g f hfg
|
||||
rw [P_P_P!_accCube' g f hfg] at h1
|
||||
|
|
@ -135,7 +139,7 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols}
|
|||
|
||||
lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
|
||||
(LIC : LineInCubicPerm S) : LineInPlaneCond S := by
|
||||
refine @Prop_three (2 * n.succ.succ + 1) LineInPlaneProp S (oddShiftSndEmbed 0) (oddShiftFstEmbed 0)
|
||||
refine @Prop_three (2 * n.succ.succ + 1) LineInPlaneProp S (oddShiftSnd 0) (oddShiftFst 0)
|
||||
oddShiftZero ?_ ?_ ?_ ?_
|
||||
· exact ne_of_beq_false rfl
|
||||
· exact ne_of_beq_false rfl
|
||||
|
|
|
|||
|
|
@ -33,13 +33,13 @@ open VectorLikeOddPlane
|
|||
show that this can be extended to a complete solution. -/
|
||||
def parameterizationAsLinear (g f : Fin n → ℚ) (a : ℚ) :
|
||||
(PureU1 (2 * n + 1)).LinSols :=
|
||||
a • ((accCubeTriLinSymm (sndPlane f) (sndPlane f) (fstPlane g)) • P' g +
|
||||
(- accCubeTriLinSymm (fstPlane g) sndPlanestPlane g) (P! f)) • P!' f)
|
||||
a • ((accCubeTriLinSymm (P! f) (P! f) (P g)) • P' g +
|
||||
(- accCubeTriLinSymm (P g) (P g) (P! f)) • P!' f)
|
||||
|
||||
lemma parameterizationAsLinear_val (g f : Fin n → ℚ) (a : ℚ) :
|
||||
(parameterizationAsLinear g f a).val =
|
||||
a • ((accCubeTriLinSymm (sndPlane f) (sndPlane f) (fstPlane g)) • fstPlane g +
|
||||
(- accCubeTriLinSymm (fstPlane g) sndPlanestPlanesndPlane) (P! f)) • P! f) := by
|
||||
a • ((accCubeTriLinSymm (P! f) (P! f) (P g)) • P g +
|
||||
(- accCubeTriLinSymm (P g) (P g) (P! f)) • P! f) := by
|
||||
rw [parameterizationAsLinear]
|
||||
change a • (_ • (P' g).val + _ • (P!' f).val) = _
|
||||
rw [P'_val, P!'_val]
|
||||
|
|
@ -64,12 +64,12 @@ def parameterization (g f : Fin n → ℚ) (a : ℚ) :
|
|||
⟨⟨parameterizationAsLinear g f a, fun i => Fin.elim0 i⟩,
|
||||
parameterizationCharge_cube g f a⟩
|
||||
|
||||
lemma anomalyFree_param {S : (PureU1fstPlasndPlane(2 * n + 1)).Sols}
|
||||
(g f : Fin n → ℚ) (fstPlaneS : sndPlanestPlaneval = P g + P! f) :
|
||||
accCubeTriLinSymm (P sndPlane (P gsndPlane(P! ffstPlane =
|
||||
lemma anomalyFree_param {S : (PureU1 (2 * n + 1)).Sols}
|
||||
(g f : Fin n → ℚ) (hS : S.val = P g + P! f) :
|
||||
accCubeTriLinSymm (P g) (P g) (P! f) =
|
||||
- accCubeTriLinSymm (P! f) (P! f) (P g) := by
|
||||
have hC := S.cubicSol
|
||||
rw [hS] at hCfstPlanesndPlane
|
||||
rw [hS] at hC
|
||||
change (accCube (2 * n + 1)) (P g + P! f) = 0 at hC
|
||||
erw [TriLinearSymm.toCubic_add] at hC
|
||||
erw [P_accCube] at hC
|
||||
|
|
@ -78,12 +78,12 @@ lemma anomalyFree_param {S : (PureU1fstPlasndPlane(2 * n + 1)).Sols}
|
|||
|
||||
/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠ 0`.
|
||||
In this case our parameterization above will be able to recover this point. -/
|
||||
def GenericCase (S : (PureU1 (2 * n.succfstPlasndPlane+ 1)).Sols) : Prop :=
|
||||
∀ (g f : Fin n.succfstPlane→ ℚ)sndPlanestPlane_ : S.val = P g + P! f),
|
||||
def GenericCase (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
|
||||
∀ (g f : Fin n.succ → ℚ) (_ : S.val = P g + P! f),
|
||||
accCubeTriLinSymm (P g) (P g) (P! f) ≠ 0
|
||||
|
||||
lemma genericCase_exists (S : (PureU1 (2 * nfstPlasndPlanesucc + 1)).Sols)
|
||||
(hs : ∃ (g f : Fin fstPlane.sucsndPlanestPlane→ ℚ), S.val = P g + P! f ∧
|
||||
lemma genericCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
|
||||
(hs : ∃ (g f : Fin n.succ → ℚ), S.val = P g + P! f ∧
|
||||
accCubeTriLinSymm (P g) (P g) (P! f) ≠ 0) : GenericCase S := by
|
||||
intro g f hS hC
|
||||
obtain ⟨g', f', hS', hC'⟩ := hs
|
||||
|
|
@ -94,12 +94,12 @@ lemma genericCase_exists (S : (PureU1 (2 * nfstPlasndPlanesucc + 1)).Sols)
|
|||
|
||||
/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠ 0`.
|
||||
In this case we will show that S is zero if it is true for all permutations. -/
|
||||
def SpecialCase (S : (PureU1 (2 * n.succfstPlasndPlane+ 1)).Sols) : Prop :=
|
||||
∀ (g f : Fin n.succfstPlane→ ℚ)sndPlanestPlane_ : S.val = P g + P! f),
|
||||
def SpecialCase (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
|
||||
∀ (g f : Fin n.succ → ℚ) (_ : S.val = P g + P! f),
|
||||
accCubeTriLinSymm (P g) (P g) (P! f) = 0
|
||||
|
||||
lemma specialCase_exists (S : (PureU1 (2 * nfstPlasndPlanesucc + 1)).Sols)
|
||||
(hs : ∃ (g f : Fin fstPlane.sucsndPlanestPlane→ ℚ), S.val = P g + P! f ∧
|
||||
lemma specialCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
|
||||
(hs : ∃ (g f : Fin n.succ → ℚ), S.val = P g + P! f ∧
|
||||
accCubeTriLinSymm (P g) (P g) (P! f) = 0) : SpecialCase S := by
|
||||
intro g f hS
|
||||
obtain ⟨g', f', hS', hC'⟩ := hs
|
||||
|
|
@ -110,8 +110,8 @@ lemma specialCase_exists (S : (PureU1 (2 * nfstPlasndPlanesucc + 1)).Sols)
|
|||
|
||||
lemma generic_or_special (S : (PureU1 (2 * n.succ + 1)).Sols) :
|
||||
GenericCase S ∨ SpecialCase S := by
|
||||
obtain ⟨g, f, h⟩ := span_basifstPlane S.1sndPlanestPlane
|
||||
have h1 : accCubeTriLinfstPlaneymm sndPlanestPlane g) (P g) (P! f) ≠ 0 ∨
|
||||
obtain ⟨g, f, h⟩ := span_basis S.1.1
|
||||
have h1 : accCubeTriLinSymm (P g) (P g) (P! f) ≠ 0 ∨
|
||||
accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by
|
||||
exact ne_or_eq _ _
|
||||
cases h1 <;> rename_i h1
|
||||
|
|
@ -120,11 +120,11 @@ lemma generic_or_special (S : (PureU1 (2 * n.succ + 1)).Sols) :
|
|||
|
||||
theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : GenericCase S) :
|
||||
∃ g f a, S = parameterization g f a := by
|
||||
obtain ⟨g, f, hS⟩ := span_basisndPlaneS.1.1sndPlanetPlane
|
||||
obtain ⟨g, f, hS⟩ := span_basis S.1.1
|
||||
use g, f, (accCubeTriLinSymm (P! f) (P! f) (P g))⁻¹
|
||||
rw [parameterization]
|
||||
apply ACCSystem.Sols.ext
|
||||
rw [parameterizationAsLifstPlaneesndPlane_val]
|
||||
rw [parameterizationAsLinear_val]
|
||||
change S.val = _ • (_ • P g + _• P! f)
|
||||
rw [anomalyFree_param _ _ hS, neg_neg, ← smul_add, smul_smul, inv_mul_cancel₀, one_smul]
|
||||
· exact hS
|
||||
|
|
@ -143,7 +143,7 @@ lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols}
|
|||
accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
|
||||
accCubeTriLinSymm.map_smul₃, h]
|
||||
rw [anomalyFree_param _ _ hS] at h
|
||||
simp only [Nat.succ_eq_addsndPlanene, asndPlaneCubeTfstPlaneiLinSymm_toFun_apply_apply, neg_eq_zero] at h
|
||||
simp only [Nat.succ_eq_add_one, accCubeTriLinSymm_toFun_apply_apply, neg_eq_zero] at h
|
||||
change accCubeTriLinSymm (P! f) (P! f) (P g) = 0 at h
|
||||
erw [h]
|
||||
simp
|
||||
|
|
|
|||
|
|
@ -90,7 +90,6 @@ lemma phaseShift_coe_matrix (a b c : ℝ) : ↑(phaseShift a b c) = phaseShiftMa
|
|||
def PhaseShiftRelation (U V : unitaryGroup (Fin 3) ℂ) : Prop :=
|
||||
∃ a b c e f g, U = phaseShift a b c * V * phaseShift e f g
|
||||
|
||||
|
||||
/-- The relation `PhaseShiftRelation` is reflective. -/
|
||||
lemma phaseShiftRelation_refl (U : unitaryGroup (Fin 3) ℂ) : PhaseShiftRelation U U := by
|
||||
use 0, 0, 0, 0, 0, 0
|
||||
|
|
|
|||
|
|
@ -342,7 +342,7 @@ lemma σSAL_decomp (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
|
|||
ring
|
||||
|
||||
/-- The component of a self-adjoint matrix in the direction `σ0` under
|
||||
the basis formed by the covaraiant Pauli matrices. -/
|
||||
the basis formed by the covaraiant Pauli matrices. -/
|
||||
@[simp]
|
||||
lemma σSAL_repr_inl_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
|
||||
σSAL.repr M (Sum.inl 0) = 1 / 2 * Matrix.trace (σ0 * M.1) := by
|
||||
|
|
@ -359,7 +359,7 @@ lemma σSAL_repr_inl_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
|
|||
simp [σSAL]
|
||||
|
||||
/-- The component of a self-adjoint matrix in the direction `-σ1` under
|
||||
the basis formed by the covaraiant Pauli matrices. -/
|
||||
the basis formed by the covaraiant Pauli matrices. -/
|
||||
@[simp]
|
||||
lemma σSAL_repr_inr_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
|
||||
σSAL.repr M (Sum.inr 0) = - 1 / 2 * Matrix.trace (σ1 * M.1) := by
|
||||
|
|
@ -376,7 +376,7 @@ lemma σSAL_repr_inr_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
|
|||
simp [σSAL]
|
||||
|
||||
/-- The component of a self-adjoint matrix in the direction `-σ2` under
|
||||
the basis formed by the covaraiant Pauli matrices. -/
|
||||
the basis formed by the covaraiant Pauli matrices. -/
|
||||
@[simp]
|
||||
lemma σSAL_repr_inr_1 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
|
||||
σSAL.repr M (Sum.inr 1) = - 1 / 2 * Matrix.trace (σ2 * M.1) := by
|
||||
|
|
@ -393,7 +393,7 @@ lemma σSAL_repr_inr_1 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
|
|||
simp [σSAL]
|
||||
|
||||
/-- The component of a self-adjoint matrix in the direction `-σ3` under
|
||||
the basis formed by the covaraiant Pauli matrices. -/
|
||||
the basis formed by the covaraiant Pauli matrices. -/
|
||||
@[simp]
|
||||
lemma σSAL_repr_inr_2 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
|
||||
σSAL.repr M (Sum.inr 2) = - 1 / 2 * Matrix.trace (σ3 * M.1) := by
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue