1. Physlib
  2. QFT
  3. QED
  4. AnomalyCancellation
  5. LineInPlaneCond
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.ConstAbs

Line in plane condition

We say a LinSol satisfies the line in plane condition if for all distinct i1, i2, i3 in Fin n, we have S i1 = S i2 or S i1 = - S i2 or 2 S i3 + S i1 + S i2 = 0.

We look at various consequences of this. The main reference for this material is

    https://arxiv.org/pdf/1912.04804.pdf

We will show that n ≥ 4 the line in plane condition on solutions implies the constAbs condition.

@[expose] public section

The proposition on three rationals to satisfy the linInPlane condition.

def LineInPlaneProp : ℚ × ℚ × ℚ → Prop := fun s => s.1 = s.2.1 ∨ s.1 = - s.2.1 ∨ 2 * s.2.2 + s.1 + s.2.1 = 0

The proposition on a LinSol to satisfy the linInPlane condition.

def LineInPlaneCond (S : (PureU1 n).LinSols) : Prop := ∀ (i1 i2 i3 : Fin n) (_ : i1 ≠ i2) (_ : i2 ≠ i3) (_ : i1 ≠ i3), LineInPlaneProp (S.val i1, (S.val i2, S.val i3))
lemma lineInPlaneCond_perm {S : (PureU1 n).LinSols} (hS : LineInPlaneCond S) (M : (FamilyPermutations n).group) : LineInPlaneCond ((FamilyPermutations n).linSolRep M S) := n:ℕS:(PureU1 n).LinSolshS:LineInPlaneCond SM:(FamilyPermutations n).group⊢ LineInPlaneCond (((FamilyPermutations n).linSolRep M) S) n:ℕS:(PureU1 n).LinSolshS:LineInPlaneCond SM:(FamilyPermutations n).groupi1:Fin ni2:Fin ni3:Fin nh1:i1 ≠ i2h2:i2 ≠ i3h3:i1 ≠ i3⊢ LineInPlaneProp ((((FamilyPermutations n).linSolRep M) S).val i1, (((FamilyPermutations n).linSolRep M) S).val i2, (((FamilyPermutations n).linSolRep M) S).val i3) n:ℕS:(PureU1 n).LinSolshS:LineInPlaneCond SM:(FamilyPermutations n).groupi1:Fin ni2:Fin ni3:Fin nh1:i1 ≠ i2h2:i2 ≠ i3h3:i1 ≠ i3⊢ LineInPlaneProp (S.val (M.invFun i1), S.val (M.invFun i2), S.val (M.invFun i3)) n:ℕS:(PureU1 n).LinSolshS:LineInPlaneCond SM:(FamilyPermutations n).groupi1:Fin ni2:Fin ni3:Fin nh1:i1 ≠ i2h2:i2 ≠ i3h3:i1 ≠ i3⊢ M.invFun i1 ≠ M.invFun i2n:ℕS:(PureU1 n).LinSolshS:LineInPlaneCond SM:(FamilyPermutations n).groupi1:Fin ni2:Fin ni3:Fin nh1:i1 ≠ i2h2:i2 ≠ i3h3:i1 ≠ i3⊢ M.invFun i2 ≠ M.invFun i3n:ℕS:(PureU1 n).LinSolshS:LineInPlaneCond SM:(FamilyPermutations n).groupi1:Fin ni2:Fin ni3:Fin nh1:i1 ≠ i2h2:i2 ≠ i3h3:i1 ≠ i3⊢ M.invFun i1 ≠ M.invFun i3 all_goals All goals completed! 🐙n:ℕS:(PureU1 n.succ.succ).LinSolshS:∀ (i1 i2 i3 : Fin n.succ.succ), i1 ≠ i2 → i2 ≠ i3 → i1 ≠ i3 → S.val i1 = S.val i2 ∨ S.val i1 = -S.val i2 ∨ 2 * S.val i3 + S.val i1 + S.val i2 = 0h:¬S.val (Fin.last n).castSucc = S.val (Fin.last (n + 1)) ∧ ¬S.val (Fin.last n).castSucc = -S.val (Fin.last (n + 1))h1:∀ (i : Fin n), S.val i.castSucc.castSucc = -(S.val (Fin.last n).castSucc + S.val (Fin.last n).succ) / 2h2:S.val (Fin.last (n + 1)) = -(∑ i, S.val i.castSucc.castSucc + S.val (Fin.last n).castSucc)⊢ (2 - ↑n) * S.val (Fin.last (n + 1)) = -(2 - ↑n) * S.val (Fin.last n).castSucc n:ℕS:(PureU1 n.succ.succ).LinSolshS:∀ (i1 i2 i3 : Fin n.succ.succ), i1 ≠ i2 → i2 ≠ i3 → i1 ≠ i3 → S.val i1 = S.val i2 ∨ S.val i1 = -S.val i2 ∨ 2 * S.val i3 + S.val i1 + S.val i2 = 0h:¬S.val (Fin.last n).castSucc = S.val (Fin.last (n + 1)) ∧ ¬S.val (Fin.last n).castSucc = -S.val (Fin.last (n + 1))h1:∀ (i : Fin n), S.val i.castSucc.castSucc = -(S.val (Fin.last n).castSucc + S.val (Fin.last n).succ) / 2h2:S.val (Fin.last (n + 1)) = -S.val (Fin.last n).castSucc + -(↑n * ((-S.val (Fin.last (n + 1)) + -S.val (Fin.last n).castSucc) / 2))⊢ (2 - ↑n) * S.val (Fin.last (n + 1)) = -(2 - ↑n) * S.val (Fin.last n).castSucc n:ℕS:(PureU1 n.succ.succ).LinSolshS:∀ (i1 i2 i3 : Fin n.succ.succ), i1 ≠ i2 → i2 ≠ i3 → i1 ≠ i3 → S.val i1 = S.val i2 ∨ S.val i1 = -S.val i2 ∨ 2 * S.val i3 + S.val i1 + S.val i2 = 0h:¬S.val (Fin.last n).castSucc = S.val (Fin.last (n + 1)) ∧ ¬S.val (Fin.last n).castSucc = -S.val (Fin.last (n + 1))h1:∀ (i : Fin n), S.val i.castSucc.castSucc = -(S.val (Fin.last n).castSucc + S.val (Fin.last n).succ) / 2h2:S.val (Fin.last (n + 1)) * 2 = -(S.val (Fin.last n).castSucc * 2) + -(↑n * (-S.val (Fin.last (n + 1)) + -S.val (Fin.last n).castSucc))⊢ (2 - ↑n) * S.val (Fin.last (n + 1)) = -(2 - ↑n) * S.val (Fin.last n).castSucc All goals completed! 🐙n:ℕS:(PureU1 n.succ.succ.succ.succ.succ).LinSolshS:LineInPlaneCond Sh:(2 - ↑(n + 3)) * S.val (Fin.last (n + 3 + 1)) = -(2 - ↑(n + 3)) * S.val (Fin.last (n + 3)).castSucchn:¬S.val (Fin.last (n + 2 + 1)).castSucc = S.val (Fin.last (n + 3 + 1)) ∧ ¬S.val (Fin.last (n + 2 + 1)).castSucc = -S.val (Fin.last (n + 3 + 1))hx:2 - ↑(n + 3) ≠ 0ht:S.val (Fin.last n.succ.succ.succ).succ = -S.val (Fin.last n.succ.succ.succ).castSucc⊢ False All goals completed! 🐙n:ℕS:(PureU1 n.succ.succ.succ.succ.succ).LinSolshS:LineInPlaneCond Shneq:(Fin.last n.succ.succ.succ).castSucc ≠ (Fin.last n.succ.succ.succ).succ⊢ ∀ (i j : Fin n.succ.succ.succ.succ.succ), i ≠ j → ConstAbsProp (S.val i, S.val j) n:ℕS:(PureU1 n.succ.succ.succ.succ.succ).LinSolshS:LineInPlaneCond Shneq:(Fin.last n.succ.succ.succ).castSucc ≠ (Fin.last n.succ.succ.succ).succ⊢ ∀ (f : (FamilyPermutations n.succ.succ.succ.succ.succ).group), ConstAbsProp ((((FamilyPermutations n.succ.succ.succ.succ.succ).linSolRep f) S).val (Fin.last n.succ.succ.succ).castSucc, (((FamilyPermutations n.succ.succ.succ.succ.succ).linSolRep f) S).val (Fin.last n.succ.succ.succ).succ) n:ℕS:(PureU1 n.succ.succ.succ.succ.succ).LinSolshS:LineInPlaneCond Shneq:(Fin.last n.succ.succ.succ).castSucc ≠ (Fin.last n.succ.succ.succ).succM:(FamilyPermutations n.succ.succ.succ.succ.succ).group⊢ ConstAbsProp ((((FamilyPermutations n.succ.succ.succ.succ.succ).linSolRep M) S).val (Fin.last n.succ.succ.succ).castSucc, (((FamilyPermutations n.succ.succ.succ.succ.succ).linSolRep M) S).val (Fin.last n.succ.succ.succ).succ) All goals completed! 🐙All goals completed! 🐙 n:ℕS:(PureU1 n.succ.succ.succ.succ.succ).LinSolshS:LineInPlaneCond Si:Fin (PureU1 n.succ.succ.succ.succ.succ).numberChargesj:Fin (PureU1 n.succ.succ.succ.succ.succ).numberChargeshij:i ≠ j⊢ S.val i ^ 2 = S.val j ^ 2 All goals completed! 🐙S:(PureU1 4).SolshS:LineInPlaneCond S.toLinSolshn:¬S.val 0 = S.val 1 ∧ ¬S.val 0 = -S.val 1hcube:S.val 0 ^ 3 + S.val 1 ^ 3 + S.val 2 ^ 3 + S.val 3 ^ 3 = 0l012:2 * S.val 2 + S.val 0 + S.val 1 = 0l013:2 * S.val 3 + S.val 0 + S.val 1 = 0diff_sq_mul_sum_eq_zero:(S.val 0 - S.val 1) ^ 2 * (S.val 0 + S.val 1) = 0⊢ False S:(PureU1 4).SolshS:LineInPlaneCond S.toLinSolshn:¬S.val 0 = S.val 1 ∧ ¬S.val 0 = -S.val 1hcube:S.val 0 ^ 3 + S.val 1 ^ 3 + S.val 2 ^ 3 + S.val 3 ^ 3 = 0l012:2 * S.val 2 + S.val 0 + S.val 1 = 0l013:2 * S.val 3 + S.val 0 + S.val 1 = 0diff_sq_mul_sum_eq_zero:(S.val 0 - S.val 1) ^ 2 * (S.val 0 + S.val 1) = 0h:(S.val 0 - S.val 1) ^ 2 = 0⊢ FalseS:(PureU1 4).SolshS:LineInPlaneCond S.toLinSolshn:¬S.val 0 = S.val 1 ∧ ¬S.val 0 = -S.val 1hcube:S.val 0 ^ 3 + S.val 1 ^ 3 + S.val 2 ^ 3 + S.val 3 ^ 3 = 0l012:2 * S.val 2 + S.val 0 + S.val 1 = 0l013:2 * S.val 3 + S.val 0 + S.val 1 = 0diff_sq_mul_sum_eq_zero:(S.val 0 - S.val 1) ^ 2 * (S.val 0 + S.val 1) = 0h:S.val 0 + S.val 1 = 0⊢ False S:(PureU1 4).SolshS:LineInPlaneCond S.toLinSolshn:¬S.val 0 = S.val 1 ∧ ¬S.val 0 = -S.val 1hcube:S.val 0 ^ 3 + S.val 1 ^ 3 + S.val 2 ^ 3 + S.val 3 ^ 3 = 0l012:2 * S.val 2 + S.val 0 + S.val 1 = 0l013:2 * S.val 3 + S.val 0 + S.val 1 = 0diff_sq_mul_sum_eq_zero:(S.val 0 - S.val 1) ^ 2 * (S.val 0 + S.val 1) = 0h:(S.val 0 - S.val 1) ^ 2 = 0⊢ False All goals completed! 🐙 S:(PureU1 4).SolshS:LineInPlaneCond S.toLinSolshn:¬S.val 0 = S.val 1 ∧ ¬S.val 0 = -S.val 1hcube:S.val 0 ^ 3 + S.val 1 ^ 3 + S.val 2 ^ 3 + S.val 3 ^ 3 = 0l012:2 * S.val 2 + S.val 0 + S.val 1 = 0l013:2 * S.val 3 + S.val 0 + S.val 1 = 0diff_sq_mul_sum_eq_zero:(S.val 0 - S.val 1) ^ 2 * (S.val 0 + S.val 1) = 0h:S.val 0 + S.val 1 = 0⊢ False exact hn.2 (S:(PureU1 4).SolshS:LineInPlaneCond S.toLinSolshn:¬S.val 0 = S.val 1 ∧ ¬S.val 0 = -S.val 1hcube:S.val 0 ^ 3 + S.val 1 ^ 3 + S.val 2 ^ 3 + S.val 3 ^ 3 = 0l012:2 * S.val 2 + S.val 0 + S.val 1 = 0l013:2 * S.val 3 + S.val 0 + S.val 1 = 0diff_sq_mul_sum_eq_zero:(S.val 0 - S.val 1) ^ 2 * (S.val 0 + S.val 1) = 0h:S.val 0 + S.val 1 = 0⊢ S.val 0 = -S.val 1 All goals completed! 🐙)lemma linesInPlane_eq_sq_four {S : (PureU1 4).Sols} (hS : LineInPlaneCond S.1.1) : ∀ (i j : Fin 4) (_ : i ≠ j), ConstAbsProp (S.val i, S.val j) := S:(PureU1 4).SolshS:LineInPlaneCond S.toLinSols⊢ ∀ (i j : Fin 4), i ≠ j → ConstAbsProp (S.val i, S.val j) S:(PureU1 4).SolshS:LineInPlaneCond S.toLinSols⊢ ∀ (f : (FamilyPermutations 4).group), ConstAbsProp ((((FamilyPermutations 4).linSolRep f) S.toLinSols).val 0, (((FamilyPermutations 4).linSolRep f) S.toLinSols).val 1) S:(PureU1 4).SolshS:LineInPlaneCond S.toLinSolsM:(FamilyPermutations 4).group⊢ ConstAbsProp ((((FamilyPermutations 4).linSolRep M) S.toLinSols).val 0, (((FamilyPermutations 4).linSolRep M) S.toLinSols).val 1) S:(PureU1 4).SolshS:LineInPlaneCond S.toLinSolsM:(FamilyPermutations 4).groupS':(PureU1 4).Sols := (MulAction.toFun (FamilyPermutations 4).group (PureU1 4).Sols) S M⊢ ConstAbsProp ((((FamilyPermutations 4).linSolRep M) S.toLinSols).val 0, (((FamilyPermutations 4).linSolRep M) S.toLinSols).val 1) All goals completed! 🐙All goals completed! 🐙 S:(PureU1 4).SolshS:LineInPlaneCond S.toLinSolsi:Fin (PureU1 4).numberChargesj:Fin (PureU1 4).numberChargeshij:i ≠ j⊢ S.val i ^ 2 = S.val j ^ 2 All goals completed! 🐙theorem linesInPlane_constAbs_AF (S : (PureU1 (n.succ.succ.succ.succ)).Sols) (hS : LineInPlaneCond S.1.1) : ConstAbs S.val := n:ℕS:(PureU1 n.succ.succ.succ.succ).SolshS:LineInPlaneCond S.toLinSols⊢ ConstAbs S.val n:ℕS:(PureU1 (Nat.succ 0).succ.succ.succ).SolshS:LineInPlaneCond S.toLinSols⊢ ConstAbs S.valn:ℕn✝:ℕa✝:∀ (S : (PureU1 n✝.succ.succ.succ.succ).Sols), LineInPlaneCond S.toLinSols → ConstAbs S.valS:(PureU1 (n✝ + 1).succ.succ.succ.succ).SolshS:LineInPlaneCond S.toLinSols⊢ ConstAbs S.val n:ℕS:(PureU1 (Nat.succ 0).succ.succ.succ).SolshS:LineInPlaneCond S.toLinSols⊢ ConstAbs S.val All goals completed! 🐙 n:ℕn✝:ℕa✝:∀ (S : (PureU1 n✝.succ.succ.succ.succ).Sols), LineInPlaneCond S.toLinSols → ConstAbs S.valS:(PureU1 (n✝ + 1).succ.succ.succ.succ).SolshS:LineInPlaneCond S.toLinSols⊢ ConstAbs S.val All goals completed! 🐙