1. Physlib
  2. QFT
  3. QED
  4. AnomalyCancellation
  5. Permutations
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.Basic public import Physlib.QFT.AnomalyCancellation.GroupActions

Permutations of Pure U(1) ACC

We define the permutation group action on the charges of the Pure U(1) ACC system. We further define the action on the ACC System.

@[expose] public section

The permutation group of the n-fermions.

@[simp] def PermGroup (n : ℕ) := Equiv.Perm (Fin n)

The type PermGroup n inherits the instance of a group from Equiv.Perm.

instance {n : ℕ} : Group (PermGroup n) := Equiv.Perm.permGroup

The image of an element of permGroup under the representation on charges.

@[simps!] def chargeMap {n : ℕ} (f : PermGroup n) : (PureU1 n).Charges →ₗ[ℚ] (PureU1 n).Charges where toFun S := S ∘ f.toFun map_add' _ _ := rfl map_smul' _ _:= rfl

The representation of permGroup acting on the vector space of charges.

@[simp] def permCharges {n : ℕ} : Representation ℚ (PermGroup n) (PureU1 n).Charges where toFun f := chargeMap f⁻¹ map_mul' f g := n:ℕf:PermGroup ng:PermGroup n⊢ chargeMap (f * g)⁻¹ = chargeMap f⁻¹ * chargeMap g⁻¹ All goals completed! 🐙 map_one' := n:ℕ⊢ chargeMap 1⁻¹ = 1 All goals completed! 🐙
lemma accGrav_invariant {n : ℕ} (f : (PermGroup n)) (S : (PureU1 n).Charges) : PureU1.accGrav n (permCharges f S) = accGrav n S := n:ℕf:PermGroup nS:(PureU1 n).Charges⊢ (accGrav n) ((permCharges f) S) = (accGrav n) S n:ℕf:PermGroup nS:(PureU1 n).Charges⊢ ∑ i, ({ toFun := fun f => chargeMap f⁻¹, map_one' := ⋯, map_mul' := ⋯ } f) S i = ∑ i, S i n:ℕf:PermGroup nS:(PureU1 n).Charges⊢ {a | f⁻¹ a ≠ a} ⊆ ↑univ All goals completed! 🐙n:ℕf:PermGroup nS:(PureU1 n).Charges⊢ ∑ i, (permCharges f) S i ^ 3 = ∑ i, S i ^ 3 n:ℕf:PermGroup nS:(PureU1 n).Charges⊢ ∑ i, ((fun a => a ^ 3) ∘ S) ((Equiv.symm f) i) = ∑ i, S i ^ 3 n:ℕf:PermGroup nS:(PureU1 n).Charges⊢ {a | (Equiv.symm f) a ≠ a} ⊆ ↑univ All goals completed! 🐙

The permutations acting on the ACC system.

