Charges assignments with constant abs

We look at charge assignments in which all charges have the same absolute value.

def PureU1.ConstAbsProp : ℚ × ℚ → Prop

The condition for two rationals to have the same square (equivalent to same abs).

Equations

• PureU1.ConstAbsProp s = (s.1 ^ 2 = s.2 ^ 2)

def PureU1.ConstAbs {n : ℕ} (S : (PureU1 n).Charges) : Prop

The condition on a charge assignment S to have constant absolute value among charges.

Equations

• PureU1.ConstAbs S = ∀ (i j : Fin (PureU1 n).numberCharges), S i ^ 2 = S j ^ 2

theorem PureU1.constAbs_perm {n : ℕ} (S : (PureU1 n).Charges) (M : (FamilyPermutations n).group) : ConstAbs (((FamilyPermutations n).rep M) S) ↔ ConstAbs S

theorem PureU1.constAbs_sort {n : ℕ} {S : (PureU1 n).Charges} (CA : ConstAbs S) : ConstAbs (sort S)

def PureU1.ConstAbsSorted {n : ℕ} (S : (PureU1 n).Charges) : Prop

The condition for a set of charges to be sorted, and have constAbs

Equations

• PureU1.ConstAbsSorted S = (PureU1.ConstAbs S ∧ PureU1.Sorted S)

theorem PureU1.ConstAbsSorted.lt_eq {n : ℕ} {S : (PureU1 n.succ).Charges} (hS : ConstAbsSorted S) {k i : Fin n.succ} (hk : S k ≤ 0) (hik : i ≤ k) : S i = S k

theorem PureU1.ConstAbsSorted.val_le_zero {n : ℕ} {S : (PureU1 n.succ).Charges} (hS : ConstAbsSorted S) {i : Fin n.succ} (hi : S i ≤ 0) : S i = S 0

theorem PureU1.ConstAbsSorted.gt_eq {n : ℕ} {S : (PureU1 n.succ).Charges} (hS : ConstAbsSorted S) {k i : Fin n.succ} (hk : 0 ≤ S k) (hik : k ≤ i) : S i = S k

theorem PureU1.ConstAbsSorted.zero_gt {n : ℕ} {S : (PureU1 n.succ).Charges} (hS : ConstAbsSorted S) (h0 : 0 ≤ S 0) (i : Fin n.succ) : S 0 = S i

theorem PureU1.ConstAbsSorted.opposite_signs_eq_neg {n : ℕ} {S : (PureU1 n.succ).Charges} (hS : ConstAbsSorted S) {i j : Fin n.succ} (hi : S i ≤ 0) (hj : 0 ≤ S j) : S i = -S j

theorem PureU1.ConstAbsSorted.is_zero {n : ℕ} {S : (PureU1 n.succ).Charges} (hS : ConstAbsSorted S) (h0 : S 0 = 0) : S = 0

def PureU1.ConstAbsSorted.Boundary {n : ℕ} (S : (PureU1 n.succ).Charges) (k : Fin n) : Prop

A boundary of S : (PureU1 n.succ).charges (assumed sorted, constAbs and non-zero) is defined as a element of k ∈ Fin n such that S k.castSucc and S k.succ are different signs.

Equations

• PureU1.ConstAbsSorted.Boundary S k = (S k.castSucc < 0 ∧ 0 < S k.succ)

theorem PureU1.ConstAbsSorted.boundary_castSucc {n : ℕ} {S : (PureU1 n.succ).Charges} (hS : ConstAbsSorted S) {k : Fin n} (hk : Boundary S k) : S k.castSucc = S 0

theorem PureU1.ConstAbsSorted.boundary_succ {n : ℕ} {S : (PureU1 n.succ).Charges} (hS : ConstAbsSorted S) {k : Fin n} (hk : Boundary S k) : S k.succ = -S 0

theorem PureU1.ConstAbsSorted.boundary_split {n : ℕ} (k : Fin n) : ↑k.succ + (n.succ - ↑k.succ) = n.succ

theorem PureU1.ConstAbsSorted.boundary_accGrav' {n : ℕ} {S : (PureU1 n.succ).Charges} (k : Fin n) : (accGrav n.succ) S = ∑ i : Fin (↑k.succ + (n.succ - ↑k.succ)), S (Fin.cast ⋯ i)

