Physlib.QFT.QED.AnomalyCancellation.ConstAbs

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.QFT.QED.AnomalyCancellation.VectorLike

Charges assignments with constant abs

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

@[expose] public section

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

def ConstAbsProp : ℚ × ℚ → Prop := fun s => s.1^2 = s.2^2

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

@[simp]
def ConstAbs (S : (PureU1 n).Charges) : Prop := ∀ i j, (S i) ^ 2 = (S j) ^ 2

set_option backward.isDefEq.respectTransparency false in
lemma constAbs_perm (S : (PureU1 n).Charges) (M :(FamilyPermutations n).group) :
    ConstAbs ((FamilyPermutations n).rep M S) ↔ ConstAbs S := byn:ℕS:(PureU1 n).ChargesM:(FamilyPermutations n).group⊢ ConstAbs (((FamilyPermutations n).rep M) S) ↔ ConstAbs S
  simp only [ConstAbs, FamilyPermutations, PermGroup, permCharges,
    MonoidHom.coe_mk, OneHom.coe_mk, chargeMap_apply]n:ℕS:(PureU1 n).ChargesM:(FamilyPermutations n).group⊢ (∀ (i j : Fin (PureU1 n).numberCharges), S (M⁻¹ i) ^ 2 = S (M⁻¹ j) ^ 2) ↔
  ∀ (i j : Fin (PureU1 n).numberCharges), S i ^ 2 = S j ^ 2
  refine Iff.intro (fun h i j => ?_) (fun h i j => h (M.invFun i) (M.invFun j))n:ℕS:(PureU1 n).ChargesM:(FamilyPermutations n).grouph:∀ (i j : Fin (PureU1 n).numberCharges), S (M⁻¹ i) ^ 2 = S (M⁻¹ j) ^ 2i:Fin (PureU1 n).numberChargesj:Fin (PureU1 n).numberCharges⊢ S i ^ 2 = S j ^ 2
  have h2 := h (M.toFun i) (M.toFun j)n:ℕS:(PureU1 n).ChargesM:(FamilyPermutations n).grouph:∀ (i j : Fin (PureU1 n).numberCharges), S (M⁻¹ i) ^ 2 = S (M⁻¹ j) ^ 2i:Fin (PureU1 n).numberChargesj:Fin (PureU1 n).numberChargesh2:S (M⁻¹ (M.toFun i)) ^ 2 = S (M⁻¹ (M.toFun j)) ^ 2⊢ S i ^ 2 = S j ^ 2
  simp only [Equiv.toFun_as_coe, Equiv.Perm.coe_inv, Equiv.symm_apply_apply] at h2n:ℕS:(PureU1 n).ChargesM:(FamilyPermutations n).grouph:∀ (i j : Fin (PureU1 n).numberCharges), S (M⁻¹ i) ^ 2 = S (M⁻¹ j) ^ 2i:Fin (PureU1 n).numberChargesj:Fin (PureU1 n).numberChargesh2:S i ^ 2 = S j ^ 2⊢ S i ^ 2 = S j ^ 2
  exact h2All goals completed! 🐙



lemma constAbs_sort {S : (PureU1 n).Charges} (CA : ConstAbs S) : ConstAbs (sort S) := byn:ℕS:(PureU1 n).ChargesCA:ConstAbs S⊢ ConstAbs (sort S)
  rw [sortn:ℕS:(PureU1 n).ChargesCA:ConstAbs S⊢ ConstAbs (((FamilyPermutations n).rep (Equiv.symm (Tuple.sort S))) S)n:ℕS:(PureU1 n).ChargesCA:ConstAbs S⊢ ConstAbs (((FamilyPermutations n).rep (Equiv.symm (Tuple.sort S))) S)]n:ℕS:(PureU1 n).ChargesCA:ConstAbs S⊢ ConstAbs (((FamilyPermutations n).rep (Equiv.symm (Tuple.sort S))) S)
  exact (constAbs_perm S _).mpr CAAll goals completed! 🐙

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

def ConstAbsSorted (S : (PureU1 n).Charges) : Prop := ConstAbs S ∧ Sorted S

              

include hS in
lemma lt_eq {k i : Fin n.succ} (hk : S k ≤ 0) (hik : i ≤ k) : S i = S k := byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:S k ≤ 0hik:i ≤ k⊢ S i = S k
  have hSS := hS.2 i k hikn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:S k ≤ 0hik:i ≤ khSS:S i ≤ S k⊢ S i = S k
  have ht := hS.1 i kn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:S k ≤ 0hik:i ≤ khSS:S i ≤ S kht:S i ^ 2 = S k ^ 2⊢ S i = S k
  rw [sq_eq_sq_iff_eq_or_eq_negn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:S k ≤ 0hik:i ≤ khSS:S i ≤ S kht:S i = S k ∨ S i = -S k⊢ S i = S kn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:S k ≤ 0hik:i ≤ khSS:S i ≤ S kht:S i = S k ∨ S i = -S k⊢ S i = S k] at htn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:S k ≤ 0hik:i ≤ khSS:S i ≤ S kht:S i = S k ∨ S i = -S k⊢ S i = S k
  cases htinln:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:S k ≤ 0hik:i ≤ khSS:S i ≤ S kh✝:S i = S k⊢ S i = S kinrn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:S k ≤ 0hik:i ≤ khSS:S i ≤ S kh✝:S i = -S k⊢ S i = S k <;>inln:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:S k ≤ 0hik:i ≤ khSS:S i ≤ S kh✝:S i = S k⊢ S i = S kinrn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:S k ≤ 0hik:i ≤ khSS:S i ≤ S kh✝:S i = -S k⊢ S i = S k rename_i hinrn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:S k ≤ 0hik:i ≤ khSS:S i ≤ S kh:S i = -S k⊢ S i = S k
  ·inln:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:S k ≤ 0hik:i ≤ khSS:S i ≤ S kh:S i = S k⊢ S i = S k exact hAll goals completed! 🐙
  ·inrn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:S k ≤ 0hik:i ≤ khSS:S i ≤ S kh:S i = -S k⊢ S i = S k linarithAll goals completed! 🐙include hS in