@[simp] def FamilyPermutations (n : ℕ) : ACCSystemGroupAction (PureU1 n) where group := PermGroup n groupInst := inferInstance rep := permCharges linearInvariant := n:ℕ⊢ ∀ (i : Fin (PureU1 n).numberLinear) (g : PermGroup n) (S : (PureU1 n).Charges), ((PureU1 n).linearACCs i) ((permCharges g) S) = ((PureU1 n).linearACCs i) S n:ℕi:Fin (PureU1 n).numberLinear⊢ ∀ (g : PermGroup n) (S : (PureU1 n).Charges), ((PureU1 n).linearACCs i) ((permCharges g) S) = ((PureU1 n).linearACCs i) S match i with n:ℕi:Fin (PureU1 n).numberLinearisLt✝:0 < (PureU1 n).numberLinear⊢ ∀ (g : PermGroup n) (S : (PureU1 n).Charges), ((PureU1 n).linearACCs ⟨0, isLt✝⟩) ((permCharges g) S) = ((PureU1 n).linearACCs ⟨0, isLt✝⟩) S All goals completed! 🐙 quadInvariant := n:ℕ⊢ ∀ (i : Fin (PureU1 n).numberQuadratic) (g : PermGroup n) (S : (PureU1 n).Charges), ((PureU1 n).quadraticACCs i) ((permCharges g) S) = ((PureU1 n).quadraticACCs i) S n:ℕi:Fin (PureU1 n).numberQuadratic⊢ ∀ (g : PermGroup n) (S : (PureU1 n).Charges), ((PureU1 n).quadraticACCs i) ((permCharges g) S) = ((PureU1 n).quadraticACCs i) S n:ℕi✝:Fin (PureU1 n).numberQuadratici:Fin 0⊢ ∀ (g : PermGroup n) (S : (PureU1 n).Charges), ((PureU1 n).quadraticACCs i) ((permCharges g) S) = ((PureU1 n).quadraticACCs i) S All goals completed! 🐙 cubicInvariant := accCube_invariant
lemma FamilyPermutations_charges_apply (S : (PureU1 n).Charges) (i : Fin n) (f : (FamilyPermutations n).group) : ((FamilyPermutations n).rep f S) i = S (f.invFun i) := n:ℕS:(PureU1 n).Chargesi:Fin nf:(FamilyPermutations n).group⊢ ((FamilyPermutations n).rep f) S i = S (f.invFun i) All goals completed! 🐙lemma FamilyPermutations_anomalyFreeLinear_apply (S : (PureU1 n).LinSols) (i : Fin n) (f : (FamilyPermutations n).group) : ((FamilyPermutations n).linSolRep f S).val i = S.val (f.invFun i) := n:ℕS:(PureU1 n).LinSolsi:Fin nf:(FamilyPermutations n).group⊢ (((FamilyPermutations n).linSolRep f) S).val i = S.val (f.invFun i) All goals completed! 🐙

Given two distinct elements, an embedding of Fin 2 into Fin n.