theorem PureU1.ConstAbsSorted.boundary_accGrav'' {n : ℕ} {S : (PureU1 n.succ).Charges} (hS : ConstAbsSorted S) (k : Fin n) (hk : Boundary S k) : (accGrav n.succ) S = (2 * ↑↑k + 1 - ↑n) * S 0

def PureU1.ConstAbsSorted.HasBoundary {n : ℕ} (S : (PureU1 n.succ).Charges) : Prop

A S ∈ charges has a boundary if there exists a k ∈ Fin n which is a boundary.

Equations

• PureU1.ConstAbsSorted.HasBoundary S = ∃ (k : Fin n), PureU1.ConstAbsSorted.Boundary S k

theorem PureU1.ConstAbsSorted.not_hasBoundary_zero_le {n : ℕ} {S : (PureU1 n.succ).Charges} (hS : ConstAbsSorted S) (hnot : ¬HasBoundary S) (h0 : S 0 < 0) (i : Fin (PureU1 n.succ).numberCharges) : S 0 = S i

theorem PureU1.ConstAbsSorted.not_hasBoundry_zero {n : ℕ} {S : (PureU1 n.succ).Charges} (hS : ConstAbsSorted S) (hnot : ¬HasBoundary S) (i : Fin n.succ) : S 0 = S i

theorem PureU1.ConstAbsSorted.not_hasBoundary_grav {n : ℕ} {S : (PureU1 n.succ).Charges} (hS : ConstAbsSorted S) (hnot : ¬HasBoundary S) : (accGrav n.succ) S = ↑n.succ * S 0

theorem PureU1.ConstAbsSorted.AFL_hasBoundary {n : ℕ} {A : (PureU1 n.succ).LinSols} (hA : ConstAbsSorted A.val) (h : A.val 0 ≠ 0) : HasBoundary A.val

theorem PureU1.ConstAbsSorted.AFL_odd_noBoundary {n : ℕ} {A : (PureU1 (2 * n + 1)).LinSols} (h : ConstAbsSorted A.val) (hA : A.val 0 ≠ 0) : ¬HasBoundary A.val

theorem PureU1.ConstAbsSorted.AFL_odd_zero {n : ℕ} {A : (PureU1 (2 * n + 1)).LinSols} (h : ConstAbsSorted A.val) : A.val 0 = 0

theorem PureU1.ConstAbsSorted.AFL_odd {n : ℕ} (A : (PureU1 (2 * n + 1)).LinSols) (h : ConstAbsSorted A.val) : A = 0

theorem PureU1.ConstAbsSorted.AFL_even_Boundary {n : ℕ} {A : (PureU1 (2 * n.succ)).LinSols} (h : ConstAbsSorted A.val) (hA : A.val 0 ≠ 0) {k : Fin (2 * n + 1)} (hk : Boundary A.val k) : ↑k = n

theorem PureU1.ConstAbsSorted.AFL_even_below' {n : ℕ} {A : (PureU1 (2 * n.succ)).LinSols} (h : ConstAbsSorted A.val) (hA : A.val 0 ≠ 0) (i : Fin n.succ) : A.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = A.val 0

theorem PureU1.ConstAbsSorted.AFL_even_below {n : ℕ} (A : (PureU1 (2 * n.succ)).LinSols) (h : ConstAbsSorted A.val) (i : Fin n.succ) : A.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = A.val 0

theorem PureU1.ConstAbsSorted.AFL_even_above' {n : ℕ} {A : (PureU1 (2 * n.succ)).LinSols} (h : ConstAbsSorted A.val) (hA : A.val 0 ≠ 0) (i : Fin n.succ) : A.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -A.val 0

theorem PureU1.ConstAbsSorted.AFL_even_above {n : ℕ} (A : (PureU1 (2 * n.succ)).LinSols) (h : ConstAbsSorted A.val) (i : Fin n.succ) : A.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -A.val 0

theorem PureU1.ConstAbs.boundary_value_odd {n : ℕ} (S : (PureU1 (2 * n + 1)).LinSols) (hs : ConstAbs S.val) : S = 0

theorem PureU1.ConstAbs.boundary_value_even {n : ℕ} (S : (PureU1 (2 * n.succ)).LinSols) (hs : ConstAbs S.val) : VectorLikeEven S.val