lemma val_le_zero {i : Fin n.succ} (hi : S i ≤ 0) : S i = S (0 : Fin n.succ) := byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Si:Fin n.succhi:S i ≤ 0⊢ S i = S 0
  symmn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Si:Fin n.succhi:S i ≤ 0⊢ S 0 = S i
  apply lt_eq hS hin:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Si:Fin n.succhi:S i ≤ 0⊢ 0 ≤ i
  exact Fin.zero_le iAll goals completed! 🐙

include hS in
lemma gt_eq {k i: Fin n.succ} (hk : 0 ≤ S k) (hik : k ≤ i) : S i = S k := byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:0 ≤ S khik:k ≤ i⊢ S i = S k
  have hSS := hS.2 k i hikn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:0 ≤ S khik:k ≤ ihSS:S k ≤ S i⊢ S i = S k
  have ht := hS.1 i kn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:0 ≤ S khik:k ≤ ihSS:S k ≤ S iht:S i ^ 2 = S k ^ 2⊢ S i = S k
  rw [sq_eq_sq_iff_eq_or_eq_negn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:0 ≤ S khik:k ≤ ihSS:S k ≤ S iht:S i = S k ∨ S i = -S k⊢ S i = S kn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:0 ≤ S khik:k ≤ ihSS:S k ≤ S iht:S i = S k ∨ S i = -S k⊢ S i = S k] at htn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:0 ≤ S khik:k ≤ ihSS:S k ≤ S iht:S i = S k ∨ S i = -S k⊢ S i = S k
  cases htinln:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:0 ≤ S khik:k ≤ ihSS:S k ≤ S ih✝:S i = S k⊢ S i = S kinrn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:0 ≤ S khik:k ≤ ihSS:S k ≤ S ih✝:S i = -S k⊢ S i = S k <;>inln:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:0 ≤ S khik:k ≤ ihSS:S k ≤ S ih✝:S i = S k⊢ S i = S kinrn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:0 ≤ S khik:k ≤ ihSS:S k ≤ S ih✝:S i = -S k⊢ S i = S k rename_i hinrn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:0 ≤ S khik:k ≤ ihSS:S k ≤ S ih:S i = -S k⊢ S i = S k
  ·inln:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:0 ≤ S khik:k ≤ ihSS:S k ≤ S ih:S i = S k⊢ S i = S k exact hAll goals completed! 🐙
  ·inrn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin n.succi:Fin n.succhk:0 ≤ S khik:k ≤ ihSS:S k ≤ S ih:S i = -S k⊢ S i = S k linarithAll goals completed! 🐙include hS in
lemma zero_gt (h0 : 0 ≤ S (0 : Fin n.succ)) (i : Fin n.succ) : S (0 : Fin n.succ) = S i := byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:0 ≤ S 0i:Fin n.succ⊢ S 0 = S i
  symmn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:0 ≤ S 0i:Fin n.succ⊢ S i = S 0
  refine gt_eq hS h0 (Fin.zero_le i)All goals completed! 🐙

include hS in
lemma opposite_signs_eq_neg {i j : Fin n.succ} (hi : S i ≤ 0) (hj : 0 ≤ S j) : S i = - S j := byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Si:Fin n.succj:Fin n.succhi:S i ≤ 0hj:0 ≤ S j⊢ S i = -S j
  have hSS := hS.1 i jn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Si:Fin n.succj:Fin n.succhi:S i ≤ 0hj:0 ≤ S jhSS:S i ^ 2 = S j ^ 2⊢ S i = -S j
  rw [sq_eq_sq_iff_eq_or_eq_negn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Si:Fin n.succj:Fin n.succhi:S i ≤ 0hj:0 ≤ S jhSS:S i = S j ∨ S i = -S j⊢ S i = -S jn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Si:Fin n.succj:Fin n.succhi:S i ≤ 0hj:0 ≤ S jhSS:S i = S j ∨ S i = -S j⊢ S i = -S j] at hSSn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Si:Fin n.succj:Fin n.succhi:S i ≤ 0hj:0 ≤ S jhSS:S i = S j ∨ S i = -S j⊢ S i = -S j
  cases' hSS with h hinln:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Si:Fin n.succj:Fin n.succhi:S i ≤ 0hj:0 ≤ S jh:S i = S j⊢ S i = -S jinrn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Si:Fin n.succj:Fin n.succhi:S i ≤ 0hj:0 ≤ S jh:S i = -S j⊢ S i = -S j
  ·inln:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Si:Fin n.succj:Fin n.succhi:S i ≤ 0hj:0 ≤ S jh:S i = S j⊢ S i = -S j simp_allinln:ℕS:(PureU1 n.succ).Chargesi:Fin n.succj:Fin n.succhS:ConstAbsSorted Shi:S j ≤ 0hj:0 ≤ S jh:S i = S j⊢ S j = -S j
    linarithAll goals completed! 🐙
  ·inrn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Si:Fin n.succj:Fin n.succhi:S i ≤ 0hj:0 ≤ S jh:S i = -S j⊢ S i = -S j exact hAll goals completed! 🐙

include hS in
lemma is_zero (h0 : S (0 : Fin n.succ) = 0) : S = 0 := byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 = 0⊢ S = 0
  funext in:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 = 0i:Fin (PureU1 n.succ).numberCharges⊢ S i = 0 i
  have ht := hS.1 i (0 : Fin n.succ)n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 = 0i:Fin (PureU1 n.succ).numberChargesht:S i ^ 2 = S 0 ^ 2⊢ S i = 0 i
  rw [h0n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 = 0i:Fin (PureU1 n.succ).numberChargesht:S i ^ 2 = 0 ^ 2⊢ S i = 0 in:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 = 0i:Fin (PureU1 n.succ).numberChargesht:S i ^ 2 = 0 ^ 2⊢ S i = 0 i] at htn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 = 0i:Fin (PureU1 n.succ).numberChargesht:S i ^ 2 = 0 ^ 2⊢ S i = 0 i
  simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, pow_eq_zero_iff] at htn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 = 0i:Fin (PureU1 n.succ).numberChargesht:S i = 0⊢ S i = 0 i
  exact htAll goals completed! 🐙

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.

@[simp]
def Boundary (S : (PureU1 n.succ).Charges) (k : Fin n) : Prop := S k.castSucc < 0 ∧ 0 < S k.succ

              include hS in
