Imports
/-
Copyright (c) 2025 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.Particles.SuperSymmetry.SU5.ChargeSpectrum.PhenoConstrainedYukawa charges
i. Overview
In this module we look at the charges associated with the Yukawa terms in the super potential, and when they can regenerate phenomenologically constrained super-potential terms at different levels.
We do not not consider the regeneration of terms in the Kähler potential within this module.
ii. Key results
ofYukawaTerms: the multiset of charges associated with the Yukawa terms
ofYukawaTermsNSum: the multiset of charges associated with up-to n copies of the Yukawa terms
or equivalently the charges of singlet insertions needed to regenerate Yukawa terms.
YukawaGeneratesDangerousAtLevel: the proposition that a charge spectrum regenerates a
phenomenologically constrained term in the super-potential
with up-to n insertions of singlets needed to regenerate
the Yukawa terms.
iii. Table of contents
A. Charges of the Yukawa terms
A.1. Monotonicity of charges of the Yukawa terms
A.2. upto n-copies of charges of the Yukawa terms (aka charges of singlet insertions)
A.3. Monotonicity of set of charges of upto n-copies of the Yukawa terms
B. Regeneration of phenomenologically constrained terms via upto n Yukawa singlet insertions
B.1. Decidability of YukawaGeneratesDangerousAtLevel
B.2. Simplifications of condition for regenerating dangerous terms
B.3. Empty charge spectrum does not regenerate dangerous terms
B.4. Monotonicity of regeneration of dangerous terms in charge spectra
B.5. Monotonicity of regeneration of dangerous terms in level
iv. References
There are no known references for this module.
@[expose] public sectionA. Charges of the Yukawa terms
The collection of charges associated with Yukawa terms. Correspondingly, the (negative) of the charges of the singlets needed to regenerate all Yukawa terms in the potential.
def ofYukawaTerms (x : ChargeSpectrum 𝓩) : Multiset 𝓩 :=
x.ofPotentialTerm' topYukawa + x.ofPotentialTerm' bottomYukawaA.1. Monotonicity of charges of the Yukawa terms
lemma ofYukawaTerms_subset_of_subset [DecidableEq 𝓩] {x y : ChargeSpectrum 𝓩} (h : x ⊆ y) :
x.ofYukawaTerms ⊆ y.ofYukawaTerms := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ y⊢ x.ofYukawaTerms ⊆ y.ofYukawaTerms
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ y⊢ x.ofPotentialTerm' topYukawa + x.ofPotentialTerm' bottomYukawa ⊆
y.ofPotentialTerm' topYukawa + y.ofPotentialTerm' bottomYukawa
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ y⊢ ∀ ⦃x_1 : 𝓩⦄,
x_1 ∈ x.ofPotentialTerm' topYukawa + x.ofPotentialTerm' bottomYukawa →
x_1 ∈ y.ofPotentialTerm' topYukawa + y.ofPotentialTerm' bottomYukawa
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yz:𝓩⊢ z ∈ x.ofPotentialTerm' topYukawa + x.ofPotentialTerm' bottomYukawa →
z ∈ y.ofPotentialTerm' topYukawa + y.ofPotentialTerm' bottomYukawa
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yz:𝓩⊢ z ∈ x.ofPotentialTerm' topYukawa ∨ z ∈ x.ofPotentialTerm' bottomYukawa →
z ∈ y.ofPotentialTerm' topYukawa ∨ z ∈ y.ofPotentialTerm' bottomYukawa
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yz:𝓩hr:z ∈ x.ofPotentialTerm' topYukawa ∨ z ∈ x.ofPotentialTerm' bottomYukawa⊢ z ∈ y.ofPotentialTerm' topYukawa ∨ z ∈ y.ofPotentialTerm' bottomYukawa
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yz:𝓩hr:z ∈ x.ofPotentialTerm' topYukawa⊢ z ∈ y.ofPotentialTerm' topYukawa ∨ z ∈ y.ofPotentialTerm' bottomYukawa𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yz:𝓩hr:z ∈ x.ofPotentialTerm' bottomYukawa⊢ z ∈ y.ofPotentialTerm' topYukawa ∨ z ∈ y.ofPotentialTerm' bottomYukawa
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yz:𝓩hr:z ∈ x.ofPotentialTerm' topYukawa⊢ z ∈ y.ofPotentialTerm' topYukawa ∨ z ∈ y.ofPotentialTerm' bottomYukawa 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yz:𝓩hr:z ∈ x.ofPotentialTerm' topYukawa⊢ z ∈ y.ofPotentialTerm' topYukawa
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yz:𝓩hr:z ∈ x.ofPotentialTerm' topYukawa⊢ z ∈ x.ofPotentialTerm' topYukawa
All goals completed! 🐙
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yz:𝓩hr:z ∈ x.ofPotentialTerm' bottomYukawa⊢ z ∈ y.ofPotentialTerm' topYukawa ∨ z ∈ y.ofPotentialTerm' bottomYukawa 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yz:𝓩hr:z ∈ x.ofPotentialTerm' bottomYukawa⊢ z ∈ y.ofPotentialTerm' bottomYukawa
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yz:𝓩hr:z ∈ x.ofPotentialTerm' bottomYukawa⊢ z ∈ x.ofPotentialTerm' bottomYukawa
All goals completed! 🐙A.2. upto n-copies of charges of the Yukawa terms (aka charges of singlet insertions)
The charges of those terms which can be regenerated with up-to n
insertions of singlets needed to regenerate the Yukawa terms.
Equivalently, the sum of up-to n integers each corresponding to a charge of the
Yukawa terms.
def ofYukawaTermsNSum (x : ChargeSpectrum 𝓩) : ℕ → Multiset 𝓩
| 0 => {0}
| n + 1 => x.ofYukawaTermsNSum n + (x.ofYukawaTermsNSum n).bind fun sSum =>
(x.ofYukawaTerms.map fun s => sSum + s)A.3. Monotonicity of set of charges of upto n-copies of the Yukawa terms
lemma ofYukawaTermsNSum_subset_of_subset [DecidableEq 𝓩] {x y : ChargeSpectrum 𝓩}
(h : x ⊆ y) (n : ℕ) :
x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum n := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕ⊢ x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum n
induction n with
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ y⊢ x.ofYukawaTermsNSum 0 ⊆ y.ofYukawaTermsNSum 0 All goals completed! 🐙
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum n⊢ x.ofYukawaTermsNSum (n + 1) ⊆ y.ofYukawaTermsNSum (n + 1)
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum n⊢ (x.ofYukawaTermsNSum n + (x.ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) x.ofYukawaTerms) ⊆
y.ofYukawaTermsNSum n + (y.ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) y.ofYukawaTerms
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum n⊢ ∀ ⦃x_1 : 𝓩⦄,
(x_1 ∈
x.ofYukawaTermsNSum n +
(x.ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) x.ofYukawaTerms) →
x_1 ∈
y.ofYukawaTermsNSum n + (y.ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) y.ofYukawaTerms
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩⊢ (z ∈
x.ofYukawaTermsNSum n + (x.ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) x.ofYukawaTerms) →
z ∈ y.ofYukawaTermsNSum n + (y.ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) y.ofYukawaTerms
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩⊢ (z ∈ x.ofYukawaTermsNSum n ∨ ∃ a ∈ x.ofYukawaTermsNSum n, ∃ a_1 ∈ x.ofYukawaTerms, a + a_1 = z) →
z ∈ y.ofYukawaTermsNSum n ∨ ∃ a ∈ y.ofYukawaTermsNSum n, ∃ a_1 ∈ y.ofYukawaTerms, a + a_1 = z
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩hr:z ∈ x.ofYukawaTermsNSum n ∨ ∃ a ∈ x.ofYukawaTermsNSum n, ∃ a_1 ∈ x.ofYukawaTerms, a + a_1 = z⊢ z ∈ y.ofYukawaTermsNSum n ∨ ∃ a ∈ y.ofYukawaTermsNSum n, ∃ a_1 ∈ y.ofYukawaTerms, a + a_1 = z
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩hr:z ∈ x.ofYukawaTermsNSum n⊢ z ∈ y.ofYukawaTermsNSum n ∨ ∃ a ∈ y.ofYukawaTermsNSum n, ∃ a_1 ∈ y.ofYukawaTerms, a + a_1 = z𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩z1:𝓩hz1:z1 ∈ x.ofYukawaTermsNSum nz2:𝓩hz2:z2 ∈ x.ofYukawaTermshsum:z1 + z2 = z⊢ z ∈ y.ofYukawaTermsNSum n ∨ ∃ a ∈ y.ofYukawaTermsNSum n, ∃ a_1 ∈ y.ofYukawaTerms, a + a_1 = z
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩hr:z ∈ x.ofYukawaTermsNSum n⊢ z ∈ y.ofYukawaTermsNSum n ∨ ∃ a ∈ y.ofYukawaTermsNSum n, ∃ a_1 ∈ y.ofYukawaTerms, a + a_1 = z 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩hr:z ∈ x.ofYukawaTermsNSum n⊢ z ∈ y.ofYukawaTermsNSum n
All goals completed! 🐙
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩z1:𝓩hz1:z1 ∈ x.ofYukawaTermsNSum nz2:𝓩hz2:z2 ∈ x.ofYukawaTermshsum:z1 + z2 = z⊢ ∃ a ∈ y.ofYukawaTermsNSum n, ∃ a_1 ∈ y.ofYukawaTerms, a + a_1 = z
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩z1:𝓩hz1:z1 ∈ x.ofYukawaTermsNSum nz2:𝓩hz2:z2 ∈ x.ofYukawaTermshsum:z1 + z2 = z⊢ z1 ∈ y.ofYukawaTermsNSum n ∧ ∃ a ∈ y.ofYukawaTerms, z1 + a = z
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩z1:𝓩hz1:z1 ∈ x.ofYukawaTermsNSum nz2:𝓩hz2:z2 ∈ x.ofYukawaTermshsum:z1 + z2 = z⊢ z1 ∈ y.ofYukawaTermsNSum n𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩z1:𝓩hz1:z1 ∈ x.ofYukawaTermsNSum nz2:𝓩hz2:z2 ∈ x.ofYukawaTermshsum:z1 + z2 = z⊢ ∃ a ∈ y.ofYukawaTerms, z1 + a = z
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩z1:𝓩hz1:z1 ∈ x.ofYukawaTermsNSum nz2:𝓩hz2:z2 ∈ x.ofYukawaTermshsum:z1 + z2 = z⊢ z1 ∈ y.ofYukawaTermsNSum n All goals completed! 🐙
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩z1:𝓩hz1:z1 ∈ x.ofYukawaTermsNSum nz2:𝓩hz2:z2 ∈ x.ofYukawaTermshsum:z1 + z2 = z⊢ z2 ∈ y.ofYukawaTerms ∧ z1 + z2 = z
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩z1:𝓩hz1:z1 ∈ x.ofYukawaTermsNSum nz2:𝓩hz2:z2 ∈ x.ofYukawaTermshsum:z1 + z2 = z⊢ z2 ∈ y.ofYukawaTerms
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩h:x ⊆ yn:ℕih:x.ofYukawaTermsNSum n ⊆ y.ofYukawaTermsNSum nz:𝓩z1:𝓩hz1:z1 ∈ x.ofYukawaTermsNSum nz2:𝓩hz2:z2 ∈ x.ofYukawaTermshsum:z1 + z2 = z⊢ z2 ∈ x.ofYukawaTerms
All goals completed! 🐙B. Regeneration of phenomenologically constrained terms via upto n Yukawa singlet insertions
For charges x : Charges, the proposition which states that the singlets
needed to regenerate the Yukawa couplings regenerate a dangerous coupling
(in the superpotential) with up-to n insertions of the scalars.
Note: If defined as (x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset ≠ ∅ the execution time is greatly increased.
def YukawaGeneratesDangerousAtLevel (x : ChargeSpectrum 𝓩) (n : ℕ) : Prop :=
(x.ofYukawaTermsNSum n) ∩ x.phenoConstrainingChargesSP ≠ ∅
B.1. Decidability of YukawaGeneratesDangerousAtLevel
instance (x : ChargeSpectrum 𝓩) (n : ℕ) : Decidable (YukawaGeneratesDangerousAtLevel x n) :=
inferInstanceAs (Decidable ((x.ofYukawaTermsNSum n)
∩ x.phenoConstrainingChargesSP ≠ ∅))B.2. Simplifications of condition for regenerating dangerous terms
lemma YukawaGeneratesDangerousAtLevel_iff_inter {x : ChargeSpectrum 𝓩} {n : ℕ} :
YukawaGeneratesDangerousAtLevel x n ↔
(x.ofYukawaTermsNSum n) ∩ x.phenoConstrainingChargesSP ≠ ∅ := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩n:ℕ⊢ x.YukawaGeneratesDangerousAtLevel n ↔ x.ofYukawaTermsNSum n ∩ x.phenoConstrainingChargesSP ≠ ∅ All goals completed! 🐙𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩n:ℕh:¬(x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset = ∅hn:x.ofYukawaTermsNSum n ∩ x.phenoConstrainingChargesSP = 0i:𝓩h1:i ∈ x.ofYukawaTermsNSum nh2:i ∈ x.phenoConstrainingChargesSPh3:i ∈ x.ofYukawaTermsNSum n ∩ x.phenoConstrainingChargesSP⊢ False
All goals completed! 🐙B.3. Empty charge spectrum does not regenerate dangerous terms
@[simp]
lemma not_yukawaGeneratesDangerousAtLevel_of_empty (n : ℕ) :
¬ YukawaGeneratesDangerousAtLevel (∅ : ChargeSpectrum 𝓩) n := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩n:ℕ⊢ ¬∅.YukawaGeneratesDangerousAtLevel n
All goals completed! 🐙B.4. Monotonicity of regeneration of dangerous terms in charge spectra
If x regenerates a dangerous term with up-to n insertions of Yukawa singlets,
and x ⊆ y, then y also regenerates a dangerous term with up-to n insertions.
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩y:ChargeSpectrum 𝓩n:ℕh:x ⊆ yhx:¬∅ = ∅hn:(y.ofYukawaTermsNSum n).toFinset ∩ y.phenoConstrainingChargesSP.toFinset = ∅h1:(x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset = ∅⊢ False
All goals completed! 🐙B.5. Monotonicity of regeneration of dangerous terms in level
If x regenerates a dangerous term with up-to n insertions of Yukawa singlets,
then x also regenerates a dangerous term with up-to n + 1 insertions.
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩n:ℕhx:¬(x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset = ∅⊢ ¬(x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset = ∅ ∨
¬((x.ofYukawaTermsNSum n).bind fun sSum => Multiset.map (fun s => sSum + s) x.ofYukawaTerms).toFinset ∩
x.phenoConstrainingChargesSP.toFinset =
∅
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩n:ℕhx:¬(x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset = ∅⊢ ¬(x.ofYukawaTermsNSum n).toFinset ∩ x.phenoConstrainingChargesSP.toFinset = ∅
All goals completed! 🐙lemma yukawaGeneratesDangerousAtLevel_add_of_left {x : ChargeSpectrum 𝓩} {n k : ℕ}
(hx : x.YukawaGeneratesDangerousAtLevel n) :
x.YukawaGeneratesDangerousAtLevel (n + k) := 𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩n:ℕk:ℕhx:x.YukawaGeneratesDangerousAtLevel n⊢ x.YukawaGeneratesDangerousAtLevel (n + k)
induction k with
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩n:ℕhx:x.YukawaGeneratesDangerousAtLevel n⊢ x.YukawaGeneratesDangerousAtLevel (n + 0) All goals completed! 🐙
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩n:ℕhx:x.YukawaGeneratesDangerousAtLevel nk:ℕih:x.YukawaGeneratesDangerousAtLevel (n + k)⊢ x.YukawaGeneratesDangerousAtLevel (n + (k + 1)) All goals completed! 🐙𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩n:ℕm:ℕh:n ≤ mhx:x.YukawaGeneratesDangerousAtLevel nk:ℕhk:m - n = kh1:n + k = m⊢ x.YukawaGeneratesDangerousAtLevel m
𝓩:Typeinst✝¹:AddCommGroup 𝓩inst✝:DecidableEq 𝓩x:ChargeSpectrum 𝓩n:ℕhx:x.YukawaGeneratesDangerousAtLevel nk:ℕh:n ≤ n + khk:n + k - n = k⊢ x.YukawaGeneratesDangerousAtLevel (n + k)
All goals completed! 🐙