Documentation Verification Report

WickTerm

📁 Source: PhysLean/QFT/PerturbationTheory/WickAlgebra/WickTerm.lean

Statistics

Metric	Count
Definitions `wickTerm`	1
Theorems `mul_wickTerm_eq_sum`, `wickTerm_empty_nil`, `wickTerm_insert_none`, `wickTerm_insert_some`	4
Total	5

WickContraction

Definitions

Name	Category	Theorems
`wickTerm` 📖	CompOp	10 math math: `wickTerm_insert_some`, `FieldSpecification.wicks_theorem_congr`, `FieldSpecification.WickAlgebra.wicks_theorem_normal_order_empty`, `wickTerm_insert_none`, `FieldSpecification.WickAlgebra.wicks_theorem_normal_order`, `wickTerm_empty_nil`, `mul_wickTerm_eq_sum`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive`, `FieldSpecification.wicks_theorem`, `FieldSpecification.WickAlgebra.timeOrder_haveEqTime_split`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_wickTerm_eq_sum` 📖	mathematical	`FieldSpecification.timeOrderRel` `FieldSpecification.FieldOp`	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `FieldSpecification.WickAlgebra.ofFieldOp` `wickTerm` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `FieldStatistic.ofFinset` `uncontracted` `insertAndContract`	—	`wickTerm.eq_1` `FieldSpecification.WickAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` `uncontractedFieldOpEquiv_list_sum` `wickTerm_insert_none` `FieldStatistic.exchangeSign_mul_self` `wickTerm_insert_some`
`wickTerm_empty_nil` 📖	mathematical	—	`wickTerm` `FieldSpecification.FieldOp` `empty` `FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet`	—	`wickTerm.eq_1` `sign_empty` `timeContract_empty` `uncontractedListGet_empty` `FieldSpecification.WickAlgebra.normalOrder_ofFieldOpList_nil`
`wickTerm_insert_none` 📖	mathematical	—	`wickTerm` `FieldSpecification.FieldOp` `insertAndContract` `uncontracted` `FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `FieldStatistic.ofFinset` `sign` `timeContract` `FieldSpecification.WickAlgebra.normalOrder` `FieldSpecification.WickAlgebra.ofFieldOpList` `uncontractedListGet`	—	`wickTerm.eq_1` `FieldSpecification.WickAlgebra.normalOrder_uncontracted_none` `sign_insert_none` `timeContract_insert_none` `FieldStatistic.ofFinset_union` `timeContract_of_not_gradingCompliant`
`wickTerm_insert_some` 📖	mathematical	`FieldSpecification.timeOrderRel` `FieldSpecification.FieldOp`	`wickTerm` `insertAndContract` `uncontracted` `FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `FieldStatistic.ofFinset` `sign` `FieldSpecification.WickAlgebra.contractStateAtIndex` `uncontractedListGet` `uncontractedFieldOpEquiv` `timeContract` `FieldSpecification.WickAlgebra.normalOrder` `FieldSpecification.WickAlgebra.ofFieldOpList` `PhysLean.List.optionEraseZ`	—	`wickTerm.eq_1` `timeContract_insert_some_of_not_lt` `FieldSpecification.WickAlgebra.normalOrder_uncontracted_some` `sign_insert_some_of_lt` `FieldStatistic.exchangeSign_mul_self` `timeContract_insert_some_of_lt` `sign_insert_some_of_not_lt` `FieldSpecification.WickAlgebra.timeContract_mem_center` `timeContract_insertAndContract_some` `uncontractedList_getElem_uncontractedIndexEquiv_symm` `FieldSpecification.WickAlgebra.timeContract_zero_of_diff_grade` `FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOpF_diff_grade_zero` `timeContract_of_not_gradingCompliant`

---

← Back to Index