lemma boundary_castSucc {k : Fin n} (hk : Boundary S k) : S k.castSucc = S (0 : Fin n.succ) :=
  (lt_eq hS (le_of_lt hk.left) (Fin.zero_le k.castSucc : 0 ≤ k.castSucc)).symm

include hS in
lemma boundary_succ {k : Fin n} (hk : Boundary S k) : S k.succ = - S (0 : Fin n.succ) := byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S k⊢ S k.succ = -S 0
  have hn := boundary_castSucc hS hkn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khn:S k.castSucc = S 0⊢ S k.succ = -S 0
  rw [opposite_signs_eq_neg hS (le_of_lt hk.left) (le_of_lt hk.right)n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khn:-S k.succ = S 0⊢ S k.succ = -S 0n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khn:-S k.succ = S 0⊢ S k.succ = -S 0] at hnn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khn:-S k.succ = S 0⊢ S k.succ = -S 0
  linear_combination -(1 * hn)All goals completed! 🐙lemma boundary_split (k : Fin n) : k.succ.val + (n.succ - k.succ.val) = n.succ := byn:ℕk:Fin n⊢ ↑k.succ + (n.succ - ↑k.succ) = n.succ
  omegaAll goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma boundary_accGrav' (k : Fin n) : accGrav n.succ S =
    ∑ i : Fin (k.succ.val + (n.succ - k.succ.val)), S (Fin.cast (boundary_split k) i) := byn:ℕS:(PureU1 n.succ).Chargesk:Fin n⊢ (accGrav n.succ) S = ∑ i, S (Fin.cast ⋯ i)
  simp only [succ_eq_add_one, accGrav, LinearMap.coe_mk, AddHom.coe_mk, Fin.val_succ]n:ℕS:(PureU1 n.succ).Chargesk:Fin n⊢ ∑ i, S i = ∑ x, S (Fin.cast ⋯ x)
  erw [Finset.sum_equiv (Fin.castOrderIso (boundary_split k)).toEquivn:ℕS:(PureU1 n.succ).Chargesk:Fin n⊢ ∑ i, S i = ∑ i ∈ ?m.34, ?m.36 ihstn:ℕS:(PureU1 n.succ).Chargesk:Fin n⊢ ∀ (i : Fin (↑k.succ + (n.succ - ↑k.succ))), i ∈ univ ↔ (Fin.castOrderIso ⋯).toEquiv i ∈ ?m.34hfgn:ℕS:(PureU1 n.succ).Chargesk:Fin n⊢ ∀ i ∈ univ, S (Fin.cast ⋯ i) = ?m.36 ((Fin.castOrderIso ⋯).toEquiv i)n:ℕS:(PureU1 n.succ).Chargesk:Fin n⊢ Finset (Fin n.succ)n:ℕS:(PureU1 n.succ).Chargesk:Fin n⊢ Fin n.succ → ℚ]hstn:ℕS:(PureU1 n.succ).Chargesk:Fin n⊢ ∀ (i : Fin (↑k.succ + (n.succ - ↑k.succ))), i ∈ univ ↔ (Fin.castOrderIso ⋯).toEquiv i ∈ univhfgn:ℕS:(PureU1 n.succ).Chargesk:Fin n⊢ ∀ i ∈ univ, S (Fin.cast ⋯ i) = S ((Fin.castOrderIso ⋯).toEquiv i)
  ·hstn:ℕS:(PureU1 n.succ).Chargesk:Fin n⊢ ∀ (i : Fin (↑k.succ + (n.succ - ↑k.succ))), i ∈ univ ↔ (Fin.castOrderIso ⋯).toEquiv i ∈ univ intro ihstn:ℕS:(PureU1 n.succ).Chargesk:Fin ni:Fin (↑k.succ + (n.succ - ↑k.succ))⊢ i ∈ univ ↔ (Fin.castOrderIso ⋯).toEquiv i ∈ univ
    simp only [Fin.val_succ, mem_univ, RelIso.coe_fn_toEquiv]All goals completed! 🐙
  ·hfgn:ℕS:(PureU1 n.succ).Chargesk:Fin n⊢ ∀ i ∈ univ, S (Fin.cast ⋯ i) = S ((Fin.castOrderIso ⋯).toEquiv i) exact fun _ _ => rflAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
