From fbd100e86a4c3a0a58f34d38ce3876494b2cfe00 Mon Sep 17 00:00:00 2001 From: catlover-bot Date: Tue, 11 Aug 2026 20:52:03 +0900 Subject: [PATCH 1/3] refactor(QED): name even anomaly-cancellation planes --- .../AnomalyCancellation/Even/BasisLinear.lean | 325 ++++++++++-------- .../AnomalyCancellation/Even/LineInCubic.lean | 39 ++- .../Even/Parameterization.lean | 87 +++-- 3 files changed, 263 insertions(+), 188 deletions(-) diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean index 0b1f94138..1c20acde2 100644 --- a/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean +++ b/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean @@ -19,10 +19,12 @@ conditions. ## ii. Key results -- `P'` : The inclusion of the first plane into linear solutions -- `P_accCube` : The statement that chares from the first plane satisfy the cubic ACC -- `P!'` : The inclusion of the second plane. -- `P!_accCube` : The statement that charges from the second plane satisfy the cubic ACC +- `Unshifted.planeLinSols` : The inclusion of the unshifted plane into linear solutions +- `Unshifted.planeCharges_accCube` : The statement that charges from the unshifted plane + satisfy the cubic ACC +- `Shifted.planeLinSols` : The inclusion of the shifted plane. +- `Shifted.planeCharges_accCube` : The statement that charges from the shifted plane + satisfy the cubic ACC - `span_basis` : Every linear solution is the sum of a point from each plane. ## iii. Table of contents @@ -31,29 +33,29 @@ conditions. - A.1. The even split: Spltting the charges up via `n.succ + n.succ` - A.2. The shifted even split: Spltting the charges up via `1 + (n + n + 1)` - A.3. Lemmas relating the two splittings -- B. The first plane - - B.1. The basis vectors of the first plane as charges +- B. The unshifted plane + - B.1. The basis vectors of the unshifted plane as charges - B.2. Components of the basis vectors - B.3. The basis vectors satisfy the linear ACCs - B.4. The basis vectors satisfy the cubic ACC - B.5. The basis vectors as linear solutions - - B.6. The inclusion of the first plane into charges + - B.6. The inclusion of the unshifted plane into charges - B.7. Components of the inclusion into charges - B.8. The inclusion into charges satisfies the linear and cubic ACCs - B.9. Kernel of the inclusion into charges - B.10. The inclusion of the plane into linear solutions - B.11. The basis vectors are linearly independent - - B.12. Every vector-like even solution is in the span of the basis of the first plane -- C. The vectors of the basis spanning the second plane, via the shifted even split + - B.12. Every vector-like even solution is in the span of the basis of the unshifted plane +- C. The shifted plane - C.2. Components of the vectors - C.3. The vectors satisfy the linear ACCs - C.4. The vectors satisfy the cubic ACC - C.6. The vectors as linear solutions - - C.7. The inclusion of the second plane into charges + - C.7. The inclusion of the shifted plane into charges - C.8. Components of the inclusion into charges - C.9. The inclusion into charges satisfies the cubic ACC - C.10. Kernel of the inclusion into charges - - C.11. The inclusion of the second plane into the span of the basis + - C.11. The inclusion of the shifted plane into the span of the basis - C.12. The inclusion of the plane into linear solutions - C.13. The basis vectors are linearly independent - C.14. Properties of the basis vectors relating to the span @@ -200,17 +202,19 @@ lemma evenShiftSnd_eq_evenSnd_castSucc (j : Fin n) : evenShiftSnd j = evenSnd j. /-! -## B. The first plane +## B. The unshifted plane -/ +namespace Unshifted + /-! -### B.1. The basis vectors of the first plane as charges +### B.1. The basis vectors of the unshifted plane as charges -/ -/-- The first part of the basis as charges. -/ +/-- The unshifted part of the basis as charges. -/ def basisAsCharges (j : Fin n.succ) : (PureU1 (2 * n.succ)).Charges := fun i => if i = evenFst j then @@ -306,7 +310,7 @@ lemma basis_accCube (j : Fin n.succ) : -/ -/-- The first part of the basis as `LinSols`. -/ +/-- The unshifted part of the basis as `LinSols`. -/ @[simps!] def basis (j : Fin n.succ) : (PureU1 (2 * n.succ)).LinSols := ⟨basisAsCharges j, by @@ -316,12 +320,12 @@ def basis (j : Fin n.succ) : (PureU1 (2 * n.succ)).LinSols := /-! -### B.6. The inclusion of the first plane into charges +### B.6. The inclusion of the unshifted plane into charges -/ -/-- A point in the span of the first part of the basis as a charge. -/ -def P (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).Charges := ∑ i, f i • basisAsCharges i +/-- A point in the span of the unshifted part of the basis as a charge. -/ +def planeCharges (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).Charges := ∑ i, f i • basisAsCharges i /-! @@ -329,23 +333,26 @@ def P (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).Charges := ∑ i, f i • -/ -lemma P_evenFst (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (evenFst j) = f j := by - rw [P, sum_of_charges] +lemma planeCharges_evenFst (f : Fin n.succ → ℚ) (j : Fin n.succ) : + planeCharges f (evenFst j) = f j := by + rw [planeCharges, sum_of_charges] simp only [succ_eq_add_one, HSMul.hSMul, SMul.smul] rw [Fintype.sum_eq_single j] · simp [basis_on_evenFst_self] · exact fun k hkj => mul_eq_zero_of_right (f k) (basis_on_evenFst_other hkj) -lemma P_evenSnd (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (evenSnd j) = - f j := by - rw [P, sum_of_charges] +lemma planeCharges_evenSnd (f : Fin n.succ → ℚ) (j : Fin n.succ) : + planeCharges f (evenSnd j) = - f j := by + rw [planeCharges, sum_of_charges] simp only [succ_eq_add_one, HSMul.hSMul, SMul.smul] rw [Fintype.sum_eq_single j] · simp [basis_on_evenSnd_self] · exact fun k hkj => mul_eq_zero_of_right (f k) (basis_on_evenSnd_other hkj) -lemma P_evenSnd_evenFst (f : Fin n.succ → ℚ) : P f ∘ evenSnd = - P f ∘ evenFst := by +lemma planeCharges_evenSnd_evenFst (f : Fin n.succ → ℚ) : + planeCharges f ∘ evenSnd = - planeCharges f ∘ evenFst := by funext j - simp [P_evenFst, P_evenSnd] + simp [planeCharges_evenFst, planeCharges_evenSnd] /-! @@ -353,13 +360,14 @@ lemma P_evenSnd_evenFst (f : Fin n.succ → ℚ) : P f ∘ evenSnd = - P f ∘ e -/ -lemma P_linearACC (f : Fin n.succ → ℚ) : (accGrav (2 * n.succ)) (P f) = 0 := by - simp [accGrav, sum_even, P_evenSnd, P_evenFst] +lemma planeCharges_linearACC (f : Fin n.succ → ℚ) : + (accGrav (2 * n.succ)) (planeCharges f) = 0 := by + simp [accGrav, sum_even, planeCharges_evenSnd, planeCharges_evenFst] -lemma P_accCube (f : Fin n.succ → ℚ) : accCube (2 * n.succ) (P f) = 0 := by +lemma planeCharges_accCube (f : Fin n.succ → ℚ) : accCube (2 * n.succ) (planeCharges f) = 0 := by rw [accCube_explicit, sum_even] refine Finset.sum_eq_zero fun i _ => ?_ - simp only [succ_eq_add_one, Function.comp_apply, P_evenFst, P_evenSnd] + simp only [succ_eq_add_one, Function.comp_apply, planeCharges_evenFst, planeCharges_evenSnd] ring /-! @@ -368,8 +376,8 @@ lemma P_accCube (f : Fin n.succ → ℚ) : accCube (2 * n.succ) (P f) = 0 := by -/ -lemma P_zero (f : Fin n.succ → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by - exact fun i => (P_evenFst f i).symm.trans (congr_fun h (evenFst i)) +lemma planeCharges_zero (f : Fin n.succ → ℚ) (h : planeCharges f = 0) : ∀ i, f i = 0 := by + exact fun i => (planeCharges_evenFst f i).symm.trans (congr_fun h (evenFst i)) /-! @@ -377,11 +385,11 @@ lemma P_zero (f : Fin n.succ → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by -/ -/-- A point in the span of the first part of the basis. -/ -def P' (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).LinSols := ∑ i, f i • basis i +/-- A point in the span of the unshifted part of the basis. -/ +def planeLinSols (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).LinSols := ∑ i, f i • basis i -lemma P'_val (f : Fin n.succ → ℚ) : (P' f).val = P f := by - simp only [succ_eq_add_one, P', P] +lemma planeLinSols_val (f : Fin n.succ → ℚ) : (planeLinSols f).val = planeCharges f := by + simp only [succ_eq_add_one, planeLinSols, planeCharges] funext i rw [sum_of_anomaly_free_linear, sum_of_charges] rfl @@ -395,12 +403,12 @@ lemma P'_val (f : Fin n.succ → ℚ) : (P' f).val = P f := by theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := by apply Fintype.linearIndependent_iff.mpr intro f h - change P' f = 0 at h - exact P_zero f ((P'_val f).symm.trans (congrArg _ h)) + change planeLinSols f = 0 at h + exact planeCharges_zero f ((planeLinSols_val f).symm.trans (congrArg _ h)) /-! -### B.12. Every vector-like even solution is in the span of the basis of the first plane +### B.12. Every vector-like even solution is in the span of the basis of the unshifted plane -/ @@ -414,13 +422,13 @@ lemma vectorLikeEven_in_span (S : (PureU1 (2 * n.succ)).LinSols) use f apply ACCSystemLinear.LinSols.ext rw [sortAFL_val] - erw [P'_val] + erw [planeLinSols_val] apply ext_even · intro i - rw [P_evenFst] + rw [planeCharges_evenFst] rfl · intro i - rw [P_evenSnd] + rw [planeCharges_evenSnd] have ht := hS i 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 @@ -429,14 +437,20 @@ lemma vectorLikeEven_in_span (S : (PureU1 (2 * n.succ)).LinSols) rw [h] rfl + + +end Unshifted + /-! -## C. The vectors of the basis spanning the second plane, via the shifted even split +## C. The shifted plane -/ -/-- The second part of the basis as charges. -/ -def basis!AsCharges (j : Fin n) : (PureU1 (2 * n.succ)).Charges := +namespace Shifted + +/-- The shifted part of the basis as charges. -/ +def basisAsCharges (j : Fin n) : (PureU1 (2 * n.succ)).Charges := fun i => if i = evenShiftFst j then 1 @@ -451,27 +465,27 @@ def basis!AsCharges (j : Fin n) : (PureU1 (2 * n.succ)).Charges := -/ -lemma basis!_on_evenShiftFst_self (j : Fin n) : basis!AsCharges j (evenShiftFst j) = 1 := by - simp [basis!AsCharges] +lemma basis_on_evenShiftFst_self (j : Fin n) : basisAsCharges j (evenShiftFst j) = 1 := by + simp [basisAsCharges] set_option backward.isDefEq.respectTransparency false in -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, if_neg h1, if_neg h2] +lemma basis_on_other {k : Fin n} {j : Fin (2 * n.succ)} (h1 : j ≠ evenShiftFst k) + (h2 : j ≠ evenShiftSnd k) : basisAsCharges k j = 0 := by + simp only [basisAsCharges, if_neg h1, if_neg h2] set_option backward.isDefEq.respectTransparency false in -lemma basis!_on_evenShiftFst_other {k j : Fin n} (h : k ≠ j) : - basis!AsCharges k (evenShiftFst j) = 0 := by +lemma basis_on_evenShiftFst_other {k j : Fin n} (h : k ≠ j) : + basisAsCharges k (evenShiftFst j) = 0 := by rw [ne_eq, Fin.ext_iff] at h - refine basis!_on_other ?_ ?_ <;> + refine basis_on_other ?_ ?_ <;> simp only [ne_eq, Fin.ext_iff, evenShiftFst, evenShiftSnd, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd] <;> omega set_option backward.isDefEq.respectTransparency false in -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, evenShiftSnd, evenShiftFst] +lemma basis_evenShiftSnd_eq_neg_evenShiftFst (j i : Fin n) : + basisAsCharges j (evenShiftSnd i) = - basisAsCharges j (evenShiftFst i) := by + simp only [basisAsCharges, succ_eq_add_one, evenShiftSnd, evenShiftFst] split <;> split any_goals split any_goals split @@ -490,24 +504,24 @@ lemma basis!_evenShftSnd_eq_neg_evenShiftFst (j i : Fin n) : all_goals omega -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_evenShiftSnd_self (j : Fin n) : basisAsCharges j (evenShiftSnd j) = - 1 := by + rw [basis_evenShiftSnd_eq_neg_evenShiftFst, basis_on_evenShiftFst_self] -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] +lemma basis_on_evenShiftSnd_other {k j : Fin n} (h : k ≠ j) : + basisAsCharges k (evenShiftSnd j) = 0 := by + rw [basis_evenShiftSnd_eq_neg_evenShiftFst, basis_on_evenShiftFst_other h] rfl set_option backward.isDefEq.respectTransparency false in -lemma basis!_on_evenShiftZero (j : Fin n) : basis!AsCharges j evenShiftZero = 0 := by - refine basis!_on_other ?_ ?_ <;> +lemma basis_on_evenShiftZero (j : Fin n) : basisAsCharges j evenShiftZero = 0 := by + refine basis_on_other ?_ ?_ <;> simp only [ne_eq, Fin.ext_iff, evenShiftZero, evenShiftFst, evenShiftSnd, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, Fin.val_eq_zero] <;> omega set_option backward.isDefEq.respectTransparency false in -lemma basis!_on_evenShiftLast (j : Fin n) : basis!AsCharges j evenShiftLast = 0 := by - refine basis!_on_other ?_ ?_ <;> +lemma basis_on_evenShiftLast (j : Fin n) : basisAsCharges j evenShiftLast = 0 := by + refine basis_on_other ?_ ?_ <;> simp only [ne_eq, Fin.ext_iff, evenShiftLast, evenShiftFst, evenShiftSnd, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, Fin.val_eq_zero, add_zero] <;> omega @@ -518,9 +532,9 @@ lemma basis!_on_evenShiftLast (j : Fin n) : basis!AsCharges j evenShiftLast = 0 -/ -lemma basis!_linearACC (j : Fin n) : (accGrav (2 * n.succ)) (basis!AsCharges j) = 0 := by - simp [accGrav, sum_evenShift, basis!_on_evenShiftZero, basis!_on_evenShiftLast, - basis!_evenShftSnd_eq_neg_evenShiftFst] +lemma basis_linearACC (j : Fin n) : (accGrav (2 * n.succ)) (basisAsCharges j) = 0 := by + simp [accGrav, sum_evenShift, basis_on_evenShiftZero, basis_on_evenShiftLast, + basis_evenShiftSnd_eq_neg_evenShiftFst] /-! @@ -528,14 +542,14 @@ lemma basis!_linearACC (j : Fin n) : (accGrav (2 * n.succ)) (basis!AsCharges j) -/ -lemma basis!_accCube (j : Fin n) : - accCube (2 * n.succ) (basis!AsCharges j) = 0 := by +lemma basis_accCube (j : Fin n) : + accCube (2 * n.succ) (basisAsCharges j) = 0 := by rw [accCube_explicit, sum_evenShift] - rw [basis!_on_evenShiftLast, basis!_on_evenShiftZero] + 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] refine Finset.sum_eq_zero fun i _ => ?_ - simp only [basis!_evenShftSnd_eq_neg_evenShiftFst] + simp only [basis_evenShiftSnd_eq_neg_evenShiftFst] ring /-! @@ -544,22 +558,22 @@ lemma basis!_accCube (j : Fin n) : -/ -/-- The second part of the basis as `LinSols`. -/ +/-- The shifted part of the basis as `LinSols`. -/ @[simps!] -def basis! (j : Fin n) : (PureU1 (2 * n.succ)).LinSols := - ⟨basis!AsCharges j, by +def basis (j : Fin n) : (PureU1 (2 * n.succ)).LinSols := + ⟨basisAsCharges j, by intro i match i with - | ⟨0, _⟩ => exact basis!_linearACC j⟩ + | ⟨0, _⟩ => exact basis_linearACC j⟩ /-! -### C.7. The inclusion of the second plane into charges +### C.7. The inclusion of the shifted plane into charges -/ -/-- A point in the span of the second part of the basis as a charge. -/ -def P! (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).Charges := ∑ i, f i • basis!AsCharges i +/-- A point in the span of the shifted part of the basis as a charge. -/ +def planeCharges (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).Charges := ∑ i, f i • basisAsCharges i /-! @@ -567,25 +581,27 @@ def P! (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).Charges := ∑ i, f i • bas -/ -lemma P!_evenShiftFst (f : Fin n → ℚ) (j : Fin n) : P! f (evenShiftFst j) = f j := by - rw [P!, sum_of_charges] +lemma planeCharges_evenShiftFst (f : Fin n → ℚ) (j : Fin n) : + planeCharges f (evenShiftFst j) = f j := by + rw [planeCharges, sum_of_charges] simp only [HSMul.hSMul, SMul.smul] rw [Fintype.sum_eq_single j] - · simp [basis!_on_evenShiftFst_self] - · exact fun k hkj => mul_eq_zero_of_right (f k) (basis!_on_evenShiftFst_other hkj) + · simp [basis_on_evenShiftFst_self] + · exact fun k hkj => mul_eq_zero_of_right (f k) (basis_on_evenShiftFst_other hkj) -lemma P!_evenShiftSnd (f : Fin n → ℚ) (j : Fin n) : P! f (evenShiftSnd j) = - f j := by - rw [P!, sum_of_charges] +lemma planeCharges_evenShiftSnd (f : Fin n → ℚ) (j : Fin n) : + planeCharges f (evenShiftSnd j) = - f j := by + rw [planeCharges, sum_of_charges] simp only [HSMul.hSMul, SMul.smul] rw [Fintype.sum_eq_single j] - · simp [basis!_on_evenShiftSnd_self] - · exact fun k hkj => mul_eq_zero_of_right (f k) (basis!_on_evenShiftSnd_other hkj) + · simp [basis_on_evenShiftSnd_self] + · exact fun k hkj => mul_eq_zero_of_right (f k) (basis_on_evenShiftSnd_other hkj) -lemma P!_evenShiftZero (f : Fin n → ℚ) : P! f (evenShiftZero) = 0 := by - simp [P!, sum_of_charges, HSMul.hSMul, SMul.smul, basis!_on_evenShiftZero] +lemma planeCharges_evenShiftZero (f : Fin n → ℚ) : planeCharges f (evenShiftZero) = 0 := by + simp [planeCharges, sum_of_charges, HSMul.hSMul, SMul.smul, basis_on_evenShiftZero] -lemma P!_evenShiftLast (f : Fin n → ℚ) : P! f evenShiftLast = 0 := by - simp [P!, sum_of_charges, HSMul.hSMul, SMul.smul, basis!_on_evenShiftLast] +lemma planeCharges_evenShiftLast (f : Fin n → ℚ) : planeCharges f evenShiftLast = 0 := by + simp [planeCharges, sum_of_charges, HSMul.hSMul, SMul.smul, basis_on_evenShiftLast] /-! @@ -593,12 +609,12 @@ lemma P!_evenShiftLast (f : Fin n → ℚ) : P! f evenShiftLast = 0 := by -/ -lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n.succ) (P! f) = 0 := by - rw [accCube_explicit, sum_evenShift, P!_evenShiftZero, P!_evenShiftLast] +lemma planeCharges_accCube (f : Fin n → ℚ) : accCube (2 * n.succ) (planeCharges f) = 0 := by + rw [accCube_explicit, sum_evenShift, planeCharges_evenShiftZero, planeCharges_evenShiftLast] simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero, Function.comp_apply, zero_add] refine Finset.sum_eq_zero fun i _ => ?_ - simp only [P!_evenShiftFst, P!_evenShiftSnd] + simp only [planeCharges_evenShiftFst, planeCharges_evenShiftSnd] ring /-! @@ -607,16 +623,17 @@ lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n.succ) (P! f) = 0 := by -/ -lemma P!_zero (f : Fin n → ℚ) (h : P! f = 0) : ∀ i, f i = 0 := by - exact fun i => (P!_evenShiftFst f i).symm.trans (congr_fun h (evenShiftFst i)) +lemma planeCharges_zero (f : Fin n → ℚ) (h : planeCharges f = 0) : ∀ i, f i = 0 := by + exact fun i => (planeCharges_evenShiftFst f i).symm.trans (congr_fun h (evenShiftFst i)) /-! -### C.11. The inclusion of the second plane into the span of the basis +### C.11. The inclusion of the shifted plane into the span of the basis -/ -lemma P!_in_span (f : Fin n → ℚ) : P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges) := by +lemma planeCharges_in_span (f : Fin n → ℚ) : + planeCharges f ∈ Submodule.span ℚ (Set.range basisAsCharges) := by exact (Submodule.mem_span_range_iff_exists_fun ℚ).mpr ⟨f, rfl⟩ /-! @@ -625,11 +642,11 @@ lemma P!_in_span (f : Fin n → ℚ) : P! f ∈ Submodule.span ℚ (Set.range ba -/ -/-- A point in the span of the second part of the basis. -/ -def P!' (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).LinSols := ∑ i, f i • basis! i +/-- A point in the span of the shifted part of the basis. -/ +def planeLinSols (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).LinSols := ∑ i, f i • basis i -lemma P!'_val (f : Fin n → ℚ) : (P!' f).val = P! f := by - simp only [succ_eq_add_one, P!', P!] +lemma planeLinSols_val (f : Fin n → ℚ) : (planeLinSols f).val = planeCharges f := by + simp only [succ_eq_add_one, planeLinSols, planeCharges] funext i rw [sum_of_anomaly_free_linear, sum_of_charges] rfl @@ -640,11 +657,11 @@ lemma P!'_val (f : Fin n → ℚ) : (P!' f).val = P! f := by -/ -theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by +theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := by apply Fintype.linearIndependent_iff.mpr intro f h - change P!' f = 0 at h - exact P!_zero f ((P!'_val f).symm.trans (congrArg _ h)) + change planeLinSols f = 0 at h + exact planeCharges_zero f ((planeLinSols_val f).symm.trans (congrArg _ h)) /-! @@ -652,9 +669,9 @@ theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by -/ -lemma smul_basis!AsCharges_in_span (S : (PureU1 (2 * n.succ)).LinSols) (j : Fin n) : - (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∈ - Submodule.span ℚ (Set.range basis!AsCharges) := by +lemma smul_basisAsCharges_in_span (S : (PureU1 (2 * n.succ)).LinSols) (j : Fin n) : + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basisAsCharges j ∈ + Submodule.span ℚ (Set.range basisAsCharges) := by exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨j, rfl⟩) /-! @@ -664,22 +681,26 @@ lemma smul_basis!AsCharges_in_span (S : (PureU1 (2 * n.succ)).LinSols) (j : Fin -/ /-- 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) + adding a vector basisAsCharges j. -/ +lemma swap_as_add {S S' : (PureU1 (2 * n.succ)).LinSols} (j : Fin n) (hS : ((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S = S') : - S'.val = S.val + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j := by + S'.val = S.val + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basisAsCharges j := by funext i rw [← hS, FamilyPermutations_anomalyFreeLinear_apply] by_cases hi : i = evenShiftFst j · subst hi - simp [HSMul.hSMul, basis!_on_evenShiftFst_self, Equiv.swap_apply_left] + simp [HSMul.hSMul, basis_on_evenShiftFst_self, Equiv.swap_apply_left] · by_cases hi2 : i = evenShiftSnd j - · simp [HSMul.hSMul, hi2, basis!_on_evenShiftSnd_self, Equiv.swap_apply_right] + · simp [HSMul.hSMul, hi2, basis_on_evenShiftSnd_self, Equiv.swap_apply_right] · simp only [succ_eq_add_one, Equiv.invFun_as_coe, HSMul.hSMul, ACCSystemCharges.chargesAddCommMonoid_add, ACCSystemCharges.chargesModule_smul] - rw [basis!_on_other hi hi2] + rw [basis_on_other hi hi2] aesop + + +end Shifted + /-! ## D. Mixed cubic ACCs involving points from both planes @@ -687,32 +708,34 @@ lemma swap!_as_add {S S' : (PureU1 (2 * n.succ)).LinSols} (j : Fin n) -/ lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) : - accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) + accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) + (Shifted.basisAsCharges j) = g (j.succ) ^ 2 - g (j.castSucc) ^ 2 := by simp only [succ_eq_add_one, accCubeTriLinSymm, TriLinearSymm.mk₃_toFun_apply_apply] - erw [sum_evenShift, basis!_on_evenShiftZero, basis!_on_evenShiftLast] + erw [sum_evenShift, Shifted.basis_on_evenShiftZero, Shifted.basis_on_evenShiftLast] simp only [mul_zero, add_zero, Function.comp_apply, zero_add] - rw [Fintype.sum_eq_single j, basis!_on_evenShiftFst_self, basis!_on_evenShiftSnd_self] + rw [Fintype.sum_eq_single j, Shifted.basis_on_evenShiftFst_self, + Shifted.basis_on_evenShiftSnd_self] · simp only [evenShiftFst_eq_evenFst_succ, mul_one, evenShiftSnd_eq_evenSnd_castSucc, mul_neg] - rw [P_evenFst, P_evenSnd] + rw [Unshifted.planeCharges_evenFst, Unshifted.planeCharges_evenSnd] ring · intro k hkj - erw [basis!_on_evenShiftFst_other hkj.symm, basis!_on_evenShiftSnd_other hkj.symm] + erw [Shifted.basis_on_evenShiftFst_other hkj.symm, Shifted.basis_on_evenShiftSnd_other hkj.symm] simp only [mul_zero, add_zero] lemma P_P!_P!_accCube (g : Fin n → ℚ) (j : Fin n.succ) : - accCubeTriLinSymm (P! g) (P! g) (basisAsCharges j) - = (P! g (evenFst j))^2 - (P! g (evenSnd j))^2 := by + accCubeTriLinSymm (Shifted.planeCharges g) (Shifted.planeCharges g) (Unshifted.basisAsCharges j) + = (Shifted.planeCharges g (evenFst j))^2 - (Shifted.planeCharges g (evenSnd j))^2 := by simp only [succ_eq_add_one, accCubeTriLinSymm, TriLinearSymm.mk₃_toFun_apply_apply] erw [sum_even] simp only [Function.comp_apply] - rw [Fintype.sum_eq_single j, basis_on_evenFst_self, basis_on_evenSnd_self] + rw [Fintype.sum_eq_single j, Unshifted.basis_on_evenFst_self, Unshifted.basis_on_evenSnd_self] · simp only [mul_one, mul_neg] ring · intro k hkj - erw [basis_on_evenFst_other hkj.symm, basis_on_evenSnd_other hkj.symm] + erw [Unshifted.basis_on_evenFst_other hkj.symm, Unshifted.basis_on_evenSnd_other hkj.symm] simp only [mul_zero, add_zero] /-! @@ -729,8 +752,8 @@ lemma P_P!_P!_accCube (g : Fin n → ℚ) (j : Fin n.succ) : /-- The whole basis as `LinSols`. -/ def basisa : (Fin n.succ) ⊕ (Fin n) → (PureU1 (2 * n.succ)).LinSols := fun i => match i with - | .inl i => basis i - | .inr i => basis! i + | .inl i => Unshifted.basis i + | .inr i => Shifted.basis i /-! @@ -739,7 +762,8 @@ def basisa : (Fin n.succ) ⊕ (Fin n) → (PureU1 (2 * n.succ)).LinSols := fun i -/ /-- 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 +def Pa (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n.succ)).Charges := + Unshifted.planeCharges f + Shifted.planeCharges g /-! @@ -751,25 +775,29 @@ 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!_evenShiftFst, evenShiftFst_eq_evenFst_succ, P_evenFst] + rw [Shifted.planeCharges_evenShiftFst, evenShiftFst_eq_evenFst_succ, + Unshifted.planeCharges_evenFst] 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!_evenShiftSnd, evenShiftSnd_eq_evenSnd_castSucc, P_evenSnd] + rw [Shifted.planeCharges_evenShiftSnd, evenShiftSnd_eq_evenSnd_castSucc, + Unshifted.planeCharges_evenSnd] ring 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!_evenShiftZero, evenShiftZero_eq_evenFst_zero, P_evenFst, add_zero] + rw [Shifted.planeCharges_evenShiftZero, evenShiftZero_eq_evenFst_zero, + Unshifted.planeCharges_evenFst, add_zero] 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!_evenShiftLast, evenShiftLast_eq_evenSnd_last, P_evenSnd, add_zero] + rw [Shifted.planeCharges_evenShiftLast, evenShiftLast_eq_evenSnd_last, + Unshifted.planeCharges_evenSnd, add_zero] /-! @@ -803,9 +831,9 @@ lemma Pa_zero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) : lemma Pa_zero! (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) : ∀ i, g i = 0 := by have hf := Pa_zero f g h - rw [Pa, P] at h + rw [Pa, Unshifted.planeCharges] at h simp only [succ_eq_add_one, hf, zero_smul, sum_const_zero, zero_add] at h - exact P!_zero g h + exact Shifted.planeCharges_zero g h /-! @@ -817,7 +845,7 @@ def Pa' (f : (Fin n.succ) ⊕ (Fin n) → ℚ) : (PureU1 (2 * n.succ)).LinSols : ∑ i, f i • basisa i lemma Pa'_P'_P!' (f : (Fin n.succ) ⊕ (Fin n) → ℚ) : - Pa' f = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr) := by + Pa' f = Unshifted.planeLinSols (f ∘ Sum.inl) + Shifted.planeLinSols (f ∘ Sum.inr) := by exact Fintype.sum_sum_type _ /-! @@ -832,7 +860,8 @@ theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n) := by change Pa' f = 0 at h have h1 : (Pa' f).val = 0 := congrArg _ h rw [Pa'_P'_P!'] at h1 - simp only [ACCSystemLinear.linSolsAddCommMonoid_add_val, P'_val, P!'_val] at h1 + simp only [ACCSystemLinear.linSolsAddCommMonoid_add_val, Unshifted.planeLinSols_val, + Shifted.planeLinSols_val] at h1 have hf := Pa_zero (f ∘ Sum.inl) (f ∘ Sum.inr) h1 have hg := Pa_zero! (f ∘ Sum.inl) (f ∘ Sum.inr) h1 rintro (i | i) @@ -864,7 +893,8 @@ lemma Pa'_elim_eq_iff (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) : rw [h.left, h.right] · apply ACCSystemLinear.LinSols.ext rw [Pa'_P'_P!', Pa'_P'_P!'] - simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, P'_val, P!'_val] + simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, + Unshifted.planeLinSols_val, Shifted.planeLinSols_val] exact h lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) : @@ -902,16 +932,18 @@ noncomputable def basisaAsBasis : -/ lemma span_basis (S : (PureU1 (2 * n.succ)).LinSols) : - ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f := by + ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), + S.val = Unshifted.planeCharges g + Shifted.planeCharges f := by have h := (Submodule.mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisaAsBasis S) obtain ⟨f, hf⟩ := h simp only [succ_eq_add_one, basisaAsBasis, coe_basisOfLinearIndependentOfCardEqFinrank, Fintype.sum_sum_type] at hf - change P' _ + P!' _ = S at hf + change Unshifted.planeLinSols _ + Shifted.planeLinSols _ = S at hf use f ∘ Sum.inl use f ∘ Sum.inr rw [← hf] - simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, P'_val, P!'_val] + simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, + Unshifted.planeLinSols_val, Shifted.planeLinSols_val] rfl /-! @@ -922,23 +954,26 @@ lemma span_basis (S : (PureU1 (2 * n.succ)).LinSols) : lemma span_basis_swap! {S : (PureU1 (2 * n.succ)).LinSols} (j : Fin n) (hS : ((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (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 (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 + (h : S.val = Unshifted.planeCharges g + Shifted.planeCharges f) : + ∃ (g' : Fin n.succ → ℚ) (f' : Fin n → ℚ), + S'.val = Unshifted.planeCharges g' + Shifted.planeCharges f' ∧ + Shifted.planeCharges f' = Shifted.planeCharges f + + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • Shifted.basisAsCharges j ∧ g' = g := by + let X := Shifted.planeCharges f + + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • Shifted.basisAsCharges j + have hX : X ∈ Submodule.span ℚ (Set.range (Shifted.basisAsCharges)) := by apply Submodule.add_mem - exact (P!_in_span f) - exact (smul_basis!AsCharges_in_span S j) + exact (Shifted.planeCharges_in_span f) + exact (Shifted.smul_basisAsCharges_in_span S j) have hXsum := (Submodule.mem_span_range_iff_exists_fun ℚ).mp hX obtain ⟨f', hf'⟩ := hXsum use g use f' - change P! f' = _ at hf' + change Shifted.planeCharges f' = _ at hf' erw [hf'] simp only [and_self, and_true, X] rw [← add_assoc, ← h] - apply swap!_as_add at hS + apply Shifted.swap_as_add at hS exact hS end VectorLikeEvenPlane diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean index cdec63a4e..cb651a819 100644 --- a/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean +++ b/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean @@ -16,7 +16,7 @@ if the line through that point and through the two different planes formed by th `LinSols` lies in the cubic. We show that for a solution all its permutations satisfy this property, then there exists -a permutation for which it lies in the plane spanned by the first part of the basis. +a permutation for which it lies in the unshifted plane. The main reference for this file is: @@ -37,30 +37,39 @@ open VectorLikeEvenPlane in the basis through that point is in the cubic. -/ def LineInCubic (S : (PureU1 (2 * n.succ)).LinSols) : Prop := ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ), - accCube (2 * n.succ) (a • P g + b • P! f) = 0 + accCube (2 * n.succ) (a • Unshifted.planeCharges g + b • Shifted.planeCharges f) = 0 set_option backward.isDefEq.respectTransparency false in lemma lineInCubic_expand {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) : ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ), - 3 * a * b * (a * accCubeTriLinSymm (P g) (P g) (P! f) - + b * accCubeTriLinSymm (P! f) (P! f) (P g)) = 0 := by + 3 * a * b * + (a * accCubeTriLinSymm (Unshifted.planeCharges g) + (Unshifted.planeCharges g) (Shifted.planeCharges f) + + b * accCubeTriLinSymm (Shifted.planeCharges f) + (Shifted.planeCharges f) (Unshifted.planeCharges g)) = 0 := by intro g f hS a b have h1 := h g f hS a b - change accCubeTriLinSymm.toCubic (a • P g + b • P! f) = 0 at h1 + change accCubeTriLinSymm.toCubic + (a • Unshifted.planeCharges g + b • Shifted.planeCharges f) = 0 at h1 simp only [TriLinearSymm.toCubic_add, HomogeneousCubic.map_smul, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1 - erw [P_accCube, P!_accCube] at h1 + erw [Unshifted.planeCharges_accCube, Shifted.planeCharges_accCube] at h1 linear_combination h1 /-- This lemma states that for a given `S` of type `(PureU1 (2 * n.succ)).AnomalyFreeLinear` and a proof `h` that the line through `S` lies on a cubic curve, -for any functions `g : Fin n.succ → ℚ` and `f : Fin n → ℚ`, if `S.val = P g + P! f`, -then `accCubeTriLinSymm.toFun (P g, P g, P! f) = 0`. +for any functions `g : Fin n.succ → ℚ` and `f : Fin n → ℚ`, if +`S.val = Unshifted.planeCharges g + Shifted.planeCharges f`, +then +`accCubeTriLinSymm.toFun (Unshifted.planeCharges g, Unshifted.planeCharges g, + Shifted.planeCharges f) = 0`. -/ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) : - ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f), - accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by + ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) + (_ : S.val = Unshifted.planeCharges g + Shifted.planeCharges f), + accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) + (Shifted.planeCharges f) = 0 := by intro g f hS linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) - (lineInCubic_expand h g f hS 1 2) / 6 @@ -88,7 +97,8 @@ 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 (evenShiftSnd j) - S.val (evenShiftFst j)) - * accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := by + * accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) + (Shifted.basisAsCharges j) = 0 := by intro j g f h obtain ⟨g', f', hall⟩ := span_basis_swap! j rfl g f h have h1 := line_in_cubic_P_P_P! (lineInCubicPerm_self LIC) g f h @@ -100,7 +110,8 @@ 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)) = + accCubeTriLinSymm (Unshifted.planeCharges f) (Unshifted.planeCharges f) + (Shifted.basisAsCharges (Fin.last n)) = - (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 @@ -144,8 +155,8 @@ theorem lineInCubicPerm_vectorLike {S : (PureU1 (2 * n.succ.succ)).Sols} theorem lineInCubicPerm_in_plane (S : (PureU1 (2 * n.succ.succ)).Sols) (LIC : LineInCubicPerm S.1.1) : ∃ (M : (FamilyPermutations (2 * n.succ.succ)).group), (FamilyPermutations (2 * n.succ.succ)).linSolRep M S.1.1 - ∈ Submodule.span ℚ (Set.range basis) := - vectorLikeEven_in_span S.1.1 (lineInCubicPerm_vectorLike LIC) + ∈ Submodule.span ℚ (Set.range Unshifted.basis) := + Unshifted.vectorLikeEven_in_span S.1.1 (lineInCubicPerm_vectorLike LIC) end Even end PureU1 diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/Parameterization.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/Parameterization.lean index 5c469ac08..409df478a 100644 --- a/Physlib/QFT/QED/AnomalyCancellation/Even/Parameterization.lean +++ b/Physlib/QFT/QED/AnomalyCancellation/Even/Parameterization.lean @@ -11,7 +11,7 @@ public import Physlib.QFT.QED.AnomalyCancellation.Even.LineInCubic Given maps `g : Fin n.succ → ℚ`, `f : Fin n → ℚ` and `a : ℚ` we form a solution to the anomaly equations. We show that every solution can be got in this way, up to permutation, unless it, up to -permutation, lives in the plane spanned by the first part of the basis vector. +permutation, lives in the unshifted plane. The main reference is: @@ -29,22 +29,29 @@ open BigOperators variable {n : ℕ} open VectorLikeEvenPlane -/-- Given coefficients `g` of a point in `P` and `f` of a point in `P!`, and a rational, we get a +/-- Given coefficients `g` of a point in the unshifted plane and `f` of a point in the +shifted plane, and a rational, we get a rational `a ∈ ℚ`, we get a point in `(PureU1 (2 * n.succ)).AnomalyFreeLinear`, which we will later show extends to an anomaly free point. -/ def parameterizationAsLinear (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) : (PureU1 (2 * n.succ)).LinSols := - a • ((accCubeTriLinSymm (P! f) (P! f) (P g)) • P' g + - (- accCubeTriLinSymm (P g) (P g) (P! f)) • P!' f) + a • + ((accCubeTriLinSymm (Shifted.planeCharges f) (Shifted.planeCharges f) + (Unshifted.planeCharges g)) • Unshifted.planeLinSols g + + (- accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) + (Shifted.planeCharges f)) • Shifted.planeLinSols f) lemma parameterizationAsLinear_val (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) : (parameterizationAsLinear g f a).val = - a • ((accCubeTriLinSymm (P! f) (P! f) (P g)) • P g + - (- accCubeTriLinSymm (P g) (P g) (P! f)) • P! f) := by + a • + ((accCubeTriLinSymm (Shifted.planeCharges f) (Shifted.planeCharges f) + (Unshifted.planeCharges g)) • Unshifted.planeCharges g + + (- accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) + (Shifted.planeCharges f)) • Shifted.planeCharges f) := by rw [parameterizationAsLinear] - change a • (_ • (P' g).val + _ • (P!' f).val) = _ - rw [P'_val, P!'_val] + change a • (_ • (Unshifted.planeLinSols g).val + _ • (Shifted.planeLinSols f).val) = _ + rw [Unshifted.planeLinSols_val, Shifted.planeLinSols_val] set_option backward.isDefEq.respectTransparency false in lemma parameterizationCharge_cube (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) : @@ -52,7 +59,7 @@ lemma parameterizationCharge_cube (g : Fin n.succ → ℚ) (f : Fin n → ℚ) ( change accCubeTriLinSymm.toCubic _ = 0 rw [parameterizationAsLinear_val, HomogeneousCubic.map_smul, TriLinearSymm.toCubic_add, HomogeneousCubic.map_smul, HomogeneousCubic.map_smul] - erw [P_accCube, P!_accCube] + erw [Unshifted.planeCharges_accCube, Shifted.planeCharges_accCube] rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] @@ -65,23 +72,34 @@ def parameterization (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) : parameterizationCharge_cube g f a⟩ lemma anomalyFree_param {S : (PureU1 (2 * n.succ)).Sols} - (g : Fin n.succ → ℚ) (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 + (g : Fin n.succ → ℚ) (f : Fin n → ℚ) + (hS : S.val = Unshifted.planeCharges g + Shifted.planeCharges f) : + accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) + (Shifted.planeCharges f) = + - accCubeTriLinSymm (Shifted.planeCharges f) (Shifted.planeCharges f) + (Unshifted.planeCharges g) := by have hC := S.cubicSol rw [hS] at hC - change (accCube (2 * n.succ)) (P g + P! f) = 0 at hC - erw [TriLinearSymm.toCubic_add, P_accCube, P!_accCube] at hC + change (accCube (2 * n.succ)) (Unshifted.planeCharges g + Shifted.planeCharges f) = 0 at hC + erw [TriLinearSymm.toCubic_add, Unshifted.planeCharges_accCube, + Shifted.planeCharges_accCube] at hC linear_combination hC / 3 -/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠ 0`. +/-- A proposition on a solution which is true if +`accCubeTriLinSymm (Unshifted.planeCharges g, Unshifted.planeCharges g, + Shifted.planeCharges f) ≠ 0`. In this case our parameterization above will be able to recover this point. -/ def GenericCase (S : (PureU1 (2 * n.succ)).Sols) : Prop := - ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f), - accCubeTriLinSymm (P g) (P g) (P! f) ≠ 0 + ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) + (_ : S.val = Unshifted.planeCharges g + Shifted.planeCharges f), + accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) + (Shifted.planeCharges f) ≠ 0 lemma genericCase_exists (S : (PureU1 (2 * n.succ)).Sols) - (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f ∧ - accCubeTriLinSymm (P g) (P g) (P! f) ≠ 0) : GenericCase S := by + (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), + S.val = Unshifted.planeCharges g + Shifted.planeCharges f ∧ + accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) + (Shifted.planeCharges f) ≠ 0) : GenericCase S := by intro g f hS hC obtain ⟨g', f', hS', hC'⟩ := hs rw [hS] at hS' @@ -89,14 +107,20 @@ lemma genericCase_exists (S : (PureU1 (2 * n.succ)).Sols) rw [hS'.1, hS'.2] at hC exact hC' hC -/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) = 0`. -/ +/-- A proposition on a solution which is true if +`accCubeTriLinSymm (Unshifted.planeCharges g, Unshifted.planeCharges g, + Shifted.planeCharges f) = 0`. -/ def SpecialCase (S : (PureU1 (2 * n.succ)).Sols) : Prop := - ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f), - accCubeTriLinSymm (P g) (P g) (P! f) = 0 + ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) + (_ : S.val = Unshifted.planeCharges g + Shifted.planeCharges f), + accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) + (Shifted.planeCharges f) = 0 lemma specialCase_exists (S : (PureU1 (2 * n.succ)).Sols) - (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f ∧ - accCubeTriLinSymm (P g) (P g) (P! f) = 0) : SpecialCase S := by + (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), + S.val = Unshifted.planeCharges g + Shifted.planeCharges f ∧ + accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) + (Shifted.planeCharges f) = 0) : SpecialCase S := by intro g f hS obtain ⟨g', f', hS', hC'⟩ := hs rw [hS] at hS' @@ -107,8 +131,10 @@ lemma specialCase_exists (S : (PureU1 (2 * n.succ)).Sols) lemma generic_or_special (S : (PureU1 (2 * n.succ)).Sols) : GenericCase S ∨ SpecialCase S := by 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 + have h1 : accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) + (Shifted.planeCharges f) ≠ 0 ∨ + accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) + (Shifted.planeCharges f) = 0 := by exact ne_or_eq _ _ rcases h1 with h1 | h1 · exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩) @@ -117,7 +143,9 @@ lemma generic_or_special (S : (PureU1 (2 * n.succ)).Sols) : theorem generic_case {S : (PureU1 (2 * n.succ)).Sols} (h : GenericCase S) : ∃ g f a, S = parameterization g f a := by obtain ⟨g, f, hS⟩ := span_basis S.1.1 - use g, f, (accCubeTriLinSymm (P! f) (P! f) (P g))⁻¹ + use g, f, + (accCubeTriLinSymm (Shifted.planeCharges f) (Shifted.planeCharges f) + (Unshifted.planeCharges g))⁻¹ rw [parameterization] apply ACCSystem.Sols.ext rw [parameterizationAsLinear_val] @@ -135,14 +163,15 @@ lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols} intro g f hS a b erw [TriLinearSymm.toCubic_add] rw [HomogeneousCubic.map_smul, HomogeneousCubic.map_smul] - erw [P_accCube, P!_accCube] + erw [Unshifted.planeCharges_accCube, Shifted.planeCharges_accCube] have h := h g f hS rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃, h] rw [anomalyFree_param _ _ hS] 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 + change accCubeTriLinSymm (Shifted.planeCharges f) (Shifted.planeCharges f) + (Unshifted.planeCharges g) = 0 at h erw [h] simp @@ -157,7 +186,7 @@ theorem special_case {S : (PureU1 (2 * n.succ.succ)).Sols} SpecialCase ((FamilyPermutations (2 * n.succ.succ)).solAction.toFun _ _ S M)) : ∃ (M : (FamilyPermutations (2 * n.succ.succ)).group), ((FamilyPermutations (2 * n.succ.succ)).solAction.toFun _ _ S M).1.1 - ∈ Submodule.span ℚ (Set.range basis) := + ∈ Submodule.span ℚ (Set.range Unshifted.basis) := lineInCubicPerm_in_plane S (special_case_lineInCubic_perm h) end Even From 8d226bacd20f03cef01bc494f4201a5201fd3e09 Mon Sep 17 00:00:00 2001 From: catlover-bot Date: Tue, 11 Aug 2026 23:11:10 +0900 Subject: [PATCH 2/3] refactor(QED): update mixed-plane lemma names --- .../QED/AnomalyCancellation/Even/BasisLinear.lean | 4 ++-- .../QED/AnomalyCancellation/Even/LineInCubic.lean | 12 ++++++------ 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean index 1c20acde2..4e1d7f733 100644 --- a/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean +++ b/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean @@ -707,7 +707,7 @@ end Shifted -/ -lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) : +lemma unshifted_unshifted_shifted_accCube (g : Fin n.succ → ℚ) (j : Fin n) : accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) (Shifted.basisAsCharges j) = g (j.succ) ^ 2 - g (j.castSucc) ^ 2 := by @@ -724,7 +724,7 @@ lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) : erw [Shifted.basis_on_evenShiftFst_other hkj.symm, Shifted.basis_on_evenShiftSnd_other hkj.symm] simp only [mul_zero, add_zero] -lemma P_P!_P!_accCube (g : Fin n → ℚ) (j : Fin n.succ) : +lemma shifted_shifted_unshifted_accCube (g : Fin n → ℚ) (j : Fin n.succ) : accCubeTriLinSymm (Shifted.planeCharges g) (Shifted.planeCharges g) (Unshifted.basisAsCharges j) = (Shifted.planeCharges g (evenFst j))^2 - (Shifted.planeCharges g (evenSnd j))^2 := by simp only [succ_eq_add_one, accCubeTriLinSymm, diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean index cb651a819..353d0c722 100644 --- a/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean +++ b/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean @@ -65,7 +65,7 @@ then `accCubeTriLinSymm.toFun (Unshifted.planeCharges g, Unshifted.planeCharges g, Shifted.planeCharges f) = 0`. -/ -lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) : +lemma line_in_cubic_unshifted_unshifted_shifted {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) : ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Unshifted.planeCharges g + Shifted.planeCharges f), accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) @@ -101,21 +101,21 @@ lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ)).LinSols} (Shifted.basisAsCharges j) = 0 := by intro j g f h obtain ⟨g', f', hall⟩ := span_basis_swap! j rfl 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! + have h1 := line_in_cubic_unshifted_unshifted_shifted (lineInCubicPerm_self LIC) g f h + have h2 := line_in_cubic_unshifted_unshifted_shifted (lineInCubicPerm_self (lineInCubicPerm_permute LIC (Equiv.swap (evenShiftFst j) (evenShiftSnd j)))) g' f' hall.1 rw [hall.2.1, hall.2.2, accCubeTriLinSymm.map_add₃, h1, accCubeTriLinSymm.map_smul₃] at h2 simpa using h2 -lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ)).LinSols} +lemma unshifted_unshifted_shifted_accCube' {S : (PureU1 (2 * n.succ.succ)).LinSols} (f : Fin n.succ.succ → ℚ) (g : Fin n.succ → ℚ) (hS : S.val = Pa f g) : accCubeTriLinSymm (Unshifted.planeCharges f) (Unshifted.planeCharges f) (Shifted.basisAsCharges (Fin.last n)) = - (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), hS, Pa_evenShiftSnd, Pa_evenShiftFst, Pa_evenShiftLast, + rw [unshifted_unshifted_shifted_accCube f (Fin.last n), hS, Pa_evenShiftSnd, Pa_evenShiftFst, Pa_evenShiftLast, Fin.succ_last] ring @@ -126,7 +126,7 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols} (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 + rw [unshifted_unshifted_shifted_accCube' g f hfg] at h1 simp only [Nat.succ_eq_add_one, neg_add_rev, mul_eq_zero] at h1 rcases h1 with h1 | h1 | h1 · exact Or.inl (by linear_combination h1) From 17aebe797abe38627163c28915d728c84d92106c Mon Sep 17 00:00:00 2001 From: catlover-bot Date: Tue, 11 Aug 2026 23:14:20 +0900 Subject: [PATCH 3/3] style(QED): wrap renamed mixed-plane lemmas --- Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean index 353d0c722..59e6809ba 100644 --- a/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean +++ b/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean @@ -65,7 +65,8 @@ then `accCubeTriLinSymm.toFun (Unshifted.planeCharges g, Unshifted.planeCharges g, Shifted.planeCharges f) = 0`. -/ -lemma line_in_cubic_unshifted_unshifted_shifted {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) : +lemma line_in_cubic_unshifted_unshifted_shifted + {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) : ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Unshifted.planeCharges g + Shifted.planeCharges f), accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g) @@ -115,8 +116,8 @@ lemma unshifted_unshifted_shifted_accCube' {S : (PureU1 (2 * n.succ.succ)).LinSo - (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 [unshifted_unshifted_shifted_accCube f (Fin.last n), hS, Pa_evenShiftSnd, Pa_evenShiftFst, Pa_evenShiftLast, - Fin.succ_last] + rw [unshifted_unshifted_shifted_accCube f (Fin.last n), hS, Pa_evenShiftSnd, + Pa_evenShiftFst, Pa_evenShiftLast, Fin.succ_last] ring lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}