Bound 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.

def SMRHN.PlusU1.ExistsPlane (n : ℕ) : Prop

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.

Equations

• SMRHN.PlusU1.ExistsPlane n = ∃ (B : Fin n → (SMRHN.PlusU1 3).Charges), LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (SMRHN.PlusU1 3).IsSolution (∑ i : Fin n, f i • B i)

theorem SMRHN.PlusU1.exists_plane_exists_basis {n : ℕ} (hE : SMRHN.PlusU1.ExistsPlane n) : ∃ (B : Fin 11 ⊕ Fin n → (SMRHN.PlusU1 3).Charges), LinearIndependent ℚ B

theorem SMRHN.PlusU1.plane_exists_dim_le_7 {n : ℕ} (hn : SMRHN.PlusU1.ExistsPlane n) : n ≤ 7