Documentation Verification Report

ExtractEquiv

📁 Source: PhysLean/QFT/PerturbationTheory/WickContraction/ExtractEquiv.lean

Statistics

Metric	Count
Definitions `extractEquiv`, `fintype_succ`, `fintype_zero`	3
Theorems `extractEquiv_apply_congr_symm_apply`, `extractEquiv_equiv`, `extractEquiv_symm_none_uncontracted`, `mem_four`, `mem_three`, `sum_WickContraction_nil`, `sum_extractEquiv_congr`	7
Total	10
⚠️ With sorry `mem_four`, `mem_three`	2

WickContraction

Definitions

Name	Category	Theorems
`extractEquiv` 📖	CompOp	5 math math: `uncontractedList_extractEquiv_symm_none`, `uncontractedList_extractEquiv_symm_some`, `extractEquiv_symm_none_uncontracted`, `sum_extractEquiv_congr`, `extractEquiv_apply_congr_symm_apply`
`fintype_succ` 📖	CompOp	20 math math: `FieldSpecification.wicks_theorem_congr`, `FieldSpecification.WickAlgebra.wicks_theorem_normal_order_empty`, `card_of_isfull_even`, `wickContraction_zero_some_eq_sum`, `FieldSpecification.WickAlgebra.wicks_theorem_normal_order`, `card_of_isfull_odd`, `wickContraction_zero_none_card`, `sum_extractEquiv_congr`, `FieldSpecification.WickAlgebra.static_wick_theorem`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `wickContraction_card_eq_sum_zero_none_isSome`, `sum_haveEqTime`, `insertLift_sum`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `card_eq_cardFun`, `wickContraction_zero_some_eq_mul`, `FieldSpecification.wicks_theorem`, `FieldSpecification.WickAlgebra.timeOrder_haveEqTime_split`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eqTimeOnly`
`fintype_zero` 📖	CompOp	1 math math: `sum_WickContraction_nil`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extractEquiv_apply_congr_symm_apply` 📖	mathematical	—	`WickContraction` `congr` `uncontracted` `extractEquiv`	—	—
`extractEquiv_equiv` 📖	—	`WickContraction` `uncontracted` `uncontractedCongr`	—	—	—
`extractEquiv_symm_none_uncontracted` 📖	mathematical	—	`uncontracted` `WickContraction` `extractEquiv`	—	`insertAndContractNat_none_uncontracted`
`mem_four` 📖 ⚠️	—	—	—	—	—
`mem_three` 📖 ⚠️	—	—	—	—	—
`sum_WickContraction_nil` 📖	mathematical	—	`WickContraction` `fintype_zero` `empty`	—	—
`sum_extractEquiv_congr` 📖	mathematical	—	`WickContraction` `fintype_succ` `uncontracted` `congr` `extractEquiv`	—	—

---

← Back to Index