Imports
/-
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.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.PlaneNonSolsBound on plane dimension
We place an upper bound on the dimension of a plane of charges on which every point is a solution.
The upper bound is 7, proven in the theorem plane_exists_dim_le_7.
@[expose] public section
A proposition which is true if for a given n, a plane of charges of dimension n exists
in which each point is a solution.
def ExistsPlane (n : ℕ) : Prop := ∃ (B : Fin n → (PlusU1 3).Charges),
LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i)n:ℕE:Fin n → (PlusU1 3).ChargeshE1:∀ (g : Fin n → ℚ), ∑ i, g i • E i = 0 → ∀ (i : Fin n), g i = 0hE2:∀ (f : Fin n → ℚ), (PlusU1 3).IsSolution (∑ i, f i • E i)B:Fin 11 → (PlusU1 3).ChargeshB1:∀ (g : Fin 11 → ℚ), ∑ i, g i • B i = 0 → ∀ (i : Fin 11), g i = 0hB2:∀ (f : Fin 11 → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i) → ∑ i, f i • B i = 0Y:Fin 11 ⊕ Fin n → (PlusU1 3).Charges := Sum.elim B Eg:Fin 11 ⊕ Fin n → ℚhg:0 = ∑ x, -g (Sum.inr x) • Y (Sum.inr x)h2:∑ a₁, g (Sum.inl a₁) • Y (Sum.inl a₁) = 0h3:∀ (i : Fin 11), g (Sum.inl i) = 0⊢ ∀ (i : Fin 11 ⊕ Fin n), g i = 0
n:ℕE:Fin n → (PlusU1 3).ChargeshE1:∀ (g : Fin n → ℚ), ∑ i, g i • E i = 0 → ∀ (i : Fin n), g i = 0hE2:∀ (f : Fin n → ℚ), (PlusU1 3).IsSolution (∑ i, f i • E i)B:Fin 11 → (PlusU1 3).ChargeshB1:∀ (g : Fin 11 → ℚ), ∑ i, g i • B i = 0 → ∀ (i : Fin 11), g i = 0hB2:∀ (f : Fin 11 → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i) → ∑ i, f i • B i = 0Y:Fin 11 ⊕ Fin n → (PlusU1 3).Charges := Sum.elim B Eg:Fin 11 ⊕ Fin n → ℚhg:0 = ∑ x, -g (Sum.inr x) • Y (Sum.inr x)h2:∑ a₁, g (Sum.inl a₁) • Y (Sum.inl a₁) = 0h3:∀ (i : Fin 11), g (Sum.inl i) = 0h4:∀ (i : Fin n), -g (Sum.inr i) = 0⊢ ∀ (i : Fin 11 ⊕ Fin n), g i = 0
n:ℕE:Fin n → (PlusU1 3).ChargeshE1:∀ (g : Fin n → ℚ), ∑ i, g i • E i = 0 → ∀ (i : Fin n), g i = 0hE2:∀ (f : Fin n → ℚ), (PlusU1 3).IsSolution (∑ i, f i • E i)B:Fin 11 → (PlusU1 3).ChargeshB1:∀ (g : Fin 11 → ℚ), ∑ i, g i • B i = 0 → ∀ (i : Fin 11), g i = 0hB2:∀ (f : Fin 11 → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i) → ∑ i, f i • B i = 0Y:Fin 11 ⊕ Fin n → (PlusU1 3).Charges := Sum.elim B Eg:Fin 11 ⊕ Fin n → ℚhg:0 = ∑ x, -g (Sum.inr x) • Y (Sum.inr x)h2:∑ a₁, g (Sum.inl a₁) • Y (Sum.inl a₁) = 0h3:∀ (i : Fin 11), g (Sum.inl i) = 0h4:∀ (i : Fin n), g (Sum.inr i) = 0⊢ ∀ (i : Fin 11 ⊕ Fin n), g i = 0
All goals completed! 🐙theorem plane_exists_dim_le_7 {n : ℕ} (hn : ExistsPlane n) : n ≤ 7 := n:ℕhn:ExistsPlane n⊢ n ≤ 7
n:ℕhn:ExistsPlane nB:Fin 11 ⊕ Fin n → (PlusU1 3).ChargeshB:LinearIndependent ℚ B⊢ n ≤ 7
n:ℕhn:ExistsPlane nB:Fin 11 ⊕ Fin n → (PlusU1 3).ChargeshB:LinearIndependent ℚ Bh1:Fintype.card (Fin 11 ⊕ Fin n) ≤ Module.finrank ℚ (PlusU1 3).Charges⊢ n ≤ 7
n:ℕhn:ExistsPlane nB:Fin 11 ⊕ Fin n → (PlusU1 3).ChargeshB:LinearIndependent ℚ Bh1:11 + n ≤ 18⊢ n ≤ 7
All goals completed! 🐙