include hS in
lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) :
    accGrav n.succ S = (2 * ↑↑k + 1 - ↑n) * S (0 : Fin n.succ) := byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S k⊢ (accGrav n.succ) S = (2 * ↑↑k + 1 - ↑n) * S 0
  rw [boundary_accGrav' kn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S k⊢ ∑ i, S (Fin.cast ⋯ i) = (2 * ↑↑k + 1 - ↑n) * S 0n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S k⊢ ∑ i, S (Fin.cast ⋯ i) = (2 * ↑↑k + 1 - ↑n) * S 0]n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S k⊢ ∑ i, S (Fin.cast ⋯ i) = (2 * ↑↑k + 1 - ↑n) * S 0
  rw [Fin.sum_univ_addn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S k⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) =
  (2 * ↑↑k + 1 - ↑n) * S 0n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S k⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) =
  (2 * ↑↑k + 1 - ↑n) * S 0]n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S k⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) =
  (2 * ↑↑k + 1 - ↑n) * S 0
  have hfst (i : Fin k.succ.val) :
      S (Fin.cast (boundary_split k) (Fin.castAdd (n.succ - k.succ.val) i)) = S k.castSucc := byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S k⊢ (accGrav n.succ) S = (2 * ↑↑k + 1 - ↑n) * S 0n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucc⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) =
  (2 * ↑↑k + 1 - ↑n) * S 0
    apply lt_eq hS (le_of_lt hk.left) (Fin.is_le i)n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucc⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) =
  (2 * ↑↑k + 1 - ↑n) * S 0n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucc⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) =
  (2 * ↑↑k + 1 - ↑n) * S 0
  have hsnd (i : Fin (n.succ - k.succ.val)) :
      S (Fin.cast (boundary_split k) (Fin.natAdd (k.succ.val) i)) = S k.succ := byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S k⊢ (accGrav n.succ) S = (2 * ↑↑k + 1 - ↑n) * S 0n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucchsnd:∀ (i : Fin (n.succ - ↑k.succ)), S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) = S k.succ⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) =
  (2 * ↑↑k + 1 - ↑n) * S 0
    apply gt_eq hS (le_of_lt hk.right) (byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucci:Fin (n.succ - ↑k.succ)⊢ k.succ ≤ Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucchsnd:∀ (i : Fin (n.succ - ↑k.succ)), S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) = S k.succ⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) =
  (2 * ↑↑k + 1 - ↑n) * S 0 rw [Fin.le_defn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucci:Fin (n.succ - ↑k.succ)⊢ ↑k.succ ≤ ↑(Fin.cast ⋯ (Fin.natAdd (↑k.succ) i))n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucci:Fin (n.succ - ↑k.succ)⊢ ↑k.succ ≤ ↑(Fin.cast ⋯ (Fin.natAdd (↑k.succ) i))n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucchsnd:∀ (i : Fin (n.succ - ↑k.succ)), S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) = S k.succ⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) =
  (2 * ↑↑k + 1 - ↑n) * S 0]n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucci:Fin (n.succ - ↑k.succ)⊢ ↑k.succ ≤ ↑(Fin.cast ⋯ (Fin.natAdd (↑k.succ) i))n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucchsnd:∀ (i : Fin (n.succ - ↑k.succ)), S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) = S k.succ⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) =
  (2 * ↑↑k + 1 - ↑n) * S 0; exact le.intro rflAll goals completed! 🐙n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucchsnd:∀ (i : Fin (n.succ - ↑k.succ)), S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) = S k.succ⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) =
  (2 * ↑↑k + 1 - ↑n) * S 0)n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucchsnd:∀ (i : Fin (n.succ - ↑k.succ)), S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) = S k.succ⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) =
  (2 * ↑↑k + 1 - ↑n) * S 0
  simp only [hfst, hsnd]n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucchsnd:∀ (i : Fin (n.succ - ↑k.succ)), S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) = S k.succ⊢ ∑ x, S k.castSucc + ∑ x, S k.succ = (2 * ↑↑k + 1 - ↑n) * S 0
  simp only [Fin.val_succ, sum_const, Finset.card_fin, nsmul_eq_mul, cast_add, cast_one,
    succ_sub_succ_eq_sub, Fin.is_le', cast_sub]n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucchsnd:∀ (i : Fin (n.succ - ↑k.succ)), S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) = S k.succ⊢ (↑↑k + 1) * S k.castSucc + (↑n - ↑↑k) * S k.succ = (2 * ↑↑k + 1 - ↑n) * S 0
  rw [boundary_castSucc hS hk,n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucchsnd:∀ (i : Fin (n.succ - ↑k.succ)), S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) = S k.succ⊢ (↑↑k + 1) * S 0 + (↑n - ↑↑k) * S k.succ = (2 * ↑↑k + 1 - ↑n) * S 0n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucchsnd:∀ (i : Fin (n.succ - ↑k.succ)), S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) = S k.succ⊢ (↑↑k + 1) * S 0 + (↑n - ↑↑k) * -S 0 = (2 * ↑↑k + 1 - ↑n) * S 0 boundary_succ hS hkn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucchsnd:∀ (i : Fin (n.succ - ↑k.succ)), S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) = S k.succ⊢ (↑↑k + 1) * S 0 + (↑n - ↑↑k) * -S 0 = (2 * ↑↑k + 1 - ↑n) * S 0n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucchsnd:∀ (i : Fin (n.succ - ↑k.succ)), S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) = S k.succ⊢ (↑↑k + 1) * S 0 + (↑n - ↑↑k) * -S 0 = (2 * ↑↑k + 1 - ↑n) * S 0]n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sk:Fin nhk:Boundary S khfst:∀ (i : Fin ↑k.succ), S (Fin.cast ⋯ (Fin.castAdd (n.succ - ↑k.succ) i)) = S k.castSucchsnd:∀ (i : Fin (n.succ - ↑k.succ)), S (Fin.cast ⋯ (Fin.natAdd (↑k.succ) i)) = S k.succ⊢ (↑↑k + 1) * S 0 + (↑n - ↑↑k) * -S 0 = (2 * ↑↑k + 1 - ↑n) * S 0
  ringAll goals completed! 🐙

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

@[simp]
def HasBoundary (S : (PureU1 n.succ).Charges) : Prop :=
  ∃ (k : Fin n), Boundary S k

              include hS in
