DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

docs: Improve docs for basisLinear

Browse source
This commit is contained in:
jstoobysmith 2024-11-28 11:18:25 +00:00
parent 2ada8df0c6
commit 970b3a7436
4 changed files with 51 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

6
HepLean/AnomalyCancellation/PureU1/Basic.lean
View file

@ -150,8 +150,7 @@ lemma sum_of_charges {n : ℕ} (f : Fin k → (PureU1 n).Charges) (j : Fin n) :
· rfl
· rename_i k hl
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
have hlt := hl (f ∘ Fin.castSucc)
erw [← hlt]
erw [← hl (f ∘ Fin.castSucc)]
rfl
/-- The `j`th charge of a sum of solutions to the linear ACC is equal to the sum of
@ -162,8 +161,7 @@ lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j
· rfl
· rename_i k hl
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
have hlt := hl (f ∘ Fin.castSucc)
erw [← hlt]
erw [← hl (f ∘ Fin.castSucc)]
rfl
end PureU1

36
HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
View file

@ -33,51 +33,59 @@ lemma split_adda (n : ℕ) : ((1+n)+1) + n.succ = 2 * n.succ + 1 := by
section theDeltas
/-- A helper function for what follows. -/
/-- The inclusion of `Fin n` into `Fin ((n + 1) + n)` via the first `n`.
This is then casted to `Fin (2 * n + 1)`. -/
def δ₁ (j : Fin n) : Fin (2 * n + 1) :=
Fin.cast (split_odd n) (Fin.castAdd n (Fin.castAdd 1 j))
/-- A helper function for what follows. -/
/-- The inclusion of `Fin n` into `Fin ((n + 1) + n)` via the second `n`.
This is then casted to `Fin (2 * n + 1)`. -/
def δ₂ (j : Fin n) : Fin (2 * n + 1) :=
Fin.cast (split_odd n) (Fin.natAdd (n+1) j)
/-- A helper function for what follows. -/
/-- The element representing `1` in `Fin ((n + 1) + n)`.
This is then casted to `Fin (2 * n + 1)`. -/
def δ₃ : Fin (2 * n + 1) :=
Fin.cast (split_odd n) (Fin.castAdd n (Fin.natAdd n 1))
/-- A helper function for what follows. -/
/-- The inclusion of `Fin n` into `Fin (1 + n + n)` via the first `n`.
This is then casted to `Fin (2 * n + 1)`. -/
def δ!₁ (j : Fin n) : Fin (2 * n + 1) :=
Fin.cast (split_odd! n) (Fin.castAdd n (Fin.natAdd 1 j))
/-- A helper function for what follows. -/
/-- The inclusion of `Fin n` into `Fin (1 + n + n)` via the second `n`.
This is then casted to `Fin (2 * n + 1)`. -/
def δ!₂ (j : Fin n) : Fin (2 * n + 1) :=
Fin.cast (split_odd! n) (Fin.natAdd (1 + n) j)
/-- A helper function for what follows. -/
/-- The element representing the `1` in `Fin (1 + n + n)`.
This is then casted to `Fin (2 * n + 1)`. -/
def δ!₃ : Fin (2 * n + 1) :=
Fin.cast (split_odd! n) (Fin.castAdd n (Fin.castAdd n 1))
/-- A helper function for what follows. -/
/-- The element representing the first `1` in `Fin (1 + n + 1 + n.succ)` casted
to `Fin (2 * n.succ + 1)`. -/
def δa₁ : Fin (2 * n.succ + 1) :=
Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.castAdd n 1)))
/-- A helper function for what follows. -/
/-- The inclusion of `Fin n` into `Fin (1 + n + 1 + n.succ)` via the first `n` and casted
to `Fin (2 * n.succ + 1)`. -/
def δa₂ (j : Fin n) : Fin (2 * n.succ + 1) :=
Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.natAdd 1 j)))
/-- A helper function for what follows. -/
/-- The element representing the second `1` in `Fin (1 + n + 1 + n.succ)` casted
to `2 * n.succ + 1`. -/
def δa₃ : Fin (2 * n.succ + 1) :=
Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.natAdd (1+n) 1))
/-- A helper function for what follows. -/
/-- The inclusion of `Fin n.succ` into `Fin (1 + n + 1 + n.succ)` via the `n.succ` and casted
to `Fin (2 * n.succ + 1)`. -/
def δa₄ (j : Fin n.succ) : Fin (2 * n.succ + 1) :=
Fin.cast (split_adda n) (Fin.natAdd ((1+n)+1) j)
lemma δa₁_δ₁ : @δa₁ n = δ₁ 0 := by
exact Fin.rev_inj.mp rfl
lemma δa₁_δ₁ : @δa₁ n = δ₁ 0 := Fin.rev_inj.mp rfl
lemma δa₁_δ!₃ : @δa₁ n = δ!₃ := by
rfl
lemma δa₁_δ!₃ : @δa₁ n = δ!₃ := rfl
lemma δa₂_δ₁ (j : Fin n) : δa₂ j = δ₁ j.succ := by
rw [Fin.ext_iff]

