diff --git a/Physlib.lean b/Physlib.lean index 580bb2490..a202772e7 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -220,14 +220,14 @@ public import Physlib.QFT.PerturbationTheory.WickContraction.UncontractedList public import Physlib.QFT.QED.AnomalyCancellation.Basic public import Physlib.QFT.QED.AnomalyCancellation.BasisLinear public import Physlib.QFT.QED.AnomalyCancellation.ConstAbs -public import Physlib.QFT.QED.AnomalyCancellation.Even.BasisLinear +public import Physlib.QFT.QED.AnomalyCancellation.Even.Basis public import Physlib.QFT.QED.AnomalyCancellation.Even.LineInCubic public import Physlib.QFT.QED.AnomalyCancellation.Even.Parameterization public import Physlib.QFT.QED.AnomalyCancellation.LineInPlaneCond public import Physlib.QFT.QED.AnomalyCancellation.LowDim.One public import Physlib.QFT.QED.AnomalyCancellation.LowDim.Three public import Physlib.QFT.QED.AnomalyCancellation.LowDim.Two -public import Physlib.QFT.QED.AnomalyCancellation.Odd.BasisLinear +public import Physlib.QFT.QED.AnomalyCancellation.Odd.Basis public import Physlib.QFT.QED.AnomalyCancellation.Odd.LineInCubic public import Physlib.QFT.QED.AnomalyCancellation.Odd.Parameterization public import Physlib.QFT.QED.AnomalyCancellation.Permutations diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/Basis.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/Basis.lean new file mode 100644 index 000000000..d31ca55db --- /dev/null +++ b/Physlib/QFT/QED/AnomalyCancellation/Even/Basis.lean @@ -0,0 +1,359 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +module + +public import Physlib.QFT.QED.AnomalyCancellation.Even.Planes.ShiftPlane +/-! + +# The combined basis of the symmetric and shifted planes + +## i. Overview + +This module constructs the combined basis for the linear solutions of +`PureU1 (2 * n.succ)` by combining the two ACC-satisfying planes: + +- The *symmetric plane*, named after the symmetric (even) split `n.succ + n.succ`. + Its key results are `symmPlane` (the inclusion into linear solutions) and + `symmPlaneAsCharges_accCube` (every point satisfies the cubic anomaly cancellation condition). + +- The *shifted plane*, named after the shifted split `1 + (n + n + 1)`. + Its key results are `shiftPlane` (the inclusion into linear solutions) and + `shiftPlaneAsCharges_accCube` (every point satisfies the cubic anomaly cancellation condition). + +The main result is `span_basis`: every linear solution of `PureU1 (2 * n.succ)` can +be written as the sum of a point from the symmetric plane and a point from the shifted +plane. + +## ii. Key results + +- `basis` : The combined basis vectors from both planes +- `basis_linear_independent` : The combined basis vectors are linearly independent +- `basisAsBasis` : The combined basis vectors form a basis +- `span_basis` : Every linear solution is the sum of a point from each plane + +## iii. Table of contents + +- 1. The combined basis + - 1.1. As a map into linear solutions + - 1.2. Inclusion of the span of the basis into charges + - 1.3. Components of the inclusion into charges + - 1.4. Kernel of the inclusion into charges + - 1.5. The inclusion of the span of the basis into linear solutions + - 1.6. The combined basis vectors are linearly independent + - 1.7. Injectivity of the inclusion into linear solutions + - 1.8. Cardinality of the basis + - 1.9. The basis vectors as a basis +- 2. Every linear solution is the sum of a point from each plane + - 2.1. Relation under permutations +- 3. Mixed cubic anomaly cancellation conditions involving both planes + +## iv. References + +- https://arxiv.org/pdf/1912.04804.pdf + +-/ + +@[expose] public section + +open Nat Module Finset BigOperators + +namespace PureU1 + +variable {n : ℕ} + +namespace VectorLikeEvenPlane + +/-! + +## 1. The combined basis + +-/ + +/-! + +### 1.1. As a map into linear solutions + +-/ +/-- The whole basis as `LinSols`. -/ +def basis : (Fin n.succ) ⊕ (Fin n) → (PureU1 (2 * n.succ)).LinSols := fun i => + match i with + | .inl i => symmBasis i + | .inr i => shiftBasis i + +/-! + +### 1.2. Inclusion of the span of the basis into charges + +-/ + +/-- A point in the span of the basis as a charge. -/ +def basisCharge (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n.succ)).Charges := + symmPlaneAsCharges f + shiftPlaneAsCharges g + +/-! + +### 1.3. Components of the inclusion into charges + +-/ + +lemma basisCharge_evenShiftFst (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) : + basisCharge f g (evenShiftFst j) = f j.succ + g j := by + rw [basisCharge] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + rw [shiftPlaneAsCharges_evenShiftFst, evenShiftFst_eq_evenFst_succ, symmPlaneAsCharges_evenFst] + +lemma basisCharge_evenShiftSnd (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) : + basisCharge f g (evenShiftSnd j) = - f j.castSucc - g j := by + rw [basisCharge] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + rw [shiftPlaneAsCharges_evenShiftSnd, evenShiftSnd_eq_evenSnd_castSucc, symmPlaneAsCharges_evenSnd] + ring + +lemma basisCharge_evenShiftZero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : + basisCharge f g (evenShiftZero) = f 0 := by + rw [basisCharge] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + rw [shiftPlaneAsCharges_evenShiftZero, evenShiftZero_eq_evenFst_zero, symmPlaneAsCharges_evenFst] + exact Rat.add_zero (f 0) + +lemma basisCharge_evenShiftLast (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : + basisCharge f g (evenShiftLast) = - f (Fin.last n) := by + rw [basisCharge] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + rw [shiftPlaneAsCharges_evenShiftLast, evenShiftLast_eq_evenSnd_last, symmPlaneAsCharges_evenSnd] + exact Rat.add_zero (-f (Fin.last n)) + +/-! + +### 1.4. Kernel of the inclusion into charges + +-/ + +set_option backward.isDefEq.respectTransparency false in +lemma basisCharge_zero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : basisCharge f g = 0) : + ∀ i, f i = 0 := by + have h₃ := basisCharge_evenShiftZero f g + rw [h] at h₃ + change 0 = f 0 at h₃ + intro i + have hinduc (iv : ℕ) (hiv : iv < n.succ) : f ⟨iv, hiv⟩ = 0 := by + induction iv + exact h₃.symm + rename_i iv hi + have hivi : iv < n.succ := lt_of_succ_lt hiv + have hi2 := hi hivi + have h1 := basisCharge_evenShiftFst f g ⟨iv, succ_lt_succ_iff.mp hiv⟩ + have h2 := basisCharge_evenShiftSnd f g ⟨iv, succ_lt_succ_iff.mp hiv⟩ + rw [h] at h1 h2 + simp only [Fin.succ_mk, Fin.castSucc_mk] at h1 h2 + erw [hi2] at h2 + change 0 = _ at h2 + simp only [neg_zero, zero_sub, zero_eq_neg] at h2 + rw [h2] at h1 + exact right_eq_add.mp h1 + exact hinduc i.val i.prop + +lemma basisCharge_zero_shift (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : basisCharge f g = 0) : + ∀ i, g i = 0 := by + have hf := basisCharge_zero f g h + rw [basisCharge, symmPlaneAsCharges] at h + simp only [succ_eq_add_one, hf, zero_smul, sum_const_zero, zero_add] at h + exact shiftPlaneAsCharges_zero g h + +/-! + +### 1.5. The inclusion of the span of the basis into linear solutions + +-/ +/-- A point in the span of the whole basis. -/ +def spanBasis (f : (Fin n.succ) ⊕ (Fin n) → ℚ) : (PureU1 (2 * n.succ)).LinSols := + ∑ i, f i • basis i + +lemma spanBasis_symmPlane_shiftPlane (f : (Fin n.succ) ⊕ (Fin n) → ℚ) : + spanBasis f = symmPlane (f ∘ Sum.inl) + shiftPlane (f ∘ Sum.inr) := by + exact Fintype.sum_sum_type _ + +/-! + +### 1.6. The combined basis vectors are linearly independent + +-/ + +theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := by + apply Fintype.linearIndependent_iff.mpr + intro f h + change spanBasis f = 0 at h + have h1 : (spanBasis f).val = 0 := + (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0) + (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h)))) + (ACCSystemLinear.LinSols.val 0))).mp rfl + rw [spanBasis_symmPlane_shiftPlane] at h1 + change (symmPlane (f ∘ Sum.inl)).val + + (shiftPlane (f ∘ Sum.inr)).val = 0 at h1 + rw [shiftPlane_val, symmPlane_val] at h1 + change basisCharge (f ∘ Sum.inl) (f ∘ Sum.inr) = 0 at h1 + have hf := basisCharge_zero (f ∘ Sum.inl) (f ∘ Sum.inr) h1 + have hg := basisCharge_zero_shift (f ∘ Sum.inl) (f ∘ Sum.inr) h1 + intro i + simp_all + cases i + · simp_all + · simp_all +/-! + +### 1.7. Injectivity of the inclusion into linear solutions + +-/ + +lemma spanBasis_eq (f f' : (Fin n.succ) ⊕ (Fin n) → ℚ) : spanBasis f = spanBasis f' ↔ f = f' := by + refine Iff.intro (fun h => (funext (fun i => ?_))) (fun h => ?_) + · rw [spanBasis, spanBasis] at h + have h1 : ∑ i : Fin (succ n) ⊕ Fin n, (f i + (- f' i)) • basis i = 0 := by + simp only [add_smul, neg_smul] + rw [Finset.sum_add_distrib] + rw [h] + rw [← Finset.sum_add_distrib] + simp + have h2 : ∀ i, (f i + (- f' i)) = 0 := by + exact Fintype.linearIndependent_iff.mp (@basis_linear_independent n) + (fun i => f i + -f' i) h1 + have h2i := h2 i + linarith + · rw [h] + +lemma spanBasis_elim_eq_iff (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) : + spanBasis (Sum.elim g f) = spanBasis (Sum.elim g' f') ↔ basisCharge g f = basisCharge g' f' := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + · rw [spanBasis_eq, Sum.elim_eq_iff] at h + rw [h.left, h.right] + · apply ACCSystemLinear.LinSols.ext + rw [spanBasis_symmPlane_shiftPlane, spanBasis_symmPlane_shiftPlane] + simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, + symmPlane_val, shiftPlane_val] + exact h + +lemma basisCharge_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) : + basisCharge g f = basisCharge g' f' ↔ g = g' ∧ f = f' := by + rw [← spanBasis_elim_eq_iff, ← Sum.elim_eq_iff] + exact spanBasis_eq _ _ + +/-! + +### 1.8. Cardinality of the basis + +-/ + +lemma basis_card : Fintype.card ((Fin n.succ) ⊕ (Fin n)) = + Module.finrank ℚ (PureU1 (2 * n.succ)).LinSols := by + erw [BasisLinear.finrank_AnomalyFreeLinear] + simp only [Fintype.card_sum, Fintype.card_fin, mul_eq] + exact split_odd n + +/-! + +### 1.9. The basis vectors as a basis + +-/ + +/-- The basis formed out of our `basis` vectors. -/ +noncomputable def basisAsBasis : + Basis (Fin (succ n) ⊕ Fin n) ℚ (PureU1 (2 * succ n)).LinSols := + basisOfLinearIndependentOfCardEqFinrank (@basis_linear_independent n) basis_card + +/-! + +## 2. Every linear solution is the sum of a point from each plane + +-/ + +lemma span_basis (S : (PureU1 (2 * n.succ)).LinSols) : + ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = symmPlaneAsCharges g + shiftPlaneAsCharges f := by + have h := (Submodule.mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisAsBasis S) + obtain ⟨f, hf⟩ := h + simp only [succ_eq_add_one, basisAsBasis, coe_basisOfLinearIndependentOfCardEqFinrank, + Fintype.sum_sum_type] at hf + change symmPlane _ + shiftPlane _ = S at hf + use f ∘ Sum.inl + use f ∘ Sum.inr + rw [← hf] + simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, + symmPlane_val, shiftPlane_val] + rfl + +/-! + +### 2.1. Relation under permutations + +-/ +lemma span_basis_swapShift {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 = symmPlaneAsCharges g + shiftPlaneAsCharges f) : ∃ (g' : Fin n.succ → ℚ) (f' : Fin n → ℚ), + S'.val = symmPlaneAsCharges g' + shiftPlaneAsCharges f' ∧ shiftPlaneAsCharges f' = shiftPlaneAsCharges f + + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • shiftBasisAsCharges j ∧ g' = g := by + let X := shiftPlaneAsCharges f + + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • shiftBasisAsCharges j + have hX : X ∈ Submodule.span ℚ (Set.range (shiftBasisAsCharges)) := by + apply Submodule.add_mem + exact (shiftPlaneAsCharges_in_span f) + exact (smul_shiftBasisAsCharges_in_span S j) + have hXsum := (Submodule.mem_span_range_iff_exists_fun ℚ).mp hX + obtain ⟨f', hf'⟩ := hXsum + use g + use f' + change shiftPlaneAsCharges f' = _ at hf' + erw [hf'] + simp only [and_self, and_true, X] + rw [← add_assoc, ← h] + apply linSolRep_swap_evenShift_eq_add at hS + exact hS + +/-! + +## 3. Mixed cubic anomaly cancellation conditions involving both planes + +-/ + +set_option backward.isDefEq.respectTransparency false in +lemma symmPlane_symmPlane_shiftBasisAsCharges_accCube (g : Fin n.succ → ℚ) (j : Fin n) : + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftBasisAsCharges j) + = 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_evenShift, shiftBasisAsCharges_on_evenShiftZero, shiftBasisAsCharges_on_evenShiftLast] + simp only [mul_zero, add_zero, Function.comp_apply, zero_add] + rw [Finset.sum_eq_single j, shiftBasisAsCharges_on_evenShiftFst_self, + shiftBasisAsCharges_on_evenShiftSnd_self] + · simp only [evenShiftFst_eq_evenFst_succ, mul_one, evenShiftSnd_eq_evenSnd_castSucc, mul_neg] + rw [symmPlaneAsCharges_evenFst, symmPlaneAsCharges_evenSnd] + ring + · intro k _ hkj + erw [shiftBasisAsCharges_on_evenShiftFst_other hkj.symm, + shiftBasisAsCharges_on_evenShiftSnd_other hkj.symm] + simp only [mul_zero, add_zero] + · simp + +set_option backward.isDefEq.respectTransparency false in +lemma shiftPlane_shiftPlane_symmBasisAsCharges_accCube (g : Fin n → ℚ) (j : Fin n.succ) : + accCubeTriLinSymm (shiftPlaneAsCharges g) (shiftPlaneAsCharges g) (symmBasisAsCharges j) + = (shiftPlaneAsCharges g (evenFst j))^2 - (shiftPlaneAsCharges g (evenSnd j))^2 := by + simp only [succ_eq_add_one, accCubeTriLinSymm, PureU1Charges_numberCharges, + TriLinearSymm.mk₃_toFun_apply_apply] + rw [sum_even] + simp only [Function.comp_apply] + rw [Finset.sum_eq_single j, symmBasisAsCharges_on_evenFst_self, + symmBasisAsCharges_on_evenSnd_self] + · simp only [mul_one, mul_neg] + ring + · intro k _ hkj + erw [symmBasisAsCharges_on_evenFst_other hkj.symm, + symmBasisAsCharges_on_evenSnd_other hkj.symm] + simp only [mul_zero, add_zero] + · simp + +end VectorLikeEvenPlane + +end PureU1 diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean deleted file mode 100644 index d36052459..000000000 --- a/Physlib/QFT/QED/AnomalyCancellation/Even/BasisLinear.lean +++ /dev/null @@ -1,1056 +0,0 @@ -/- -Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Tooby-Smith --/ -module - -public import Physlib.QFT.QED.AnomalyCancellation.BasisLinear -public import Physlib.QFT.QED.AnomalyCancellation.VectorLike -/-! - -# Splitting the linear solutions in the even case into two ACC-satisfying planes - -## i. Overview - -We split the linear solutions of `PureU1 (2 * n.succ)` into two planes, -where every point in either plane satisfies both the linear and cubic anomaly cancellation -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 -- `span_basis` : Every linear solution is the sum of a point from each plane. - -## iii. Table of contents - -- A. Splitting the charges up into groups - - 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.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.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 - - 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.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.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 - - C.15. Permutations as additions of basis vectors -- D. Mixed cubic ACCs involving points from both planes -- E. The combined basis - - E.1. As a map into linear solutions - - E.2. Inclusion of the span of the basis into charges - - E.3. Components of the inclusion into charges - - E.4. Kernel of the inclusion into charges - - E.5. The inclusion of the span of the basis into linear solutions - - E.6. The combined basis vectors are linearly independent - - E.7. Injectivity of the inclusion into linear solutions - - E.8. Cardinality of the basis - - E.9. The basis vectors as a basis -- F. Every Lienar solution is the sum of a point from each plane - - F.1. Relation under permutations - -## iv. References - -- https://arxiv.org/pdf/1912.04804.pdf - --/ - -@[expose] public section - -open Nat Module Finset BigOperators - -namespace PureU1 - -variable {n : ℕ} - -namespace VectorLikeEvenPlane - -/-! - -## A. Splitting the charges up into groups - -We have `2 * n.succ` charges, which we split up in the following ways: - -`| evenFst j (0 to n) | evenSnd j (n.succ to n + n.succ)|` - -``` -| evenShiftZero (0) | evenShiftFst j (1 to n) | - evenShiftSnd j (n.succ to 2 * n) | evenShiftLast (2 * n.succ - 1) | -``` - --/ - -/-! - -### A.1. The even split: Spltting the charges up via `n.succ + n.succ` - --/ - -/-- The inclusion of `Fin n.succ` into `Fin (n.succ + n.succ)` via the first `n.succ`, - casted into `Fin (2 * n.succ)`. -/ -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 evenSnd (j : Fin n.succ) : Fin (2 * n.succ) := - Fin.cast (split_equal n.succ) (Fin.natAdd n.succ j) - -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 : 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 : evenSnd j = i := by - simp only [succ_eq_add_one, evenSnd, Fin.ext_iff, Fin.val_cast, Fin.val_natAdd, j] - omega - rw [h3] at h2 - exact h2 - -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 - 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 - -/-! - -### A.2. The shifted even split: Spltting the charges up via `1 + (n + n + 1)` - --/ - -lemma n_cond₂ (n : ℕ) : 1 + ((n + n) + 1) = 2 * n.succ := by - linarith - -/-- The inclusion of `Fin n` into `Fin (1 + (n + n + 1))` via the first `n`, - casted into `Fin (2 * n.succ)`. -/ -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 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 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 evenShiftLast : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.natAdd 1 (Fin.natAdd (n + n) 0))) - -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 - simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv] - · exact fun _ _ => rfl - rw [h1] - rw [Fin.sum_univ_add, Fin.sum_univ_add, Fin.sum_univ_add, Finset.sum_add_distrib] - simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply] - repeat rw [Rat.add_assoc] - apply congrArg - rw [Rat.add_comm] - rw [← Rat.add_assoc] - nth_rewrite 2 [Rat.add_comm] - repeat rw [Rat.add_assoc] - nth_rewrite 2 [Rat.add_comm] - rfl - -/-! - -### A.3. Lemmas relating the two splittings - --/ -lemma evenShiftZero_eq_evenFst_zero : @evenShiftZero n = evenFst 0 := rfl - -lemma evenShiftLast_eq_evenSnd_last: @evenShiftLast n = evenSnd (Fin.last n) := by - rw [Fin.ext_iff] - simp only [succ_eq_add_one, evenShiftLast, Fin.isValue, Fin.val_cast, Fin.val_natAdd, - Fin.val_eq_zero, add_zero, evenSnd, Fin.natAdd_last, Fin.val_last] - omega - -lemma evenShiftFst_eq_evenFst_succ (j : Fin n) : evenShiftFst j = evenFst j.succ := by - rw [Fin.ext_iff, evenFst, evenShiftFst] - simp only [Fin.val_cast, Fin.val_natAdd, Fin.val_castAdd, Fin.val_succ] - ring - -lemma evenShiftSnd_eq_evenSnd_castSucc (j : Fin n) : evenShiftSnd j = evenSnd j.castSucc := by - rw [Fin.ext_iff, evenSnd, evenShiftSnd] - simp only [Fin.val_cast, Fin.val_natAdd, Fin.val_castAdd, Fin.val_castSucc] - ring_nf - rw [Nat.succ_eq_add_one] - ring - -/-! - -## B. The first plane - --/ - -/-! - -### B.1. The basis vectors of the first plane as charges - --/ - -/-- The first part of the basis as charges. -/ -def basisAsCharges (j : Fin n.succ) : (PureU1 (2 * n.succ)).Charges := - fun i => - if i = evenFst j then - 1 - else - if i = evenSnd j then - - 1 - else - 0 - -/-! - -### B.2. Components of the basis vectors - --/ - -lemma basis_on_evenFst_self (j : Fin n.succ) : basisAsCharges j (evenFst j) = 1 := by - simp [basisAsCharges] - -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 - simp_all - rw [Fin.ext_iff] at h - simp_all - · split - · rename_i h1 h2 - simp_all only [succ_eq_add_one, ne_eq, Fin.natAdd_eq_addNat, Fin.cast_inj, neg_eq_zero, - one_ne_zero] - rw [Fin.ext_iff] at h2 - simp only [Fin.val_castAdd, Fin.val_addNat] at h2 - omega - · rfl - -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_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 - any_goals split - any_goals rfl - all_goals - rename_i h1 h2 - rw [Fin.ext_iff] at h1 h2 - simp_all - all_goals - rename_i h3 - rw [Fin.ext_iff] at h3 - simp_all - all_goals omega - -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_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 - -/-! - -### B.3. The basis vectors satisfy the linear ACCs - --/ - -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_even] - simp [basis_evenSnd_eq_neg_evenFst] -/-! - -### B.4. The basis vectors satisfy the cubic ACC - --/ -lemma basis_accCube (j : Fin n.succ) : - accCube (2 * n.succ) (basisAsCharges j) = 0 := by - rw [accCube_explicit, sum_even] - apply Finset.sum_eq_zero - intro i _ - simp only [succ_eq_add_one, Function.comp_apply, basis_evenSnd_eq_neg_evenFst] - ring - -/-! - -### B.5. The basis vectors as linear solutions - --/ - -/-- The first part of the basis as `LinSols`. -/ -@[simps!] -def basis (j : Fin n.succ) : (PureU1 (2 * n.succ)).LinSols := - ⟨basisAsCharges j, by - intro i - simp only [succ_eq_add_one, PureU1_numberLinear] at i - match i with - | 0 => - exact basis_linearACC j⟩ - -/-! - -### B.6. The inclusion of the first 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 - -/-! - -### B.7. Components of the inclusion into charges - --/ - -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_evenFst_self] - exact Rat.mul_one (f j) - · intro k _ 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_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_evenSnd_self, mul_neg, mul_one] - · intro k _ hkj - simp only [basis_on_evenSnd_other hkj, mul_zero] - · simp - -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_evenFst, P_evenSnd] - -/-! - -### B.8. The inclusion into charges satisfies the linear and cubic ACCs - --/ - -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_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_even] - apply Finset.sum_eq_zero - intro i _ - simp only [succ_eq_add_one, Function.comp_apply, P_evenFst, P_evenSnd] - ring - -/-! - -### B.9. Kernel of the inclusion into charges - --/ - -lemma P_zero (f : Fin n.succ → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by - intro i - erw [← P_evenFst f] - rw [h] - rfl - -/-! - -### B.10. The inclusion of the plane into linear solutions - --/ - -/-- 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 - -lemma P'_val (f : Fin n.succ → ℚ) : (P' f).val = P f := by - simp only [succ_eq_add_one, P', P] - funext i - rw [sum_of_anomaly_free_linear, sum_of_charges] - rfl - -/-! - -### B.11. The basis vectors are linearly independent - --/ - -theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := by - apply Fintype.linearIndependent_iff.mpr - intro f h - change P' f = 0 at h - have h1 : (P' f).val = 0 := - (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0) - (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h)))) - (ACCSystemLinear.LinSols.val 0))).mp rfl - rw [P'_val] at h1 - exact P_zero f h1 - -/-! - -### B.12. Every vector-like even solution is in the span of the basis of the first plane - --/ - -lemma vectorLikeEven_in_span (S : (PureU1 (2 * n.succ)).LinSols) - (hS : VectorLikeEven S.val) : ∃ (M : (FamilyPermutations (2 * n.succ)).group), - (FamilyPermutations (2 * n.succ)).linSolRep M S ∈ Submodule.span ℚ (Set.range basis) := by - use (Tuple.sort S.val).symm - change sortAFL S ∈ Submodule.span ℚ (Set.range basis) - rw [Submodule.mem_span_range_iff_exists_fun ℚ] - 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_even - · intro i - rw [P_evenFst] - rfl - · intro i - rw [P_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 - rw [ht] - ring - rw [h] - rfl - -/-! - -## C. The vectors of the basis spanning the second plane, via the shifted even split - --/ - -/-- The second part of the basis as charges. -/ -def basis!AsCharges (j : Fin n) : (PureU1 (2 * n.succ)).Charges := - fun i => - if i = evenShiftFst j then - 1 - else - if i = evenShiftSnd j then - - 1 - else - 0 -/-! - -### C.2. Components of the vectors - --/ - -lemma basis!_on_evenShiftFst_self (j : Fin n) : basis!AsCharges j (evenShiftFst j) = 1 := by - simp [basis!AsCharges] - -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_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 [evenShiftFst, succ_eq_add_one, evenShiftSnd] - split - · rename_i h1 - rw [Fin.ext_iff] at h1 - simp_all - rw [Fin.ext_iff] at h - simp_all - · split - · rename_i h1 h2 - simp_all - rw [Fin.ext_iff] at h2 - simp only [Fin.val_castAdd, Fin.val_addNat] at h2 - omega - · rfl - -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 - any_goals rfl - all_goals - rename_i h1 h2 - rw [Fin.ext_iff] at h1 h2 - simp_all only [Fin.natAdd_eq_addNat, Fin.cast_inj, Fin.val_cast, Fin.val_natAdd, - Fin.val_castAdd, add_right_inj, Fin.val_addNat, add_eq_left] - · subst h1 - exact Fin.elim0 i - all_goals - rename_i h3 - rw [Fin.ext_iff] at h3 - simp_all only [Fin.val_natAdd, Fin.val_castAdd, Fin.val_addNat, not_true_eq_false] - 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_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_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 [evenShiftZero, succ_eq_add_one, Fin.isValue, evenShiftFst, Fin.ext_iff, - Fin.val_cast, Fin.val_castAdd, Fin.val_eq_zero, Fin.val_natAdd] at h - omega - · split <;> rename_i h2 - · simp only [evenShiftZero, succ_eq_add_one, Fin.isValue, evenShiftSnd, Fin.ext_iff, - Fin.val_cast, Fin.val_castAdd, Fin.val_eq_zero, Fin.val_natAdd] at h2 - omega - · rfl - -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, evenShiftLast, Fin.isValue, Fin.val_cast, Fin.val_natAdd, - Fin.val_eq_zero, add_zero, evenShiftFst, Fin.val_castAdd, add_right_inj] at h - omega - · split <;> rename_i h2 - · rw [Fin.ext_iff] at h2 - simp only [succ_eq_add_one, evenShiftLast, Fin.isValue, Fin.val_cast, Fin.val_natAdd, - Fin.val_eq_zero, add_zero, evenShiftSnd, Fin.val_castAdd, add_right_inj] at h2 - omega - · rfl - -/-! - -### C.3. The vectors satisfy the linear ACCs - --/ - -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_evenShift, basis!_on_evenShiftZero, basis!_on_evenShiftLast] - simp [basis!_evenShftSnd_eq_neg_evenShiftFst] - -/-! - -### C.4. The vectors satisfy the cubic ACC - --/ - -set_option backward.isDefEq.respectTransparency false in -lemma basis!_accCube (j : Fin n) : - accCube (2 * n.succ) (basis!AsCharges j) = 0 := by - 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!_evenShftSnd_eq_neg_evenShiftFst] - ring - -/-! - -### C.6. The vectors as linear solutions - --/ -/-- The second part of the basis as `LinSols`. -/ -@[simps!] -def basis! (j : Fin n) : (PureU1 (2 * n.succ)).LinSols := - ⟨basis!AsCharges j, by - intro i - simp only [succ_eq_add_one, PureU1_numberLinear] at i - match i with - | 0 => - exact basis!_linearACC j⟩ - -/-! - -### C.7. The inclusion of the second 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 - -/-! - -### C.8. Components of the inclusion into charges - --/ - -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_evenShiftFst_self] - exact Rat.mul_one (f j) - · intro k _ 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 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_evenShiftSnd_self] - exact mul_neg_one (f j) - · intro k _ hkj - rw [basis!_on_evenShiftSnd_other hkj] - exact Rat.mul_zero (f k) - · simp - -lemma P!_evenShiftZero (f : Fin n → ℚ) : P! f (evenShiftZero) = 0 := by - rw [P!, sum_of_charges] - simp [HSMul.hSMul, SMul.smul, basis!_on_evenShiftZero] - -lemma P!_evenShiftLast (f : Fin n → ℚ) : P! f evenShiftLast = 0 := by - rw [P!, sum_of_charges] - simp [HSMul.hSMul, SMul.smul, basis!_on_evenShiftLast] - -/-! - -### C.9. The inclusion into charges satisfies the cubic ACC - --/ - -set_option backward.isDefEq.respectTransparency false in -lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n.succ) (P! f) = 0 := by - 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!_evenShiftFst, P!_evenShiftSnd] - ring - -/-! - -### C.10. Kernel of the inclusion into charges - --/ - -lemma P!_zero (f : Fin n → ℚ) (h : P! f = 0) : ∀ i, f i = 0 := by - intro i - rw [← P!_evenShiftFst f] - rw [h] - rfl - -/-! - -### C.11. The inclusion of the second plane into the span of the basis - --/ - -lemma P!_in_span (f : Fin n → ℚ) : P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges) := by - rw [(Submodule.mem_span_range_iff_exists_fun ℚ)] - use f - rfl - -/-! - -### C.12. The inclusion of the plane into linear solutions - --/ - -/-- 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 - -lemma P!'_val (f : Fin n → ℚ) : (P!' f).val = P! f := by - simp only [succ_eq_add_one, P!', P!] - funext i - rw [sum_of_anomaly_free_linear, sum_of_charges] - rfl - -/-! - -### C.13. The basis vectors are linearly independent - --/ - -theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by - apply Fintype.linearIndependent_iff.mpr - intro f h - change P!' f = 0 at h - have h1 : (P!' f).val = 0 := - (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0) - (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h)))) - (ACCSystemLinear.LinSols.val 0))).mp rfl - rw [P!'_val] at h1 - exact P!_zero f h1 - -/-! - -### C.14. Properties of the basis vectors relating to the span - --/ - -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 - apply Submodule.smul_mem - apply SetLike.mem_of_subset - · exact Submodule.subset_span - · simp_all only [Set.mem_range, exists_apply_eq_apply] - -/-! - -### C.15. Permutations as additions of basis vectors - --/ - -/-- 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 - (Equiv.swap (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 = evenShiftFst j - · subst hi - 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 only [succ_eq_add_one, Equiv.invFun_as_coe, HSMul.hSMul, - ACCSystemCharges.chargesAddCommMonoid_add, ACCSystemCharges.chargesModule_smul] - rw [basis!_on_other hi hi2] - aesop -/-! - -## D. Mixed cubic ACCs involving points from both planes - --/ - -set_option backward.isDefEq.respectTransparency false in -lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) : - accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) - = 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_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_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_evenShiftFst_other hkj.symm, basis!_on_evenShiftSnd_other hkj.symm] - simp only [mul_zero, add_zero] - · simp - -set_option backward.isDefEq.respectTransparency false in -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 - simp only [succ_eq_add_one, accCubeTriLinSymm, PureU1Charges_numberCharges, - TriLinearSymm.mk₃_toFun_apply_apply] - rw [sum_even] - simp only [Function.comp_apply] - 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_evenFst_other hkj.symm, basis_on_evenSnd_other hkj.symm] - simp only [mul_zero, add_zero] - · simp - -/-! - -## E. The combined basis - --/ - -/-! - -### E.1. As a map into linear solutions - --/ -/-- 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 - -/-! - -### E.2. Inclusion of the span of the basis into charges - --/ - -/-- 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 - -/-! - -### E.3. Components of the inclusion into charges - --/ - -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] - -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] - 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] - exact Rat.add_zero (f 0) - -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] - exact Rat.add_zero (-f (Fin.last n)) - -/-! - -### E.4. Kernel of the inclusion into charges - --/ - -set_option backward.isDefEq.respectTransparency false in -lemma Pa_zero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) : - ∀ i, f i = 0 := by - have h₃ := Pa_evenShitZero f g - rw [h] at h₃ - change 0 = f 0 at h₃ - intro i - have hinduc (iv : ℕ) (hiv : iv < n.succ) : f ⟨iv, hiv⟩ = 0 := by - induction iv - exact h₃.symm - rename_i iv hi - have hivi : iv < n.succ := lt_of_succ_lt hiv - have hi2 := hi hivi - 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, Fin.castSucc_mk] at h1 h2 - erw [hi2] at h2 - change 0 = _ at h2 - simp only [neg_zero, zero_sub, zero_eq_neg] at h2 - rw [h2] at h1 - exact right_eq_add.mp h1 - exact hinduc i.val i.prop - -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 - simp only [succ_eq_add_one, hf, zero_smul, sum_const_zero, zero_add] at h - exact P!_zero g h - -/-! - -### E.5. The inclusion of the span of the basis into linear solutions - --/ -/-- A point in the span of the whole basis. -/ -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 - exact Fintype.sum_sum_type _ - -/-! - -### E.6. The combined basis vectors are linearly independent - --/ - -theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n) := by - apply Fintype.linearIndependent_iff.mpr - intro f h - change Pa' f = 0 at h - have h1 : (Pa' f).val = 0 := - (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0) - (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h)))) - (ACCSystemLinear.LinSols.val 0))).mp rfl - rw [Pa'_P'_P!'] at h1 - change (P' (f ∘ Sum.inl)).val + (P!' (f ∘ Sum.inr)).val = 0 at h1 - rw [P!'_val, P'_val] at h1 - change Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0 at h1 - have hf := Pa_zero (f ∘ Sum.inl) (f ∘ Sum.inr) h1 - have hg := Pa_zero! (f ∘ Sum.inl) (f ∘ Sum.inr) h1 - intro i - simp_all - cases i - · simp_all - · simp_all -/-! - -### E.7. Injectivity of the inclusion into linear solutions - --/ - -lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n) → ℚ) : Pa' f = Pa' f' ↔ f = f' := by - refine Iff.intro (fun h => (funext (fun i => ?_))) (fun h => ?_) - · rw [Pa', Pa'] at h - have h1 : ∑ i : Fin (succ n) ⊕ Fin n, (f i + (- f' i)) • basisa i = 0 := by - simp only [add_smul, neg_smul] - rw [Finset.sum_add_distrib] - rw [h] - rw [← Finset.sum_add_distrib] - simp - have h2 : ∀ i, (f i + (- f' i)) = 0 := by - exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent n) - (fun i => f i + -f' i) h1 - have h2i := h2 i - linarith - · rw [h] - -lemma Pa'_elim_eq_iff (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) : - Pa' (Sum.elim g f) = Pa' (Sum.elim g' f') ↔ Pa g f = Pa g' f' := by - refine Iff.intro (fun h => ?_) (fun h => ?_) - · rw [Pa'_eq, Sum.elim_eq_iff] at h - 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] - exact h - -lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) : - Pa g f = Pa g' f' ↔ g = g' ∧ f = f' := by - rw [← Pa'_elim_eq_iff, ← Sum.elim_eq_iff] - exact Pa'_eq _ _ - -/-! - -### E.8. Cardinality of the basis - --/ - -lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n)) = - Module.finrank ℚ (PureU1 (2 * n.succ)).LinSols := by - erw [BasisLinear.finrank_AnomalyFreeLinear] - simp only [Fintype.card_sum, Fintype.card_fin, mul_eq] - exact split_odd n - -/-! - -### E.9. The basis vectors as a basis - --/ - -/-- The basis formed out of our `basisa` vectors. -/ -noncomputable def basisaAsBasis : - Basis (Fin (succ n) ⊕ Fin n) ℚ (PureU1 (2 * succ n)).LinSols := - basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card - -/-! - -## F. Every Lienar solution is the sum of a point from each plane - --/ - -lemma span_basis (S : (PureU1 (2 * n.succ)).LinSols) : - ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! 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 - use f ∘ Sum.inl - use f ∘ Sum.inr - rw [← hf] - simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, P'_val, P!'_val] - rfl - -/-! - -### F.1. Relation under permutations - --/ -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 - apply Submodule.add_mem - exact (P!_in_span f) - exact (smul_basis!AsCharges_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' - erw [hf'] - simp only [and_self, and_true, X] - rw [← add_assoc, ← h] - apply swap!_as_add at hS - exact hS - -end VectorLikeEvenPlane - -end PureU1 diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean index 337937d6f..1054d8295 100644 --- a/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean +++ b/Physlib/QFT/QED/AnomalyCancellation/Even/LineInCubic.lean @@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith -/ module -public import Physlib.QFT.QED.AnomalyCancellation.Even.BasisLinear +public import Physlib.QFT.QED.AnomalyCancellation.Even.Basis public import Physlib.QFT.QED.AnomalyCancellation.LineInPlaneCond /-! @@ -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 plane spanned by the symmetric part of the basis. The main reference for this file is: @@ -36,40 +36,40 @@ open VectorLikeEvenPlane /-- A property on `LinSols`, satisfied if every point on the line between the two planes 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 + ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = basisCharge g f) (a b : ℚ), + accCube (2 * n.succ) (a • symmPlaneAsCharges g + b • shiftPlaneAsCharges 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 + ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = basisCharge g f) (a b : ℚ), + 3 * a * b * (a * accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) + + b * accCubeTriLinSymm (shiftPlaneAsCharges f) (shiftPlaneAsCharges f) (symmPlaneAsCharges 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 • symmPlaneAsCharges g + b • shiftPlaneAsCharges f) = 0 at h1 simp only [TriLinearSymm.toCubic_add] at h1 simp only [HomogeneousCubic.map_smul, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1 conv_lhs at h1 => enter [1, 1, 1, 2] change accCube _ _ - rw [P_accCube] + rw [symmPlaneAsCharges_accCube] conv_lhs at h1 => enter [1, 1, 2, 2] change accCube _ _ - rw [P!_accCube] + rw [shiftPlaneAsCharges_accCube] rw [← h1] ring /-- 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 = symmPlaneAsCharges g + shiftPlaneAsCharges f`, +then `accCubeTriLinSymm.toFun (symmPlaneAsCharges g, symmPlaneAsCharges g, shiftPlaneAsCharges 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 +lemma line_in_cubic_symmPlane_symmPlane_shiftPlane {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) : + ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = symmPlaneAsCharges g + shiftPlaneAsCharges f), + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges 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 @@ -98,42 +98,42 @@ lemma lineInCubicPerm_permute {S : (PureU1 (2 * n.succ)).LinSols} set_option backward.isDefEq.respectTransparency false in 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), + ∀ (j : Fin n) (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = basisCharge g f), (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) - * accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := by + * accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftBasisAsCharges j) = 0 := by intro j g f h let S' := (FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j)) S have hSS' : ((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (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! + obtain ⟨g', f', hall⟩ := span_basis_swapShift j hSS' g f h + have h1 := line_in_cubic_symmPlane_symmPlane_shiftPlane (lineInCubicPerm_self LIC) g f h + have h2 := line_in_cubic_symmPlane_symmPlane_shiftPlane (lineInCubicPerm_self (lineInCubicPerm_permute LIC (Equiv.swap (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 -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)) = +lemma symmPlane_symmPlane_shiftBasisAsCharges_accCube' {S : (PureU1 (2 * n.succ.succ)).LinSols} + (f : Fin n.succ.succ → ℚ) (g : Fin n.succ → ℚ) (hS : S.val = basisCharge f g) : + accCubeTriLinSymm (symmPlaneAsCharges f) (symmPlaneAsCharges f) (shiftBasisAsCharges (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)] - have h1 := Pa_evenShiftLast f g - have h2 := Pa_evenShiftFst f g (Fin.last n) - have h3 := Pa_evenShiftSnd f g (Fin.last n) + rw [symmPlane_symmPlane_shiftBasisAsCharges_accCube f (Fin.last n)] + have h1 := basisCharge_evenShiftLast f g + have h2 := basisCharge_evenShiftFst f g (Fin.last n) + have h3 := basisCharge_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 evenShiftLast := by + have hl : f (Fin.succ (Fin.last n)) = - basisCharge 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 (evenShiftFst (Fin.last n)) + Pa f g evenShiftLast := by + have hg : g (Fin.last n) = basisCharge f g (evenShiftFst (Fin.last n)) + basisCharge f g evenShiftLast := by linear_combination -(1 * h2) have hll : f (Fin.castSucc (Fin.last n)) = - - (Pa f g (evenShiftSnd (Fin.last n)) + Pa f g (evenShiftFst (Fin.last n)) - + Pa f g evenShiftLast) := by + - (basisCharge f g (evenShiftSnd (Fin.last n)) + basisCharge f g (evenShiftFst (Fin.last n)) + + basisCharge f g evenShiftLast) := by linear_combination h3 - 1 * hg rw [← hS] at hl hll rw [hl, hll] @@ -146,7 +146,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 [symmPlane_symmPlane_shiftBasisAsCharges_accCube' g f hfg] at h1 simp only [Nat.succ_eq_add_one, neg_add_rev, mul_eq_zero] at h1 cases h1 <;> rename_i h1 · left @@ -180,7 +180,7 @@ 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) := + ∈ Submodule.span ℚ (Set.range symmBasis) := vectorLikeEven_in_span S.1.1 (lineInCubicPerm_vectorLike LIC) end Even diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/Parameterization.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/Parameterization.lean index 5c469ac08..ed4c6b14c 100644 --- a/Physlib/QFT/QED/AnomalyCancellation/Even/Parameterization.lean +++ b/Physlib/QFT/QED/AnomalyCancellation/Even/Parameterization.lean @@ -35,16 +35,16 @@ point in `(PureU1 (2 * n.succ)).AnomalyFreeLinear`, which we will later show ext 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 (shiftPlaneAsCharges f) (shiftPlaneAsCharges f) (symmPlaneAsCharges g)) • symmPlane g + + (- accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f)) • shiftPlane 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 (shiftPlaneAsCharges f) (shiftPlaneAsCharges f) (symmPlaneAsCharges g)) • symmPlaneAsCharges g + + (- accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f)) • shiftPlaneAsCharges f) := by rw [parameterizationAsLinear] - change a • (_ • (P' g).val + _ • (P!' f).val) = _ - rw [P'_val, P!'_val] + change a • (_ • (symmPlane g).val + _ • (shiftPlane f).val) = _ + rw [symmPlane_val, shiftPlane_val] set_option backward.isDefEq.respectTransparency false in lemma parameterizationCharge_cube (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) : @@ -52,7 +52,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 [symmPlaneAsCharges_accCube, shiftPlaneAsCharges_accCube] rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] @@ -65,50 +65,50 @@ 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 = symmPlaneAsCharges g + shiftPlaneAsCharges f) : + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) = - accCubeTriLinSymm (shiftPlaneAsCharges f) (shiftPlaneAsCharges f) (symmPlaneAsCharges 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)) (symmPlaneAsCharges g + shiftPlaneAsCharges f) = 0 at hC + erw [TriLinearSymm.toCubic_add, symmPlaneAsCharges_accCube, shiftPlaneAsCharges_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 (symmPlaneAsCharges g, symmPlaneAsCharges g, shiftPlaneAsCharges 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 = symmPlaneAsCharges g + shiftPlaneAsCharges f), + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges 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 = symmPlaneAsCharges g + shiftPlaneAsCharges f ∧ + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) ≠ 0) : GenericCase S := by intro g f hS hC obtain ⟨g', f', hS', hC'⟩ := hs rw [hS] at hS' - erw [Pa_eq] at hS' + erw [basisCharge_eq] at hS' 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 (symmPlaneAsCharges g, symmPlaneAsCharges g, shiftPlaneAsCharges 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 = symmPlaneAsCharges g + shiftPlaneAsCharges f), + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges 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 = symmPlaneAsCharges g + shiftPlaneAsCharges f ∧ + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) = 0) : SpecialCase S := by intro g f hS obtain ⟨g', f', hS', hC'⟩ := hs rw [hS] at hS' - erw [Pa_eq] at hS' + erw [basisCharge_eq] at hS' rw [hS'.1, hS'.2] exact hC' 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 (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) ≠ 0 ∨ + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) = 0 := by exact ne_or_eq _ _ rcases h1 with h1 | h1 · exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩) @@ -117,7 +117,7 @@ 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 (shiftPlaneAsCharges f) (shiftPlaneAsCharges f) (symmPlaneAsCharges g))⁻¹ rw [parameterization] apply ACCSystem.Sols.ext rw [parameterizationAsLinear_val] @@ -135,14 +135,14 @@ 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 [symmPlaneAsCharges_accCube, shiftPlaneAsCharges_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 (shiftPlaneAsCharges f) (shiftPlaneAsCharges f) (symmPlaneAsCharges g) = 0 at h erw [h] simp @@ -157,7 +157,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 symmBasis) := lineInCubicPerm_in_plane S (special_case_lineInCubic_perm h) end Even diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/Planes/ShiftPlane.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/Planes/ShiftPlane.lean new file mode 100644 index 000000000..558e76ced --- /dev/null +++ b/Physlib/QFT/QED/AnomalyCancellation/Even/Planes/ShiftPlane.lean @@ -0,0 +1,453 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +module + +public import Physlib.QFT.QED.AnomalyCancellation.Even.Planes.SymmPlane +/-! + +# The shifted plane for the even case + +## i. Overview + +This module defines the *shifted plane* for the even case of anomaly cancellation +in `PureU1 (2 * n.succ)`. It is called "shifted" because these positions come from +the shifted even split `1 + (n + n + 1)`, where the charges are grouped around the +boundary rather than symmetrically. + +## ii. Key definitions and results + +- `shiftBasisAsCharges` : The basis vectors of the shifted plane as charges. +- `shiftBasis` : The basis vectors as `LinSols`. +- `shiftPlaneAsCharges` : A point in the span of the shifted basis as a charge, + i.e., the inclusion of the shifted plane into charges. +- `shiftPlane` : The inclusion of the shifted plane into linear solutions. +- `shiftPlaneAsCharges_accCube` : Charges from the shifted plane satisfy the cubic ACC. +- `shiftBasis_linear_independent` : The shifted basis vectors are linearly independent. + +## iii. Table of contents + +- A.1. The shifted even split: Splitting the charges up via `1 + (n + n + 1)` +- A.2. Lemmas relating the two splittings +- B. The shifted plane + - B.1. The basis vectors of the shifted 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 `LinSols` + - B.6. The basis vectors are linearly independent + - B.7. Permutations as additions of basis vectors + - B.8. The inclusion of the shifted plane into charges + - B.9. Components of the shifted plane + - B.10. Points satisfy the cubic ACC + - B.11. Kernel of the inclusion + - B.12. The inclusion of the plane into `LinSols` + +## iv. References + +- https://arxiv.org/pdf/1912.04804.pdf + +-/ + +@[expose] public section + +open Nat Module Finset BigOperators + +namespace PureU1 + +variable {n : ℕ} + +namespace VectorLikeEvenPlane + +/-! + +### A.1. The shifted even split: Splitting the charges up via `1 + (n + n + 1)` + +-/ + +lemma n_cond₂ (n : ℕ) : 1 + ((n + n) + 1) = 2 * n.succ := by + linarith + +/-- The inclusion of `Fin n` into `Fin (1 + (n + n + 1))` via the first `n`, + casted into `Fin (2 * n.succ)`. -/ +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 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 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 evenShiftLast : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.natAdd 1 (Fin.natAdd (n + n) 0))) + +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 + simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv] + · exact fun _ _ => rfl + rw [h1] + rw [Fin.sum_univ_add, Fin.sum_univ_add, Fin.sum_univ_add, Finset.sum_add_distrib] + simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply] + repeat rw [Rat.add_assoc] + apply congrArg + rw [Rat.add_comm] + rw [← Rat.add_assoc] + nth_rewrite 2 [Rat.add_comm] + repeat rw [Rat.add_assoc] + nth_rewrite 2 [Rat.add_comm] + rfl + +/-! + +### A.2. Lemmas relating the two splittings + +-/ +lemma evenShiftZero_eq_evenFst_zero : @evenShiftZero n = evenFst 0 := rfl + +lemma evenShiftLast_eq_evenSnd_last: @evenShiftLast n = evenSnd (Fin.last n) := by + rw [Fin.ext_iff] + simp only [succ_eq_add_one, evenShiftLast, Fin.isValue, Fin.val_cast, Fin.val_natAdd, + Fin.val_eq_zero, add_zero, evenSnd, Fin.natAdd_last, Fin.val_last] + omega + +lemma evenShiftFst_eq_evenFst_succ (j : Fin n) : evenShiftFst j = evenFst j.succ := by + rw [Fin.ext_iff, evenFst, evenShiftFst] + simp only [Fin.val_cast, Fin.val_natAdd, Fin.val_castAdd, Fin.val_succ] + ring + +lemma evenShiftSnd_eq_evenSnd_castSucc (j : Fin n) : evenShiftSnd j = evenSnd j.castSucc := by + rw [Fin.ext_iff, evenSnd, evenShiftSnd] + simp only [Fin.val_cast, Fin.val_natAdd, Fin.val_castAdd, Fin.val_castSucc] + ring_nf + rw [Nat.succ_eq_add_one] + ring + +/-! + +## B. The shifted plane + +-/ + +/-! + +### B.1. The basis vectors of the shifted plane as charges + +-/ + +/-- The basis vectors of the shifted plane as charges. -/ +def shiftBasisAsCharges (j : Fin n) : (PureU1 (2 * n.succ)).Charges := + fun i => + if i = evenShiftFst j then + 1 + else + if i = evenShiftSnd j then + - 1 + else + 0 +/-! + +### B.2. Components of the basis vectors + +-/ + +lemma shiftBasisAsCharges_on_evenShiftFst_self (j : Fin n) : + shiftBasisAsCharges j (evenShiftFst j) = 1 := by + simp [shiftBasisAsCharges] + +lemma shiftBasisAsCharges_on_other {k : Fin n} {j : Fin (2 * n.succ)} (h1 : j ≠ evenShiftFst k) + (h2 : j ≠ evenShiftSnd k) : shiftBasisAsCharges k j = 0 := by + simp only [shiftBasisAsCharges, succ_eq_add_one, PureU1_numberCharges] + simp_all only [ne_eq, ↓reduceIte] + +lemma shiftBasisAsCharges_on_evenShiftFst_other {k j : Fin n} (h : k ≠ j) : + shiftBasisAsCharges k (evenShiftFst j) = 0 := by + simp only [shiftBasisAsCharges, succ_eq_add_one, PureU1_numberCharges] + simp only [evenShiftFst, succ_eq_add_one, evenShiftSnd] + split + · rename_i h1 + rw [Fin.ext_iff] at h1 + simp_all + rw [Fin.ext_iff] at h + simp_all + · split + · rename_i h1 h2 + simp_all + rw [Fin.ext_iff] at h2 + simp only [Fin.val_castAdd, Fin.val_addNat] at h2 + omega + · rfl + +lemma shiftBasisAsCharges_evenShiftSnd_eq_neg_evenShiftFst (j i : Fin n) : + shiftBasisAsCharges j (evenShiftSnd i) = - shiftBasisAsCharges j (evenShiftFst i) := by + simp only [shiftBasisAsCharges, succ_eq_add_one, PureU1_numberCharges, evenShiftSnd, evenShiftFst] + split <;> split + any_goals split + any_goals split + any_goals rfl + all_goals + rename_i h1 h2 + rw [Fin.ext_iff] at h1 h2 + simp_all only [Fin.natAdd_eq_addNat, Fin.cast_inj, Fin.val_cast, Fin.val_natAdd, + Fin.val_castAdd, add_right_inj, Fin.val_addNat, add_eq_left] + · subst h1 + exact Fin.elim0 i + all_goals + rename_i h3 + rw [Fin.ext_iff] at h3 + simp_all only [Fin.val_natAdd, Fin.val_castAdd, Fin.val_addNat, not_true_eq_false] + all_goals + omega + +lemma shiftBasisAsCharges_on_evenShiftSnd_self (j : Fin n) : + shiftBasisAsCharges j (evenShiftSnd j) = - 1 := by + rw [shiftBasisAsCharges_evenShiftSnd_eq_neg_evenShiftFst, + shiftBasisAsCharges_on_evenShiftFst_self] + +lemma shiftBasisAsCharges_on_evenShiftSnd_other {k j : Fin n} (h : k ≠ j) : + shiftBasisAsCharges k (evenShiftSnd j) = 0 := by + rw [shiftBasisAsCharges_evenShiftSnd_eq_neg_evenShiftFst, + shiftBasisAsCharges_on_evenShiftFst_other h] + rfl + +lemma shiftBasisAsCharges_on_evenShiftZero (j : Fin n) : + shiftBasisAsCharges j evenShiftZero = 0 := by + simp only [shiftBasisAsCharges, succ_eq_add_one, PureU1_numberCharges] + split<;> rename_i h + · simp only [evenShiftZero, succ_eq_add_one, Fin.isValue, evenShiftFst, Fin.ext_iff, + Fin.val_cast, Fin.val_castAdd, Fin.val_eq_zero, Fin.val_natAdd] at h + omega + · split <;> rename_i h2 + · simp only [evenShiftZero, succ_eq_add_one, Fin.isValue, evenShiftSnd, Fin.ext_iff, + Fin.val_cast, Fin.val_castAdd, Fin.val_eq_zero, Fin.val_natAdd] at h2 + omega + · rfl + +lemma shiftBasisAsCharges_on_evenShiftLast (j : Fin n) : + shiftBasisAsCharges j evenShiftLast = 0 := by + simp only [shiftBasisAsCharges, succ_eq_add_one, PureU1_numberCharges] + split <;> rename_i h + · rw [Fin.ext_iff] at h + simp only [succ_eq_add_one, evenShiftLast, Fin.isValue, Fin.val_cast, Fin.val_natAdd, + Fin.val_eq_zero, add_zero, evenShiftFst, Fin.val_castAdd, add_right_inj] at h + omega + · split <;> rename_i h2 + · rw [Fin.ext_iff] at h2 + simp only [succ_eq_add_one, evenShiftLast, Fin.isValue, Fin.val_cast, Fin.val_natAdd, + Fin.val_eq_zero, add_zero, evenShiftSnd, Fin.val_castAdd, add_right_inj] at h2 + omega + · rfl + +/-! + +### B.3. The basis vectors satisfy the linear ACCs + +-/ + +lemma shiftBasisAsCharges_linearACC (j : Fin n) : + (accGrav (2 * n.succ)) (shiftBasisAsCharges j) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + rw [sum_evenShift, shiftBasisAsCharges_on_evenShiftZero, shiftBasisAsCharges_on_evenShiftLast] + simp [shiftBasisAsCharges_evenShiftSnd_eq_neg_evenShiftFst] + +/-! + +### B.4. The basis vectors satisfy the cubic ACC + +-/ + +set_option backward.isDefEq.respectTransparency false in +lemma shiftBasisAsCharges_accCube (j : Fin n) : + accCube (2 * n.succ) (shiftBasisAsCharges j) = 0 := by + rw [accCube_explicit, sum_evenShift] + rw [shiftBasisAsCharges_on_evenShiftLast, shiftBasisAsCharges_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 [shiftBasisAsCharges_evenShiftSnd_eq_neg_evenShiftFst] + ring + +/-! + +### B.5. The basis vectors as `LinSols` + +-/ +/-- The basis vectors of the shifted plane as `LinSols`. -/ +@[simps!] +def shiftBasis (j : Fin n) : (PureU1 (2 * n.succ)).LinSols := + ⟨shiftBasisAsCharges j, by + intro i + simp only [succ_eq_add_one, PureU1_numberLinear] at i + match i with + | 0 => + exact shiftBasisAsCharges_linearACC j⟩ + +/-! + +### B.6. The basis vectors are linearly independent + +-/ + +theorem shiftBasis_linear_independent : LinearIndependent ℚ (@shiftBasis n) := by + apply Fintype.linearIndependent_iff.mpr + intro f h + have h1 : (∑ i, f i • shiftBasis i).val = 0 := + (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0) + (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h)))) + (ACCSystemLinear.LinSols.val 0))).mp rfl + have h2 : shiftPlaneAsCharges f = 0 := by + have : (∑ i, f i • shiftBasis i).val = shiftPlaneAsCharges f := by + simp only [succ_eq_add_one, shiftPlaneAsCharges] + funext i + rw [sum_of_anomaly_free_linear, sum_of_charges] + simp [shiftBasis_val] + rw [← this, h1] + exact shiftPlaneAsCharges_zero f h2 + +/-! + +### B.7. Permutations as additions of basis vectors + +-/ + +/-- Swapping the elements evenShiftFst j and evenShiftSnd j is equivalent to + adding a vector shiftBasisAsCharges j. -/ +lemma linSolRep_swap_evenShift_eq_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)) • + shiftBasisAsCharges j := by + funext i + rw [← hS, FamilyPermutations_anomalyFreeLinear_apply] + by_cases hi : i = evenShiftFst j + · subst hi + simp [HSMul.hSMul, shiftBasisAsCharges_on_evenShiftFst_self, Equiv.swap_apply_left] + · by_cases hi2 : i = evenShiftSnd j + · simp [HSMul.hSMul, hi2, shiftBasisAsCharges_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 [shiftBasisAsCharges_on_other hi hi2] + aesop + +/-! + +### B.8. The inclusion of the shifted plane into charges + +-/ + +/-- A point in the span of the shifted basis as a charge. -/ +def shiftPlaneAsCharges (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).Charges := + ∑ i, f i • shiftBasisAsCharges i + +/-! + +### B.9. Components of the shifted plane + +-/ + +lemma shiftPlaneAsCharges_evenShiftFst (f : Fin n → ℚ) (j : Fin n) : + shiftPlaneAsCharges f (evenShiftFst j) = f j := by + rw [shiftPlaneAsCharges, sum_of_charges] + simp only [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + · rw [shiftBasisAsCharges_on_evenShiftFst_self] + exact Rat.mul_one (f j) + · intro k _ hkj + rw [shiftBasisAsCharges_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 shiftPlaneAsCharges_evenShiftSnd (f : Fin n → ℚ) (j : Fin n) : + shiftPlaneAsCharges f (evenShiftSnd j) = - f j := by + rw [shiftPlaneAsCharges, sum_of_charges] + simp only [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + · rw [shiftBasisAsCharges_on_evenShiftSnd_self] + exact mul_neg_one (f j) + · intro k _ hkj + rw [shiftBasisAsCharges_on_evenShiftSnd_other hkj] + exact Rat.mul_zero (f k) + · simp + +lemma shiftPlaneAsCharges_evenShiftZero (f : Fin n → ℚ) : shiftPlaneAsCharges f (evenShiftZero) = 0 := by + rw [shiftPlaneAsCharges, sum_of_charges] + simp [HSMul.hSMul, SMul.smul, shiftBasisAsCharges_on_evenShiftZero] + +lemma shiftPlaneAsCharges_evenShiftLast (f : Fin n → ℚ) : shiftPlaneAsCharges f evenShiftLast = 0 := by + rw [shiftPlaneAsCharges, sum_of_charges] + simp [HSMul.hSMul, SMul.smul, shiftBasisAsCharges_on_evenShiftLast] + +/-! + +### B.10. Points satisfy the cubic ACC + +-/ + +set_option backward.isDefEq.respectTransparency false in +lemma shiftPlaneAsCharges_accCube (f : Fin n → ℚ) : accCube (2 * n.succ) (shiftPlaneAsCharges f) = 0 := by + rw [accCube_explicit, sum_evenShift, shiftPlaneAsCharges_evenShiftZero, shiftPlaneAsCharges_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 [shiftPlaneAsCharges_evenShiftFst, shiftPlaneAsCharges_evenShiftSnd] + ring + +/-! + +### B.11. Kernel of the inclusion + +-/ + +lemma shiftPlaneAsCharges_zero (f : Fin n → ℚ) (h : shiftPlaneAsCharges f = 0) : ∀ i, f i = 0 := by + intro i + rw [← shiftPlaneAsCharges_evenShiftFst f] + rw [h] + rfl + +lemma shiftPlaneAsCharges_in_span (f : Fin n → ℚ) : + shiftPlaneAsCharges f ∈ Submodule.span ℚ (Set.range shiftBasisAsCharges) := by + rw [(Submodule.mem_span_range_iff_exists_fun ℚ)] + use f + rfl + +lemma smul_shiftBasisAsCharges_in_span (S : (PureU1 (2 * n.succ)).LinSols) (j : Fin n) : + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • shiftBasisAsCharges j ∈ + Submodule.span ℚ (Set.range shiftBasisAsCharges) := by + apply Submodule.smul_mem + apply SetLike.mem_of_subset + · exact Submodule.subset_span + · simp_all only [Set.mem_range, exists_apply_eq_apply] + +/-! + +### B.12. The inclusion of the plane into `LinSols` + +-/ + +/-- A point in the span of the shifted basis as a linear solution. -/ +def shiftPlane (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).LinSols := + ∑ i, f i • shiftBasis i + +lemma shiftPlane_val (f : Fin n → ℚ) : + (shiftPlane f).val = shiftPlaneAsCharges f := by + simp only [succ_eq_add_one, shiftPlane, shiftPlaneAsCharges] + funext i + rw [sum_of_anomaly_free_linear, sum_of_charges] + rfl + +end VectorLikeEvenPlane + +end PureU1 diff --git a/Physlib/QFT/QED/AnomalyCancellation/Even/Planes/SymmPlane.lean b/Physlib/QFT/QED/AnomalyCancellation/Even/Planes/SymmPlane.lean new file mode 100644 index 000000000..4b47445e3 --- /dev/null +++ b/Physlib/QFT/QED/AnomalyCancellation/Even/Planes/SymmPlane.lean @@ -0,0 +1,377 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +module + +public import Physlib.QFT.QED.AnomalyCancellation.BasisLinear +public import Physlib.QFT.QED.AnomalyCancellation.VectorLike +/-! + +# The symmetric plane for the even case + +## i. Overview + +This module defines the *symmetric plane* for the even case of anomaly cancellation +in `PureU1 (2 * n.succ)`. It is called "symmetric" because these positions come from +the symmetric (even) split `n.succ + n.succ`, where the first and second halves are +paired symmetrically. + +## ii. Key definitions and results + +- `symmBasisAsCharges` : The basis vectors of the symmetric plane as charges. +- `symmBasis` : The basis vectors as `LinSols`. +- `symmPlaneAsCharges` : A point in the span of the symmetric basis as a charge, + i.e., the inclusion of the symmetric plane into charges. +- `symmPlane` : The inclusion of the symmetric plane into linear solutions. +- `symmPlaneAsCharges_accCube` : Charges from the symmetric plane satisfy the cubic ACC. +- `symmBasis_linear_independent` : The symmetric basis vectors are linearly independent. +- `vectorLikeEven_in_span` : Every vector-like even solution is in the span of the symmetric basis. + +## iii. Table of contents + +- A.1. The even split: Splitting the charges up via `n.succ + n.succ` +- B. The first plane (symmetric plane) + - B.1. The basis vectors of the symmetric 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 symmetric 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 symmetric plane + +## iv. References + +- https://arxiv.org/pdf/1912.04804.pdf + +-/ + +@[expose] public section + +open Nat Module Finset BigOperators + +namespace PureU1 + +variable {n : ℕ} + +namespace VectorLikeEvenPlane + +/-! + +### A.1. The even split: Splitting the charges up via `n.succ + n.succ` + +-/ + +/-- The inclusion of `Fin n.succ` into `Fin (n.succ + n.succ)` via the first `n.succ`, + casted into `Fin (2 * n.succ)`. -/ +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 evenSnd (j : Fin n.succ) : Fin (2 * n.succ) := + Fin.cast (split_equal n.succ) (Fin.natAdd n.succ j) + +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 : 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 : evenSnd j = i := by + simp only [succ_eq_add_one, evenSnd, Fin.ext_iff, Fin.val_cast, Fin.val_natAdd, j] + omega + rw [h3] at h2 + exact h2 + +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 + 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 + +/-! + +## B. The first plane (symmetric plane) + +-/ + +/-! + +### B.1. The basis vectors of the symmetric plane as charges + +-/ + +/-- The basis vectors of the symmetric plane as charges. -/ +def symmBasisAsCharges (j : Fin n.succ) : (PureU1 (2 * n.succ)).Charges := + fun i => + if i = evenFst j then + 1 + else + if i = evenSnd j then + - 1 + else + 0 + +/-! + +### B.2. Components of the basis vectors + +-/ + +lemma symmBasisAsCharges_on_evenFst_self (j : Fin n.succ) : + symmBasisAsCharges j (evenFst j) = 1 := by + simp [symmBasisAsCharges] + +lemma symmBasisAsCharges_on_evenFst_other {k j : Fin n.succ} (h : k ≠ j) : + symmBasisAsCharges k (evenFst j) = 0 := by + simp only [symmBasisAsCharges, succ_eq_add_one, PureU1_numberCharges, evenFst, evenSnd] + split + · rename_i h1 + rw [Fin.ext_iff] at h1 + simp_all + rw [Fin.ext_iff] at h + simp_all + · split + · rename_i h1 h2 + simp_all only [succ_eq_add_one, ne_eq, Fin.natAdd_eq_addNat, Fin.cast_inj, neg_eq_zero, + one_ne_zero] + rw [Fin.ext_iff] at h2 + simp only [Fin.val_castAdd, Fin.val_addNat] at h2 + omega + · rfl + +lemma symmBasisAsCharges_on_other {k : Fin n.succ} {j : Fin (2 * n.succ)} (h1 : j ≠ evenFst k) + (h2 : j ≠ evenSnd k) : symmBasisAsCharges k j = 0 := by + simp only [symmBasisAsCharges, succ_eq_add_one, PureU1_numberCharges] + simp_all only [ne_eq, ↓reduceIte] + +lemma symmBasisAsCharges_evenSnd_eq_neg_evenFst (j i : Fin n.succ) : + symmBasisAsCharges j (evenSnd i) = - symmBasisAsCharges j (evenFst i) := by + simp only [symmBasisAsCharges, succ_eq_add_one, PureU1_numberCharges, evenSnd, evenFst] + split <;> split + any_goals split + any_goals rfl + any_goals split + any_goals rfl + all_goals + rename_i h1 h2 + rw [Fin.ext_iff] at h1 h2 + simp_all + all_goals + rename_i h3 + rw [Fin.ext_iff] at h3 + simp_all + all_goals omega + +lemma symmBasisAsCharges_on_evenSnd_self (j : Fin n.succ) : + symmBasisAsCharges j (evenSnd j) = - 1 := by + rw [symmBasisAsCharges_evenSnd_eq_neg_evenFst, symmBasisAsCharges_on_evenFst_self] + +lemma symmBasisAsCharges_on_evenSnd_other {k j : Fin n.succ} (h : k ≠ j) : + symmBasisAsCharges k (evenSnd j) = 0 := by + rw [symmBasisAsCharges_evenSnd_eq_neg_evenFst, symmBasisAsCharges_on_evenFst_other h] + rfl + +/-! + +### B.3. The basis vectors satisfy the linear ACCs + +-/ + +lemma symmBasisAsCharges_linearACC (j : Fin n.succ) : + (accGrav (2 * n.succ)) (symmBasisAsCharges j) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + rw [sum_even] + simp [symmBasisAsCharges_evenSnd_eq_neg_evenFst] +/-! + +### B.4. The basis vectors satisfy the cubic ACC + +-/ +lemma symmBasisAsCharges_accCube (j : Fin n.succ) : + accCube (2 * n.succ) (symmBasisAsCharges j) = 0 := by + rw [accCube_explicit, sum_even] + apply Finset.sum_eq_zero + intro i _ + simp only [succ_eq_add_one, Function.comp_apply, symmBasisAsCharges_evenSnd_eq_neg_evenFst] + ring + +/-! + +### B.5. The basis vectors as linear solutions + +-/ + +/-- The basis vectors of the symmetric plane as `LinSols`. -/ +@[simps!] +def symmBasis (j : Fin n.succ) : (PureU1 (2 * n.succ)).LinSols := + ⟨symmBasisAsCharges j, by + intro i + simp only [succ_eq_add_one, PureU1_numberLinear] at i + match i with + | 0 => + exact symmBasisAsCharges_linearACC j⟩ + +/-! + +### B.6. The inclusion of the symmetric plane into charges + +-/ + +/-- A point in the span of the symmetric basis as a charge. -/ +def symmPlaneAsCharges (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).Charges := + ∑ i, f i • symmBasisAsCharges i + +/-! + +### B.7. Components of the inclusion into charges + +-/ + +lemma symmPlaneAsCharges_evenFst (f : Fin n.succ → ℚ) (j : Fin n.succ) : + symmPlaneAsCharges f (evenFst j) = f j := by + rw [symmPlaneAsCharges, sum_of_charges] + simp only [succ_eq_add_one, HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + · rw [symmBasisAsCharges_on_evenFst_self] + exact Rat.mul_one (f j) + · intro k _ hkj + rw [symmBasisAsCharges_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 symmPlaneAsCharges_evenSnd (f : Fin n.succ → ℚ) (j : Fin n.succ) : + symmPlaneAsCharges f (evenSnd j) = - f j := by + rw [symmPlaneAsCharges, sum_of_charges] + simp only [succ_eq_add_one, HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + · simp only [symmBasisAsCharges_on_evenSnd_self, mul_neg, mul_one] + · intro k _ hkj + simp only [symmBasisAsCharges_on_evenSnd_other hkj, mul_zero] + · simp + +lemma symmPlaneAsCharges_evenSnd_evenFst (f : Fin n.succ → ℚ) : + symmPlaneAsCharges f ∘ evenSnd = - symmPlaneAsCharges f ∘ evenFst := by + funext j + simp only [PureU1_numberCharges, Function.comp_apply, Pi.neg_apply] + rw [symmPlaneAsCharges_evenFst, symmPlaneAsCharges_evenSnd] + +/-! + +### B.8. The inclusion into charges satisfies the linear and cubic ACCs + +-/ + +lemma symmPlaneAsCharges_linearACC (f : Fin n.succ → ℚ) : + (accGrav (2 * n.succ)) (symmPlaneAsCharges f) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + rw [sum_even] + simp [symmPlaneAsCharges_evenSnd, symmPlaneAsCharges_evenFst] + +lemma symmPlaneAsCharges_accCube (f : Fin n.succ → ℚ) : + accCube (2 * n.succ) (symmPlaneAsCharges f) = 0 := by + rw [accCube_explicit, sum_even] + apply Finset.sum_eq_zero + intro i _ + simp only [succ_eq_add_one, Function.comp_apply, symmPlaneAsCharges_evenFst, symmPlaneAsCharges_evenSnd] + ring + +/-! + +### B.9. Kernel of the inclusion into charges + +-/ + +lemma symmPlaneAsCharges_zero (f : Fin n.succ → ℚ) (h : symmPlaneAsCharges f = 0) : ∀ i, f i = 0 := by + intro i + erw [← symmPlaneAsCharges_evenFst f] + rw [h] + rfl + +/-! + +### B.10. The inclusion of the plane into linear solutions + +-/ + +/-- A point in the span of the symmetric basis as a linear solution. -/ +def symmPlane (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).LinSols := + ∑ i, f i • symmBasis i + +lemma symmPlane_val (f : Fin n.succ → ℚ) : + (symmPlane f).val = symmPlaneAsCharges f := by + simp only [succ_eq_add_one, symmPlane, symmPlaneAsCharges] + funext i + rw [sum_of_anomaly_free_linear, sum_of_charges] + rfl + +/-! + +### B.11. The basis vectors are linearly independent + +-/ + +theorem symmBasis_linear_independent : LinearIndependent ℚ (@symmBasis n) := by + apply Fintype.linearIndependent_iff.mpr + intro f h + change symmPlane f = 0 at h + have h1 : (symmPlane f).val = 0 := + (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0) + (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h)))) + (ACCSystemLinear.LinSols.val 0))).mp rfl + rw [symmPlane_val] at h1 + exact symmPlaneAsCharges_zero f h1 + +/-! + +### B.12. Every vector-like even solution is in the span of the basis of the symmetric plane + +-/ + +lemma vectorLikeEven_in_span (S : (PureU1 (2 * n.succ)).LinSols) + (hS : VectorLikeEven S.val) : ∃ (M : (FamilyPermutations (2 * n.succ)).group), + (FamilyPermutations (2 * n.succ)).linSolRep M S ∈ + Submodule.span ℚ (Set.range symmBasis) := by + use (Tuple.sort S.val).symm + change sortAFL S ∈ Submodule.span ℚ (Set.range symmBasis) + rw [Submodule.mem_span_range_iff_exists_fun ℚ] + let f : Fin n.succ → ℚ := fun i => (sortAFL S).val (evenFst i) + use f + apply ACCSystemLinear.LinSols.ext + rw [sortAFL_val] + erw [symmPlane_val] + apply ext_even + · intro i + rw [symmPlaneAsCharges_evenFst] + rfl + · intro i + rw [symmPlaneAsCharges_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 + rw [ht] + ring + rw [h] + rfl + +end VectorLikeEvenPlane + +end PureU1 diff --git a/Physlib/QFT/QED/AnomalyCancellation/Odd/Basis.lean b/Physlib/QFT/QED/AnomalyCancellation/Odd/Basis.lean new file mode 100644 index 000000000..e1cf2fbeb --- /dev/null +++ b/Physlib/QFT/QED/AnomalyCancellation/Odd/Basis.lean @@ -0,0 +1,341 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +module + +public import Physlib.QFT.QED.AnomalyCancellation.Odd.Planes.ShiftPlane +/-! +# The combined basis for the odd case + +This file combines the symmetric and shifted planes into a single basis for the linear solutions +of `PureU1 (2 * n + 1)`. Every linear solution is the sum of a point from each plane. + +## Key results + +- `span_basis` : Every linear solution is the sum of a point from each plane. +- `symmPlane` : The inclusion of the symmetric plane into linear solutions. +- `shiftPlane` : The inclusion of the shifted plane into linear solutions. +- `basis_linear_independent` : The combined basis vectors are linearly independent. +- `basisAsBasis` : The combined basis as a `Basis`. + +## Table of contents + +- 1. The combined basis + - 1.1. The combined basis as `LinSols` + - 1.2. The inclusion of the span of the combined basis into charges + - 1.3. Components of the inclusion + - 1.4. Kernel of the inclusion into charges + - 1.5. The inclusion of the span of the combined basis into LinSols + - 1.6. The combined basis vectors are linearly independent + - 1.7. Injectivity of the inclusion into linear solutions + - 1.8. Cardinality of the basis + - 1.9. The basis vectors as a basis +- 2. Every linear solution is the sum of a point from each plane + - 2.1. Relation under permutations +- 3. Mixed cubic anomaly cancellation conditions involving both planes + +-/ + +@[expose] public section + +open Module Nat Finset BigOperators + +namespace PureU1 + +variable {n : ℕ} + +namespace VectorLikeOddPlane + +/-! + +## 1. The combined basis + +-/ + +/-! + +### 1.1. The combined basis as `LinSols` + +-/ + +/-- The whole basis as `LinSols`. -/ +def basis : Fin n ⊕ Fin n → (PureU1 (2 * n + 1)).LinSols := fun i => + match i with + | .inl i => symmBasis i + | .inr i => shiftBasis i + +/-! + +### 1.2. The inclusion of the span of the combined basis into charges + +-/ + +/-- A point in the span of the basis as a charge. -/ +def basisCharge (f : Fin n → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := + symmPlaneAsCharges f + shiftPlaneAsCharges g + +/-! + +### 1.3. Components of the inclusion + +-/ + +lemma basisCharge_oddShiftShiftZero (f g : Fin n.succ → ℚ) : basisCharge f g oddShiftShiftZero = f 0 := by + rw [basisCharge] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + nth_rewrite 1 [oddShiftShiftZero_eq_oddFst_zero] + rw [oddShiftShiftZero_eq_oddShiftZero] + rw [shiftPlaneAsCharges_oddShiftZero, oddShiftZero_eq_oddFst, symmPlaneAsCharges_oddFst] + exact Rat.add_zero (f 0) + +lemma basisCharge_oddShiftShiftFst (f g : Fin n.succ → ℚ) (j : Fin n) : + basisCharge f g (oddShiftShiftFst j) = f j.succ + g j.castSucc := by + rw [basisCharge] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + nth_rewrite 1 [oddShiftShiftFst_eq_oddFst_succ] + rw [oddShiftShiftFst_eq_oddShiftFst_castSucc] + rw [shiftPlaneAsCharges_oddShiftFst, oddShiftFst_castSucc_eq_oddFst_succ, symmPlaneAsCharges_oddFst] + +lemma basisCharge_oddShiftShiftMid (f g : Fin n.succ → ℚ) : + basisCharge f g oddShiftShiftMid = g (Fin.last n) := by + rw [basisCharge] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + nth_rewrite 1 [oddShiftShiftMid_eq_oddMid] + rw [oddShiftShiftMid_eq_oddShiftFst_last] + rw [shiftPlaneAsCharges_oddShiftFst, oddShiftFst_last_eq_oddMid, symmPlaneAsCharges_oddMid] + exact Rat.zero_add (g (Fin.last n)) + +lemma basisCharge_oddShiftShiftSnd (f g : Fin n.succ → ℚ) (j : Fin n.succ) : + basisCharge f g (oddShiftShiftSnd j) = - f j - g j := by + rw [basisCharge] + simp only [ACCSystemCharges.chargesAddCommMonoid_add] + nth_rewrite 1 [oddShiftShiftSnd_eq_oddSnd] + rw [oddShiftShiftSnd_eq_oddShiftSnd] + rw [shiftPlaneAsCharges_oddShiftSnd, oddShiftSnd_eq_oddSnd, symmPlaneAsCharges_oddSnd] + ring + +/-! + +### 1.4. Kernel of the inclusion into charges + +-/ + +set_option backward.isDefEq.respectTransparency false in +lemma basisCharge_zero (f g : Fin n.succ → ℚ) (h : basisCharge f g = 0) : + ∀ i, f i = 0 := by + have h₃ := basisCharge_oddShiftShiftZero f g + rw [h] at h₃ + change 0 = _ at h₃ + intro i + have hinduc (iv : ℕ) (hiv : iv < n.succ) : f ⟨iv, hiv⟩ = 0 := by + induction iv + exact h₃.symm + rename_i iv hi + have hivi : iv < n.succ := lt_of_succ_lt hiv + have hi2 := hi hivi + have h1 := basisCharge_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 := basisCharge_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 + +lemma basisCharge_zero_shift (f g : Fin n.succ → ℚ) (h : basisCharge f g = 0) : + ∀ i, g i = 0 := by + have hf := basisCharge_zero f g h + rw [basisCharge, symmPlaneAsCharges] at h + simp only [succ_eq_add_one, hf, zero_smul, sum_const_zero, zero_add] at h + exact shiftPlaneAsCharges_zero g h + +/-! + +### 1.5. The inclusion of the span of the combined basis into LinSols + +-/ + +/-- A point in the span of the whole basis. -/ +def spanBasis (f : (Fin n) ⊕ (Fin n) → ℚ) : (PureU1 (2 * n + 1)).LinSols := + ∑ i, f i • basis i + +lemma spanBasis_symmPlane_shiftPlane (f : (Fin n) ⊕ (Fin n) → ℚ) : + spanBasis f = symmPlane (f ∘ Sum.inl) + shiftPlane (f ∘ Sum.inr) := by + exact Fintype.sum_sum_type _ + +/-! + +### 1.6. The combined basis vectors are linearly independent + +-/ + +theorem basis_linear_independent : LinearIndependent ℚ (@basis n.succ) := by + apply Fintype.linearIndependent_iff.mpr + intro f h + change spanBasis f = 0 at h + have h1 : (spanBasis f).val = 0 := + (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0) + (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h)))) + (ACCSystemLinear.LinSols.val 0))).mp rfl + rw [spanBasis_symmPlane_shiftPlane] at h1 + change (symmPlane (f ∘ Sum.inl)).val + (shiftPlane (f ∘ Sum.inr)).val = 0 at h1 + rw [shiftPlane_val, symmPlane_val] at h1 + change basisCharge (f ∘ Sum.inl) (f ∘ Sum.inr) = 0 at h1 + have hf := basisCharge_zero (f ∘ Sum.inl) (f ∘ Sum.inr) h1 + have hg := basisCharge_zero_shift (f ∘ Sum.inl) (f ∘ Sum.inr) h1 + intro i + simp_all only [succ_eq_add_one, Function.comp_apply] + cases i + · simp_all + · simp_all + +/-! + +### 1.7. Injectivity of the inclusion into linear solutions + +-/ + +lemma spanBasis_eq (f f' : (Fin n.succ) ⊕ (Fin n.succ) → ℚ) : spanBasis f = spanBasis f' ↔ f = f' := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + · funext i + rw [spanBasis, spanBasis] at h + have h1 : ∑ i : Fin n.succ ⊕ Fin n.succ, (f i + (- f' i)) • basis i = 0 := by + simp only [add_smul, neg_smul] + rw [Finset.sum_add_distrib] + rw [h] + rw [← Finset.sum_add_distrib] + simp + have h2 : ∀ i, (f i + (- f' i)) = 0 := by + exact Fintype.linearIndependent_iff.mp (@basis_linear_independent n) + (fun i => f i + -f' i) h1 + have h2i := h2 i + linarith + · rw [h] + +lemma spanBasis_elim_eq_iff (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) : + spanBasis (Sum.elim g f) = spanBasis (Sum.elim g' f') ↔ basisCharge g f = basisCharge g' f' := by + refine Iff.intro (fun h => ?_) (fun h => ?_) + · rw [spanBasis_eq, Sum.elim_eq_iff] at h + rw [h.left, h.right] + · apply ACCSystemLinear.LinSols.ext + rw [spanBasis_symmPlane_shiftPlane, spanBasis_symmPlane_shiftPlane] + simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, + symmPlane_val, shiftPlane_val] + exact h + +lemma basisCharge_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) : + basisCharge g f = basisCharge g' f' ↔ g = g' ∧ f = f' := by + rw [← spanBasis_elim_eq_iff] + rw [← Sum.elim_eq_iff] + exact spanBasis_eq _ _ + +/-! + +### 1.8. Cardinality of the basis + +-/ + +lemma basis_card : Fintype.card ((Fin n.succ) ⊕ (Fin n.succ)) = + Module.finrank ℚ (PureU1 (2 * n.succ + 1)).LinSols := by + erw [BasisLinear.finrank_AnomalyFreeLinear] + simp only [Fintype.card_sum, Fintype.card_fin] + exact Eq.symm (Nat.two_mul n.succ) + +/-! + +### 1.9. The basis vectors as a basis + +-/ + +/-- The basis formed out of our basis vectors. -/ +noncomputable def basisAsBasis : + Basis (Fin n.succ ⊕ Fin n.succ) ℚ (PureU1 (2 * n.succ + 1)).LinSols := + basisOfLinearIndependentOfCardEqFinrank (@basis_linear_independent n) basis_card + +/-! + +## 2. Every linear solution is the sum of a point from each plane + +-/ + +lemma span_basis (S : (PureU1 (2 * n.succ + 1)).LinSols) : + ∃ (g f : Fin n.succ → ℚ), S.val = symmPlaneAsCharges g + shiftPlaneAsCharges f := by + have h := (Submodule.mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisAsBasis S) + obtain ⟨f, hf⟩ := h + simp only [succ_eq_add_one, basisAsBasis, coe_basisOfLinearIndependentOfCardEqFinrank, + Fintype.sum_sum_type] at hf + change symmPlane _ + shiftPlane _ = S at hf + use f ∘ Sum.inl + use f ∘ Sum.inr + rw [← hf] + simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, + symmPlane_val, shiftPlane_val] + rfl + +/-! + +### 2.1. Relation under permutations + +-/ + +lemma span_basis_swapShift {S : (PureU1 (2 * n.succ + 1)).LinSols} (j : Fin n.succ) + (hS : ((FamilyPermutations (2 * n.succ + 1)).linSolRep + (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S') (g f : Fin n.succ → ℚ) + (hS1 : S.val = symmPlaneAsCharges g + shiftPlaneAsCharges f) : ∃ (g' f' : Fin n.succ → ℚ), + S'.val = symmPlaneAsCharges g' + shiftPlaneAsCharges f' ∧ shiftPlaneAsCharges f' = shiftPlaneAsCharges f + + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • shiftBasisAsCharges j ∧ g' = g := by + let X := shiftPlaneAsCharges f + + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • shiftBasisAsCharges j + have hf : shiftPlaneAsCharges f ∈ Submodule.span ℚ (Set.range shiftBasisAsCharges) := by + rw [(Submodule.mem_span_range_iff_exists_fun ℚ)] + use f + rfl + have hP : (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • shiftBasisAsCharges j ∈ + Submodule.span ℚ (Set.range shiftBasisAsCharges) := by + apply Submodule.smul_mem + apply SetLike.mem_of_subset + apply Submodule.subset_span + simp_all only [Set.mem_range, exists_apply_eq_apply] + have hX : X ∈ Submodule.span ℚ (Set.range (shiftBasisAsCharges)) := by + apply Submodule.add_mem + exact hf + exact hP + have hXsum := (Submodule.mem_span_range_iff_exists_fun ℚ).mp hX + obtain ⟨f', hf'⟩ := hXsum + use g + use f' + change shiftPlaneAsCharges f' = _ at hf' + erw [hf'] + simp only [and_self, and_true, X] + rw [← add_assoc, ← hS1] + apply linSolRep_swap_oddShift_eq_add at hS + exact hS + +/-! + +## 3. Mixed cubic anomaly cancellation conditions involving both planes + +-/ + +set_option backward.isDefEq.respectTransparency false in +lemma symmPlane_symmPlane_shiftBasisAsCharges_accCube (g : Fin n → ℚ) (j : Fin n) : + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftBasisAsCharges j) + = (symmPlaneAsCharges g (oddShiftFst j))^2 - (g j)^2 := by + simp only [accCubeTriLinSymm, PureU1Charges_numberCharges, TriLinearSymm.mk₃_toFun_apply_apply] + rw [sum_oddShift, shiftBasisAsCharges_on_oddShiftZero] + simp only [mul_zero, Function.comp_apply, zero_add] + rw [Finset.sum_eq_single j, shiftBasisAsCharges_on_oddShiftFst_self, + shiftBasisAsCharges_on_oddShiftSnd_self] + · rw [← oddSnd_eq_oddShiftSnd, symmPlaneAsCharges_oddSnd] + ring + · intro k _ hkj + erw [shiftBasisAsCharges_on_oddShiftFst_other hkj.symm, + shiftBasisAsCharges_on_oddShiftSnd_other hkj.symm] + simp only [mul_zero, add_zero] + · simp + +end VectorLikeOddPlane + +end PureU1 diff --git a/Physlib/QFT/QED/AnomalyCancellation/Odd/BasisLinear.lean b/Physlib/QFT/QED/AnomalyCancellation/Odd/BasisLinear.lean deleted file mode 100644 index 7257d0bb6..000000000 --- a/Physlib/QFT/QED/AnomalyCancellation/Odd/BasisLinear.lean +++ /dev/null @@ -1,1031 +0,0 @@ -/- -Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Tooby-Smith --/ -module - -public import Physlib.QFT.QED.AnomalyCancellation.BasisLinear -public import Physlib.QFT.QED.AnomalyCancellation.VectorLike -/-! -# Splitting the linear solutions in the odd case into two ACC-satisfying planes - -## i. Overview - -We split the linear solutions of `PureU1 (2 * n + 1)` into two planes, -where every point in either plane satisfies both the linear and cubic anomaly cancellation -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 -- `span_basis` : Every linear solution is the sum of a point from each plane. - -## iii. Table of contents - -- A. Splitting the charges up into groups - - A.1. The symmetric split: Spltting the charges up via `(n + 1) + 1` - - A.2. The shifted split: Spltting the charges up via `1 + n + n` - - A.3. The shifte shifted split: Spltting the charges up via `((1+n)+1) + n.succ` - - A.4. Relating the splittings together -- B. The first plane - - B.1. The basis vectors of the first plane as charges - - B.2. Components of the basis vectors as charges - - B.3. The basis vectors satisfy the linear ACCs - - B.4. The basis vectors as `LinSols` - - B.5. The inclusion of the first plane into charges - - B.6. Components of the first plane - - B.7. Points on the first plane satisfies the ACCs - - B.8. Kernel of the inclusion into charges - - B.9. The basis vectors are linearly independent -- C. The second plane - - C.1. The basis vectors of the second plane as charges - - C.2. Components of the basis vectors as charges - - C.3. The basis vectors satisfy the linear ACCs - - C.4. The basis vectors as `LinSols` - - C.5. Permutations equal adding basis vectors - - C.6. The inclusion of the second plane into charges - - C.7. Components of the second plane - - C.8. Points on the second plane satisfies the ACCs - - C.9. Kernel of the inclusion into charges - - C.10. The inclusion of the second plane into LinSols - - C.11. The basis vectors are linearly independent -- D. The mixed cubic ACC from points in both planes -- E. The combined basis - - E.1. The combined basis as `LinSols` - - E.2. The inclusion of the span of the combined basis into charges - - E.3. Components of the inclusion - - E.4. Kernel of the inclusion into charges - - E.5. The inclusion of the span of the combined basis into LinSols - - E.6. The combined basis vectors are linearly independent - - E.7. Injectivity of the inclusion into linear solutions - - E.8. Cardinality of the basis - - E.9. The basis vectors as a basis -- F. Every Lienar solution is the sum of a point from each plane - - F.1. Relation under permutations - -## iv. References - -- https://arxiv.org/pdf/1912.04804.pdf - --/ - -@[expose] public section - -open Module Nat Finset BigOperators - -namespace PureU1 - -variable {n : ℕ} - -namespace VectorLikeOddPlane - -/-! - -## A. Splitting the charges up into groups - -We have `2 * n + 1` charges, which we split up in the following ways: - -`| evenFst j (0 to n) | evenSnd j (n.succ to n + n.succ)|` - -``` -| evenShiftZero (0) | evenShiftFst j (1 to n) | - evenShiftSnd j (n.succ to 2 * n) | evenShiftLast (2 * n.succ - 1) | -``` - --/ - -section theDeltas - -/-! - -### A.1. The symmetric split: Spltting the charges up via `(n + 1) + 1` - --/ - -lemma odd_shift_eq (n : ℕ) : (1 + n) + n = 2 * n +1 := by - omega - -/-- The inclusion of `Fin n` into `Fin ((n + 1) + n)` via the first `n`. - This is then casted to `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 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)`. - This is then casted to `Fin (2 * n + 1)`. -/ -def oddMid : Fin (2 * n + 1) := - Fin.cast (split_odd n) (Fin.castAdd n (Fin.natAdd n 1)) - -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 - simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv] - · exact fun _ _ => rfl - rw [h1] - rw [Fin.sum_univ_add, Fin.sum_univ_add] - simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply] - nth_rewrite 2 [add_comm] - rw [add_assoc] - rw [Finset.sum_add_distrib] - rfl - -/-! - -### A.2. The shifted split: Spltting the charges up via `1 + n + n` - --/ - -/-- The inclusion of `Fin n` into `Fin (1 + n + n)` via the first `n`. - This is then casted to `Fin (2 * n + 1)`. -/ -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 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 (odd_shift_eq n) (Fin.castAdd n (Fin.castAdd n 1)) - -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 - rw [h1, Fin.sum_univ_add, Fin.sum_univ_add] - simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply] - rw [add_assoc, Finset.sum_add_distrib] - rfl - -/-! - -### A.3. The shifted shifted split: Spltting the charges up via `((1+n)+1) + n.succ` - --/ - -lemma odd_shift_shift_eq (n : ℕ) : ((1+n)+1) + n.succ = 2 * n.succ + 1 := by - omega - -/-- The element representing the first `1` in `Fin (1 + n + 1 + n.succ)` casted - to `Fin (2 * n.succ + 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 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 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 oddShiftShiftSnd (j : Fin n.succ) : Fin (2 * n.succ + 1) := - Fin.cast (odd_shift_shift_eq n) (Fin.natAdd ((1+n)+1) j) - -/-! - -### A.4. Relating the splittings together - --/ -lemma oddShiftShiftZero_eq_oddFst_zero : @oddShiftShiftZero n = oddFst 0 := - Fin.rev_inj.mp rfl - -lemma oddShiftShiftZero_eq_oddShiftZero : @oddShiftShiftZero n = oddShiftZero := rfl - -lemma oddShiftShiftFst_eq_oddFst_succ (j : Fin n) : - oddShiftShiftFst j = oddFst j.succ := by - rw [Fin.ext_iff] - simp only [succ_eq_add_one, oddShiftShiftFst, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, - oddFst, Fin.val_succ] - exact Nat.add_comm 1 ↑j - -lemma oddShiftShiftFst_eq_oddShiftFst_castSucc (j : Fin n) : - oddShiftShiftFst j = oddShiftFst j.castSucc := by - rfl - -lemma oddShiftShiftMid_eq_oddMid : @oddShiftShiftMid n = oddMid := by - rw [Fin.ext_iff] - simp only [succ_eq_add_one, oddShiftShiftMid, Fin.isValue, Fin.val_cast, Fin.val_castAdd, - Fin.val_natAdd, Fin.val_eq_zero, add_zero, oddMid] - exact Nat.add_comm 1 n - -lemma oddShiftShiftMid_eq_oddShiftFst_last : oddShiftShiftMid = oddShiftFst (Fin.last n) := by - rfl - -lemma oddShiftShiftSnd_eq_oddSnd (j : Fin n.succ) : oddShiftShiftSnd j = oddSnd j := by - rw [Fin.ext_iff] - simp only [succ_eq_add_one, oddShiftShiftSnd, Fin.val_cast, Fin.val_natAdd, oddSnd, add_left_inj] - exact Nat.add_comm 1 n - -lemma oddShiftShiftSnd_eq_oddShiftSnd (j : Fin n.succ) : oddShiftShiftSnd j = oddShiftSnd j := by - rw [Fin.ext_iff] - rfl - -lemma oddSnd_eq_oddShiftSnd (j : Fin n) : oddSnd j = oddShiftSnd j := by - rw [Fin.ext_iff] - simp only [oddSnd, Fin.val_cast, Fin.val_natAdd, oddShiftSnd, add_left_inj] - exact Nat.add_comm n 1 - -lemma oddShiftZero_eq_oddFst : oddShiftZero = oddFst (0 : Fin n.succ) := by - ext - simp [oddShiftZero, oddFst] - -lemma oddShiftFst_castSucc_eq_oddFst_succ (j : Fin n) : - oddShiftFst j.castSucc = oddFst j.succ := by - rw [Fin.ext_iff] - simp only [oddShiftFst, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, oddFst, Fin.val_succ] - exact Nat.add_comm 1 ↑j - -lemma oddShiftFst_last_eq_oddMid : oddShiftFst (Fin.last n) = oddMid := by - rw [Fin.ext_iff] - simp only [oddShiftFst, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, oddMid, Fin.val_last] - exact Nat.add_comm 1 n - -lemma oddShiftSnd_eq_oddSnd (j : Fin n) : oddShiftSnd j = oddSnd j := by - rw [Fin.ext_iff] - simp only [oddShiftSnd, Fin.val_cast, Fin.val_natAdd, oddSnd, add_left_inj] - ring - -end theDeltas - -/-! - -## B. The first plane - --/ - -/-! - -### B.1. The basis vectors of the first plane as charges - --/ - -/-- The first part of the basis as charge assignments. -/ -def basisAsCharges (j : Fin n) : (PureU1 (2 * n + 1)).Charges := - fun i => - if i = oddFst j then - 1 - else - if i = oddSnd j then - - 1 - else - 0 - -/-! - -### B.2. Components of the basis vectors as charges - --/ - -lemma basis_on_oddFst_self (j : Fin n) : basisAsCharges j (oddFst j) = 1 := by - simp [basisAsCharges] - -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 [oddFst, oddSnd] - split - · rename_i h1 - rw [Fin.ext_iff] at h1 - simp_all - rw [Fin.ext_iff] at h - simp_all - · split - · rename_i h1 h2 - simp_all - rw [Fin.ext_iff] at h2 - simp only [Fin.val_castAdd, Fin.val_natAdd] at h2 - omega - · rfl - -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_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 - any_goals rfl - all_goals - rename_i h1 h2 - rw [Fin.ext_iff] at h1 h2 - simp_all only [Fin.cast_inj, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, neg_neg, - add_eq_right, AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, not_false_eq_true] - all_goals - rename_i h3 - rw [Fin.ext_iff] at h3 - simp_all only [Fin.val_natAdd, Fin.val_castAdd, add_eq_right, - AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, not_false_eq_true] - all_goals - omega - -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_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_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.val_cast, Fin.val_castAdd, Fin.val_natAdd, Fin.val_eq_zero, - add_zero, oddFst] at h - omega - · split <;> rename_i h2 - · rw [Fin.ext_iff] at h2 - simp only [oddMid, Fin.isValue, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, - Fin.val_eq_zero, add_zero, oddSnd] at h2 - omega - · rfl - -/-! - -### B.3. The basis vectors satisfy the linear ACCs - --/ - -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_odd] - simp [basis_oddSnd_eq_minus_oddFst, basis_on_oddMid] - -/-! - -### B.4. The basis vectors as `LinSols` - --/ - -/-- The first part of the basis as `LinSols`. -/ -@[simps!] -def basis (j : Fin n) : (PureU1 (2 * n + 1)).LinSols := - ⟨basisAsCharges j, by - intro i - simp only [PureU1_numberLinear] at i - match i with - | 0 => - exact basis_linearACC j⟩ - -/-! - -### B.5. The inclusion of the first plane into charges - --/ - -/-- A point in the span of the first part of the basis as a charge. -/ -def P (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := ∑ i, f i • basisAsCharges i - -/-! - -### B.6. Components of the first plane - --/ - -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_oddFst_self] - exact Rat.mul_one (f j) - · intro k _ 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_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_oddSnd_self] - exact mul_neg_one (f j) - · intro k _ hkj - rw [basis_on_oddSnd_other hkj] - exact Rat.mul_zero (f k) - · simp - -lemma P_oddMid (f : Fin n → ℚ) : P f oddMid = 0 := by - rw [P, sum_of_charges] - simp [HSMul.hSMul, SMul.smul, basis_on_oddMid] - -/-! - -### B.7. Points on the first plane satisfies the ACCs - --/ - -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_odd] - simp [P_oddSnd, P_oddFst, P_oddMid] - -set_option backward.isDefEq.respectTransparency false in -lemma P_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P f) = 0 := by - 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_oddFst, P_oddSnd] - ring - -/-! - -### B.8. Kernel of the inclusion into charges - --/ - -lemma P_zero (f : Fin n → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by - intro i - erw [← P_oddFst f] - rw [h] - rfl - -/-- A point in the span of the first part of the basis. -/ -def P' (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols := ∑ i, f i • basis i - -lemma P'_val (f : Fin n → ℚ) : (P' f).val = P f := by - simp only [P', P] - funext i - rw [sum_of_anomaly_free_linear, sum_of_charges] - rfl - -/-! - -### B.9. The basis vectors are linearly independent - --/ - -theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := by - apply Fintype.linearIndependent_iff.mpr - intro f h - change P' f = 0 at h - have h1 : (P' f).val = 0 := - (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0) - (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h)))) - (ACCSystemLinear.LinSols.val 0))).mp rfl - rw [P'_val] at h1 - exact P_zero f h1 - -/-! - -## C. The second plane - --/ - -/-! - -### C.1. The basis vectors of the second plane as 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 = oddShiftFst j then - 1 - else - if i = oddShiftSnd j then - - 1 - else - 0 - -/-! - -### C.2. Components of the basis vectors as charges - --/ - -lemma basis!_on_oddShiftFst_self (j : Fin n) : basis!AsCharges j (oddShiftFst j) = 1 := by - simp [basis!AsCharges] - -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 [oddShiftFst, oddShiftSnd] - split - · rename_i h1 - rw [Fin.ext_iff] at h1 - simp_all - rw [Fin.ext_iff] at h - simp_all - · split - · rename_i h1 h2 - simp_all - rw [Fin.ext_iff] at h2 - simp only [Fin.val_castAdd, Fin.val_natAdd] at h2 - omega - rfl - -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!_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 - any_goals rfl - all_goals rename_i h1 h2 - all_goals rw [Fin.ext_iff] at h1 h2 - all_goals simp_all - · subst h1 - exact Fin.elim0 i - all_goals rename_i h3 - all_goals rw [Fin.ext_iff] at h3 - all_goals simp_all - all_goals omega - -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_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_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.val_cast, Fin.val_castAdd, Fin.val_eq_zero, - oddShiftFst, Fin.val_natAdd] at h - omega - · split <;> rename_i h2 - · rw [Fin.ext_iff] at h2 - simp only [oddShiftZero, Fin.isValue, Fin.val_cast, Fin.val_castAdd, Fin.val_eq_zero, - oddShiftSnd, Fin.val_natAdd] at h2 - omega - · rfl - -/-! - -### C.3. The basis vectors satisfy the linear ACCs - --/ - -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_oddShift, basis!_on_oddShiftZero] - simp [basis!_oddShiftSnd_eq_minus_oddShiftFst] - -/-! - -### C.4. The basis vectors as `LinSols` - --/ - -/-- The second part of the basis as `LinSols`. -/ -@[simps!] -def basis! (j : Fin n) : (PureU1 (2 * n + 1)).LinSols := - ⟨basis!AsCharges j, by - intro i - simp only [PureU1_numberLinear] at i - match i with - | 0 => - exact basis!_linearACC j⟩ - -/-! - -### C.5. Permutations equal adding basis vectors - --/ - -/-- 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 - (Equiv.swap (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 = oddShiftFst j - · subst hi - simp [HSMul.hSMul, basis!_on_oddShiftFst_self, Equiv.swap_apply_left] - · by_cases hi2 : i = oddShiftSnd j - · subst hi2 - simp [HSMul.hSMul,basis!_on_oddShiftSnd_self, Equiv.swap_apply_right] - · simp only [Equiv.invFun_as_coe, HSMul.hSMul, ACCSystemCharges.chargesAddCommMonoid_add, - ACCSystemCharges.chargesModule_smul] - rw [basis!_on_other hi hi2] - aesop - -/-! - -### C.6. The inclusion of the second 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 + 1)).Charges := ∑ i, f i • basis!AsCharges i - -/-! - -### C.7. Components of the second plane - --/ - -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_oddShiftFst_self] - exact Rat.mul_one (f j) - · intro k _ 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!_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_oddShiftSnd_self] - exact mul_neg_one (f j) - · intro k _ hkj - rw [basis!_on_oddShiftSnd_other hkj] - exact Rat.mul_zero (f k) - · simp - -lemma P!_oddShiftZero (f : Fin n → ℚ) : P! f oddShiftZero = 0 := by - rw [P!, sum_of_charges] - simp [HSMul.hSMul, SMul.smul, basis!_on_oddShiftZero] - -/-! - -### C.8. Points on the second plane satisfies the ACCs - --/ - -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_oddShift] - simp [P!_oddShiftSnd, P!_oddShiftFst, P!_oddShiftZero] - -set_option backward.isDefEq.respectTransparency false in -lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P! f) = 0 := by - 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!_oddShiftFst, P!_oddShiftSnd] - ring - -/-! - -### C.9. Kernel of the inclusion into charges - --/ - -lemma P!_zero (f : Fin n → ℚ) (h : P! f = 0) : ∀ i, f i = 0 := by - intro i - rw [← P!_oddShiftFst f] - rw [h] - rfl - -/-! - -### C.10. The inclusion of the second plane into LinSols - --/ - -/-- A point in the span of the second part of the basis. -/ -def P!' (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols := ∑ i, f i • basis! i - -lemma P!'_val (f : Fin n → ℚ) : (P!' f).val = P! f := by - simp only [P!', P!] - funext i - rw [sum_of_anomaly_free_linear, sum_of_charges] - rfl - -/-! - -### C.11. The basis vectors are linearly independent - --/ - -theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by - apply Fintype.linearIndependent_iff.mpr - intro f h - change P!' f = 0 at h - have h1 : (P!' f).val = 0 := - (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0) - (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h)))) - (ACCSystemLinear.LinSols.val 0))).mp rfl - rw [P!'_val] at h1 - exact P!_zero f h1 - -/-! - -## D. The mixed cubic ACC from points in both planes - --/ - -set_option backward.isDefEq.respectTransparency false in -lemma P_P_P!_accCube (g : Fin n → ℚ) (j : Fin n) : - accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) - = (P g (oddShiftFst j))^2 - (g j)^2 := by - simp only [accCubeTriLinSymm, PureU1Charges_numberCharges, TriLinearSymm.mk₃_toFun_apply_apply] - rw [sum_oddShift, basis!_on_oddShiftZero] - simp only [mul_zero, Function.comp_apply, zero_add] - 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_oddShiftFst_other hkj.symm, basis!_on_oddShiftSnd_other hkj.symm] - simp only [mul_zero, add_zero] - · simp - -/-! - -## E. The combined basis - --/ - -/-! - -### E.1. The combined basis as `LinSols` - --/ - -/-- The whole basis as `LinSols`. -/ -def basisa : Fin n ⊕ Fin n → (PureU1 (2 * n + 1)).LinSols := fun i => - match i with - | .inl i => basis i - | .inr i => basis! i - -/-! - -### E.2. The inclusion of the span of the combined basis into charges - --/ - -/-- 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 - -/-! - -### E.3. Components of the inclusion - --/ - -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 [oddShiftShiftZero_eq_oddFst_zero] - rw [oddShiftShiftZero_eq_oddShiftZero] - rw [P!_oddShiftZero, oddShiftZero_eq_oddFst, P_oddFst] - exact Rat.add_zero (f 0) - -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 [oddShiftShiftFst_eq_oddFst_succ] - rw [oddShiftShiftFst_eq_oddShiftFst_castSucc] - rw [P!_oddShiftFst, oddShiftFst_castSucc_eq_oddFst_succ, P_oddFst] - -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 [oddShiftShiftMid_eq_oddMid] - rw [oddShiftShiftMid_eq_oddShiftFst_last] - rw [P!_oddShiftFst, oddShiftFst_last_eq_oddMid, P_oddMid] - exact Rat.zero_add (g (Fin.last n)) - -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 [oddShiftShiftSnd_eq_oddSnd] - rw [oddShiftShiftSnd_eq_oddShiftSnd] - rw [P!_oddShiftSnd, oddShiftSnd_eq_oddSnd, P_oddSnd] - ring - -/-! - -### E.4. Kernel of the inclusion into charges - --/ - -set_option backward.isDefEq.respectTransparency false in -lemma Pa_zero (f g : Fin n.succ → ℚ) (h : Pa f g = 0) : - ∀ i, f i = 0 := by - have h₃ := Pa_oddShiftShiftZero f g - rw [h] at h₃ - change 0 = _ at h₃ - intro i - have hinduc (iv : ℕ) (hiv : iv < n.succ) : f ⟨iv, hiv⟩ = 0 := by - induction iv - exact h₃.symm - rename_i iv hi - have hivi : iv < n.succ := lt_of_succ_lt hiv - have hi2 := hi 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_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 - -lemma Pa_zero! (f g : Fin n.succ → ℚ) (h : Pa f g = 0) : - ∀ i, g i = 0 := by - have hf := Pa_zero f g h - rw [Pa, P] at h - simp only [succ_eq_add_one, hf, zero_smul, sum_const_zero, zero_add] at h - exact P!_zero g h - -/-! - -### E.5. The inclusion of the span of the combined basis into LinSols - --/ - -/-- A point in the span of the whole basis. -/ -def Pa' (f : (Fin n) ⊕ (Fin n) → ℚ) : (PureU1 (2 * n + 1)).LinSols := - ∑ i, f i • basisa i - -lemma Pa'_P'_P!' (f : (Fin n) ⊕ (Fin n) → ℚ) : - Pa' f = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr) := by - exact Fintype.sum_sum_type _ - -/-! - -### E.6. The combined basis vectors are linearly independent - --/ - -theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n.succ) := by - apply Fintype.linearIndependent_iff.mpr - intro f h - change Pa' f = 0 at h - have h1 : (Pa' f).val = 0 := - (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0) - (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h)))) - (ACCSystemLinear.LinSols.val 0))).mp rfl - rw [Pa'_P'_P!'] at h1 - change (P' (f ∘ Sum.inl)).val + (P!' (f ∘ Sum.inr)).val = 0 at h1 - rw [P!'_val, P'_val] at h1 - change Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0 at h1 - have hf := Pa_zero (f ∘ Sum.inl) (f ∘ Sum.inr) h1 - have hg := Pa_zero! (f ∘ Sum.inl) (f ∘ Sum.inr) h1 - intro i - simp_all only [succ_eq_add_one, Function.comp_apply] - cases i - · simp_all - · simp_all - -/-! - -### E.7. Injectivity of the inclusion into linear solutions - --/ - -lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n.succ) → ℚ) : Pa' f = Pa' f' ↔ f = f' := by - refine Iff.intro (fun h => ?_) (fun h => ?_) - · funext i - rw [Pa', Pa'] at h - have h1 : ∑ i : Fin n.succ ⊕ Fin n.succ, (f i + (- f' i)) • basisa i = 0 := by - simp only [add_smul, neg_smul] - rw [Finset.sum_add_distrib] - rw [h] - rw [← Finset.sum_add_distrib] - simp - have h2 : ∀ i, (f i + (- f' i)) = 0 := by - exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent n) - (fun i => f i + -f' i) h1 - have h2i := h2 i - linarith - · rw [h] - -lemma Pa'_elim_eq_iff (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) : - Pa' (Sum.elim g f) = Pa' (Sum.elim g' f') ↔ Pa g f = Pa g' f' := by - refine Iff.intro (fun h => ?_) (fun h => ?_) - · rw [Pa'_eq, Sum.elim_eq_iff] at h - 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] - exact h - -lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) : - Pa g f = Pa g' f' ↔ g = g' ∧ f = f' := by - rw [← Pa'_elim_eq_iff] - rw [← Sum.elim_eq_iff] - exact Pa'_eq _ _ - -/-! - -### E.8. Cardinality of the basis - --/ - -lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n.succ)) = - Module.finrank ℚ (PureU1 (2 * n.succ + 1)).LinSols := by - erw [BasisLinear.finrank_AnomalyFreeLinear] - simp only [Fintype.card_sum, Fintype.card_fin] - exact Eq.symm (Nat.two_mul n.succ) - -/-! - -### E.9. The basis vectors as a basis - --/ - -/-- The basis formed out of our basisa vectors. -/ -noncomputable def basisaAsBasis : - Basis (Fin n.succ ⊕ Fin n.succ) ℚ (PureU1 (2 * n.succ + 1)).LinSols := - basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card - -/-! - -## F. Every Lienar solution is the sum of a point from each plane - --/ - -lemma span_basis (S : (PureU1 (2 * n.succ + 1)).LinSols) : - ∃ (g f : Fin n.succ → ℚ), S.val = P g + P! 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 - use f ∘ Sum.inl - use f ∘ Sum.inr - rw [← hf] - simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, P'_val, P!'_val] - rfl - -/-! - -### F.1. Relation under permutations - --/ - -lemma span_basis_swap! {S : (PureU1 (2 * n.succ + 1)).LinSols} (j : Fin n.succ) - (hS : ((FamilyPermutations (2 * n.succ + 1)).linSolRep - (Equiv.swap (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 (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 [(Submodule.mem_span_range_iff_exists_fun ℚ)] - use f - rfl - 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 - apply Submodule.subset_span - simp_all only [Set.mem_range, exists_apply_eq_apply] - have hX : X ∈ Submodule.span ℚ (Set.range (basis!AsCharges)) := by - apply Submodule.add_mem - exact hf - exact hP - have hXsum := (Submodule.mem_span_range_iff_exists_fun ℚ).mp hX - obtain ⟨f', hf'⟩ := hXsum - use g - use f' - change P! f' = _ at hf' - erw [hf'] - simp only [and_self, and_true, X] - rw [← add_assoc, ← hS1] - apply swap!_as_add at hS - exact hS - -end VectorLikeOddPlane - -end PureU1 diff --git a/Physlib/QFT/QED/AnomalyCancellation/Odd/LineInCubic.lean b/Physlib/QFT/QED/AnomalyCancellation/Odd/LineInCubic.lean index a2115ba7f..377470bfe 100644 --- a/Physlib/QFT/QED/AnomalyCancellation/Odd/LineInCubic.lean +++ b/Physlib/QFT/QED/AnomalyCancellation/Odd/LineInCubic.lean @@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.QFT.QED.AnomalyCancellation.LineInPlaneCond -public import Physlib.QFT.QED.AnomalyCancellation.Odd.BasisLinear +public import Physlib.QFT.QED.AnomalyCancellation.Odd.Basis /-! # Line In Cubic Odd case @@ -35,30 +35,30 @@ open VectorLikeOddPlane /-- A property on `LinSols`, satisfied if every point on the line between the two planes in the basis through that point is in the cubic. -/ def LineInCubic (S : (PureU1 (2 * n + 1)).LinSols) : Prop := - ∀ (g f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ), - accCube (2 * n + 1) (a • P g + b • P! f) = 0 + ∀ (g f : Fin n → ℚ) (_ : S.val = basisCharge g f) (a b : ℚ), + accCube (2 * n + 1) (a • symmPlaneAsCharges g + b • shiftPlaneAsCharges f) = 0 set_option backward.isDefEq.respectTransparency false in /-- The condition that a linear solution sits on a line between the two planes within the cubic expands into a on `accCubeTriLinSymm` applied to the points within the planes. -/ lemma lineInCubic_expand {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S) : - ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) (a b : ℚ), - 3 * a * b * (a * accCubeTriLinSymm (P g) (P g) (P! f) - + b * accCubeTriLinSymm (P! f) (P! f) (P g)) = 0 := by + ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = symmPlaneAsCharges g + shiftPlaneAsCharges f) (a b : ℚ), + 3 * a * b * (a * accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) + + b * accCubeTriLinSymm (shiftPlaneAsCharges f) (shiftPlaneAsCharges f) (symmPlaneAsCharges 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 • symmPlaneAsCharges g + b • shiftPlaneAsCharges f) = 0 at h1 simp only [TriLinearSymm.toCubic_add] at h1 simp only [HomogeneousCubic.map_smul, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1 - erw [P_accCube, P!_accCube] at h1 + erw [symmPlaneAsCharges_accCube, shiftPlaneAsCharges_accCube] at h1 rw [← h1] ring -lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S) : - ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f), - accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by +lemma line_in_cubic_symmPlane_symmPlane_shiftPlane {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S) : + ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = symmPlaneAsCharges g + shiftPlaneAsCharges f), + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges 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 @@ -81,36 +81,36 @@ lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols} set_option backward.isDefEq.respectTransparency false in 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), + ∀ (j : Fin n.succ) (g f : Fin n.succ → ℚ) (_ : S.val = basisCharge g f), (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) - * accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := by + * accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftBasisAsCharges j) = 0 := by intro j g f h let S' := (FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j)) S have hSS' : ((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (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 + obtain ⟨g', f', hall⟩ := span_basis_swapShift j hSS' g f h + have h1 := line_in_cubic_symmPlane_symmPlane_shiftPlane (lineInCubicPerm_self LIC) g f h + have h2 := line_in_cubic_symmPlane_symmPlane_shiftPlane (lineInCubicPerm_self (lineInCubicPerm_permute LIC (Equiv.swap (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 -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) = +lemma symmPlane_symmPlane_shiftBasisAsCharges_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols} + (f g : Fin n.succ.succ → ℚ) (hS : S.val = basisCharge f g) : + accCubeTriLinSymm (symmPlaneAsCharges f) (symmPlaneAsCharges f) (shiftBasisAsCharges 0) = (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_oddShiftShiftZero f g] + rw [symmPlane_symmPlane_shiftBasisAsCharges_accCube f 0] + rw [← basisCharge_oddShiftShiftZero f g] rw [← hS] have ht : oddShiftFst (0 : Fin n.succ.succ) = oddFst 1 := rfl nth_rewrite 1 [ht] - rw [P_oddFst] - have h1 := Pa_oddShiftShiftZero f g - have h4 := Pa_oddShiftShiftSnd f g 0 - have h2 := Pa_oddShiftShiftFst f g 0 + rw [symmPlaneAsCharges_oddFst] + have h1 := basisCharge_oddShiftShiftZero f g + have h4 := basisCharge_oddShiftShiftSnd f g 0 + have h2 := basisCharge_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 (oddShiftShiftFst 0) + S.val oddShiftShiftZero + @@ -126,7 +126,7 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols} 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 + rw [symmPlane_symmPlane_shiftBasisAsCharges_accCube' g f hfg] at h1 simp only [Nat.succ_eq_add_one, mul_eq_zero] at h1 cases h1 <;> rename_i h1 · left diff --git a/Physlib/QFT/QED/AnomalyCancellation/Odd/Parameterization.lean b/Physlib/QFT/QED/AnomalyCancellation/Odd/Parameterization.lean index 567fbb4a6..4fd783e85 100644 --- a/Physlib/QFT/QED/AnomalyCancellation/Odd/Parameterization.lean +++ b/Physlib/QFT/QED/AnomalyCancellation/Odd/Parameterization.lean @@ -30,16 +30,16 @@ 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 (P! f) (P! f) (P g)) • P' g + - (- accCubeTriLinSymm (P g) (P g) (P! f)) • P!' f) + a • ((accCubeTriLinSymm (shiftPlaneAsCharges f) (shiftPlaneAsCharges f) (symmPlaneAsCharges g)) • symmPlane g + + (- accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f)) • shiftPlane f) lemma parameterizationAsLinear_val (g 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 (shiftPlaneAsCharges f) (shiftPlaneAsCharges f) (symmPlaneAsCharges g)) • symmPlaneAsCharges g + + (- accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f)) • shiftPlaneAsCharges f) := by rw [parameterizationAsLinear] - change a • (_ • (P' g).val + _ • (P!' f).val) = _ - rw [P'_val, P!'_val] + change a • (_ • (symmPlane g).val + _ • (shiftPlane f).val) = _ + rw [symmPlane_val, shiftPlane_val] set_option backward.isDefEq.respectTransparency false in /-- The parameterization satisfies the cubic ACC. -/ @@ -50,7 +50,7 @@ lemma parameterizationCharge_cube (g f : Fin n → ℚ) (a : ℚ) : rw [HomogeneousCubic.map_smul] rw [TriLinearSymm.toCubic_add] rw [HomogeneousCubic.map_smul, HomogeneousCubic.map_smul] - erw [P_accCube g, P!_accCube f] + erw [symmPlaneAsCharges_accCube g, shiftPlaneAsCharges_accCube f] rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] @@ -63,54 +63,54 @@ def parameterization (g f : Fin n → ℚ) (a : ℚ) : parameterizationCharge_cube g f a⟩ 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 + (g f : Fin n → ℚ) (hS : S.val = symmPlaneAsCharges g + shiftPlaneAsCharges f) : + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) = + - accCubeTriLinSymm (shiftPlaneAsCharges f) (shiftPlaneAsCharges f) (symmPlaneAsCharges g) := by have hC := S.cubicSol rw [hS] at hC - change (accCube (2 * n + 1)) (P g + P! f) = 0 at hC + change (accCube (2 * n + 1)) (symmPlaneAsCharges g + shiftPlaneAsCharges f) = 0 at hC erw [TriLinearSymm.toCubic_add] at hC - erw [P_accCube] at hC - erw [P!_accCube] at hC + erw [symmPlaneAsCharges_accCube] at hC + erw [shiftPlaneAsCharges_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 (symmPlaneAsCharges g, symmPlaneAsCharges g, shiftPlaneAsCharges f) ≠ 0`. In this case our parameterization above will be able to recover this point. -/ 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 + ∀ (g f : Fin n.succ → ℚ) (_ : S.val = symmPlaneAsCharges g + shiftPlaneAsCharges f), + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) ≠ 0 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 + (hs : ∃ (g f : Fin n.succ → ℚ), S.val = symmPlaneAsCharges g + shiftPlaneAsCharges f ∧ + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) ≠ 0) : GenericCase S := by intro g f hS hC obtain ⟨g', f', hS', hC'⟩ := hs rw [hS] at hS' - erw [Pa_eq] at hS' + erw [basisCharge_eq] at hS' 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 (symmPlaneAsCharges g, symmPlaneAsCharges g, shiftPlaneAsCharges 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.succ + 1)).Sols) : Prop := - ∀ (g f : Fin n.succ → ℚ) (_ : S.val = P g + P! f), - accCubeTriLinSymm (P g) (P g) (P! f) = 0 + ∀ (g f : Fin n.succ → ℚ) (_ : S.val = symmPlaneAsCharges g + shiftPlaneAsCharges f), + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) = 0 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 + (hs : ∃ (g f : Fin n.succ → ℚ), S.val = symmPlaneAsCharges g + shiftPlaneAsCharges f ∧ + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) = 0) : SpecialCase S := by intro g f hS obtain ⟨g', f', hS', hC'⟩ := hs rw [hS] at hS' - erw [Pa_eq] at hS' + erw [basisCharge_eq] at hS' rw [hS'.1, hS'.2] exact hC' lemma generic_or_special (S : (PureU1 (2 * n.succ + 1)).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 (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) ≠ 0 ∨ + accCubeTriLinSymm (symmPlaneAsCharges g) (symmPlaneAsCharges g) (shiftPlaneAsCharges f) = 0 := by exact ne_or_eq _ _ cases h1 <;> rename_i h1 · exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩) @@ -119,7 +119,7 @@ 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_basis S.1.1 - use g, f, (accCubeTriLinSymm (P! f) (P! f) (P g))⁻¹ + use g, f, (accCubeTriLinSymm (shiftPlaneAsCharges f) (shiftPlaneAsCharges f) (symmPlaneAsCharges g))⁻¹ rw [parameterization] apply ACCSystem.Sols.ext rw [parameterizationAsLinear_val] @@ -135,14 +135,14 @@ lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols} intro g f hS a b erw [TriLinearSymm.toCubic_add] rw [HomogeneousCubic.map_smul, HomogeneousCubic.map_smul] - erw [P_accCube, P!_accCube] + erw [symmPlaneAsCharges_accCube, shiftPlaneAsCharges_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 (shiftPlaneAsCharges f) (shiftPlaneAsCharges f) (symmPlaneAsCharges g) = 0 at h erw [h] simp diff --git a/Physlib/QFT/QED/AnomalyCancellation/Odd/Planes/ShiftPlane.lean b/Physlib/QFT/QED/AnomalyCancellation/Odd/Planes/ShiftPlane.lean new file mode 100644 index 000000000..f7e0a8796 --- /dev/null +++ b/Physlib/QFT/QED/AnomalyCancellation/Odd/Planes/ShiftPlane.lean @@ -0,0 +1,462 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +module + +public import Physlib.QFT.QED.AnomalyCancellation.Odd.Planes.SymmPlane +/-! +# The shifted plane for the odd case + +This file defines the shifted plane for `PureU1 (2 * n + 1)`. + +The shifted plane arises from the shifted split `1 + n + n` of the `2 * n + 1` charges. +It is called "shifted" because the positions (`oddShiftFst`, `oddShiftSnd`, `oddShiftZero`) +come from this shifted split, which places the distinguished element at position `0` rather +than in the middle. + +## Main definitions + +- `shiftBasisAsCharges` : The basis vectors of the shifted plane as charges. +- `shiftBasis` : The basis vectors of the shifted plane as `LinSols`. +- `shiftPlaneAsCharges` : A point in the span of the shifted basis as a charge assignment. +- `shiftPlane` : A point in the span of the shifted basis as a linear solution. + +## Key results + +- `shiftPlaneAsCharges_accCube` : Charges from the shifted plane satisfy the cubic ACC. +- `shiftBasis_linear_independent` : The shifted basis vectors are linearly independent. +- `linSolRep_swap_oddShift_eq_add` : Swapping elements equals adding a basis vector. + +## Table of contents + +- A.1. The shifted split: Splitting the charges up via `1 + n + n` +- A.2. The shifted shifted split: Splitting the charges up via `((1+n)+1) + n.succ` +- A.3. Relating the splittings together +- B. The shifted plane + - B.1. The basis vectors of the shifted plane as charges + - B.2. Components of the basis vectors as charges + - B.3. The basis vectors satisfy the linear ACCs + - B.4. The basis vectors as `LinSols` + - B.5. The basis vectors are linearly independent + - B.6. Permutations equal adding basis vectors + - B.7. The inclusion of the shifted plane into charges (`shiftPlaneAsCharges`) + - B.8. Components of the shifted plane + - B.9. Points on the shifted plane satisfy the ACCs + - B.10. Kernel of the inclusion into charges + - B.11. The inclusion of the shifted plane into `LinSols` (`shiftPlane`) + +-/ + +@[expose] public section + +open Module Nat Finset BigOperators + +namespace PureU1 + +variable {n : ℕ} + +namespace VectorLikeOddPlane + +section theDeltas + +/-! + +### A.1. The shifted split: Splitting the charges up via `1 + n + n` + +-/ + +/-- The inclusion of `Fin n` into `Fin (1 + n + n)` via the first `n`. + This is then casted to `Fin (2 * n + 1)`. -/ +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 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 (odd_shift_eq n) (Fin.castAdd n (Fin.castAdd n 1)) + +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 + rw [h1, Fin.sum_univ_add, Fin.sum_univ_add] + simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply] + rw [add_assoc, Finset.sum_add_distrib] + rfl + +/-! + +### A.2. The shifted shifted split: Splitting the charges up via `((1+n)+1) + n.succ` + +-/ + +lemma odd_shift_shift_eq (n : ℕ) : ((1+n)+1) + n.succ = 2 * n.succ + 1 := by + omega + +/-- The element representing the first `1` in `Fin (1 + n + 1 + n.succ)` casted + to `Fin (2 * n.succ + 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 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 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 oddShiftShiftSnd (j : Fin n.succ) : Fin (2 * n.succ + 1) := + Fin.cast (odd_shift_shift_eq n) (Fin.natAdd ((1+n)+1) j) + +/-! + +### A.3. Relating the splittings together + +-/ +lemma oddShiftShiftZero_eq_oddFst_zero : @oddShiftShiftZero n = oddFst 0 := + Fin.rev_inj.mp rfl + +lemma oddShiftShiftZero_eq_oddShiftZero : @oddShiftShiftZero n = oddShiftZero := rfl + +lemma oddShiftShiftFst_eq_oddFst_succ (j : Fin n) : + oddShiftShiftFst j = oddFst j.succ := by + rw [Fin.ext_iff] + simp only [succ_eq_add_one, oddShiftShiftFst, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, + oddFst, Fin.val_succ] + exact Nat.add_comm 1 ↑j + +lemma oddShiftShiftFst_eq_oddShiftFst_castSucc (j : Fin n) : + oddShiftShiftFst j = oddShiftFst j.castSucc := by + rfl + +lemma oddShiftShiftMid_eq_oddMid : @oddShiftShiftMid n = oddMid := by + rw [Fin.ext_iff] + simp only [succ_eq_add_one, oddShiftShiftMid, Fin.isValue, Fin.val_cast, Fin.val_castAdd, + Fin.val_natAdd, Fin.val_eq_zero, add_zero, oddMid] + exact Nat.add_comm 1 n + +lemma oddShiftShiftMid_eq_oddShiftFst_last : oddShiftShiftMid = oddShiftFst (Fin.last n) := by + rfl + +lemma oddShiftShiftSnd_eq_oddSnd (j : Fin n.succ) : oddShiftShiftSnd j = oddSnd j := by + rw [Fin.ext_iff] + simp only [succ_eq_add_one, oddShiftShiftSnd, Fin.val_cast, Fin.val_natAdd, oddSnd, add_left_inj] + exact Nat.add_comm 1 n + +lemma oddShiftShiftSnd_eq_oddShiftSnd (j : Fin n.succ) : oddShiftShiftSnd j = oddShiftSnd j := by + rw [Fin.ext_iff] + rfl + +lemma oddSnd_eq_oddShiftSnd (j : Fin n) : oddSnd j = oddShiftSnd j := by + rw [Fin.ext_iff] + simp only [oddSnd, Fin.val_cast, Fin.val_natAdd, oddShiftSnd, add_left_inj] + exact Nat.add_comm n 1 + +lemma oddShiftZero_eq_oddFst : oddShiftZero = oddFst (0 : Fin n.succ) := by + ext + simp [oddShiftZero, oddFst] + +lemma oddShiftFst_castSucc_eq_oddFst_succ (j : Fin n) : + oddShiftFst j.castSucc = oddFst j.succ := by + rw [Fin.ext_iff] + simp only [oddShiftFst, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, oddFst, Fin.val_succ] + exact Nat.add_comm 1 ↑j + +lemma oddShiftFst_last_eq_oddMid : oddShiftFst (Fin.last n) = oddMid := by + rw [Fin.ext_iff] + simp only [oddShiftFst, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, oddMid, Fin.val_last] + exact Nat.add_comm 1 n + +lemma oddShiftSnd_eq_oddSnd (j : Fin n) : oddShiftSnd j = oddSnd j := by + rw [Fin.ext_iff] + simp only [oddShiftSnd, Fin.val_cast, Fin.val_natAdd, oddSnd, add_left_inj] + ring + +end theDeltas + +/-! + +## B. The shifted plane + +-/ + +/-! + +### B.1. The basis vectors of the shifted plane as charges + +-/ + +/-- The basis vectors of the shifted plane as charge assignments. -/ +def shiftBasisAsCharges (j : Fin n) : (PureU1 (2 * n + 1)).Charges := + fun i => + if i = oddShiftFst j then + 1 + else + if i = oddShiftSnd j then + - 1 + else + 0 + +/-! + +### B.2. Components of the basis vectors as charges + +-/ + +lemma shiftBasisAsCharges_on_oddShiftFst_self (j : Fin n) : + shiftBasisAsCharges j (oddShiftFst j) = 1 := by + simp [shiftBasisAsCharges] + +lemma shiftBasisAsCharges_on_oddShiftFst_other {k j : Fin n} (h : k ≠ j) : + shiftBasisAsCharges k (oddShiftFst j) = 0 := by + simp only [shiftBasisAsCharges, PureU1_numberCharges] + simp only [oddShiftFst, oddShiftSnd] + split + · rename_i h1 + rw [Fin.ext_iff] at h1 + simp_all + rw [Fin.ext_iff] at h + simp_all + · split + · rename_i h1 h2 + simp_all + rw [Fin.ext_iff] at h2 + simp only [Fin.val_castAdd, Fin.val_natAdd] at h2 + omega + rfl + +lemma shiftBasisAsCharges_on_other {k : Fin n} {j : Fin (2 * n + 1)} + (h1 : j ≠ oddShiftFst k) (h2 : j ≠ oddShiftSnd k) : + shiftBasisAsCharges k j = 0 := by + simp only [shiftBasisAsCharges, PureU1_numberCharges] + simp_all only [ne_eq, ↓reduceIte] + +lemma shiftBasisAsCharges_oddShiftSnd_eq_minus_oddShiftFst (j i : Fin n) : + shiftBasisAsCharges j (oddShiftSnd i) = - shiftBasisAsCharges j (oddShiftFst i) := by + simp only [shiftBasisAsCharges, PureU1_numberCharges, oddShiftSnd, oddShiftFst] + split <;> split + any_goals split + any_goals split + any_goals rfl + all_goals rename_i h1 h2 + all_goals rw [Fin.ext_iff] at h1 h2 + all_goals simp_all + · subst h1 + exact Fin.elim0 i + all_goals rename_i h3 + all_goals rw [Fin.ext_iff] at h3 + all_goals simp_all + all_goals omega + +lemma shiftBasisAsCharges_on_oddShiftSnd_self (j : Fin n) : + shiftBasisAsCharges j (oddShiftSnd j) = - 1 := by + rw [shiftBasisAsCharges_oddShiftSnd_eq_minus_oddShiftFst, + shiftBasisAsCharges_on_oddShiftFst_self] + +lemma shiftBasisAsCharges_on_oddShiftSnd_other {k j : Fin n} (h : k ≠ j) : + shiftBasisAsCharges k (oddShiftSnd j) = 0 := by + rw [shiftBasisAsCharges_oddShiftSnd_eq_minus_oddShiftFst, + shiftBasisAsCharges_on_oddShiftFst_other h] + rfl + +lemma shiftBasisAsCharges_on_oddShiftZero (j : Fin n) : + shiftBasisAsCharges j oddShiftZero = 0 := by + simp only [shiftBasisAsCharges, PureU1_numberCharges] + split <;> rename_i h + · rw [Fin.ext_iff] at h + simp only [oddShiftZero, Fin.isValue, Fin.val_cast, Fin.val_castAdd, Fin.val_eq_zero, + oddShiftFst, Fin.val_natAdd] at h + omega + · split <;> rename_i h2 + · rw [Fin.ext_iff] at h2 + simp only [oddShiftZero, Fin.isValue, Fin.val_cast, Fin.val_castAdd, Fin.val_eq_zero, + oddShiftSnd, Fin.val_natAdd] at h2 + omega + · rfl + +/-! + +### B.3. The basis vectors satisfy the linear ACCs + +-/ + +lemma shiftBasisAsCharges_linearACC (j : Fin n) : + (accGrav (2 * n + 1)) (shiftBasisAsCharges j) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + rw [sum_oddShift, shiftBasisAsCharges_on_oddShiftZero] + simp [shiftBasisAsCharges_oddShiftSnd_eq_minus_oddShiftFst] + +/-! + +### B.4. The basis vectors as `LinSols` + +-/ + +/-- The basis vectors of the shifted plane as `LinSols`. -/ +@[simps!] +def shiftBasis (j : Fin n) : (PureU1 (2 * n + 1)).LinSols := + ⟨shiftBasisAsCharges j, by + intro i + simp only [PureU1_numberLinear] at i + match i with + | 0 => + exact shiftBasisAsCharges_linearACC j⟩ + +/-! + +### B.5. The basis vectors are linearly independent + +-/ + +theorem shiftBasis_linear_independent : LinearIndependent ℚ (@shiftBasis n) := by + apply Fintype.linearIndependent_iff.mpr + intro f h + change shiftPlane f = 0 at h + have h1 : (shiftPlane f).val = 0 := + (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0) + (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h)))) + (ACCSystemLinear.LinSols.val 0))).mp rfl + rw [shiftPlane_val] at h1 + exact shiftPlaneAsCharges_zero f h1 + +/-! + +### B.6. Permutations equal adding basis vectors + +-/ + +/-- Swapping the elements oddShiftFst j and oddShiftSnd j is equivalent to adding a vector + shiftBasisAsCharges j. -/ +lemma linSolRep_swap_oddShift_eq_add {S S' : (PureU1 (2 * n + 1)).LinSols} (j : Fin n) + (hS : ((FamilyPermutations (2 * n + 1)).linSolRep + (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S') : + S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • + shiftBasisAsCharges j := by + funext i + rw [← hS, FamilyPermutations_anomalyFreeLinear_apply] + by_cases hi : i = oddShiftFst j + · subst hi + simp [HSMul.hSMul, shiftBasisAsCharges_on_oddShiftFst_self, Equiv.swap_apply_left] + · by_cases hi2 : i = oddShiftSnd j + · subst hi2 + simp [HSMul.hSMul, shiftBasisAsCharges_on_oddShiftSnd_self, Equiv.swap_apply_right] + · simp only [Equiv.invFun_as_coe, HSMul.hSMul, ACCSystemCharges.chargesAddCommMonoid_add, + ACCSystemCharges.chargesModule_smul] + rw [shiftBasisAsCharges_on_other hi hi2] + aesop + +/-! + +### B.7. The inclusion of the shifted plane into charges (`shiftPlaneAsCharges`) + +-/ + +/-- A point in the span of the shifted plane basis as a charge. -/ +def shiftPlaneAsCharges (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := + ∑ i, f i • shiftBasisAsCharges i + +/-! + +### B.8. Components of the shifted plane + +-/ + +lemma shiftPlaneAsCharges_oddShiftFst (f : Fin n → ℚ) (j : Fin n) : + shiftPlaneAsCharges f (oddShiftFst j) = f j := by + rw [shiftPlaneAsCharges, sum_of_charges] + simp only [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + · rw [shiftBasisAsCharges_on_oddShiftFst_self] + exact Rat.mul_one (f j) + · intro k _ hkj + rw [shiftBasisAsCharges_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 shiftPlaneAsCharges_oddShiftSnd (f : Fin n → ℚ) (j : Fin n) : + shiftPlaneAsCharges f (oddShiftSnd j) = - f j := by + rw [shiftPlaneAsCharges, sum_of_charges] + simp only [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + · rw [shiftBasisAsCharges_on_oddShiftSnd_self] + exact mul_neg_one (f j) + · intro k _ hkj + rw [shiftBasisAsCharges_on_oddShiftSnd_other hkj] + exact Rat.mul_zero (f k) + · simp + +lemma shiftPlaneAsCharges_oddShiftZero (f : Fin n → ℚ) : shiftPlaneAsCharges f oddShiftZero = 0 := by + rw [shiftPlaneAsCharges, sum_of_charges] + simp [HSMul.hSMul, SMul.smul, shiftBasisAsCharges_on_oddShiftZero] + +/-! + +### B.9. Points on the shifted plane satisfy the ACCs + +-/ + +lemma shiftPlaneAsCharges_linearACC (f : Fin n → ℚ) : + (accGrav (2 * n + 1)) (shiftPlaneAsCharges f) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + rw [sum_oddShift] + simp [shiftPlaneAsCharges_oddShiftSnd, shiftPlaneAsCharges_oddShiftFst, shiftPlaneAsCharges_oddShiftZero] + +set_option backward.isDefEq.respectTransparency false in +lemma shiftPlaneAsCharges_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (shiftPlaneAsCharges f) = 0 := by + rw [accCube_explicit, sum_oddShift, shiftPlaneAsCharges_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 [shiftPlaneAsCharges_oddShiftFst, shiftPlaneAsCharges_oddShiftSnd] + ring + +/-! + +### B.10. Kernel of the inclusion into charges + +-/ + +lemma shiftPlaneAsCharges_zero (f : Fin n → ℚ) (h : shiftPlaneAsCharges f = 0) : ∀ i, f i = 0 := by + intro i + rw [← shiftPlaneAsCharges_oddShiftFst f] + rw [h] + rfl + +/-! + +### B.11. The inclusion of the shifted plane into `LinSols` + +-/ + +/-- A point in the span of the shifted plane basis. -/ +def shiftPlane (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols := + ∑ i, f i • shiftBasis i + +lemma shiftPlane_val (f : Fin n → ℚ) : + (shiftPlane f).val = shiftPlaneAsCharges f := by + simp only [shiftPlane, shiftPlaneAsCharges] + funext i + rw [sum_of_anomaly_free_linear, sum_of_charges] + rfl + +end VectorLikeOddPlane + +end PureU1 diff --git a/Physlib/QFT/QED/AnomalyCancellation/Odd/Planes/SymmPlane.lean b/Physlib/QFT/QED/AnomalyCancellation/Odd/Planes/SymmPlane.lean new file mode 100644 index 000000000..6dbec64e2 --- /dev/null +++ b/Physlib/QFT/QED/AnomalyCancellation/Odd/Planes/SymmPlane.lean @@ -0,0 +1,344 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +module + +public import Physlib.QFT.QED.AnomalyCancellation.BasisLinear +public import Physlib.QFT.QED.AnomalyCancellation.VectorLike +/-! +# The symmetric plane for the odd case + +This file defines the symmetric plane for `PureU1 (2 * n + 1)`. + +The symmetric plane arises from the symmetric split `(n + 1) + n` of the `2 * n + 1` charges. +It is called "symmetric" because the positions (`oddFst`, `oddSnd`, `oddMid`) come from this +symmetric split, which divides the charges into two groups of size `n` and a middle element. + +## Main definitions + +- `symmPlaneAsCharges` : A point in the span of the symmetric basis as a charge assignment. +- `symmPlane` : A point in the span of the symmetric basis as a linear solution. +- `symmBasis` : The basis vectors of the symmetric plane as `LinSols`. +- `symmBasisAsCharges` : The basis vectors of the symmetric plane as charges. + +## Key results + +- `symmPlaneAsCharges_accCube` : Charges from the symmetric plane satisfy the cubic ACC. +- `symmBasis_linear_independent` : The symmetric basis vectors are linearly independent. + +## Table of contents + +- A.1. The symmetric split: Splitting the charges up via `(n + 1) + n` +- B. The first plane (symmetric plane) + - B.1. The basis vectors of the first plane as charges + - B.2. Components of the basis vectors as charges + - B.3. The basis vectors satisfy the linear ACCs + - B.4. The basis vectors as `LinSols` + - B.5. The inclusion of the first plane into charges + - B.6. Components of the first plane + - B.7. Points on the first plane satisfies the ACCs + - B.8. Kernel of the inclusion into charges + - B.9. The inclusion of the first plane into `LinSols` + - B.10. The basis vectors are linearly independent + +-/ + +@[expose] public section + +open Module Nat Finset BigOperators + +namespace PureU1 + +variable {n : ℕ} + +namespace VectorLikeOddPlane + +/-! + +## A.1. The symmetric split: Splitting the charges up via `(n + 1) + n` + +We split `2 * n + 1` charges using the symmetric split `(n + 1) + n`. + +-/ + +section theDeltas + +lemma odd_shift_eq (n : ℕ) : (1 + n) + n = 2 * n +1 := by + omega + +/-- The inclusion of `Fin n` into `Fin ((n + 1) + n)` via the first `n`. + This is then casted to `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 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)`. + This is then casted to `Fin (2 * n + 1)`. -/ +def oddMid : Fin (2 * n + 1) := + Fin.cast (split_odd n) (Fin.castAdd n (Fin.natAdd n 1)) + +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 + simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv] + · exact fun _ _ => rfl + rw [h1] + rw [Fin.sum_univ_add, Fin.sum_univ_add] + simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply] + nth_rewrite 2 [add_comm] + rw [add_assoc] + rw [Finset.sum_add_distrib] + rfl + +end theDeltas + +/-! + +## B. The first plane (symmetric plane) + +The symmetric plane is constructed from the symmetric split `(n + 1) + n`. + +-/ + +/-! + +### B.1. The basis vectors of the first plane as charges + +-/ + +/-- The first part of the basis as charge assignments. -/ +def symmBasisAsCharges (j : Fin n) : (PureU1 (2 * n + 1)).Charges := + fun i => + if i = oddFst j then + 1 + else + if i = oddSnd j then + - 1 + else + 0 + +/-! + +### B.2. Components of the basis vectors as charges + +-/ + +lemma symmBasisAsCharges_on_oddFst_self (j : Fin n) : symmBasisAsCharges j (oddFst j) = 1 := by + simp [symmBasisAsCharges] + +lemma symmBasisAsCharges_on_oddFst_other {k j : Fin n} (h : k ≠ j) : + symmBasisAsCharges k (oddFst j) = 0 := by + simp only [symmBasisAsCharges, PureU1_numberCharges] + simp only [oddFst, oddSnd] + split + · rename_i h1 + rw [Fin.ext_iff] at h1 + simp_all + rw [Fin.ext_iff] at h + simp_all + · split + · rename_i h1 h2 + simp_all + rw [Fin.ext_iff] at h2 + simp only [Fin.val_castAdd, Fin.val_natAdd] at h2 + omega + · rfl + +lemma symmBasisAsCharges_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ oddFst k) + (h2 : j ≠ oddSnd k) : + symmBasisAsCharges k j = 0 := by + simp only [symmBasisAsCharges, PureU1_numberCharges] + simp_all only [ne_eq, ↓reduceIte] + +lemma symmBasisAsCharges_oddSnd_eq_minus_oddFst (j i : Fin n) : + symmBasisAsCharges j (oddSnd i) = - symmBasisAsCharges j (oddFst i) := by + simp only [symmBasisAsCharges, PureU1_numberCharges, oddSnd, oddFst] + split <;> split + any_goals split + any_goals split + any_goals rfl + all_goals + rename_i h1 h2 + rw [Fin.ext_iff] at h1 h2 + simp_all only [Fin.cast_inj, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, neg_neg, + add_eq_right, AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, not_false_eq_true] + all_goals + rename_i h3 + rw [Fin.ext_iff] at h3 + simp_all only [Fin.val_natAdd, Fin.val_castAdd, add_eq_right, + AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, not_false_eq_true] + all_goals + omega + +lemma symmBasisAsCharges_on_oddSnd_self (j : Fin n) : + symmBasisAsCharges j (oddSnd j) = - 1 := by + rw [symmBasisAsCharges_oddSnd_eq_minus_oddFst, symmBasisAsCharges_on_oddFst_self] + +lemma symmBasisAsCharges_on_oddSnd_other {k j : Fin n} (h : k ≠ j) : + symmBasisAsCharges k (oddSnd j) = 0 := by + rw [symmBasisAsCharges_oddSnd_eq_minus_oddFst, symmBasisAsCharges_on_oddFst_other h] + rfl + +lemma symmBasisAsCharges_on_oddMid (j : Fin n) : symmBasisAsCharges j oddMid = 0 := by + simp only [symmBasisAsCharges, PureU1_numberCharges] + split <;> rename_i h + · rw [Fin.ext_iff] at h + simp only [oddMid, Fin.isValue, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, Fin.val_eq_zero, + add_zero, oddFst] at h + omega + · split <;> rename_i h2 + · rw [Fin.ext_iff] at h2 + simp only [oddMid, Fin.isValue, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, + Fin.val_eq_zero, add_zero, oddSnd] at h2 + omega + · rfl + +/-! + +### B.3. The basis vectors satisfy the linear ACCs + +-/ + +lemma symmBasisAsCharges_linearACC (j : Fin n) : + (accGrav (2 * n + 1)) (symmBasisAsCharges j) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + erw [sum_odd] + simp [symmBasisAsCharges_oddSnd_eq_minus_oddFst, symmBasisAsCharges_on_oddMid] + +/-! + +### B.4. The basis vectors as `LinSols` + +-/ + +/-- The first part of the basis as `LinSols`. -/ +@[simps!] +def symmBasis (j : Fin n) : (PureU1 (2 * n + 1)).LinSols := + ⟨symmBasisAsCharges j, by + intro i + simp only [PureU1_numberLinear] at i + match i with + | 0 => + exact symmBasisAsCharges_linearACC j⟩ + +/-! + +### B.5. The inclusion of the first plane into charges + +-/ + +/-- A point in the span of the first part of the basis as a charge. -/ +def symmPlaneAsCharges (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := + ∑ i, f i • symmBasisAsCharges i + +/-! + +### B.6. Components of the first plane + +-/ + +lemma symmPlaneAsCharges_oddFst (f : Fin n → ℚ) (j : Fin n) : symmPlaneAsCharges f (oddFst j) = f j := by + rw [symmPlaneAsCharges, sum_of_charges] + simp only [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + · rw [symmBasisAsCharges_on_oddFst_self] + exact Rat.mul_one (f j) + · intro k _ hkj + rw [symmBasisAsCharges_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 symmPlaneAsCharges_oddSnd (f : Fin n → ℚ) (j : Fin n) : symmPlaneAsCharges f (oddSnd j) = - f j := by + rw [symmPlaneAsCharges, sum_of_charges] + simp only [HSMul.hSMul, SMul.smul] + rw [Finset.sum_eq_single j] + · rw [symmBasisAsCharges_on_oddSnd_self] + exact mul_neg_one (f j) + · intro k _ hkj + rw [symmBasisAsCharges_on_oddSnd_other hkj] + exact Rat.mul_zero (f k) + · simp + +lemma symmPlaneAsCharges_oddMid (f : Fin n → ℚ) : symmPlaneAsCharges f oddMid = 0 := by + rw [symmPlaneAsCharges, sum_of_charges] + simp [HSMul.hSMul, SMul.smul, symmBasisAsCharges_on_oddMid] + +/-! + +### B.7. Points on the first plane satisfies the ACCs + +-/ + +lemma symmPlaneAsCharges_linearACC (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (symmPlaneAsCharges f) = 0 := by + rw [accGrav] + simp only [LinearMap.coe_mk, AddHom.coe_mk] + rw [sum_odd] + simp [symmPlaneAsCharges_oddSnd, symmPlaneAsCharges_oddFst, symmPlaneAsCharges_oddMid] + +set_option backward.isDefEq.respectTransparency false in +lemma symmPlaneAsCharges_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (symmPlaneAsCharges f) = 0 := by + rw [accCube_explicit, sum_odd, symmPlaneAsCharges_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 [symmPlaneAsCharges_oddFst, symmPlaneAsCharges_oddSnd] + ring + +/-! + +### B.8. Kernel of the inclusion into charges + +-/ + +lemma symmPlaneAsCharges_zero (f : Fin n → ℚ) (h : symmPlaneAsCharges f = 0) : ∀ i, f i = 0 := by + intro i + erw [← symmPlaneAsCharges_oddFst f] + rw [h] + rfl + +/-! + +### B.9. The inclusion of the first plane into `LinSols` + +-/ + +/-- A point in the span of the first part of the basis. -/ +def symmPlane (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols := + ∑ i, f i • symmBasis i + +lemma symmPlane_val (f : Fin n → ℚ) : (symmPlane f).val = symmPlaneAsCharges f := by + simp only [symmPlane, symmPlaneAsCharges] + funext i + rw [sum_of_anomaly_free_linear, sum_of_charges] + rfl + +/-! + +### B.10. The basis vectors are linearly independent + +-/ + +theorem symmBasis_linear_independent : LinearIndependent ℚ (@symmBasis n) := by + apply Fintype.linearIndependent_iff.mpr + intro f h + change symmPlane f = 0 at h + have h1 : (symmPlane f).val = 0 := + (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0) + (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h)))) + (ACCSystemLinear.LinSols.val 0))).mp rfl + rw [symmPlane_val] at h1 + exact symmPlaneAsCharges_zero f h1 + +end VectorLikeOddPlane + +end PureU1