lemma not_hasBoundary_zero_le (hnot : ¬ (HasBoundary S)) (h0 : S (0 : Fin n.succ) < 0) :
    ∀ i, S (0 : Fin n.succ) = S i := byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Shnot:¬HasBoundary Sh0:S 0 < 0⊢ ∀ (i : Fin (PureU1 n.succ).numberCharges), S 0 = S i
  intro ⟨i, hi⟩n:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Shnot:¬HasBoundary Sh0:S 0 < 0i:ℕhi:i < (PureU1 n.succ).numberCharges⊢ S 0 = S ⟨i, hi⟩
  simp only [HasBoundary, Boundary, not_exists, not_and, not_lt] at hnotn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 < 0i:ℕhi:i < (PureU1 n.succ).numberChargeshnot:∀ (x : Fin n), S x.castSucc < 0 → S x.succ ≤ 0⊢ S 0 = S ⟨i, hi⟩
  induction izeron:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 < 0hnot:∀ (x : Fin n), S x.castSucc < 0 → S x.succ ≤ 0hi:0 < (PureU1 n.succ).numberCharges⊢ S 0 = S ⟨0, hi⟩succn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 < 0hnot:∀ (x : Fin n), S x.castSucc < 0 → S x.succ ≤ 0n✝:ℕa✝:∀ (hi : n✝ < (PureU1 n.succ).numberCharges), S 0 = S ⟨n✝, hi⟩hi:n✝ + 1 < (PureU1 n.succ).numberCharges⊢ S 0 = S ⟨n✝ + 1, hi⟩
  ·zeron:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 < 0hnot:∀ (x : Fin n), S x.castSucc < 0 → S x.succ ≤ 0hi:0 < (PureU1 n.succ).numberCharges⊢ S 0 = S ⟨0, hi⟩ rflAll goals completed! 🐙
  ·succn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 < 0hnot:∀ (x : Fin n), S x.castSucc < 0 → S x.succ ≤ 0n✝:ℕa✝:∀ (hi : n✝ < (PureU1 n.succ).numberCharges), S 0 = S ⟨n✝, hi⟩hi:n✝ + 1 < (PureU1 n.succ).numberCharges⊢ S 0 = S ⟨n✝ + 1, hi⟩ rename_i i hiisuccn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 < 0hnot:∀ (x : Fin n), S x.castSucc < 0 → S x.succ ≤ 0i:ℕhii:∀ (hi : n✝ < (PureU1 n.succ).numberCharges), S 0 = S ⟨n✝, hi⟩hi:n✝ + 1 < (PureU1 n.succ).numberCharges⊢ S 0 = S ⟨n✝ + 1, hi⟩
    have hnott := hnot ⟨i, succ_lt_succ_iff.mp hi⟩succn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 < 0hnot:∀ (x : Fin n), S x.castSucc < 0 → S x.succ ≤ 0i:ℕhii:∀ (hi : n✝ < (PureU1 n.succ).numberCharges), S 0 = S ⟨n✝, hi⟩hi:n✝ + 1 < (PureU1 n.succ).numberChargeshnott:S ⟨i, ⋯⟩.castSucc < 0 → S ⟨i, ⋯⟩.succ ≤ 0⊢ S 0 = S ⟨n✝ + 1, hi⟩
    have hii := hii (lt_of_succ_lt hi)succn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 < 0hnot:∀ (x : Fin n), S x.castSucc < 0 → S x.succ ≤ 0i:ℕhii✝:∀ (hi : n✝ < (PureU1 n.succ).numberCharges), S 0 = S ⟨n✝, hi⟩hi:n✝ + 1 < (PureU1 n.succ).numberChargeshnott:S ⟨i, ⋯⟩.castSucc < 0 → S ⟨i, ⋯⟩.succ ≤ 0hii:S 0 = S ⟨i, ⋯⟩⊢ S 0 = S ⟨n✝ + 1, hi⟩
    erw [← hiisuccn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 < 0hnot:∀ (x : Fin n), S x.castSucc < 0 → S x.succ ≤ 0i:ℕhii✝:∀ (hi : n✝ < (PureU1 n.succ).numberCharges), S 0 = S ⟨n✝, hi⟩hi:n✝ + 1 < (PureU1 n.succ).numberChargeshnott:S 0 < 0 → S ⟨i, ⋯⟩.succ ≤ 0hii:S 0 = S ⟨i, ⋯⟩⊢ S 0 = S ⟨n✝ + 1, hi⟩]succn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Sh0:S 0 < 0hnot:∀ (x : Fin n), S x.castSucc < 0 → S x.succ ≤ 0i:ℕhii✝:∀ (hi : n✝ < (PureU1 n.succ).numberCharges), S 0 = S ⟨n✝, hi⟩hi:n✝ + 1 < (PureU1 n.succ).numberChargeshnott:S 0 < 0 → S ⟨i, ⋯⟩.succ ≤ 0hii:S 0 = S ⟨i, ⋯⟩⊢ S 0 = S ⟨n✝ + 1, hi⟩ at hnott
    exact (val_le_zero hS (hnott h0)).symmAll goals completed! 🐙include hS in
lemma not_hasBoundry_zero (hnot : ¬ (HasBoundary S)) (i : Fin n.succ) :
    S (0 : Fin n.succ) = S i := byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Shnot:¬HasBoundary Si:Fin n.succ⊢ S 0 = S i
  by_cases hi : S (0 : Fin n.succ) < 0posn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Shnot:¬HasBoundary Si:Fin n.succhi:S 0 < 0⊢ S 0 = S inegn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Shnot:¬HasBoundary Si:Fin n.succhi:¬S 0 < 0⊢ S 0 = S i
  ·posn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Shnot:¬HasBoundary Si:Fin n.succhi:S 0 < 0⊢ S 0 = S i exact not_hasBoundary_zero_le hS hnot hi iAll goals completed! 🐙
  ·negn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Shnot:¬HasBoundary Si:Fin n.succhi:¬S 0 < 0⊢ S 0 = S i simp only [not_lt] at hinegn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Shnot:¬HasBoundary Si:Fin n.succhi:0 ≤ S 0⊢ S 0 = S i
    exact zero_gt hS hi iAll goals completed! 🐙include hS in
lemma not_hasBoundary_grav (hnot : ¬ (HasBoundary S)) :
    accGrav n.succ S = n.succ * S (0 : Fin n.succ) := byn:ℕS:(PureU1 n.succ).ChargeshS:ConstAbsSorted Shnot:¬HasBoundary S⊢ (accGrav n.succ) S = ↑n.succ * S 0
  simp [accGrav, ← not_hasBoundry_zero hS hnot]All goals completed! 🐙

