From ebf4ba4b9a8b7366c9128e010ab0fd0e2b17fab2 Mon Sep 17 00:00:00 2001 From: Nicola Bernini Date: Wed, 1 Jul 2026 11:52:55 +0200 Subject: [PATCH 1/8] feat: Add DropPair ProdP commutation lemma for one orientation --- .../Tensors/Contraction/Products.lean | 28 +++++++++++++++++++ .../Relativity/Tensors/Contraction/Pure.lean | 2 -- .../Tensors/Contraction/SuccSuccAbove.lean | 14 ++++++++++ Physlib/Relativity/Tensors/Reindexing.lean | 12 ++++++++ 4 files changed, 54 insertions(+), 2 deletions(-) diff --git a/Physlib/Relativity/Tensors/Contraction/Products.lean b/Physlib/Relativity/Tensors/Contraction/Products.lean index 0d95a6abb..8ea93fc72 100644 --- a/Physlib/Relativity/Tensors/Contraction/Products.lean +++ b/Physlib/Relativity/Tensors/Contraction/Products.lean @@ -89,6 +89,34 @@ lemma Pure.prodP_dropPair {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} (by rw [Fin.succSuccAbove_comm_natAdd i j])] simp [LinearEquiv.cast_apply] +set_option backward.isDefEq.respectTransparency false in +/-- Dropping a pair of indices in the left factor of a product of pure tensors agrees, + up to the canonical reindexing, with dropping the corresponding pair after taking + the product. -/ +lemma Pure.dropPair_prodP {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} + {c1 : Fin n1 → C} + (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) + (p : Pure S c) (p1 : Pure S c1) : + (dropPair i j hij.1 p).prodP p1 = permP _ (IsReindexing.append_succSuccAbove_castAdd i j) + (dropPair (Fin.castAdd n1 i) (Fin.castAdd n1 j) + (by simp_all [Fin.ext_iff]) (p.prodP p1)) := by + ext x + obtain ⟨x, rfl⟩ := finSumFinEquiv.surjective x + rw [prodP_apply_finSumFinEquiv] + simp only [Function.comp_apply, finSumFinEquiv_apply_left, finSumFinEquiv_apply_right, dropPair, + permP, Nat.add_eq, id_eq] + match x with + | Sum.inl m => + simp only [finSumFinEquiv_apply_left] + rw [← congr_right (p.prodP p1) _ (Fin.castAdd n1 (i.succSuccAbove j m)) + (by rw [Fin.succSuccAbove_comm_castAdd i j])] + simp [LinearEquiv.cast_apply] + | Sum.inr m => + simp only [finSumFinEquiv_apply_right] + rw [← congr_right (p.prodP p1) _ (Fin.natAdd (n + 1 + 1) m) + (by rw [Fin.succSuccAbove_castAdd_apply_natAdd i j])] + simp [LinearEquiv.cast_apply] + set_option backward.isDefEq.respectTransparency false in lemma Pure.prodP_contrP_snd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} {c1 : Fin n1 → C} diff --git a/Physlib/Relativity/Tensors/Contraction/Pure.lean b/Physlib/Relativity/Tensors/Contraction/Pure.lean index 87e256b57..44be64088 100644 --- a/Physlib/Relativity/Tensors/Contraction/Pure.lean +++ b/Physlib/Relativity/Tensors/Contraction/Pure.lean @@ -118,8 +118,6 @@ lemma dropPair_update_succSuccAbove {n : ℕ} [inst : DecidableEq (Fin (n + 1 +1 · simp [h] · simp [h] -TODO "Prove lemmas relating to the commutation rules of `dropPair` and `prodP`." - @[simp] lemma dropPair_permP {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} {c1 : Fin (n1 + 1 + 1) → C} (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j) diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean index 93388c825..b32353db4 100644 --- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean +++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean @@ -250,6 +250,20 @@ lemma succSuccAbove_comm_natAdd {n n1 : ℕ} simp only [succSuccAbove, val_natAdd, add_lt_add_iff_left, add_le_add_iff_left, Fin.ext_iff] grind +lemma succSuccAbove_comm_castAdd {n n1 : ℕ} + (i j : Fin (n + 1 + 1)) (m : Fin n) : + succSuccAbove (n := n + n1) (Fin.castAdd n1 i) (Fin.castAdd n1 j) (Fin.castAdd n1 m) + = Fin.castAdd n1 (succSuccAbove i j m) := by + simp only [Fin.ext_iff, succSuccAbove_val, castAdd] + grind (splits := 20) + +lemma succSuccAbove_castAdd_apply_natAdd {n n1 : ℕ} + (i j : Fin (n + 1 + 1)) (m : Fin n1) : + succSuccAbove (n := n + n1) (Fin.castAdd n1 i) (Fin.castAdd n1 j) (Fin.natAdd n m) + = Fin.natAdd (n + 1 + 1) m := by + simp only [Fin.ext_iff, succSuccAbove_val, natAdd, castAdd] + grind (splits := 20) + /-! ## predPredAbove diff --git a/Physlib/Relativity/Tensors/Reindexing.lean b/Physlib/Relativity/Tensors/Reindexing.lean index 09b30038c..ab7c0e4f1 100644 --- a/Physlib/Relativity/Tensors/Reindexing.lean +++ b/Physlib/Relativity/Tensors/Reindexing.lean @@ -283,6 +283,18 @@ lemma append_succSuccAbove_natAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} apply And.intro (Function.bijective_id) simp [forall_fin_add, succSuccAbove_comm_natAdd i j, succSuccAbove_natAdd_apply_castAdd i j] +/-- Removing two entries from the left component of `Fin.append c c1` commutes with the + append: removing the `i`-th and `j`-th entries of `c` and then appending `c1` matches + removing the corresponding entries of `Fin.append c c1`, via the identity permutation. + This is used for the commutation of taking a *product* of tensors + with *contraction* of indices. -/ +lemma append_succSuccAbove_castAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} + {c1 : Fin n1 → C} (i j : Fin (n + 1 + 1)) : + IsReindexing (Fin.append c c1 ∘ (Fin.castAdd n1 i).succSuccAbove (Fin.castAdd n1 j)) + (Fin.append (c ∘ i.succSuccAbove j) c1) id := by + apply And.intro (Function.bijective_id) + simp [forall_fin_add, succSuccAbove_comm_castAdd i j, succSuccAbove_castAdd_apply_natAdd i j] + /-- Given a reindexing of `c` by `c1` via `σ` for which the index `i` is sent to `0`, removing the `i`-th entry of `c1` and the first entry of `c` yields a reindexing of `c ∘ Fin.succ` by `c1 ∘ i.succAbove` via the map sending `j` to the predecessor of From 02d05aef976cc668ce9dd1a623d15a501fe305e3 Mon Sep 17 00:00:00 2001 From: Nicola Bernini Date: Wed, 1 Jul 2026 17:30:07 +0200 Subject: [PATCH 2/8] fix: Trying to Fix the Build --- .../Relativity/Tensors/Contraction/Products.lean | 2 +- .../Tensors/Contraction/SuccSuccAbove.lean | 14 ++++++++------ Physlib/Relativity/Tensors/Reindexing.lean | 4 ++-- 3 files changed, 11 insertions(+), 9 deletions(-) diff --git a/Physlib/Relativity/Tensors/Contraction/Products.lean b/Physlib/Relativity/Tensors/Contraction/Products.lean index 8ea93fc72..acee2c6f3 100644 --- a/Physlib/Relativity/Tensors/Contraction/Products.lean +++ b/Physlib/Relativity/Tensors/Contraction/Products.lean @@ -104,7 +104,7 @@ lemma Pure.dropPair_prodP {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} obtain ⟨x, rfl⟩ := finSumFinEquiv.surjective x rw [prodP_apply_finSumFinEquiv] simp only [Function.comp_apply, finSumFinEquiv_apply_left, finSumFinEquiv_apply_right, dropPair, - permP, Nat.add_eq, id_eq] + permP, Nat.add_eq] match x with | Sum.inl m => simp only [finSumFinEquiv_apply_left] diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean index b32353db4..645dc96bb 100644 --- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean +++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean @@ -252,16 +252,18 @@ lemma succSuccAbove_comm_natAdd {n n1 : ℕ} lemma succSuccAbove_comm_castAdd {n n1 : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n) : - succSuccAbove (n := n + n1) (Fin.castAdd n1 i) (Fin.castAdd n1 j) (Fin.castAdd n1 m) - = Fin.castAdd n1 (succSuccAbove i j m) := by - simp only [Fin.ext_iff, succSuccAbove_val, castAdd] + succSuccAbove (Fin.castAdd n1 i) (Fin.castAdd n1 j) + (Fin.cast (by grind) (Fin.castAdd n1 m)) = + Fin.castAdd n1 (succSuccAbove i j m) := by + simp only [Fin.ext_iff, succSuccAbove_val, val_cast, castAdd] grind (splits := 20) lemma succSuccAbove_castAdd_apply_natAdd {n n1 : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n1) : - succSuccAbove (n := n + n1) (Fin.castAdd n1 i) (Fin.castAdd n1 j) (Fin.natAdd n m) - = Fin.natAdd (n + 1 + 1) m := by - simp only [Fin.ext_iff, succSuccAbove_val, natAdd, castAdd] + succSuccAbove (Fin.castAdd n1 i) (Fin.castAdd n1 j) + (Fin.cast (by grind) (Fin.natAdd n m)) = + Fin.natAdd (n + 1 + 1) m := by + simp only [Fin.ext_iff, succSuccAbove_val, val_cast, natAdd, castAdd] grind (splits := 20) /-! diff --git a/Physlib/Relativity/Tensors/Reindexing.lean b/Physlib/Relativity/Tensors/Reindexing.lean index ab7c0e4f1..815c76d2b 100644 --- a/Physlib/Relativity/Tensors/Reindexing.lean +++ b/Physlib/Relativity/Tensors/Reindexing.lean @@ -291,8 +291,8 @@ lemma append_succSuccAbove_natAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} lemma append_succSuccAbove_castAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} {c1 : Fin n1 → C} (i j : Fin (n + 1 + 1)) : IsReindexing (Fin.append c c1 ∘ (Fin.castAdd n1 i).succSuccAbove (Fin.castAdd n1 j)) - (Fin.append (c ∘ i.succSuccAbove j) c1) id := by - apply And.intro (Function.bijective_id) + (Fin.append (c ∘ i.succSuccAbove j) c1) (Fin.cast (by grind)) := by + apply And.intro (finCongr (by grind)).bijective simp [forall_fin_add, succSuccAbove_comm_castAdd i j, succSuccAbove_castAdd_apply_natAdd i j] /-- Given a reindexing of `c` by `c1` via `σ` for which the index `i` is sent to `0`, From 0ef48e9bd3a8db8ce974df5ec663d4d731d9c731 Mon Sep 17 00:00:00 2001 From: Nicola Bernini Date: Wed, 1 Jul 2026 19:30:35 +0200 Subject: [PATCH 3/8] fix: Trying to Fix --- Physlib/Relativity/Tensors/Contraction/Products.lean | 4 ++-- Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Physlib/Relativity/Tensors/Contraction/Products.lean b/Physlib/Relativity/Tensors/Contraction/Products.lean index acee2c6f3..9e9cb8ec5 100644 --- a/Physlib/Relativity/Tensors/Contraction/Products.lean +++ b/Physlib/Relativity/Tensors/Contraction/Products.lean @@ -108,12 +108,12 @@ lemma Pure.dropPair_prodP {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} match x with | Sum.inl m => simp only [finSumFinEquiv_apply_left] - rw [← congr_right (p.prodP p1) _ (Fin.castAdd n1 (i.succSuccAbove j m)) + rw [← congr_right (p.prodP p1) _ (Fin.cast (by grind) (Fin.castAdd n1 (i.succSuccAbove j m))) (by rw [Fin.succSuccAbove_comm_castAdd i j])] simp [LinearEquiv.cast_apply] | Sum.inr m => simp only [finSumFinEquiv_apply_right] - rw [← congr_right (p.prodP p1) _ (Fin.natAdd (n + 1 + 1) m) + rw [← congr_right (p.prodP p1) _ (Fin.cast (by grind) (Fin.natAdd (n + 1 + 1) m)) (by rw [Fin.succSuccAbove_castAdd_apply_natAdd i j])] simp [LinearEquiv.cast_apply] diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean index 645dc96bb..cef7727dd 100644 --- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean +++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean @@ -254,7 +254,7 @@ lemma succSuccAbove_comm_castAdd {n n1 : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n) : succSuccAbove (Fin.castAdd n1 i) (Fin.castAdd n1 j) (Fin.cast (by grind) (Fin.castAdd n1 m)) = - Fin.castAdd n1 (succSuccAbove i j m) := by + Fin.cast (by grind) (Fin.castAdd n1 (succSuccAbove i j m)) := by simp only [Fin.ext_iff, succSuccAbove_val, val_cast, castAdd] grind (splits := 20) @@ -262,7 +262,7 @@ lemma succSuccAbove_castAdd_apply_natAdd {n n1 : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n1) : succSuccAbove (Fin.castAdd n1 i) (Fin.castAdd n1 j) (Fin.cast (by grind) (Fin.natAdd n m)) = - Fin.natAdd (n + 1 + 1) m := by + Fin.cast (by grind) (Fin.natAdd (n + 1 + 1) m) := by simp only [Fin.ext_iff, succSuccAbove_val, val_cast, natAdd, castAdd] grind (splits := 20) From 3d805ad670d0b52fac71dc04cc8db74198e0d5d8 Mon Sep 17 00:00:00 2001 From: Nicola Bernini Date: Wed, 1 Jul 2026 20:44:29 +0200 Subject: [PATCH 4/8] fix: avoid ambiguous succSuccAbove cast simplification Co-authored-by: Claude Opus 4.8 --- Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean index cef7727dd..ac407dcde 100644 --- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean +++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean @@ -255,7 +255,7 @@ lemma succSuccAbove_comm_castAdd {n n1 : ℕ} succSuccAbove (Fin.castAdd n1 i) (Fin.castAdd n1 j) (Fin.cast (by grind) (Fin.castAdd n1 m)) = Fin.cast (by grind) (Fin.castAdd n1 (succSuccAbove i j m)) := by - simp only [Fin.ext_iff, succSuccAbove_val, val_cast, castAdd] + simp only [Fin.ext_iff, succSuccAbove, val_cast, castAdd] grind (splits := 20) lemma succSuccAbove_castAdd_apply_natAdd {n n1 : ℕ} @@ -263,7 +263,7 @@ lemma succSuccAbove_castAdd_apply_natAdd {n n1 : ℕ} succSuccAbove (Fin.castAdd n1 i) (Fin.castAdd n1 j) (Fin.cast (by grind) (Fin.natAdd n m)) = Fin.cast (by grind) (Fin.natAdd (n + 1 + 1) m) := by - simp only [Fin.ext_iff, succSuccAbove_val, val_cast, natAdd, castAdd] + simp only [Fin.ext_iff, succSuccAbove, val_cast, natAdd, castAdd] grind (splits := 20) /-! From 04c763cb6631f16f3552397fa4ef8859aeea69bd Mon Sep 17 00:00:00 2001 From: Nicola Bernini Date: Fri, 3 Jul 2026 15:52:43 +0200 Subject: [PATCH 5/8] fix: make succSuccAbove cast lengths explicit Co-authored-by: Claude Opus 4.8 --- Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean index ac407dcde..b76d5cc73 100644 --- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean +++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean @@ -252,16 +252,16 @@ lemma succSuccAbove_comm_natAdd {n n1 : ℕ} lemma succSuccAbove_comm_castAdd {n n1 : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n) : - succSuccAbove (Fin.castAdd n1 i) (Fin.castAdd n1 j) - (Fin.cast (by grind) (Fin.castAdd n1 m)) = + succSuccAbove (n := n + n1) (Fin.cast (by grind) (Fin.castAdd n1 i)) + (Fin.cast (by grind) (Fin.castAdd n1 j)) (Fin.castAdd n1 m) = Fin.cast (by grind) (Fin.castAdd n1 (succSuccAbove i j m)) := by simp only [Fin.ext_iff, succSuccAbove, val_cast, castAdd] grind (splits := 20) lemma succSuccAbove_castAdd_apply_natAdd {n n1 : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n1) : - succSuccAbove (Fin.castAdd n1 i) (Fin.castAdd n1 j) - (Fin.cast (by grind) (Fin.natAdd n m)) = + succSuccAbove (n := n + n1) (Fin.cast (by grind) (Fin.castAdd n1 i)) + (Fin.cast (by grind) (Fin.castAdd n1 j)) (Fin.natAdd n m) = Fin.cast (by grind) (Fin.natAdd (n + 1 + 1) m) := by simp only [Fin.ext_iff, succSuccAbove, val_cast, natAdd, castAdd] grind (splits := 20) From e3d3abdba7561de1ef19324b7e808044b73b25e4 Mon Sep 17 00:00:00 2001 From: Nicola Bernini Date: Fri, 3 Jul 2026 16:23:12 +0200 Subject: [PATCH 6/8] fix: require distinct indices for castAdd drop-pair lemmas Co-authored-by: Claude Opus 4.8 --- Physlib/Relativity/Tensors/Contraction/Products.lean | 6 +++--- Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean | 4 ++-- Physlib/Relativity/Tensors/Reindexing.lean | 5 +++-- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/Physlib/Relativity/Tensors/Contraction/Products.lean b/Physlib/Relativity/Tensors/Contraction/Products.lean index 9e9cb8ec5..5767c6fdb 100644 --- a/Physlib/Relativity/Tensors/Contraction/Products.lean +++ b/Physlib/Relativity/Tensors/Contraction/Products.lean @@ -97,7 +97,7 @@ lemma Pure.dropPair_prodP {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} {c1 : Fin n1 → C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) (p1 : Pure S c1) : - (dropPair i j hij.1 p).prodP p1 = permP _ (IsReindexing.append_succSuccAbove_castAdd i j) + (dropPair i j hij.1 p).prodP p1 = permP _ (IsReindexing.append_succSuccAbove_castAdd i j hij.1) (dropPair (Fin.castAdd n1 i) (Fin.castAdd n1 j) (by simp_all [Fin.ext_iff]) (p.prodP p1)) := by ext x @@ -109,12 +109,12 @@ lemma Pure.dropPair_prodP {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} | Sum.inl m => simp only [finSumFinEquiv_apply_left] rw [← congr_right (p.prodP p1) _ (Fin.cast (by grind) (Fin.castAdd n1 (i.succSuccAbove j m))) - (by rw [Fin.succSuccAbove_comm_castAdd i j])] + (by rw [Fin.succSuccAbove_comm_castAdd i j hij.1])] simp [LinearEquiv.cast_apply] | Sum.inr m => simp only [finSumFinEquiv_apply_right] rw [← congr_right (p.prodP p1) _ (Fin.cast (by grind) (Fin.natAdd (n + 1 + 1) m)) - (by rw [Fin.succSuccAbove_castAdd_apply_natAdd i j])] + (by rw [Fin.succSuccAbove_castAdd_apply_natAdd i j hij.1])] simp [LinearEquiv.cast_apply] set_option backward.isDefEq.respectTransparency false in diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean index b76d5cc73..a1751e33e 100644 --- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean +++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean @@ -251,7 +251,7 @@ lemma succSuccAbove_comm_natAdd {n n1 : ℕ} grind lemma succSuccAbove_comm_castAdd {n n1 : ℕ} - (i j : Fin (n + 1 + 1)) (m : Fin n) : + (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin n) : succSuccAbove (n := n + n1) (Fin.cast (by grind) (Fin.castAdd n1 i)) (Fin.cast (by grind) (Fin.castAdd n1 j)) (Fin.castAdd n1 m) = Fin.cast (by grind) (Fin.castAdd n1 (succSuccAbove i j m)) := by @@ -259,7 +259,7 @@ lemma succSuccAbove_comm_castAdd {n n1 : ℕ} grind (splits := 20) lemma succSuccAbove_castAdd_apply_natAdd {n n1 : ℕ} - (i j : Fin (n + 1 + 1)) (m : Fin n1) : + (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin n1) : succSuccAbove (n := n + n1) (Fin.cast (by grind) (Fin.castAdd n1 i)) (Fin.cast (by grind) (Fin.castAdd n1 j)) (Fin.natAdd n m) = Fin.cast (by grind) (Fin.natAdd (n + 1 + 1) m) := by diff --git a/Physlib/Relativity/Tensors/Reindexing.lean b/Physlib/Relativity/Tensors/Reindexing.lean index 815c76d2b..38ca37ce5 100644 --- a/Physlib/Relativity/Tensors/Reindexing.lean +++ b/Physlib/Relativity/Tensors/Reindexing.lean @@ -289,11 +289,12 @@ lemma append_succSuccAbove_natAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} This is used for the commutation of taking a *product* of tensors with *contraction* of indices. -/ lemma append_succSuccAbove_castAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} - {c1 : Fin n1 → C} (i j : Fin (n + 1 + 1)) : + {c1 : Fin n1 → C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) : IsReindexing (Fin.append c c1 ∘ (Fin.castAdd n1 i).succSuccAbove (Fin.castAdd n1 j)) (Fin.append (c ∘ i.succSuccAbove j) c1) (Fin.cast (by grind)) := by apply And.intro (finCongr (by grind)).bijective - simp [forall_fin_add, succSuccAbove_comm_castAdd i j, succSuccAbove_castAdd_apply_natAdd i j] + simp [forall_fin_add, succSuccAbove_comm_castAdd i j hij, + succSuccAbove_castAdd_apply_natAdd i j hij] /-- Given a reindexing of `c` by `c1` via `σ` for which the index `i` is sent to `0`, removing the `i`-th entry of `c1` and the first entry of `c` yields a reindexing of From d22d471ca321fd1abb0ea26978db518d38171854 Mon Sep 17 00:00:00 2001 From: Nicola Bernini Date: Fri, 3 Jul 2026 19:39:00 +0200 Subject: [PATCH 7/8] fix: make append castAdd reindexing use identity Co-authored-by: Claude Opus 4.8 --- Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean | 2 +- Physlib/Relativity/Tensors/Reindexing.lean | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean index a1751e33e..84b6df588 100644 --- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean +++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean @@ -251,7 +251,7 @@ lemma succSuccAbove_comm_natAdd {n n1 : ℕ} grind lemma succSuccAbove_comm_castAdd {n n1 : ℕ} - (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin n) : + (i j : Fin (n + 1 + 1)) (_hij : i ≠ j) (m : Fin n) : succSuccAbove (n := n + n1) (Fin.cast (by grind) (Fin.castAdd n1 i)) (Fin.cast (by grind) (Fin.castAdd n1 j)) (Fin.castAdd n1 m) = Fin.cast (by grind) (Fin.castAdd n1 (succSuccAbove i j m)) := by diff --git a/Physlib/Relativity/Tensors/Reindexing.lean b/Physlib/Relativity/Tensors/Reindexing.lean index 38ca37ce5..c30ea89d6 100644 --- a/Physlib/Relativity/Tensors/Reindexing.lean +++ b/Physlib/Relativity/Tensors/Reindexing.lean @@ -290,9 +290,10 @@ lemma append_succSuccAbove_natAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} with *contraction* of indices. -/ lemma append_succSuccAbove_castAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} {c1 : Fin n1 → C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) : - IsReindexing (Fin.append c c1 ∘ (Fin.castAdd n1 i).succSuccAbove (Fin.castAdd n1 j)) - (Fin.append (c ∘ i.succSuccAbove j) c1) (Fin.cast (by grind)) := by - apply And.intro (finCongr (by grind)).bijective + IsReindexing (n := n + n1) (m := n + n1) + (Fin.append c c1 ∘ (Fin.castAdd n1 i).succSuccAbove (Fin.castAdd n1 j)) + (Fin.append (c ∘ i.succSuccAbove j) c1) id := by + apply And.intro Function.bijective_id simp [forall_fin_add, succSuccAbove_comm_castAdd i j hij, succSuccAbove_castAdd_apply_natAdd i j hij] From 30cf76f0506e3c2708ae0f3073f8d3141b3399f5 Mon Sep 17 00:00:00 2001 From: Nicola Bernini Date: Fri, 3 Jul 2026 21:01:25 +0200 Subject: [PATCH 8/8] fix: drop fragile left-factor dropPair commutation Co-authored-by: Claude Opus 4.8 --- .../Tensors/Contraction/Products.lean | 28 ------------------- .../Tensors/Contraction/SuccSuccAbove.lean | 16 ----------- Physlib/Relativity/Tensors/Reindexing.lean | 14 ---------- 3 files changed, 58 deletions(-) diff --git a/Physlib/Relativity/Tensors/Contraction/Products.lean b/Physlib/Relativity/Tensors/Contraction/Products.lean index 5767c6fdb..0d95a6abb 100644 --- a/Physlib/Relativity/Tensors/Contraction/Products.lean +++ b/Physlib/Relativity/Tensors/Contraction/Products.lean @@ -89,34 +89,6 @@ lemma Pure.prodP_dropPair {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} (by rw [Fin.succSuccAbove_comm_natAdd i j])] simp [LinearEquiv.cast_apply] -set_option backward.isDefEq.respectTransparency false in -/-- Dropping a pair of indices in the left factor of a product of pure tensors agrees, - up to the canonical reindexing, with dropping the corresponding pair after taking - the product. -/ -lemma Pure.dropPair_prodP {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} - {c1 : Fin n1 → C} - (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) - (p : Pure S c) (p1 : Pure S c1) : - (dropPair i j hij.1 p).prodP p1 = permP _ (IsReindexing.append_succSuccAbove_castAdd i j hij.1) - (dropPair (Fin.castAdd n1 i) (Fin.castAdd n1 j) - (by simp_all [Fin.ext_iff]) (p.prodP p1)) := by - ext x - obtain ⟨x, rfl⟩ := finSumFinEquiv.surjective x - rw [prodP_apply_finSumFinEquiv] - simp only [Function.comp_apply, finSumFinEquiv_apply_left, finSumFinEquiv_apply_right, dropPair, - permP, Nat.add_eq] - match x with - | Sum.inl m => - simp only [finSumFinEquiv_apply_left] - rw [← congr_right (p.prodP p1) _ (Fin.cast (by grind) (Fin.castAdd n1 (i.succSuccAbove j m))) - (by rw [Fin.succSuccAbove_comm_castAdd i j hij.1])] - simp [LinearEquiv.cast_apply] - | Sum.inr m => - simp only [finSumFinEquiv_apply_right] - rw [← congr_right (p.prodP p1) _ (Fin.cast (by grind) (Fin.natAdd (n + 1 + 1) m)) - (by rw [Fin.succSuccAbove_castAdd_apply_natAdd i j hij.1])] - simp [LinearEquiv.cast_apply] - set_option backward.isDefEq.respectTransparency false in lemma Pure.prodP_contrP_snd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} {c1 : Fin n1 → C} diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean index 84b6df588..93388c825 100644 --- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean +++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean @@ -250,22 +250,6 @@ lemma succSuccAbove_comm_natAdd {n n1 : ℕ} simp only [succSuccAbove, val_natAdd, add_lt_add_iff_left, add_le_add_iff_left, Fin.ext_iff] grind -lemma succSuccAbove_comm_castAdd {n n1 : ℕ} - (i j : Fin (n + 1 + 1)) (_hij : i ≠ j) (m : Fin n) : - succSuccAbove (n := n + n1) (Fin.cast (by grind) (Fin.castAdd n1 i)) - (Fin.cast (by grind) (Fin.castAdd n1 j)) (Fin.castAdd n1 m) = - Fin.cast (by grind) (Fin.castAdd n1 (succSuccAbove i j m)) := by - simp only [Fin.ext_iff, succSuccAbove, val_cast, castAdd] - grind (splits := 20) - -lemma succSuccAbove_castAdd_apply_natAdd {n n1 : ℕ} - (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin n1) : - succSuccAbove (n := n + n1) (Fin.cast (by grind) (Fin.castAdd n1 i)) - (Fin.cast (by grind) (Fin.castAdd n1 j)) (Fin.natAdd n m) = - Fin.cast (by grind) (Fin.natAdd (n + 1 + 1) m) := by - simp only [Fin.ext_iff, succSuccAbove, val_cast, natAdd, castAdd] - grind (splits := 20) - /-! ## predPredAbove diff --git a/Physlib/Relativity/Tensors/Reindexing.lean b/Physlib/Relativity/Tensors/Reindexing.lean index c30ea89d6..09b30038c 100644 --- a/Physlib/Relativity/Tensors/Reindexing.lean +++ b/Physlib/Relativity/Tensors/Reindexing.lean @@ -283,20 +283,6 @@ lemma append_succSuccAbove_natAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} apply And.intro (Function.bijective_id) simp [forall_fin_add, succSuccAbove_comm_natAdd i j, succSuccAbove_natAdd_apply_castAdd i j] -/-- Removing two entries from the left component of `Fin.append c c1` commutes with the - append: removing the `i`-th and `j`-th entries of `c` and then appending `c1` matches - removing the corresponding entries of `Fin.append c c1`, via the identity permutation. - This is used for the commutation of taking a *product* of tensors - with *contraction* of indices. -/ -lemma append_succSuccAbove_castAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C} - {c1 : Fin n1 → C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) : - IsReindexing (n := n + n1) (m := n + n1) - (Fin.append c c1 ∘ (Fin.castAdd n1 i).succSuccAbove (Fin.castAdd n1 j)) - (Fin.append (c ∘ i.succSuccAbove j) c1) id := by - apply And.intro Function.bijective_id - simp [forall_fin_add, succSuccAbove_comm_castAdd i j hij, - succSuccAbove_castAdd_apply_natAdd i j hij] - /-- Given a reindexing of `c` by `c1` via `σ` for which the index `i` is sent to `0`, removing the `i`-th entry of `c1` and the first entry of `c` yields a reindexing of `c ∘ Fin.succ` by `c1 ∘ i.succAbove` via the map sending `j` to the predecessor of