def permTwoInj : Fin 2 ↪ Fin n where toFun s := match s with | 0 => i | 1 => j inj' s1 s2 := n:ℕi:Fin nj:Fin ni':Fin nj':Fin nhij:i ≠ jhij':i' ≠ j's1:Fin 2s2:Fin 2⊢ (fun s => match s with | 0 => i | 1 => j) s1 = (fun s => match s with | 0 => i | 1 => j) s2 → s1 = s2 All goals completed! 🐙
lemma permTwoInj_fst : i ∈ Set.range ⇑(permTwoInj hij) := n:ℕi:Fin nj:Fin nhij:i ≠ j⊢ i ∈ Set.range ⇑(permTwoInj hij) n:ℕi:Fin nj:Fin nhij:i ≠ j⊢ ∃ y, (permTwoInj hij) y = i n:ℕi:Fin nj:Fin nhij:i ≠ j⊢ (permTwoInj hij) 0 = i All goals completed! 🐙lemma permTwoInj_fst_apply : (Function.Embedding.toEquivRange (permTwoInj hij)).symm ⟨i, permTwoInj_fst hij⟩ = 0 := n:ℕi:Fin nj:Fin nhij:i ≠ j⊢ (permTwoInj hij).toEquivRange.symm ⟨i, ⋯⟩ = 0 All goals completed! 🐙lemma permTwoInj_snd : j ∈ Set.range ⇑(permTwoInj hij) := n:ℕi:Fin nj:Fin nhij:i ≠ j⊢ j ∈ Set.range ⇑(permTwoInj hij) n:ℕi:Fin nj:Fin nhij:i ≠ j⊢ ∃ y, (permTwoInj hij) y = j n:ℕi:Fin nj:Fin nhij:i ≠ j⊢ (permTwoInj hij) 1 = j All goals completed! 🐙lemma permTwoInj_snd_apply : (Function.Embedding.toEquivRange (permTwoInj hij)).symm ⟨j, permTwoInj_snd hij⟩ = 1 := n:ℕi:Fin nj:Fin nhij:i ≠ j⊢ (permTwoInj hij).toEquivRange.symm ⟨j, ⋯⟩ = 1 All goals completed! 🐙n:ℕi:Fin nj:Fin ni':Fin nj':Fin nhij:i ≠ jhij':i' ≠ j'⊢ ((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange).extendSubtype.toFun i' = i n:ℕi:Fin nj:Fin ni':Fin nj':Fin nhij:i ≠ jhij':i' ≠ j'ht:((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange).extendSubtype i' = ↑(((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange) ⟨i', ⋯⟩)⊢ ((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange).extendSubtype.toFun i' = i n:ℕi:Fin nj:Fin ni':Fin nj':Fin nhij:i ≠ jhij':i' ≠ j'ht:((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange).extendSubtype i' = (permTwoInj hij) ((permTwoInj hij').toEquivRange.symm ⟨i', ⋯⟩)⊢ ((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange).extendSubtype.toFun i' = i n:ℕi:Fin nj:Fin ni':Fin nj':Fin nhij:i ≠ jhij':i' ≠ j'ht:((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange).extendSubtype i' = (permTwoInj hij) ((permTwoInj hij').toEquivRange.symm ⟨i', ⋯⟩)⊢ (permTwoInj hij) 0 = i All goals completed! 🐙n:ℕi:Fin nj:Fin ni':Fin nj':Fin nhij:i ≠ jhij':i' ≠ j'⊢ ((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange).extendSubtype.toFun j' = j n:ℕi:Fin nj:Fin ni':Fin nj':Fin nhij:i ≠ jhij':i' ≠ j'ht:((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange).extendSubtype j' = ↑(((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange) ⟨j', ⋯⟩)⊢ ((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange).extendSubtype.toFun j' = j n:ℕi:Fin nj:Fin ni':Fin nj':Fin nhij:i ≠ jhij':i' ≠ j'ht:((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange).extendSubtype j' = (permTwoInj hij) ((permTwoInj hij').toEquivRange.symm ⟨j', ⋯⟩)⊢ ((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange).extendSubtype.toFun j' = j n:ℕi:Fin nj:Fin ni':Fin nj':Fin nhij:i ≠ jhij':i' ≠ j'ht:((permTwoInj hij').toEquivRange.symm.trans (permTwoInj hij).toEquivRange).extendSubtype j' = (permTwoInj hij) ((permTwoInj hij').toEquivRange.symm ⟨j', ⋯⟩)⊢ (permTwoInj hij) 1 = j All goals completed! 🐙

Given three distinct elements an embedding of Fin 3 into Fin n.

def permThreeInj : Fin 3 ↪ Fin n where toFun s := match s with | 0 => i | 1 => j | 2 => k inj' s1 s2 := n:ℕi:Fin nj:Fin nk:Fin ni':Fin nj':Fin nk':Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ khij':i' ≠ j'hjk':j' ≠ k'hik':i' ≠ k's1:Fin 3s2:Fin 3⊢ (fun s => match s with | 0 => i | 1 => j | 2 => k) s1 = (fun s => match s with | 0 => i | 1 => j | 2 => k) s2 → s1 = s2 All goals completed! 🐙
lemma permThreeInj_fst : i ∈ Set.range ⇑(permThreeInj hij hjk hik) := n:ℕi:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ k⊢ i ∈ Set.range ⇑(permThreeInj hij hjk hik) n:ℕi:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ k⊢ ∃ y, (permThreeInj hij hjk hik) y = i n:ℕi:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ k⊢ (permThreeInj hij hjk hik) 0 = i All goals completed! 🐙lemma permThreeInj_fst_apply : (Function.Embedding.toEquivRange (permThreeInj hij hjk hik)).symm ⟨i, permThreeInj_fst hij hjk hik⟩ = 0 := n:ℕi:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ k⊢ (permThreeInj hij hjk hik).toEquivRange.symm ⟨i, ⋯⟩ = 0 All goals completed! 🐙lemma permThreeInj_snd : j ∈ Set.range ⇑(permThreeInj hij hjk hik) := n:ℕi:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ k⊢ j ∈ Set.range ⇑(permThreeInj hij hjk hik) n:ℕi:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ k⊢ ∃ y, (permThreeInj hij hjk hik) y = j n:ℕi:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ k⊢ (permThreeInj hij hjk hik) 1 = j All goals completed! 🐙lemma permThreeInj_snd_apply : (Function.Embedding.toEquivRange (permThreeInj hij hjk hik)).symm ⟨j, permThreeInj_snd hij hjk hik⟩ = 1 := n:ℕi:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ k⊢ (permThreeInj hij hjk hik).toEquivRange.symm ⟨j, ⋯⟩ = 1 All goals completed! 🐙lemma permThreeInj_thd : k ∈ Set.range ⇑(permThreeInj hij hjk hik) := n:ℕi:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ k⊢ k ∈ Set.range ⇑(permThreeInj hij hjk hik) n:ℕi:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ k⊢ ∃ y, (permThreeInj hij hjk hik) y = k n:ℕi:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ k⊢ (permThreeInj hij hjk hik) 2 = k All goals completed! 🐙lemma permThreeInj_thd_apply : (Function.Embedding.toEquivRange (permThreeInj hij hjk hik)).symm ⟨k, permThreeInj_thd hij hjk hik⟩ = 2 := n:ℕi:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ k⊢ (permThreeInj hij hjk hik).toEquivRange.symm ⟨k, ⋯⟩ = 2 All goals completed! 🐙n:ℕi:Fin nj:Fin nk:Fin ni':Fin nj':Fin nk':Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ khij':i' ≠ j'hjk':j' ≠ k'hik':i' ≠ k'⊢ ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype.toFun i' = i n:ℕi:Fin nj:Fin nk:Fin ni':Fin nj':Fin nk':Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ khij':i' ≠ j'hjk':j' ≠ k'hik':i' ≠ k'ht:((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype i' = ↑(((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange) ⟨i', ⋯⟩)⊢ ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype.toFun i' = i n:ℕi:Fin nj:Fin nk:Fin ni':Fin nj':Fin nk':Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ khij':i' ≠ j'hjk':j' ≠ k'hik':i' ≠ k'ht:((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype i' = (permThreeInj hij hjk hik) ((permThreeInj hij' hjk' hik').toEquivRange.symm ⟨i', ⋯⟩)⊢ ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype.toFun i' = i n:ℕi:Fin nj:Fin nk:Fin ni':Fin nj':Fin nk':Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ khij':i' ≠ j'hjk':j' ≠ k'hik':i' ≠ k'ht:((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype i' = (permThreeInj hij hjk hik) ((permThreeInj hij' hjk' hik').toEquivRange.symm ⟨i', ⋯⟩)⊢ (permThreeInj hij hjk hik) 0 = i All goals completed! 🐙n:ℕi:Fin nj:Fin nk:Fin ni':Fin nj':Fin nk':Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ khij':i' ≠ j'hjk':j' ≠ k'hik':i' ≠ k'⊢ ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype.toFun j' = j n:ℕi:Fin nj:Fin nk:Fin ni':Fin nj':Fin nk':Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ khij':i' ≠ j'hjk':j' ≠ k'hik':i' ≠ k'ht:((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype j' = ↑(((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange) ⟨j', ⋯⟩)⊢ ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype.toFun j' = j n:ℕi:Fin nj:Fin nk:Fin ni':Fin nj':Fin nk':Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ khij':i' ≠ j'hjk':j' ≠ k'hik':i' ≠ k'ht:((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype j' = (permThreeInj hij hjk hik) ((permThreeInj hij' hjk' hik').toEquivRange.symm ⟨j', ⋯⟩)⊢ ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype.toFun j' = j n:ℕi:Fin nj:Fin nk:Fin ni':Fin nj':Fin nk':Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ khij':i' ≠ j'hjk':j' ≠ k'hik':i' ≠ k'ht:((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype j' = (permThreeInj hij hjk hik) ((permThreeInj hij' hjk' hik').toEquivRange.symm ⟨j', ⋯⟩)⊢ (permThreeInj hij hjk hik) 1 = j All goals completed! 🐙n:ℕi:Fin nj:Fin nk:Fin ni':Fin nj':Fin nk':Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ khij':i' ≠ j'hjk':j' ≠ k'hik':i' ≠ k'⊢ ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype.toFun k' = k n:ℕi:Fin nj:Fin nk:Fin ni':Fin nj':Fin nk':Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ khij':i' ≠ j'hjk':j' ≠ k'hik':i' ≠ k'ht:((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype k' = ↑(((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange) ⟨k', ⋯⟩)⊢ ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype.toFun k' = k n:ℕi:Fin nj:Fin nk:Fin ni':Fin nj':Fin nk':Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ khij':i' ≠ j'hjk':j' ≠ k'hik':i' ≠ k'ht:((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype k' = (permThreeInj hij hjk hik) ((permThreeInj hij' hjk' hik').toEquivRange.symm ⟨k', ⋯⟩)⊢ ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype.toFun k' = k n:ℕi:Fin nj:Fin nk:Fin ni':Fin nj':Fin nk':Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ khij':i' ≠ j'hjk':j' ≠ k'hik':i' ≠ k'ht:((permThreeInj hij' hjk' hik').toEquivRange.symm.trans (permThreeInj hij hjk hik).toEquivRange).extendSubtype k' = (permThreeInj hij hjk hik) ((permThreeInj hij' hjk' hik').toEquivRange.symm ⟨k', ⋯⟩)⊢ (permThreeInj hij hjk hik) 2 = k All goals completed! 🐙n:ℕP:ℚ × ℚ → PropS:(PureU1 n).LinSolsa:Fin nb:Fin nhab:a ≠ bh:∀ (f : (FamilyPermutations n).group), P ((((FamilyPermutations n).linSolRep f) S).val a, (((FamilyPermutations n).linSolRep f) S).val b)i:Fin nj:Fin nhij:i ≠ jh1:P (S.val ((Equiv.symm (permTwo hij hab)).invFun a), S.val ((Equiv.symm (permTwo hij hab)).invFun b))⊢ P (S.val i, S.val j) n:ℕP:ℚ × ℚ → PropS:(PureU1 n).LinSolsa:Fin nb:Fin nhab:a ≠ bh:∀ (f : (FamilyPermutations n).group), P ((((FamilyPermutations n).linSolRep f) S).val a, (((FamilyPermutations n).linSolRep f) S).val b)i:Fin nj:Fin nhij:i ≠ jh1:P (S.val ((permTwo hij hab) a), S.val ((permTwo hij hab) b))⊢ P (S.val i, S.val j) n:ℕP:ℚ × ℚ → PropS:(PureU1 n).LinSolsa:Fin nb:Fin nhab:a ≠ bh:∀ (f : (FamilyPermutations n).group), P ((((FamilyPermutations n).linSolRep f) S).val a, (((FamilyPermutations n).linSolRep f) S).val b)i:Fin nj:Fin nhij:i ≠ jh1:P (S.val ((permTwo hij hab).toFun a), S.val ((permTwo hij hab).toFun b))⊢ P (S.val i, S.val j) erw [n:ℕP:ℚ × ℚ → PropS:(PureU1 n).LinSolsa:Fin nb:Fin nhab:a ≠ bh:∀ (f : (FamilyPermutations n).group), P ((((FamilyPermutations n).linSolRep f) S).val a, (((FamilyPermutations n).linSolRep f) S).val b)i:Fin nj:Fin nhij:i ≠ jh1:P (S.val i, S.val ((permTwo hij hab).toFun b))⊢ P (S.val i, S.val j)n:ℕP:ℚ × ℚ → PropS:(PureU1 n).LinSolsa:Fin nb:Fin nhab:a ≠ bh:∀ (f : (FamilyPermutations n).group), P ((((FamilyPermutations n).linSolRep f) S).val a, (((FamilyPermutations n).linSolRep f) S).val b)i:Fin nj:Fin nhij:i ≠ jh1:P (S.val i, S.val j)⊢ P (S.val i, S.val j)n:ℕP:ℚ × ℚ → PropS:(PureU1 n).LinSolsa:Fin nb:Fin nhab:a ≠ bh:∀ (f : (FamilyPermutations n).group), P ((((FamilyPermutations n).linSolRep f) S).val a, (((FamilyPermutations n).linSolRep f) S).val b)i:Fin nj:Fin nhij:i ≠ jh1:P (S.val i, S.val j)⊢ P (S.val i, S.val j) at h1 All goals completed! 🐙n:ℕP:ℚ × ℚ × ℚ → PropS:(PureU1 n).LinSolsa:Fin nb:Fin nc:Fin nhab:a ≠ bhac:a ≠ chbc:b ≠ ch:∀ (f : (FamilyPermutations n).group), P ((((FamilyPermutations n).linSolRep f) S).val a, (((FamilyPermutations n).linSolRep f) S).val b, (((FamilyPermutations n).linSolRep f) S).val c)i:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ kh1:P (S.val ((Equiv.symm (permThree hij hjk hik hab hbc hac)).invFun a), S.val ((Equiv.symm (permThree hij hjk hik hab hbc hac)).invFun b), S.val ((Equiv.symm (permThree hij hjk hik hab hbc hac)).invFun c))⊢ P (S.val i, S.val j, S.val k) n:ℕP:ℚ × ℚ × ℚ → PropS:(PureU1 n).LinSolsa:Fin nb:Fin nc:Fin nhab:a ≠ bhac:a ≠ chbc:b ≠ ch:∀ (f : (FamilyPermutations n).group), P ((((FamilyPermutations n).linSolRep f) S).val a, (((FamilyPermutations n).linSolRep f) S).val b, (((FamilyPermutations n).linSolRep f) S).val c)i:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ kh1:P (S.val ((permThree hij hjk hik hab hbc hac) a), S.val ((permThree hij hjk hik hab hbc hac) b), S.val ((permThree hij hjk hik hab hbc hac) c))⊢ P (S.val i, S.val j, S.val k) n:ℕP:ℚ × ℚ × ℚ → PropS:(PureU1 n).LinSolsa:Fin nb:Fin nc:Fin nhab:a ≠ bhac:a ≠ chbc:b ≠ ch:∀ (f : (FamilyPermutations n).group), P ((((FamilyPermutations n).linSolRep f) S).val a, (((FamilyPermutations n).linSolRep f) S).val b, (((FamilyPermutations n).linSolRep f) S).val c)i:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ kh1:P (S.val ((permThree hij hjk hik hab hbc hac).toFun a), S.val ((permThree hij hjk hik hab hbc hac).toFun b), S.val ((permThree hij hjk hik hab hbc hac).toFun c))⊢ P (S.val i, S.val j, S.val k) erw [n:ℕP:ℚ × ℚ × ℚ → PropS:(PureU1 n).LinSolsa:Fin nb:Fin nc:Fin nhab:a ≠ bhac:a ≠ chbc:b ≠ ch:∀ (f : (FamilyPermutations n).group), P ((((FamilyPermutations n).linSolRep f) S).val a, (((FamilyPermutations n).linSolRep f) S).val b, (((FamilyPermutations n).linSolRep f) S).val c)i:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ kh1:P (S.val i, S.val ((permThree hij hjk hik hab hbc hac).toFun b), S.val ((permThree hij hjk hik hab hbc hac).toFun c))⊢ P (S.val i, S.val j, S.val k)n:ℕP:ℚ × ℚ × ℚ → PropS:(PureU1 n).LinSolsa:Fin nb:Fin nc:Fin nhab:a ≠ bhac:a ≠ chbc:b ≠ ch:∀ (f : (FamilyPermutations n).group), P ((((FamilyPermutations n).linSolRep f) S).val a, (((FamilyPermutations n).linSolRep f) S).val b, (((FamilyPermutations n).linSolRep f) S).val c)i:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ kh1:P (S.val i, S.val j, S.val ((permThree hij hjk hik hab hbc hac).toFun c))⊢ P (S.val i, S.val j, S.val k) n:ℕP:ℚ × ℚ × ℚ → PropS:(PureU1 n).LinSolsa:Fin nb:Fin nc:Fin nhab:a ≠ bhac:a ≠ chbc:b ≠ ch:∀ (f : (FamilyPermutations n).group), P ((((FamilyPermutations n).linSolRep f) S).val a, (((FamilyPermutations n).linSolRep f) S).val b, (((FamilyPermutations n).linSolRep f) S).val c)i:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ kh1:P (S.val i, S.val j, S.val k)⊢ P (S.val i, S.val j, S.val k)n:ℕP:ℚ × ℚ × ℚ → PropS:(PureU1 n).LinSolsa:Fin nb:Fin nc:Fin nhab:a ≠ bhac:a ≠ chbc:b ≠ ch:∀ (f : (FamilyPermutations n).group), P ((((FamilyPermutations n).linSolRep f) S).val a, (((FamilyPermutations n).linSolRep f) S).val b, (((FamilyPermutations n).linSolRep f) S).val c)i:Fin nj:Fin nk:Fin nhij:i ≠ jhjk:j ≠ khik:i ≠ kh1:P (S.val i, S.val j, S.val k)⊢ P (S.val i, S.val j, S.val k) at h1 All goals completed! 🐙