include hA in
lemma AFL_hasBoundary (h : A.val (0 : Fin n.succ) ≠ 0) : HasBoundary A.val := byn:ℕA:(PureU1 n.succ).LinSolshA:ConstAbsSorted A.valh:A.val 0 ≠ 0⊢ HasBoundary A.val
  by_contra hnn:ℕA:(PureU1 n.succ).LinSolshA:ConstAbsSorted A.valh:A.val 0 ≠ 0hn:¬HasBoundary A.val⊢ False
  have h0 := not_hasBoundary_grav hA hnn:ℕA:(PureU1 n.succ).LinSolshA:ConstAbsSorted A.valh:A.val 0 ≠ 0hn:¬HasBoundary A.valh0:(accGrav n.succ) A.val = ↑n.succ * A.val 0⊢ False
  simp only [succ_eq_add_one, accGrav, LinearMap.coe_mk, AddHom.coe_mk, cast_add, cast_one] at h0n:ℕA:(PureU1 n.succ).LinSolshA:ConstAbsSorted A.valh:A.val 0 ≠ 0hn:¬HasBoundary A.valh0:∑ i, A.val i = (↑n + 1) * A.val 0⊢ False
  rw [pureU1_linear An:ℕA:(PureU1 n.succ).LinSolshA:ConstAbsSorted A.valh:A.val 0 ≠ 0hn:¬HasBoundary A.valh0:0 = (↑n + 1) * A.val 0⊢ Falsen:ℕA:(PureU1 n.succ).LinSolshA:ConstAbsSorted A.valh:A.val 0 ≠ 0hn:¬HasBoundary A.valh0:0 = (↑n + 1) * A.val 0⊢ False] at h0n:ℕA:(PureU1 n.succ).LinSolshA:ConstAbsSorted A.valh:A.val 0 ≠ 0hn:¬HasBoundary A.valh0:0 = (↑n + 1) * A.val 0⊢ False
  simp only [zero_eq_mul] at h0n:ℕA:(PureU1 n.succ).LinSolshA:ConstAbsSorted A.valh:A.val 0 ≠ 0hn:¬HasBoundary A.valh0:↑n + 1 = 0 ∨ A.val 0 = 0⊢ False
  cases' h0inln:ℕA:(PureU1 n.succ).LinSolshA:ConstAbsSorted A.valh:A.val 0 ≠ 0hn:¬HasBoundary A.valh✝:↑n + 1 = 0⊢ Falseinrn:ℕA:(PureU1 n.succ).LinSolshA:ConstAbsSorted A.valh:A.val 0 ≠ 0hn:¬HasBoundary A.valh✝:A.val 0 = 0⊢ False
  ·inln:ℕA:(PureU1 n.succ).LinSolshA:ConstAbsSorted A.valh:A.val 0 ≠ 0hn:¬HasBoundary A.valh✝:↑n + 1 = 0⊢ False linarithAll goals completed! 🐙
  ·inrn:ℕA:(PureU1 n.succ).LinSolshA:ConstAbsSorted A.valh:A.val 0 ≠ 0hn:¬HasBoundary A.valh✝:A.val 0 = 0⊢ False simp_allAll goals completed! 🐙

lemma AFL_odd_noBoundary {A : (PureU1 (2 * n + 1)).LinSols} (h : ConstAbsSorted A.val)
    (hA : A.val (0 : Fin (2*n +1)) ≠ 0) : ¬ HasBoundary A.val := byn:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0⊢ ¬HasBoundary A.val
  by_contra hnn:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0hn:HasBoundary A.val⊢ False
  obtain ⟨k, hk⟩ := hnn:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val k⊢ False
  have h0 := boundary_accGrav'' h k hkn:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:(accGrav (2 * n).succ) A.val = (2 * ↑↑k + 1 - ↑(2 * n)) * A.val 0⊢ False
  simp only [succ_eq_add_one, accGrav, LinearMap.coe_mk, AddHom.coe_mk, cast_mul, cast_ofNat] at h0n:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:∑ i, A.val i = (2 * ↑↑k + 1 - 2 * ↑n) * A.val 0⊢ False
  rw [pureU1_linear An:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:0 = (2 * ↑↑k + 1 - 2 * ↑n) * A.val 0⊢ Falsen:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:0 = (2 * ↑↑k + 1 - 2 * ↑n) * A.val 0⊢ False] at h0n:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:0 = (2 * ↑↑k + 1 - 2 * ↑n) * A.val 0⊢ False
  simp only [zero_eq_mul, hA, or_false] at h0n:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:2 * ↑↑k + 1 - 2 * ↑n = 0⊢ False
  have h1 : 2 * n = 2 * k.val + 1 := byn:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0⊢ ¬HasBoundary A.valn:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:2 * ↑↑k + 1 - 2 * ↑n = 0h1:2 * n = 2 * ↑k + 1⊢ False
    rw [← @Nat.cast_inj ℚn:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:2 * ↑↑k + 1 - 2 * ↑n = 0⊢ ↑(2 * n) = ↑(2 * ↑k + 1)n:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:2 * ↑↑k + 1 - 2 * ↑n = 0⊢ ↑(2 * n) = ↑(2 * ↑k + 1)n:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:2 * ↑↑k + 1 - 2 * ↑n = 0h1:2 * n = 2 * ↑k + 1⊢ False]n:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:2 * ↑↑k + 1 - 2 * ↑n = 0⊢ ↑(2 * n) = ↑(2 * ↑k + 1)n:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:2 * ↑↑k + 1 - 2 * ↑n = 0h1:2 * n = 2 * ↑k + 1⊢ False
    simp only [cast_mul, cast_ofNat, cast_add, cast_one]n:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:2 * ↑↑k + 1 - 2 * ↑n = 0⊢ 2 * ↑n = 2 * ↑↑k + 1n:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:2 * ↑↑k + 1 - 2 * ↑n = 0h1:2 * n = 2 * ↑k + 1⊢ False
    linear_combination - h0n:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:2 * ↑↑k + 1 - 2 * ↑n = 0h1:2 * n = 2 * ↑k + 1⊢ Falsen:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n)hk:Boundary A.val kh0:2 * ↑↑k + 1 - 2 * ↑n = 0h1:2 * n = 2 * ↑k + 1⊢ False
  omegaAll goals completed! 🐙lemma AFL_odd_zero {A : (PureU1 (2 * n + 1)).LinSols} (h : ConstAbsSorted A.val) :
    A.val (0 : Fin (2 * n + 1)) = 0 := byn:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.val⊢ A.val 0 = 0
  by_contra hnn:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.valhn:¬A.val 0 = 0⊢ False
  exact (AFL_odd_noBoundary h hn) (AFL_hasBoundary h hn)All goals completed! 🐙theorem AFL_odd (A : (PureU1 (2 * n + 1)).LinSols) (h : ConstAbsSorted A.val) :
    A = 0 := byn:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.val⊢ A = 0
  apply ACCSystemLinear.LinSols.extn:ℕA:(PureU1 (2 * n + 1)).LinSolsh:ConstAbsSorted A.val⊢ A.val = ACCSystemLinear.LinSols.val 0
  exact is_zero h (AFL_odd_zero h)All goals completed! 🐙