3
HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
View file

@ -40,6 +40,9 @@ 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
/-- 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)

47
HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
View file

@ -30,22 +30,23 @@ variable {n : ℕ}
open VectorLikeOddPlane
/-- Given a `g f : Fin n → ℚ` and a `a : ℚ` we form a linear solution. We will later
show that this can be extended to a complete solution. -/
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 (sndPlane f) (sndPlane f) (fstPlane g)) • P' g +
(- accCubeTriLinSymm (fstPlane g) sndPlanestPlane g) (P! f)) • P!' 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 (sndPlane f) (sndPlane f) (fstPlane g)) • fstPlane g +
(- accCubeTriLinSymm (fstPlane g) sndPlanestPlanesndPlane) (P! f)) • P! f) := by
rw [parameterizationAsLinear]
change a • (_ • (P' g).val + _ • (P!' f).val) = _
rw [P'_val, P!'_val]
/-- The parameterization satisfies the cubic ACC. -/
lemma parameterizationCharge_cube (g f : Fin n → ℚ) (a : ℚ) :
(accCube (2 * n + 1)) (parameterizationAsLinear g f a).val = 0 := by
accCube (2 * n + 1) (parameterizationAsLinear g f a).val = 0 := by
change accCubeTriLinSymm.toCubic _ = 0
rw [parameterizationAsLinear_val]
rw [HomogeneousCubic.map_smul]
@ -63,12 +64,12 @@ def parameterization (g f : Fin n → ℚ) (a : ℚ) :
⟨⟨parameterizationAsLinear g f a, fun i => Fin.elim0 i⟩,
parameterizationCharge_cube g f a⟩
lemma anomalyFree_param {S : (PureU1 (2 * n + 1)).Sols}
(g f : Fin n → ℚ) (hS : S.val = P g + P! f) :
accCubeTriLinSymm (P g) (P g) (P! f) =
lemma anomalyFree_param {S : (PureU1fstPlasndPlane(2 * n + 1)).Sols}
(g f : Fin n → ℚ) (fstPlaneS : sndPlanestPlaneval = P g + P! f) :
accCubeTriLinSymm (P sndPlane (P gsndPlane(P! ffstPlane =
- accCubeTriLinSymm (P! f) (P! f) (P g) := by
have hC := S.cubicSol
rw [hS] at hC
rw [hS] at hCfstPlanesndPlane
change (accCube (2 * n + 1)) (P g + P! f) = 0 at hC
erw [TriLinearSymm.toCubic_add] at hC
erw [P_accCube] at hC
@ -77,12 +78,12 @@ lemma anomalyFree_param {S : (PureU1 (2 * n + 1)).Sols}
/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠ 0`.
In this case our parameterization above will be able to recover this point. -/
def GenericCase (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
∀ (g f : Fin n.succ → ℚ) (_ : S.val = P g + P! f),
def GenericCase (S : (PureU1 (2 * n.succfstPlasndPlane+ 1)).Sols) : Prop :=
∀ (g f : Fin n.succfstPlane→ ℚ)sndPlanestPlane_ : S.val = P g + P! f),
accCubeTriLinSymm (P g) (P g) (P! f) ≠ 0
lemma genericCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
(hs : ∃ (g f : Fin n.succ → ℚ), S.val = P g + P! f ∧
lemma genericCase_exists (S : (PureU1 (2 * nfstPlasndPlanesucc + 1)).Sols)
(hs : ∃ (g f : Fin fstPlane.sucsndPlanestPlane→ ℚ), S.val = P g + P! f ∧
accCubeTriLinSymm (P g) (P g) (P! f) ≠ 0) : GenericCase S := by
intro g f hS hC
obtain ⟨g', f', hS', hC'⟩ := hs
@ -93,12 +94,12 @@ lemma genericCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠ 0`.
In this case we will show that S is zero if it is true for all permutations. -/
def SpecialCase (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
∀ (g f : Fin n.succ → ℚ) (_ : S.val = P g + P! f),
def SpecialCase (S : (PureU1 (2 * n.succfstPlasndPlane+ 1)).Sols) : Prop :=
∀ (g f : Fin n.succfstPlane→ ℚ)sndPlanestPlane_ : S.val = P g + P! f),
accCubeTriLinSymm (P g) (P g) (P! f) = 0
lemma specialCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
(hs : ∃ (g f : Fin n.succ → ℚ), S.val = P g + P! f ∧
lemma specialCase_exists (S : (PureU1 (2 * nfstPlasndPlanesucc + 1)).Sols)
(hs : ∃ (g f : Fin fstPlane.sucsndPlanestPlane→ ℚ), S.val = P g + P! f ∧
accCubeTriLinSymm (P g) (P g) (P! f) = 0) : SpecialCase S := by
intro g f hS
obtain ⟨g', f', hS', hC'⟩ := hs
@ -109,8 +110,8 @@ lemma specialCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
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 ∨
obtain ⟨g, f, h⟩ := span_basifstPlane S.1sndPlanestPlane
have h1 : accCubeTriLinfstPlaneymm sndPlanestPlane g) (P g) (P! f) ≠ 0 ∨
accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by
exact ne_or_eq _ _
cases h1 <;> rename_i h1
@ -119,11 +120,11 @@ lemma generic_or_special (S : (PureU1 (2 * n.succ + 1)).Sols) :
theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : GenericCase S) :
∃ g f a, S = parameterization g f a := by
obtain ⟨g, f, hS⟩ := span_basis S.1.1
obtain ⟨g, f, hS⟩ := span_basisndPlaneS.1.1sndPlanetPlane
use g, f, (accCubeTriLinSymm (P! f) (P! f) (P g))⁻¹
rw [parameterization]
apply ACCSystem.Sols.ext
rw [parameterizationAsLinear_val]
rw [parameterizationAsLifstPlaneesndPlane_val]
change S.val = _ • (_ • P g + _• P! f)
rw [anomalyFree_param _ _ hS, neg_neg, ← smul_add, smul_smul, inv_mul_cancel₀, one_smul]
· exact hS
@ -142,7 +143,7 @@ lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols}
accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
accCubeTriLinSymm.map_smul₃, h]
rw [anomalyFree_param _ _ hS] at h
simp only [Nat.succ_eq_add_one, accCubeTriLinSymm_toFun_apply_apply, neg_eq_zero] at h
simp only [Nat.succ_eq_addsndPlanene, asndPlaneCubeTfstPlaneiLinSymm_toFun_apply_apply, neg_eq_zero] at h
change accCubeTriLinSymm (P! f) (P! f) (P g) = 0 at h
erw [h]
simp