Imports
/- Copyright (c) 2025 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.PerturbationTheory.FieldOpFreeAlgebra.Grading public import Physlib.QFT.PerturbationTheory.FieldStatistics.ExchangeSign

Super Commute

@[expose] public section

The super commutator on the FieldOpFreeAlgebra.

@[inherit_doc superCommuteF] scoped[FieldSpecification.FieldOpFreeAlgebra] notation "[" φs "," φs' "]ₛF" => superCommuteF φs φs'

The super commutator of different types of elements

lemma superCommuteF_ofCrAnListF_ofCrAnListF (φs φs' : List 𝓕.CrAnFieldOp) : [ofCrAnListF φs, ofCrAnListF φs']ₛF = ofCrAnListF (φs ++ φs') - 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') ofCrAnListF (φs' ++ φs) := 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp(superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') = ofCrAnListF (φs ++ φs') - (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics φs') ofCrAnListF (φs' ++ φs) All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOpofCrAnListF [φ] * ofCrAnListF [φ'] - (exchangeSign (ofList 𝓕.crAnStatistics [φ])) (ofList 𝓕.crAnStatistics [φ']) (ofCrAnListF [φ'] * ofCrAnListF [φ]) = ofCrAnListF [φ] * ofCrAnListF [φ'] - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics φ') ofCrAnListF [φ'] * ofCrAnListF [φ] All goals completed! 🐙𝓕:FieldSpecificationφcas:List 𝓕.CrAnFieldOpφs:List 𝓕.FieldOpofCrAnListF φcas * ofFieldOpListF φs - (exchangeSign (ofList 𝓕.crAnStatistics φcas)) (ofList 𝓕.fieldOpStatistic φs) (ofFieldOpListF φs * ofCrAnListF φcas) = ofCrAnListF φcas * ofFieldOpListF φs - (exchangeSign (ofList 𝓕.crAnStatistics φcas)) (ofList 𝓕.fieldOpStatistic φs) ofFieldOpListF φs * ofCrAnListF φcas All goals completed! 🐙All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpofFieldOpF φ * ofFieldOpListF φs - (exchangeSign (ofList 𝓕.fieldOpStatistic [φ])) (ofList 𝓕.fieldOpStatistic φs) ofFieldOpListF φs * ofFieldOpF φ = ofFieldOpF φ * ofFieldOpListF φs - (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) ofFieldOpListF φs * ofFieldOpF φ All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpofFieldOpListF φs * ofFieldOpF φ - (exchangeSign (ofList 𝓕.fieldOpStatistic φs)) (ofList 𝓕.fieldOpStatistic [φ]) ofFieldOpF φ * ofFieldOpListF φs = ofFieldOpListF φs * ofFieldOpF φ - (exchangeSign (ofList 𝓕.fieldOpStatistic φs)) (𝓕|>ₛφ) ofFieldOpF φ * ofFieldOpListF φs All goals completed! 🐙lemma superCommuteF_anPartF_crPartF (φ φ' : 𝓕.FieldOp) : [anPartF φ, crPartF φ']ₛF = anPartF φ * crPartF φ' - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') crPartF φ' * anPartF φ := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp(superCommuteF (anPartF φ)) (crPartF φ') = anPartF φ * crPartF φ' - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') crPartF φ' * anPartF φ match φ, φ' with 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumx✝:𝓕.FieldOp(superCommuteF (anPartF (FieldOp.inAsymp φ))) (crPartF x✝) = anPartF (FieldOp.inAsymp φ) * crPartF x✝ - (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (𝓕|>ₛx✝) crPartF x✝ * anPartF (FieldOp.inAsymp φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':𝓕.FieldOpx✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (anPartF x✝)) (crPartF (FieldOp.outAsymp φ)) = anPartF x✝ * crPartF (FieldOp.outAsymp φ) - (exchangeSign (𝓕|>ₛx✝)) (𝓕|>ₛFieldOp.outAsymp φ) crPartF (FieldOp.outAsymp φ) * anPartF x✝ All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφ':((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime(superCommuteF (anPartF (FieldOp.position φ))) (crPartF (FieldOp.position φ')) = anPartF (FieldOp.position φ) * crPartF (FieldOp.position φ') - (exchangeSign (𝓕|>ₛFieldOp.position φ)) (𝓕|>ₛFieldOp.position φ') crPartF (FieldOp.position φ') * anPartF (FieldOp.position φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφ':((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime(superCommuteF (anPartF (FieldOp.outAsymp φ))) (crPartF (FieldOp.position φ')) = anPartF (FieldOp.outAsymp φ) * crPartF (FieldOp.position φ') - (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛFieldOp.position φ') crPartF (FieldOp.position φ') * anPartF (FieldOp.outAsymp φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφ':((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (anPartF (FieldOp.position φ))) (crPartF (FieldOp.inAsymp φ')) = anPartF (FieldOp.position φ) * crPartF (FieldOp.inAsymp φ') - (exchangeSign (𝓕|>ₛFieldOp.position φ)) (𝓕|>ₛFieldOp.inAsymp φ') crPartF (FieldOp.inAsymp φ') * anPartF (FieldOp.position φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφ':((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (anPartF (FieldOp.outAsymp φ))) (crPartF (FieldOp.inAsymp φ')) = anPartF (FieldOp.outAsymp φ) * crPartF (FieldOp.inAsymp φ') - (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛFieldOp.inAsymp φ') crPartF (FieldOp.inAsymp φ') * anPartF (FieldOp.outAsymp φ) All goals completed! 🐙lemma superCommuteF_crPartF_anPartF (φ φ' : 𝓕.FieldOp) : [crPartF φ, anPartF φ']ₛF = crPartF φ * anPartF φ' - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') anPartF φ' * crPartF φ := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp(superCommuteF (crPartF φ)) (anPartF φ') = crPartF φ * anPartF φ' - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') anPartF φ' * crPartF φ match φ, φ' with 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumx✝:𝓕.FieldOp(superCommuteF (crPartF (FieldOp.outAsymp φ))) (anPartF x✝) = crPartF (FieldOp.outAsymp φ) * anPartF x✝ - (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛx✝) anPartF x✝ * crPartF (FieldOp.outAsymp φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':𝓕.FieldOpx✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (crPartF x✝)) (anPartF (FieldOp.inAsymp φ)) = crPartF x✝ * anPartF (FieldOp.inAsymp φ) - (exchangeSign (𝓕|>ₛx✝)) (𝓕|>ₛFieldOp.inAsymp φ) anPartF (FieldOp.inAsymp φ) * crPartF x✝ All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφ':((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime(superCommuteF (crPartF (FieldOp.position φ))) (anPartF (FieldOp.position φ')) = crPartF (FieldOp.position φ) * anPartF (FieldOp.position φ') - (exchangeSign (𝓕|>ₛFieldOp.position φ)) (𝓕|>ₛFieldOp.position φ') anPartF (FieldOp.position φ') * crPartF (FieldOp.position φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφ':((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (crPartF (FieldOp.position φ))) (anPartF (FieldOp.outAsymp φ')) = crPartF (FieldOp.position φ) * anPartF (FieldOp.outAsymp φ') - (exchangeSign (𝓕|>ₛFieldOp.position φ)) (𝓕|>ₛFieldOp.outAsymp φ') anPartF (FieldOp.outAsymp φ') * crPartF (FieldOp.position φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφ':((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime(superCommuteF (crPartF (FieldOp.inAsymp φ))) (anPartF (FieldOp.position φ')) = crPartF (FieldOp.inAsymp φ) * anPartF (FieldOp.position φ') - (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (𝓕|>ₛFieldOp.position φ') anPartF (FieldOp.position φ') * crPartF (FieldOp.inAsymp φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφ':((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (crPartF (FieldOp.inAsymp φ))) (anPartF (FieldOp.outAsymp φ')) = crPartF (FieldOp.inAsymp φ) * anPartF (FieldOp.outAsymp φ') - (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (𝓕|>ₛFieldOp.outAsymp φ') anPartF (FieldOp.outAsymp φ') * crPartF (FieldOp.inAsymp φ) All goals completed! 🐙lemma superCommuteF_crPartF_crPartF (φ φ' : 𝓕.FieldOp) : [crPartF φ, crPartF φ']ₛF = crPartF φ * crPartF φ' - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') crPartF φ' * crPartF φ := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp(superCommuteF (crPartF φ)) (crPartF φ') = crPartF φ * crPartF φ' - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') crPartF φ' * crPartF φ match φ, φ' with 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumx✝:𝓕.FieldOp(superCommuteF (crPartF (FieldOp.outAsymp φ))) (crPartF x✝) = crPartF (FieldOp.outAsymp φ) * crPartF x✝ - (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛx✝) crPartF x✝ * crPartF (FieldOp.outAsymp φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':𝓕.FieldOpx✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (crPartF x✝)) (crPartF (FieldOp.outAsymp φ)) = crPartF x✝ * crPartF (FieldOp.outAsymp φ) - (exchangeSign (𝓕|>ₛx✝)) (𝓕|>ₛFieldOp.outAsymp φ) crPartF (FieldOp.outAsymp φ) * crPartF x✝ All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφ':((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime(superCommuteF (crPartF (FieldOp.position φ))) (crPartF (FieldOp.position φ')) = crPartF (FieldOp.position φ) * crPartF (FieldOp.position φ') - (exchangeSign (𝓕|>ₛFieldOp.position φ)) (𝓕|>ₛFieldOp.position φ') crPartF (FieldOp.position φ') * crPartF (FieldOp.position φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφ':((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (crPartF (FieldOp.position φ))) (crPartF (FieldOp.inAsymp φ')) = crPartF (FieldOp.position φ) * crPartF (FieldOp.inAsymp φ') - (exchangeSign (𝓕|>ₛFieldOp.position φ)) (𝓕|>ₛFieldOp.inAsymp φ') crPartF (FieldOp.inAsymp φ') * crPartF (FieldOp.position φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφ':((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime(superCommuteF (crPartF (FieldOp.inAsymp φ))) (crPartF (FieldOp.position φ')) = crPartF (FieldOp.inAsymp φ) * crPartF (FieldOp.position φ') - (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (𝓕|>ₛFieldOp.position φ') crPartF (FieldOp.position φ') * crPartF (FieldOp.inAsymp φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφ':((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (crPartF (FieldOp.inAsymp φ))) (crPartF (FieldOp.inAsymp φ')) = crPartF (FieldOp.inAsymp φ) * crPartF (FieldOp.inAsymp φ') - (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (𝓕|>ₛFieldOp.inAsymp φ') crPartF (FieldOp.inAsymp φ') * crPartF (FieldOp.inAsymp φ) All goals completed! 🐙lemma superCommuteF_anPartF_anPartF (φ φ' : 𝓕.FieldOp) : [anPartF φ, anPartF φ']ₛF = anPartF φ * anPartF φ' - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') anPartF φ' * anPartF φ := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp(superCommuteF (anPartF φ)) (anPartF φ') = anPartF φ * anPartF φ' - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') anPartF φ' * anPartF φ match φ, φ' with 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumx✝:𝓕.FieldOp(superCommuteF (anPartF (FieldOp.inAsymp φ))) (anPartF x✝) = anPartF (FieldOp.inAsymp φ) * anPartF x✝ - (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (𝓕|>ₛx✝) anPartF x✝ * anPartF (FieldOp.inAsymp φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':𝓕.FieldOpx✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (anPartF x✝)) (anPartF (FieldOp.inAsymp φ)) = anPartF x✝ * anPartF (FieldOp.inAsymp φ) - (exchangeSign (𝓕|>ₛx✝)) (𝓕|>ₛFieldOp.inAsymp φ) anPartF (FieldOp.inAsymp φ) * anPartF x✝ All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφ':((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime(superCommuteF (anPartF (FieldOp.position φ))) (anPartF (FieldOp.position φ')) = anPartF (FieldOp.position φ) * anPartF (FieldOp.position φ') - (exchangeSign (𝓕|>ₛFieldOp.position φ)) (𝓕|>ₛFieldOp.position φ') anPartF (FieldOp.position φ') * anPartF (FieldOp.position φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeφ':((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (anPartF (FieldOp.position φ))) (anPartF (FieldOp.outAsymp φ')) = anPartF (FieldOp.position φ) * anPartF (FieldOp.outAsymp φ') - (exchangeSign (𝓕|>ₛFieldOp.position φ)) (𝓕|>ₛFieldOp.outAsymp φ') anPartF (FieldOp.outAsymp φ') * anPartF (FieldOp.position φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφ':((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime(superCommuteF (anPartF (FieldOp.outAsymp φ))) (anPartF (FieldOp.position φ')) = anPartF (FieldOp.outAsymp φ) * anPartF (FieldOp.position φ') - (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛFieldOp.position φ') anPartF (FieldOp.position φ') * anPartF (FieldOp.outAsymp φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ'✝:𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumφ':((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (anPartF (FieldOp.outAsymp φ))) (anPartF (FieldOp.outAsymp φ')) = anPartF (FieldOp.outAsymp φ) * anPartF (FieldOp.outAsymp φ') - (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛFieldOp.outAsymp φ') anPartF (FieldOp.outAsymp φ') * anPartF (FieldOp.outAsymp φ) All goals completed! 🐙lemma superCommuteF_crPartF_ofFieldOpListF (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : [crPartF φ, ofFieldOpListF φs]ₛF = crPartF φ * ofFieldOpListF φs - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) ofFieldOpListF φs * crPartF φ := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp(superCommuteF (crPartF φ)) (ofFieldOpListF φs) = crPartF φ * ofFieldOpListF φs - (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) ofFieldOpListF φs * crPartF φ match φ with 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (crPartF (FieldOp.inAsymp φ))) (ofFieldOpListF φs) = crPartF (FieldOp.inAsymp φ) * ofFieldOpListF φs - (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (ofList 𝓕.fieldOpStatistic φs) ofFieldOpListF φs * crPartF (FieldOp.inAsymp φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime(superCommuteF (crPartF (FieldOp.position φ))) (ofFieldOpListF φs) = crPartF (FieldOp.position φ) * ofFieldOpListF φs - (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic φs) ofFieldOpListF φs * crPartF (FieldOp.position φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (crPartF (FieldOp.outAsymp φ))) (ofFieldOpListF φs) = crPartF (FieldOp.outAsymp φ) * ofFieldOpListF φs - (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic φs) ofFieldOpListF φs * crPartF (FieldOp.outAsymp φ) All goals completed! 🐙lemma superCommuteF_anPartF_ofFieldOpListF (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : [anPartF φ, ofFieldOpListF φs]ₛF = anPartF φ * ofFieldOpListF φs - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) ofFieldOpListF φs * anPartF φ := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp(superCommuteF (anPartF φ)) (ofFieldOpListF φs) = anPartF φ * ofFieldOpListF φs - (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) ofFieldOpListF φs * anPartF φ match φ with 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (anPartF (FieldOp.inAsymp φ))) (ofFieldOpListF φs) = anPartF (FieldOp.inAsymp φ) * ofFieldOpListF φs - (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (ofList 𝓕.fieldOpStatistic φs) ofFieldOpListF φs * anPartF (FieldOp.inAsymp φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime(superCommuteF (anPartF (FieldOp.position φ))) (ofFieldOpListF φs) = anPartF (FieldOp.position φ) * ofFieldOpListF φs - (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic φs) ofFieldOpListF φs * anPartF (FieldOp.position φ) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum(superCommuteF (anPartF (FieldOp.outAsymp φ))) (ofFieldOpListF φs) = anPartF (FieldOp.outAsymp φ) * ofFieldOpListF φs - (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic φs) ofFieldOpListF φs * anPartF (FieldOp.outAsymp φ) All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpcrPartF φ * ofFieldOpListF [φ'] - (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic [φ']) ofFieldOpListF [φ'] * crPartF φ = crPartF φ * ofFieldOpListF [φ'] - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') ofFieldOpListF [φ'] * crPartF φ All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpanPartF φ * ofFieldOpListF [φ'] - (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic [φ']) ofFieldOpListF [φ'] * anPartF φ = anPartF φ * ofFieldOpListF [φ'] - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') ofFieldOpListF [φ'] * anPartF φ All goals completed! 🐙

Mul equal superCommuteF

Lemmas which rewrite a multiplication of two elements of the algebra as their commuted multiplication with a sign plus the super commutator.

𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpofCrAnListF φs * ofCrAnListF φs' = (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics φs') ofCrAnListF φs' * ofCrAnListF φs + (ofCrAnListF (φs ++ φs') - (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics φs') ofCrAnListF (φs' ++ φs)) All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp(exchangeSign (ofList 𝓕.crAnStatistics [φ])) (ofList 𝓕.crAnStatistics φs') ofCrAnListF φs' * ofCrAnListF [φ] + (superCommuteF (ofCrAnListF [φ])) (ofCrAnListF φs') = (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics φs') ofCrAnListF φs' * ofCrAnListF [φ] + (superCommuteF (ofCrAnListF [φ])) (ofCrAnListF φs') All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOpofFieldOpListF φs * ofFieldOpListF φs' = (exchangeSign (ofList 𝓕.fieldOpStatistic φs)) (ofList 𝓕.fieldOpStatistic φs') ofFieldOpListF φs' * ofFieldOpListF φs + (ofFieldOpListF φs * ofFieldOpListF φs' - (exchangeSign (ofList 𝓕.fieldOpStatistic φs)) (ofList 𝓕.fieldOpStatistic φs') ofFieldOpListF φs' * ofFieldOpListF φs) All goals completed! 🐙lemma ofFieldOpF_mul_ofFieldOpListF_eq_superCommuteF (φ : 𝓕.FieldOp) (φs' : List 𝓕.FieldOp) : ofFieldOpF φ * ofFieldOpListF φs' = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') ofFieldOpListF φs' * ofFieldOpF φ + [ofFieldOpF φ, ofFieldOpListF φs']ₛF := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOpofFieldOpF φ * ofFieldOpListF φs' = (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') ofFieldOpListF φs' * ofFieldOpF φ + (superCommuteF (ofFieldOpF φ)) (ofFieldOpListF φs') All goals completed! 🐙lemma ofFieldOpListF_mul_ofFieldOpF_eq_superCommuteF (φs : List 𝓕.FieldOp) (φ : 𝓕.FieldOp) : ofFieldOpListF φs * ofFieldOpF φ = 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φ) ofFieldOpF φ * ofFieldOpListF φs + [ofFieldOpListF φs, ofFieldOpF φ]ₛF := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφ:𝓕.FieldOpofFieldOpListF φs * ofFieldOpF φ = (exchangeSign (ofList 𝓕.fieldOpStatistic φs)) (𝓕|>ₛφ) ofFieldOpF φ * ofFieldOpListF φs + (superCommuteF (ofFieldOpListF φs)) (ofFieldOpF φ) All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpcrPartF φ * anPartF φ' = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') anPartF φ' * crPartF φ + (crPartF φ * anPartF φ' - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') anPartF φ' * crPartF φ) All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpanPartF φ * crPartF φ' = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') crPartF φ' * anPartF φ + (anPartF φ * crPartF φ' - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') crPartF φ' * anPartF φ) All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpcrPartF φ * crPartF φ' = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') crPartF φ' * crPartF φ + (crPartF φ * crPartF φ' - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') crPartF φ' * crPartF φ) All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpanPartF φ * anPartF φ' = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') anPartF φ' * anPartF φ + (anPartF φ * anPartF φ' - (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') anPartF φ' * anPartF φ) All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.FieldOpofCrAnListF φs * ofFieldOpListF φs' = (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic φs') ofFieldOpListF φs' * ofCrAnListF φs + (ofCrAnListF φs * ofFieldOpListF φs' - (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic φs') ofFieldOpListF φs' * ofCrAnListF φs) All goals completed! 🐙

Symmetry of the super commutator.

𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpofCrAnListF (φs ++ φs') - (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics φs') ofCrAnListF (φs' ++ φs) = -((exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics φs') ofCrAnListF (φs' ++ φs)) + ((exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics φs') * (exchangeSign (ofList 𝓕.crAnStatistics φs')) (ofList 𝓕.crAnStatistics φs)) ofCrAnListF (φs ++ φs') conv_rhs => 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp| ((exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics φs') * (exchangeSign (ofList 𝓕.crAnStatistics φs')) (ofList 𝓕.crAnStatistics φs)) ofCrAnListF (φs ++ φs') 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp| 1 ofCrAnListF (φs ++ φs') 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpofCrAnListF (φs ++ φs') - (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics φs') ofCrAnListF (φs' ++ φs) = -((exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics φs') ofCrAnListF (φs' ++ φs)) + ofCrAnListF (φs ++ φs') All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOpofCrAnOpF φ * ofCrAnOpF φ' - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics φ') (ofCrAnOpF φ' * ofCrAnOpF φ) = -((exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics φ') (ofCrAnOpF φ' * ofCrAnOpF φ)) + ((exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics φ') * (exchangeSign (𝓕.crAnStatistics φ')) (𝓕.crAnStatistics φ)) (ofCrAnOpF φ * ofCrAnOpF φ') conv_rhs => 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOp| ((exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics φ') * (exchangeSign (𝓕.crAnStatistics φ')) (𝓕.crAnStatistics φ)) (ofCrAnOpF φ * ofCrAnOpF φ') 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOp| 1 (ofCrAnOpF φ * ofCrAnOpF φ') 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOpofCrAnOpF φ * ofCrAnOpF φ' - (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics φ') (ofCrAnOpF φ' * ofCrAnOpF φ) = -((exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics φ') (ofCrAnOpF φ' * ofCrAnOpF φ)) + ofCrAnOpF φ * ofCrAnOpF φ' All goals completed! 🐙

Splitting the super commutator on lists into sums.

𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp(exchangeSign (ofList 𝓕.crAnStatistics φs)) (𝓕.crAnStatistics φ * ofList 𝓕.crAnStatistics φs') ofCrAnListF (φ :: (φs' ++ φs)) = ((exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics φs') * (exchangeSign (ofList 𝓕.crAnStatistics φs)) (𝓕.crAnStatistics φ)) ofCrAnListF (φ :: (φs' ++ φs)) All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.FieldOp(exchangeSign (ofList 𝓕.crAnStatistics φs)) ((𝓕|>ₛφ) * ofList 𝓕.fieldOpStatistic φs') (ofFieldOpF φ * (ofFieldOpListF φs' * ofCrAnListF φs)) = ((exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic φs') * (exchangeSign (ofList 𝓕.crAnStatistics φs)) (𝓕|>ₛφ)) (ofFieldOpF φ * (ofFieldOpListF φs' * ofCrAnListF φs)) All goals completed! 🐙

For a field specification 𝓕, and two lists φs = φ₀…φₙ and φs' of 𝓕.CrAnFieldOp the following super commutation relation holds:

[φs', φ₀…φₙ]ₛF = ∑ i, 𝓢(φs', φ₀…φᵢ₋₁) • φ₀…φᵢ₋₁ * [φs', φᵢ]ₛF * φᵢ₊₁ … φₙ

The proof of this relation is via induction on the length of φs.

𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφ:𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp(superCommuteF (ofCrAnListF φs)) (ofCrAnOpF φ) * ofCrAnListF φs' + (exchangeSign (ofList 𝓕.crAnStatistics φs)) (𝓕.crAnStatistics φ) ofCrAnOpF φ * n, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs')) ofCrAnListF (List.take (↑n) φs') * (superCommuteF (ofCrAnListF φs)) (ofCrAnOpF (φs'.get n)) * ofCrAnListF (List.drop (n + 1) φs') = n, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics (List.take (↑n) (φ :: φs'))) ofCrAnListF (List.take (↑n) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofCrAnOpF ((φ :: φs').get n)) * ofCrAnListF (List.drop (n + 1) (φ :: φs')) conv_rhs => 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφ:𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp| (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics (List.take (↑0) (φ :: φs'))) ofCrAnListF (List.take (↑0) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofCrAnOpF ((φ :: φs').get 0)) * ofCrAnListF (List.drop (0 + 1) (φ :: φs')) + i, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics (List.take (↑i.succ) (φ :: φs'))) ofCrAnListF (List.take (↑i.succ) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofCrAnOpF ((φ :: φs').get i.succ)) * ofCrAnListF (List.drop (i.succ + 1) (φ :: φs')) 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφ:𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp(superCommuteF (ofCrAnListF φs)) (ofCrAnOpF φ) * ofCrAnListF φs' = (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics (List.take (↑0) (φ :: φs'))) ofCrAnListF (List.take (↑0) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofCrAnOpF ((φ :: φs').get 0)) * ofCrAnListF (List.drop (0 + 1) (φ :: φs'))𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφ:𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp(exchangeSign (ofList 𝓕.crAnStatistics φs)) (𝓕.crAnStatistics φ) ofCrAnOpF φ * n, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs')) ofCrAnListF (List.take (↑n) φs') * (superCommuteF (ofCrAnListF φs)) (ofCrAnOpF (φs'.get n)) * ofCrAnListF (List.drop (n + 1) φs') = i, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics (List.take (↑i.succ) (φ :: φs'))) ofCrAnListF (List.take (↑i.succ) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofCrAnOpF ((φ :: φs').get i.succ)) * ofCrAnListF (List.drop (i.succ + 1) (φ :: φs')) 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφ:𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp(superCommuteF (ofCrAnListF φs)) (ofCrAnOpF φ) * ofCrAnListF φs' = (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics (List.take (↑0) (φ :: φs'))) ofCrAnListF (List.take (↑0) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofCrAnOpF ((φ :: φs').get 0)) * ofCrAnListF (List.drop (0 + 1) (φ :: φs')) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφ:𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp(exchangeSign (ofList 𝓕.crAnStatistics φs)) (𝓕.crAnStatistics φ) ofCrAnOpF φ * n, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs')) ofCrAnListF (List.take (↑n) φs') * (superCommuteF (ofCrAnListF φs)) (ofCrAnOpF (φs'.get n)) * ofCrAnListF (List.drop (n + 1) φs') = i, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics (List.take (↑i.succ) (φ :: φs'))) ofCrAnListF (List.take (↑i.succ) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofCrAnOpF ((φ :: φs').get i.succ)) * ofCrAnListF (List.drop (i.succ + 1) (φ :: φs')) All goals completed! 🐙
𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφ:𝓕.FieldOpφs':List 𝓕.FieldOp(superCommuteF (ofCrAnListF φs)) (ofFieldOpF φ) * ofFieldOpListF φs' + (exchangeSign (ofList 𝓕.crAnStatistics φs)) (𝓕|>ₛφ) ofFieldOpF φ * n, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs')) ofFieldOpListF (List.take (↑n) φs') * (superCommuteF (ofCrAnListF φs)) (ofFieldOpF (φs'.get n)) * ofFieldOpListF (List.drop (n + 1) φs') = n, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) (φ :: φs'))) ofFieldOpListF (List.take (↑n) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofFieldOpF ((φ :: φs').get n)) * ofFieldOpListF (List.drop (n + 1) (φ :: φs')) conv_rhs => 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφ:𝓕.FieldOpφs':List 𝓕.FieldOp| (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic (List.take (↑0) (φ :: φs'))) ofFieldOpListF (List.take (↑0) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofFieldOpF ((φ :: φs').get 0)) * ofFieldOpListF (List.drop (0 + 1) (φ :: φs')) + i, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic (List.take (↑i.succ) (φ :: φs'))) ofFieldOpListF (List.take (↑i.succ) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofFieldOpF ((φ :: φs').get i.succ)) * ofFieldOpListF (List.drop (i.succ + 1) (φ :: φs')) 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφ:𝓕.FieldOpφs':List 𝓕.FieldOp(superCommuteF (ofCrAnListF φs)) (ofFieldOpF φ) * ofFieldOpListF φs' = (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic (List.take (↑0) (φ :: φs'))) ofFieldOpListF (List.take (↑0) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofFieldOpF ((φ :: φs').get 0)) * ofFieldOpListF (List.drop (0 + 1) (φ :: φs'))𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφ:𝓕.FieldOpφs':List 𝓕.FieldOp(exchangeSign (ofList 𝓕.crAnStatistics φs)) (𝓕|>ₛφ) ofFieldOpF φ * n, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs')) ofFieldOpListF (List.take (↑n) φs') * (superCommuteF (ofCrAnListF φs)) (ofFieldOpF (φs'.get n)) * ofFieldOpListF (List.drop (n + 1) φs') = i, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic (List.take (↑i.succ) (φ :: φs'))) ofFieldOpListF (List.take (↑i.succ) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofFieldOpF ((φ :: φs').get i.succ)) * ofFieldOpListF (List.drop (i.succ + 1) (φ :: φs')) 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφ:𝓕.FieldOpφs':List 𝓕.FieldOp(superCommuteF (ofCrAnListF φs)) (ofFieldOpF φ) * ofFieldOpListF φs' = (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic (List.take (↑0) (φ :: φs'))) ofFieldOpListF (List.take (↑0) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofFieldOpF ((φ :: φs').get 0)) * ofFieldOpListF (List.drop (0 + 1) (φ :: φs')) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφ:𝓕.FieldOpφs':List 𝓕.FieldOp(exchangeSign (ofList 𝓕.crAnStatistics φs)) (𝓕|>ₛφ) ofFieldOpF φ * n, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs')) ofFieldOpListF (List.take (↑n) φs') * (superCommuteF (ofCrAnListF φs)) (ofFieldOpF (φs'.get n)) * ofFieldOpListF (List.drop (n + 1) φs') = i, (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic (List.take (↑i.succ) (φ :: φs'))) ofFieldOpListF (List.take (↑i.succ) (φ :: φs')) * (superCommuteF (ofCrAnListF φs)) (ofFieldOpF ((φ :: φs').get i.succ)) * ofFieldOpListF (List.drop (i.succ + 1) (φ :: φs')) All goals completed! 🐙𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOpofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics (φs2 ++ φs3)) ofCrAnListF (φs2 ++ φs3 ++ φs1) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics (φs3 ++ φs2)) ofCrAnListF (φs3 ++ φs2 ++ φs1)) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics (φs1 ++ φs2)) ofCrAnListF (φs1 ++ φs2 ++ φs3) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics (φs2 ++ φs1)) ofCrAnListF (φs2 ++ φs1 ++ φs3)))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics (φs3 ++ φs1)) ofCrAnListF (φs3 ++ φs1 ++ φs2) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics (φs1 ++ φs3)) ofCrAnListF (φs1 ++ φs3 ++ φs2)))) 𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOpofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2))))) 𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs1 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2))))) 𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs1 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2))))) 𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs1 = bosonich2:ofList 𝓕.crAnStatistics φs2 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs1 = bosonich2:¬ofList 𝓕.crAnStatistics φs2 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2))))) 𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = bosonich2:ofList 𝓕.crAnStatistics φs2 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = bosonich2:¬ofList 𝓕.crAnStatistics φs2 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs1 = bosonich2:ofList 𝓕.crAnStatistics φs2 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs1 = bosonich2:¬ofList 𝓕.crAnStatistics φs2 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2))))) 𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs1 = bosonich2:¬ofList 𝓕.crAnStatistics φs2 = bosonich3:ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs1 = bosonich2:¬ofList 𝓕.crAnStatistics φs2 = bosonich3:¬ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2))))) 𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = bosonich2:ofList 𝓕.crAnStatistics φs2 = bosonich3:ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = bosonich2:ofList 𝓕.crAnStatistics φs2 = bosonich3:¬ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = bosonich2:¬ofList 𝓕.crAnStatistics φs2 = bosonich3:ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = bosonich2:¬ofList 𝓕.crAnStatistics φs2 = bosonich3:¬ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs1 = bosonich2:ofList 𝓕.crAnStatistics φs2 = bosonich3:ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs1 = bosonich2:ofList 𝓕.crAnStatistics φs2 = bosonich3:¬ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs1 = bosonich2:¬ofList 𝓕.crAnStatistics φs2 = bosonich3:ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2)))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs1 = bosonich2:¬ofList 𝓕.crAnStatistics φs2 = bosonich3:¬ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs3) (-((exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3) (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs2) ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs2 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs2 ++ (φs1 ++ φs3))))) - (exchangeSign (ofList 𝓕.crAnStatistics φs1)) (ofList 𝓕.crAnStatistics φs2) (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs3 * ofList 𝓕.crAnStatistics φs1) ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (exchangeSign (ofList 𝓕.crAnStatistics φs3)) (ofList 𝓕.crAnStatistics φs1) (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (exchangeSign (ofList 𝓕.crAnStatistics φs2)) (ofList 𝓕.crAnStatistics φs1 * ofList 𝓕.crAnStatistics φs3) ofCrAnListF (φs1 ++ (φs3 ++ φs2))))) 𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = fermionich2:ofList 𝓕.crAnStatistics φs2 = fermionich3:ofList 𝓕.crAnStatistics φs3 = fermionicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - ofCrAnListF (φs1 ++ (φs3 ++ φs2))) = ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - ofCrAnListF (φs3 ++ (φs1 ++ φs2))) - (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - ofCrAnListF (φs3 ++ (φs2 ++ φs1)))) 𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = bosonich2:ofList 𝓕.crAnStatistics φs2 = bosonich3:ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - ofCrAnListF (φs1 ++ (φs2 ++ φs3))) - (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - ofCrAnListF (φs1 ++ (φs3 ++ φs2))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = bosonich2:ofList 𝓕.crAnStatistics φs2 = bosonich3:ofList 𝓕.crAnStatistics φs3 = fermionicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - ofCrAnListF (φs1 ++ (φs2 ++ φs3))) - (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - ofCrAnListF (φs1 ++ (φs3 ++ φs2))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = bosonich2:ofList 𝓕.crAnStatistics φs2 = fermionich3:ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - ofCrAnListF (φs1 ++ (φs2 ++ φs3))) - (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - ofCrAnListF (φs1 ++ (φs3 ++ φs2))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = bosonich2:ofList 𝓕.crAnStatistics φs2 = fermionich3:ofList 𝓕.crAnStatistics φs3 = fermionicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - ofCrAnListF (φs1 ++ (φs3 ++ φs2))) = ofCrAnListF (φs3 ++ (φs1 ++ φs2)) + ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) + ofCrAnListF (φs2 ++ (φs1 ++ φs3))) - (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) + ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) + ofCrAnListF (φs1 ++ (φs3 ++ φs2))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = fermionich2:ofList 𝓕.crAnStatistics φs2 = bosonich3:ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - ofCrAnListF (φs1 ++ (φs2 ++ φs3))) - (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - ofCrAnListF (φs1 ++ (φs3 ++ φs2))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = fermionich2:ofList 𝓕.crAnStatistics φs2 = bosonich3:ofList 𝓕.crAnStatistics φs3 = fermionicofCrAnListF (φs1 ++ (φs2 ++ φs3)) + ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) + ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - ofCrAnListF (φs2 ++ (φs1 ++ φs3))) - (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) + ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) + ofCrAnListF (φs1 ++ (φs2 ++ φs3))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = fermionich2:ofList 𝓕.crAnStatistics φs2 = fermionich3:ofList 𝓕.crAnStatistics φs3 = bosonicofCrAnListF (φs1 ++ (φs2 ++ φs3)) + ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (ofCrAnListF (φs1 ++ (φs3 ++ φs2)) + ofCrAnListF (φs3 ++ (φs2 ++ φs1))) = ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - ofCrAnListF (φs1 ++ (φs2 ++ φs3))) - (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) + ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) + ofCrAnListF (φs3 ++ (φs1 ++ φs2))))𝓕:FieldSpecificationφs1:List 𝓕.CrAnFieldOpφs2:List 𝓕.CrAnFieldOpφs3:List 𝓕.CrAnFieldOph1:ofList 𝓕.crAnStatistics φs1 = fermionich2:ofList 𝓕.crAnStatistics φs2 = fermionich3:ofList 𝓕.crAnStatistics φs3 = fermionicofCrAnListF (φs1 ++ (φs2 ++ φs3)) - ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - (ofCrAnListF (φs3 ++ (φs2 ++ φs1)) - ofCrAnListF (φs1 ++ (φs3 ++ φs2))) = ofCrAnListF (φs1 ++ (φs3 ++ φs2)) - ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - (ofCrAnListF (φs2 ++ (φs3 ++ φs1)) - ofCrAnListF (φs3 ++ (φs1 ++ φs2))) - (ofCrAnListF (φs3 ++ (φs1 ++ φs2)) - ofCrAnListF (φs1 ++ (φs2 ++ φs3)) - (ofCrAnListF (φs2 ++ (φs1 ++ φs3)) - ofCrAnListF (φs3 ++ (φs2 ++ φs1)))) All goals completed! 🐙

Interaction with grading.

All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f1 Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) statisticSubmodule (f1 + f2)p 0 All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f1 Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) statisticSubmodule (f1 + f2) (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f1}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f1}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f1 Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) statisticSubmodule (f1 + f2)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f1}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f1}hp1:p x hxhp2:p y hyp (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f1 Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) statisticSubmodule (f1 + f2)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f1}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f1}hp1:p x hxhp2:p y hy(superCommuteF x) (ofCrAnListF φs) + (superCommuteF y) (ofCrAnListF φs) statisticSubmodule (f1 * f2) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f1 Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) statisticSubmodule (f1 + f2) (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f1}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f1 Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) statisticSubmodule (f1 + f2)c:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f1}hp1:p x hxp (c x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f1 Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) statisticSubmodule (f1 + f2)c:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f1}hp1:p x hxc (superCommuteF x) (ofCrAnListF φs) statisticSubmodule (f1 * f2) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)φs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f1 Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) statisticSubmodule (f1 + f2)a Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f1} All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)p 0 All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2) (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f2}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f2}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f2}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f2}hp1:p x hxhp2:p y hyp (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f2}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f2}hp1:p x hxhp2:p y hy(superCommuteF a) x + (superCommuteF a) y statisticSubmodule (f1 * f2) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2) (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f2}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)c:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f2}hp1:p x hxp (c x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)c:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f2}hp1:p x hxc (superCommuteF a) x statisticSubmodule (f1 * f2) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraf1:FieldStatisticf2:FieldStatisticha:a statisticSubmodule f1hb:b statisticSubmodule f2p:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule f2 Prop := fun a2 hx => (superCommuteF a) a2 statisticSubmodule (f1 + f2)b Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = f2} All goals completed! 🐙lemma superCommuteF_bosonic_bosonic {a b : 𝓕.FieldOpFreeAlgebra} (ha : a statisticSubmodule bosonic) (hb : b statisticSubmodule bosonic) : [a, b]ₛF = a * b - b * a := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonic(superCommuteF a) b = a * b - b * a 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a(superCommuteF a) b = a * b - b * a 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ap b hb 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ap 0 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ab Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic} 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ax:𝓕.FieldOpFreeAlgebrahx:x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp (ofCrAnListF φs) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2p✝ (ofCrAnListF φs) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2p a ha 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2p 0 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2a Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic} 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2x:𝓕.FieldOpFreeAlgebrahx:x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2φs':List 𝓕.CrAnFieldOphφs':ofList 𝓕.crAnStatistics φs' = bosonicp (ofCrAnListF φs') All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2p 0 All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hp1:p x hxhp2:p y hyp (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hp1:(superCommuteF x) (ofCrAnListF φs) = x * ofCrAnListF φs - ofCrAnListF φs * xhp2:(superCommuteF y) (ofCrAnListF φs) = y * ofCrAnListF φs - ofCrAnListF φs * yx * ofCrAnListF φs - ofCrAnListF φs * x + (y * ofCrAnListF φs - ofCrAnListF φs * y) = x * ofCrAnListF φs + y * ofCrAnListF φs - (ofCrAnListF φs * x + ofCrAnListF φs * y) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2c:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hp1:p x hxp (c x) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2a Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic} All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ap 0 All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ax:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hp1:p x hxhp2:p y hyp (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ax:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hp1:(superCommuteF a) x = a * x - x * ahp2:(superCommuteF a) y = a * y - y * aa * x - x * a + (a * y - y * a) = a * x + a * y - (x * a + y * a) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ac:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hp1:p x hxp (c x) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ab Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic} All goals completed! 🐙lemma superCommuteF_bosonic_fermionic {a b : 𝓕.FieldOpFreeAlgebra} (ha : a statisticSubmodule bosonic) (hb : b statisticSubmodule fermionic) : [a, b]ₛF = a * b - b * a := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionic(superCommuteF a) b = a * b - b * a 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a(superCommuteF a) b = a * b - b * a 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ap b hb 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ap 0 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ab Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic} 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ax:𝓕.FieldOpFreeAlgebrahx:x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp (ofCrAnListF φs) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2p✝ (ofCrAnListF φs) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2p a ha 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2p 0 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2a Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic} 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2x:𝓕.FieldOpFreeAlgebrahx:x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2φs':List 𝓕.CrAnFieldOphφs':ofList 𝓕.crAnStatistics φs' = bosonicp (ofCrAnListF φs') All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2p 0 All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hp1:p x hxhp2:p y hyp (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hp1:(superCommuteF x) (ofCrAnListF φs) = x * ofCrAnListF φs - ofCrAnListF φs * xhp2:(superCommuteF y) (ofCrAnListF φs) = y * ofCrAnListF φs - ofCrAnListF φs * yx * ofCrAnListF φs - ofCrAnListF φs * x + (y * ofCrAnListF φs - ofCrAnListF φs * y) = x * ofCrAnListF φs + y * ofCrAnListF φs - (ofCrAnListF φs * x + ofCrAnListF φs * y) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2c:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hp1:p x hxp (c x) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2a Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic} All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ap 0 All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ax:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hp1:p x hxhp2:p y hyp (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ax:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hp1:(superCommuteF a) x = a * x - x * ahp2:(superCommuteF a) y = a * y - y * aa * x - x * a + (a * y - y * a) = a * x + a * y - (x * a + y * a) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ac:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hp1:p x hxp (c x) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ab Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic} All goals completed! 🐙lemma superCommuteF_fermionic_bonsonic {a b : 𝓕.FieldOpFreeAlgebra} (ha : a statisticSubmodule fermionic) (hb : b statisticSubmodule bosonic) : [a, b]ₛF = a * b - b * a := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonic(superCommuteF a) b = a * b - b * a 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a(superCommuteF a) b = a * b - b * a 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ap b hb 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ap 0 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ab Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic} 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ax:𝓕.FieldOpFreeAlgebrahx:x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp (ofCrAnListF φs) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2p✝ (ofCrAnListF φs) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2p a ha 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2p 0 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2a Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic} 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2x:𝓕.FieldOpFreeAlgebrahx:x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2φs':List 𝓕.CrAnFieldOphφs':ofList 𝓕.crAnStatistics φs' = fermionicp (ofCrAnListF φs') All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2p 0 All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hp1:p x hxhp2:p y hyp (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hp1:(superCommuteF x) (ofCrAnListF φs) = x * ofCrAnListF φs - ofCrAnListF φs * xhp2:(superCommuteF y) (ofCrAnListF φs) = y * ofCrAnListF φs - ofCrAnListF φs * yx * ofCrAnListF φs - ofCrAnListF φs * x + (y * ofCrAnListF φs - ofCrAnListF φs * y) = x * ofCrAnListF φs + y * ofCrAnListF φs - (ofCrAnListF φs * x + ofCrAnListF φs * y) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2 (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2c:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hp1:p x hxp (c x) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs - ofCrAnListF φs * a2a Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic} All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ap 0 All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ax:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hp1:p x hxhp2:p y hyp (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ax:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hp1:(superCommuteF a) x = a * x - x * ahp2:(superCommuteF a) y = a * y - y * aa * x - x * a + (a * y - y * a) = a * x + a * y - (x * a + y * a) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * a (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ac:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hp1:p x hxp (c x) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule bosonicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule bosonic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 - a2 * ab Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic} All goals completed! 🐙𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrahb:b statisticSubmodule bosonic(bosonicProjF a) * b - b * (bosonicProjF a) + ((fermionicProjF a) * b - b * (fermionicProjF a)) = ((bosonicProjF a) + (fermionicProjF a)) * b - b * ((bosonicProjF a) + (fermionicProjF a)) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrahb:b statisticSubmodule bosonic(bosonicProjF a) * b - b * (bosonicProjF a) + ((fermionicProjF a) * b - b * (fermionicProjF a)) = (bosonicProjF a) * b + (fermionicProjF a) * b - (b * (bosonicProjF a) + b * (fermionicProjF a)) All goals completed! 🐙𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonica * (bosonicProjF b) - (bosonicProjF b) * a + (a * (fermionicProjF b) - (fermionicProjF b) * a) = a * ((bosonicProjF b) + (fermionicProjF b)) - ((bosonicProjF b) + (fermionicProjF b)) * a 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonica * (bosonicProjF b) - (bosonicProjF b) * a + (a * (fermionicProjF b) - (fermionicProjF b) * a) = a * (bosonicProjF b) + a * (fermionicProjF b) - ((bosonicProjF b) * a + (fermionicProjF b) * a) All goals completed! 🐙𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrahb:b statisticSubmodule bosonica * b - b * a = -(b * a - a * b) All goals completed! 🐙𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule bosonica * b - b * a = -(b * a - a * b) All goals completed! 🐙lemma superCommuteF_fermionic_fermionic {a b : 𝓕.FieldOpFreeAlgebra} (ha : a statisticSubmodule fermionic) (hb : b statisticSubmodule fermionic) : [a, b]ₛF = a * b + b * a := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionic(superCommuteF a) b = a * b + b * a 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * a(superCommuteF a) b = a * b + b * a 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * ap b hb 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * a (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * ap 0 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * a (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * a (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * ab Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic} 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * a (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * ax:𝓕.FieldOpFreeAlgebrahx:x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp (ofCrAnListF φs) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2p✝ (ofCrAnListF φs) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2p a ha 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2 (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2p 0 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2 (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2 (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2a Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic} 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2 (x : 𝓕.FieldOpFreeAlgebra) (h : x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2x:𝓕.FieldOpFreeAlgebrahx:x {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}p x 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2φs':List 𝓕.CrAnFieldOphφs':ofList 𝓕.crAnStatistics φs' = fermionicp (ofCrAnListF φs') All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2p 0 All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2 (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hp1:p x hxhp2:p y hyp (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hp1:(superCommuteF x) (ofCrAnListF φs) = x * ofCrAnListF φs + ofCrAnListF φs * xhp2:(superCommuteF y) (ofCrAnListF φs) = y * ofCrAnListF φs + ofCrAnListF φs * yx * ofCrAnListF φs + ofCrAnListF φs * x + (y * ofCrAnListF φs + ofCrAnListF φs * y) = x * ofCrAnListF φs + y * ofCrAnListF φs + (ofCrAnListF φs * x + ofCrAnListF φs * y) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2 (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2c:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hp1:p x hxp (c x) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp✝:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * aφs:List 𝓕.CrAnFieldOphφs:ofList 𝓕.crAnStatistics φs = fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a2) (ofCrAnListF φs) = a2 * ofCrAnListF φs + ofCrAnListF φs * a2a Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic} All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * ap 0 All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * a (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}) (hy : y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p y hy p (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * ax:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hp1:p x hxhp2:p y hyp (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * ax:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hp1:(superCommuteF a) x = a * x + x * ahp2:(superCommuteF a) y = a * y + y * aa * x + x * a + (a * y + y * a) = a * x + a * y + (x * a + y * a) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * a (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * ac:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hp1:p x hxp (c x) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionicp:(a2 : 𝓕.FieldOpFreeAlgebra) a2 statisticSubmodule fermionic Prop := fun a2 hx => (superCommuteF a) a2 = a * a2 + a2 * ab Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic} All goals completed! 🐙𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraha:a statisticSubmodule fermionichb:b statisticSubmodule fermionica * b + b * a = b * a + a * b All goals completed! 🐙𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra(bosonicProjF a) * (bosonicProjF b) - (bosonicProjF b) * (bosonicProjF a) + ((fermionicProjF a) * (bosonicProjF b) - (bosonicProjF b) * (fermionicProjF a)) + ((bosonicProjF a) * (fermionicProjF b) - (fermionicProjF b) * (bosonicProjF a) + ((fermionicProjF a) * (fermionicProjF b) + (fermionicProjF b) * (fermionicProjF a))) = (bosonicProjF a) * (bosonicProjF b) - (bosonicProjF b) * (bosonicProjF a) + (bosonicProjF a) * (fermionicProjF b) - (fermionicProjF b) * (bosonicProjF a) + (fermionicProjF a) * (bosonicProjF b) - (bosonicProjF b) * (fermionicProjF a) + (fermionicProjF a) * (fermionicProjF b) + (fermionicProjF b) * (fermionicProjF a) All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs = bosonich2:¬ofList 𝓕.crAnStatistics φs' = bosonic(superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') statisticSubmodule (fermionic + fermionic) exact superCommuteF_grade (ofCrAnListF_mem_statisticSubmodule_of _ _ (𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs = bosonich2:¬ofList 𝓕.crAnStatistics φs' = bosonicofList 𝓕.crAnStatistics φs = fermionic All goals completed! 🐙)) (ofCrAnListF_mem_statisticSubmodule_of _ _ (𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOph1:¬ofList 𝓕.crAnStatistics φs = bosonich2:¬ofList 𝓕.crAnStatistics φs' = bosonicofList 𝓕.crAnStatistics φs' = fermionic All goals completed! 🐙))𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOp(superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [φ']) statisticSubmodule bosonic (superCommuteF (ofCrAnListF [φ])) (ofCrAnListF [φ']) statisticSubmodule fermionic All goals completed! 🐙𝓕:FieldSpecificationφ1:𝓕.CrAnFieldOpφ2:𝓕.CrAnFieldOpφ3:𝓕.CrAnFieldOphs:(superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3) statisticSubmodule fermionich1:ofCrAnOpF φ1 statisticSubmodule fermionic(superCommuteF (ofCrAnOpF φ1)) ((superCommuteF (ofCrAnOpF φ2)) (ofCrAnOpF φ3)) statisticSubmodule (fermionic + fermionic) All goals completed! 🐙𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule bosonic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hpx:(superCommuteF x) (ofCrAnListF φs) = x_1, ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs)hpy:(superCommuteF y) (ofCrAnListF φs) = x, ofCrAnListF (List.take (↑x) φs) * (superCommuteF y) (ofCrAnOpF φs[x]) * ofCrAnListF (List.drop (x + 1) φs) x_1, (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs) + ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF y) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs)) = x_1, ofCrAnListF (List.take (↑x_1) φs) * ((superCommuteF x) (ofCrAnOpF φs[x_1]) + (superCommuteF y) (ofCrAnOpF φs[x_1])) * ofCrAnListF (List.drop (x_1 + 1) φs) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule bosonic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hpx:(superCommuteF x) (ofCrAnListF φs) = x_1, ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs)hpy:(superCommuteF y) (ofCrAnListF φs) = x, ofCrAnListF (List.take (↑x) φs) * (superCommuteF y) (ofCrAnOpF φs[x]) * ofCrAnListF (List.drop (x + 1) φs)(fun x_1 => ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs) + ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF y) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs)) = fun x_1 => ofCrAnListF (List.take (↑x_1) φs) * ((superCommuteF x) (ofCrAnOpF φs[x_1]) + (superCommuteF y) (ofCrAnOpF φs[x_1])) * ofCrAnListF (List.drop (x_1 + 1) φs) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule bosonic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hpx:(superCommuteF x) (ofCrAnListF φs) = x_1, ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs)hpy:(superCommuteF y) (ofCrAnListF φs) = x, ofCrAnListF (List.take (↑x) φs) * (superCommuteF y) (ofCrAnOpF φs[x]) * ofCrAnListF (List.drop (x + 1) φs)n:Fin φs✝.lengthofCrAnListF (List.take (↑n) φs) * (superCommuteF x) (ofCrAnOpF φs[n]) * ofCrAnListF (List.drop (n + 1) φs) + ofCrAnListF (List.take (↑n) φs) * (superCommuteF y) (ofCrAnOpF φs[n]) * ofCrAnListF (List.drop (n + 1) φs) = ofCrAnListF (List.take (↑n) φs) * ((superCommuteF x) (ofCrAnOpF φs[n]) + (superCommuteF y) (ofCrAnOpF φs[n])) * ofCrAnListF (List.drop (n + 1) φs) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule bosonic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs) (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule bosonic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs)c:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic}hpx:p x hxp (c x) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule bosonicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule bosonic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs)a Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = bosonic} All goals completed! 🐙𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule fermionic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hpx:(superCommuteF x) (ofCrAnListF φs) = x_1, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs))hpy:(superCommuteF y) (ofCrAnListF φs) = x, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x) φs)) (ofCrAnListF (List.take (↑x) φs) * (superCommuteF y) (ofCrAnOpF φs[x]) * ofCrAnListF (List.drop (x + 1) φs)) x_1, ((exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs)) + (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF y) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs))) = x_1, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * ((superCommuteF x) (ofCrAnOpF φs[x_1]) + (superCommuteF y) (ofCrAnOpF φs[x_1])) * ofCrAnListF (List.drop (x_1 + 1) φs)) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule fermionic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hpx:(superCommuteF x) (ofCrAnListF φs) = x_1, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs))hpy:(superCommuteF y) (ofCrAnListF φs) = x, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x) φs)) (ofCrAnListF (List.take (↑x) φs) * (superCommuteF y) (ofCrAnOpF φs[x]) * ofCrAnListF (List.drop (x + 1) φs))(fun x_1 => (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs)) + (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF y) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs))) = fun x_1 => (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * ((superCommuteF x) (ofCrAnOpF φs[x_1]) + (superCommuteF y) (ofCrAnOpF φs[x_1])) * ofCrAnListF (List.drop (x_1 + 1) φs)) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule fermionic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hy:y Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hpx:(superCommuteF x) (ofCrAnListF φs) = x_1, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs))hpy:(superCommuteF y) (ofCrAnListF φs) = x, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x) φs)) (ofCrAnListF (List.take (↑x) φs) * (superCommuteF y) (ofCrAnOpF φs[x]) * ofCrAnListF (List.drop (x + 1) φs))n:Fin φs✝.length(exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) (ofCrAnListF (List.take (↑n) φs) * (superCommuteF x) (ofCrAnOpF φs[n]) * ofCrAnListF (List.drop (n + 1) φs)) + (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) (ofCrAnListF (List.take (↑n) φs) * (superCommuteF y) (ofCrAnOpF φs[n]) * ofCrAnListF (List.drop (n + 1) φs)) = (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) (ofCrAnListF (List.take (↑n) φs) * ((superCommuteF x) (ofCrAnOpF φs[n]) + (superCommuteF y) (ofCrAnOpF φs[n])) * ofCrAnListF (List.drop (n + 1) φs)) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule fermionic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs) (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}), p x hx p (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule fermionic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs)c:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hpx:p x hxp (c x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule fermionic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs)c:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hpx:(superCommuteF x) (ofCrAnListF φs) = x_1, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs)) x_1, c (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs)) = x_1, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) c (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs)) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule fermionic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs)c:x:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hpx:(superCommuteF x) (ofCrAnListF φs) = x_1, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs))(fun x_1 => c (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs))) = fun x_1 => (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) c (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs)) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule fermionic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs)c:x✝:𝓕.FieldOpFreeAlgebrahx:x Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic}hpx:(superCommuteF x) (ofCrAnListF φs) = x_1, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x_1) φs)) (ofCrAnListF (List.take (↑x_1) φs) * (superCommuteF x) (ofCrAnOpF φs[x_1]) * ofCrAnListF (List.drop (x_1 + 1) φs))x:Fin φs✝.lengthc (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x) φs)) (ofCrAnListF (List.take (↑x) φs) * (superCommuteF x✝) (ofCrAnOpF φs[x]) * ofCrAnListF (List.drop (x + 1) φs)) = (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑x) φs)) c (ofCrAnListF (List.take (↑x) φs) * (superCommuteF x✝) (ofCrAnOpF φs[x]) * ofCrAnListF (List.drop (x + 1) φs)) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraφs:List 𝓕.CrAnFieldOpha:a statisticSubmodule fermionicp:(a : 𝓕.FieldOpFreeAlgebra) a statisticSubmodule fermionic Prop := fun a ha => (superCommuteF a) (ofCrAnListF φs) = n, (exchangeSign fermionic) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) ofCrAnListF (List.take (↑n) φs) * (superCommuteF a) (ofCrAnOpF (φs.get n)) * ofCrAnListF (List.drop (n + 1) φs)a Submodule.span {a | φs, a = ofCrAnListF φs ofList 𝓕.crAnStatistics φs = fermionic} All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOph:(superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') statisticSubmodule fermionich0:¬(superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') = 0hn:ofList 𝓕.crAnStatistics φs = ofList 𝓕.crAnStatistics φs'hc:¬ofList 𝓕.crAnStatistics φs = bosonic(superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') statisticSubmodule (fermionic + fermionic) exact superCommuteF_grade (ofCrAnListF_mem_statisticSubmodule_of _ _ (𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOph:(superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') statisticSubmodule fermionich0:¬(superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') = 0hn:ofList 𝓕.crAnStatistics φs = ofList 𝓕.crAnStatistics φs'hc:¬ofList 𝓕.crAnStatistics φs = bosonicofList 𝓕.crAnStatistics φs = fermionic All goals completed! 🐙)) (ofCrAnListF_mem_statisticSubmodule_of _ _ (𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOph:(superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') statisticSubmodule fermionich0:¬(superCommuteF (ofCrAnListF φs)) (ofCrAnListF φs') = 0hn:ofList 𝓕.crAnStatistics φs = ofList 𝓕.crAnStatistics φs'hc:¬ofList 𝓕.crAnStatistics φs = bosonicofList 𝓕.crAnStatistics φs' = fermionic All goals completed! 🐙))