lemma AFL_even_Boundary {A : (PureU1 (2 * n.succ)).LinSols} (h : ConstAbsSorted A.val)
    (hA : A.val (0 : Fin (2 * n.succ)) ≠ 0) {k : Fin (2 * n + 1)} (hk : Boundary A.val k) :
    k.val = n := byn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n + 1)hk:Boundary A.val k⊢ ↑k = n
  have h0 := boundary_accGrav'' h k hkn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n + 1)hk:Boundary A.val kh0:(accGrav (Nat.mul 2 n + 1).succ) A.val = (2 * ↑↑k + 1 - ↑(Nat.mul 2 n + 1)) * A.val 0⊢ ↑k = n
  change ∑ i, A.val i = _ at h0n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n + 1)hk:Boundary A.val kh0:∑ i, A.val i = (2 * ↑↑k + 1 - ↑(Nat.mul 2 n + 1)) * A.val 0⊢ ↑k = n
  simp only [succ_eq_add_one, mul_eq, cast_add, cast_mul, cast_ofNat,
    cast_one, add_sub_add_right_eq_sub] at h0n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n + 1)hk:Boundary A.val kh0:∑ x, A.val x = (2 * ↑↑k - 2 * ↑n) * A.val 0⊢ ↑k = n
  erw [pureU1_linear An:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n + 1)hk:Boundary A.val kh0:0 = (2 * ↑↑k - 2 * ↑n) * A.val 0⊢ ↑k = n]n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n + 1)hk:Boundary A.val kh0:0 = (2 * ↑↑k - 2 * ↑n) * A.val 0⊢ ↑k = n at h0
  simp only [zero_eq_mul, hA, or_false] at h0n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n + 1)hk:Boundary A.val kh0:2 * ↑↑k - 2 * ↑n = 0⊢ ↑k = n
  rw [← @Nat.cast_inj ℚn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n + 1)hk:Boundary A.val kh0:2 * ↑↑k - 2 * ↑n = 0⊢ ↑↑k = ↑nn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n + 1)hk:Boundary A.val kh0:2 * ↑↑k - 2 * ↑n = 0⊢ ↑↑k = ↑n]n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0k:Fin (2 * n + 1)hk:Boundary A.val kh0:2 * ↑↑k - 2 * ↑n = 0⊢ ↑↑k = ↑n
  linear_combination h0 / 2All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma AFL_even_below' {A : (PureU1 (2 * n.succ)).LinSols} (h : ConstAbsSorted A.val)
    (hA : A.val (0 : Fin (2 * n.succ)) ≠ 0) (i : Fin n.succ) :
    A.val (Fin.cast (split_equal n.succ) (Fin.castAdd n.succ i)) = A.val (0 : Fin (2*n.succ)) := byn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succ⊢ A.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = A.val 0
  obtain ⟨k, hk⟩ := AFL_hasBoundary h hAn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ A.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = A.val 0
  rw [← boundary_castSucc h hkn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ A.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = A.val k.castSuccn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ A.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = A.val k.castSucc]n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ A.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = A.val k.castSucc
  apply lt_eq h (le_of_lt hk.left)n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ Fin.cast ⋯ (Fin.castAdd n.succ i) ≤ k.castSucc
  rw [Fin.le_defn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ ↑(Fin.cast ⋯ (Fin.castAdd n.succ i)) ≤ ↑k.castSuccn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ ↑(Fin.cast ⋯ (Fin.castAdd n.succ i)) ≤ ↑k.castSucc]n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ ↑(Fin.cast ⋯ (Fin.castAdd n.succ i)) ≤ ↑k.castSucc
  simp only [Fin.val_cast, Fin.val_castAdd, mul_eq, Fin.val_castSucc]n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ ↑i ≤ ↑k
  rw [AFL_even_Boundary h hA hkn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ ↑i ≤ nn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ ↑i ≤ n]n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ ↑i ≤ n
  exact Fin.is_le iAll goals completed! 🐙

lemma AFL_even_below (A : (PureU1 (2 * n.succ)).LinSols) (h : ConstAbsSorted A.val)
    (i : Fin n.succ) :
    A.val (Fin.cast (split_equal n.succ) (Fin.castAdd n.succ i))
    = A.val (0 : Fin (2*n.succ)) := byn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succ⊢ A.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = A.val 0
  by_cases hA : A.val (0 : Fin (2*n.succ)) = 0posn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:A.val 0 = 0⊢ A.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = A.val 0negn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:¬A.val 0 = 0⊢ A.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = A.val 0
  ·posn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:A.val 0 = 0⊢ A.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = A.val 0 rw [is_zero h hAposn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:A.val 0 = 0⊢ 0 (Fin.cast ⋯ (Fin.castAdd n.succ i)) = 0 0posn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:A.val 0 = 0⊢ 0 (Fin.cast ⋯ (Fin.castAdd n.succ i)) = 0 0]posn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:A.val 0 = 0⊢ 0 (Fin.cast ⋯ (Fin.castAdd n.succ i)) = 0 0
    rflAll goals completed! 🐙
  ·negn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:¬A.val 0 = 0⊢ A.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = A.val 0 exact AFL_even_below' h hA iAll goals completed! 🐙

lemma AFL_even_above' {A : (PureU1 (2 * n.succ)).LinSols} (h : ConstAbsSorted A.val)
    (hA : A.val (0 : Fin (2*n.succ)) ≠ 0) (i : Fin n.succ) :
    A.val (Fin.cast (split_equal n.succ) (Fin.natAdd n.succ i)) =
    - A.val (0 : Fin (2*n.succ)) := byn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succ⊢ A.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -A.val 0
  obtain ⟨k, hk⟩ := AFL_hasBoundary h hAn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ A.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -A.val 0
  rw [← boundary_succ h hkn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ A.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = A.val k.succn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ A.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = A.val k.succ]n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ A.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = A.val k.succ
  apply gt_eq h (le_of_lt hk.right)n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ k.succ ≤ Fin.cast ⋯ (Fin.natAdd n.succ i)
  rw [Fin.le_defn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ ↑k.succ ≤ ↑(Fin.cast ⋯ (Fin.natAdd n.succ i))n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ ↑k.succ ≤ ↑(Fin.cast ⋯ (Fin.natAdd n.succ i))]n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ ↑k.succ ≤ ↑(Fin.cast ⋯ (Fin.natAdd n.succ i))
  simp only [mul_eq, Fin.val_succ, Fin.val_cast, Fin.val_natAdd]n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ ↑k + 1 ≤ n.succ + ↑i
  rw [AFL_even_Boundary h hA hkn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ n + 1 ≤ n.succ + ↑in:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ n + 1 ≤ n.succ + ↑i]n:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.valhA:A.val 0 ≠ 0i:Fin n.succk:Fin (Nat.mul 2 n + 1)hk:Boundary A.val k⊢ n + 1 ≤ n.succ + ↑i
  exact Nat.le_add_right (n + 1) ↑iAll goals completed! 🐙

lemma AFL_even_above (A : (PureU1 (2 * n.succ)).LinSols) (h : ConstAbsSorted A.val)
    (i : Fin n.succ) :
    A.val (Fin.cast (split_equal n.succ) (Fin.natAdd n.succ i)) =
    - A.val (0 : Fin (2 * n.succ)) := byn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succ⊢ A.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -A.val 0
  by_cases hA : A.val (0 : Fin (2 * n.succ)) = 0posn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:A.val 0 = 0⊢ A.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -A.val 0negn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:¬A.val 0 = 0⊢ A.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -A.val 0
  ·posn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:A.val 0 = 0⊢ A.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -A.val 0 rw [is_zero h hAposn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:A.val 0 = 0⊢ 0 (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -0 0posn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:A.val 0 = 0⊢ 0 (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -0 0]posn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:A.val 0 = 0⊢ 0 (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -0 0
    rflAll goals completed! 🐙
  ·negn:ℕA:(PureU1 (2 * n.succ)).LinSolsh:ConstAbsSorted A.vali:Fin n.succhA:¬A.val 0 = 0⊢ A.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -A.val 0 exact AFL_even_above' h hA iAll goals completed! 🐙theorem boundary_value_odd (S : (PureU1 (2 * n + 1)).LinSols) (hs : ConstAbs S.val) :
    S = 0 :=
  have hS := And.intro (constAbs_sort hs) (sort_sorted S.val)
  sortAFL_zero S (ConstAbsSorted.AFL_odd (sortAFL S) hS)

theorem boundary_value_even (S : (PureU1 (2 * n.succ)).LinSols) (hs : ConstAbs S.val) :
    VectorLikeEven S.val := byn:ℕS:(PureU1 (2 * n.succ)).LinSolshs:ConstAbs S.val⊢ VectorLikeEven S.val
  have hS := And.intro (constAbs_sort hs) (sort_sorted S.val)n:ℕS:(PureU1 (2 * n.succ)).LinSolshs:ConstAbs S.valhS:ConstAbs (sort S.val) ∧ Sorted (sort S.val)⊢ VectorLikeEven S.val
  intro in:ℕS:(PureU1 (2 * n.succ)).LinSolshs:ConstAbs S.valhS:ConstAbs (sort S.val) ∧ Sorted (sort S.val)i:Fin n.succ⊢ sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = -sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i))
  have h1 := ConstAbsSorted.AFL_even_below (sortAFL S) hSn:ℕS:(PureU1 (2 * n.succ)).LinSolshs:ConstAbs S.valhS:ConstAbs (sort S.val) ∧ Sorted (sort S.val)i:Fin n.succh1:∀ (i : Fin n.succ), (sortAFL S).val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = (sortAFL S).val 0⊢ sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = -sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i))
  have h2 := ConstAbsSorted.AFL_even_above (sortAFL S) hSn:ℕS:(PureU1 (2 * n.succ)).LinSolshs:ConstAbs S.valhS:ConstAbs (sort S.val) ∧ Sorted (sort S.val)i:Fin n.succh1:∀ (i : Fin n.succ), (sortAFL S).val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = (sortAFL S).val 0h2:∀ (i : Fin n.succ), (sortAFL S).val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -(sortAFL S).val 0⊢ sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = -sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i))
  rw [sortAFL_valn:ℕS:(PureU1 (2 * n.succ)).LinSolshs:ConstAbs S.valhS:ConstAbs (sort S.val) ∧ Sorted (sort S.val)i:Fin n.succh1:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = sort S.val 0h2:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -sort S.val 0⊢ sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = -sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i))n:ℕS:(PureU1 (2 * n.succ)).LinSolshs:ConstAbs S.valhS:ConstAbs (sort S.val) ∧ Sorted (sort S.val)i:Fin n.succh1:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = sort S.val 0h2:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -sort S.val 0⊢ sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = -sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i))] at h1 h2n:ℕS:(PureU1 (2 * n.succ)).LinSolshs:ConstAbs S.valhS:ConstAbs (sort S.val) ∧ Sorted (sort S.val)i:Fin n.succh1:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = sort S.val 0h2:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -sort S.val 0⊢ sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = -sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i))
  rw [h1,n:ℕS:(PureU1 (2 * n.succ)).LinSolshs:ConstAbs S.valhS:ConstAbs (sort S.val) ∧ Sorted (sort S.val)i:Fin n.succh1:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = sort S.val 0h2:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -sort S.val 0⊢ sort S.val 0 = -sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i))n:ℕS:(PureU1 (2 * n.succ)).LinSolshs:ConstAbs S.valhS:ConstAbs (sort S.val) ∧ Sorted (sort S.val)i:Fin n.succh1:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = sort S.val 0h2:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -sort S.val 0⊢ sort S.val 0 = - -sort S.val 0 h2n:ℕS:(PureU1 (2 * n.succ)).LinSolshs:ConstAbs S.valhS:ConstAbs (sort S.val) ∧ Sorted (sort S.val)i:Fin n.succh1:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = sort S.val 0h2:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -sort S.val 0⊢ sort S.val 0 = - -sort S.val 0n:ℕS:(PureU1 (2 * n.succ)).LinSolshs:ConstAbs S.valhS:ConstAbs (sort S.val) ∧ Sorted (sort S.val)i:Fin n.succh1:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = sort S.val 0h2:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -sort S.val 0⊢ sort S.val 0 = - -sort S.val 0]n:ℕS:(PureU1 (2 * n.succ)).LinSolshs:ConstAbs S.valhS:ConstAbs (sort S.val) ∧ Sorted (sort S.val)i:Fin n.succh1:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.castAdd n.succ i)) = sort S.val 0h2:∀ (i : Fin n.succ), sort S.val (Fin.cast ⋯ (Fin.natAdd n.succ i)) = -sort S.val 0⊢ sort S.val 0 = - -sort S.val 0
  exact (InvolutiveNeg.neg_neg (sort S.val _)).symmAll goals completed! 🐙