Documentation Verification Report

Join

📁 Source: PhysLean/QFT/PerturbationTheory/WickContraction/Sign/Join.lean

Statistics

Metric	Count
Definitions `joinSignLeftExtra`, `joinSignRightExtra`	2
Theorems `joinSignLeftExtra_eq_joinSignRightExtra`, `joinSignRightExtra_eq_i_j_finset_eq_if`, `join_sign`, `join_sign_induction`, `join_sign_singleton`, `join_sign_timeContract`, `join_singleton_left_signFinset_eq_filter`, `join_singleton_signFinset_eq_filter`, `join_singleton_sign_left`, `join_singleton_sign_right`, `signFinset_right_map_uncontractedListEmd_eq_filter`, `sign_right_eq_prod_mul_prod`, `stat_signFinset_right`	13
Total	15

WickContraction

Definitions

Name	Category	Theorems
`joinSignLeftExtra` 📖	CompOp	2 math math: `join_singleton_sign_left`, `joinSignLeftExtra_eq_joinSignRightExtra`
`joinSignRightExtra` 📖	CompOp	3 math math: `join_singleton_sign_right`, `joinSignRightExtra_eq_i_j_finset_eq_if`, `joinSignLeftExtra_eq_joinSignRightExtra`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`joinSignLeftExtra_eq_joinSignRightExtra` 📖	mathematical	`FieldSpecification.FieldOp` `FieldSpecification.fieldOpStatistic`	`joinSignLeftExtra` `joinSignRightExtra`	—	`joinSignLeftExtra.eq_1` `FieldStatistic.ofFinset_eq_prod` `fstFieldOfContract_mem` `sndFieldOfContract_mem` `prod_finset_eq_mul_fst_snd` `fstFieldOfContract_getDual?` `sndFieldOfContract_getDual?` `prod_join` `mem_singleton` `singleton_prod` `join_fstFieldOfContract_joinLiftLeft` `singleton_fstFieldOfContract` `join_sndFieldOfContract_joinLift` `singleton_sndFieldOfContract` `join_fstFieldOfContract_joinLiftRight` `join_sndFieldOfContract_joinLiftRight` `getElem_uncontractedListEmd` `joinSignRightExtra_eq_i_j_finset_eq_if` `singleton_uncontractedEmd_neq_right` `uncontractedListEmd_strictMono` `fstFieldOfContract_lt_sndFieldOfContract` `FieldStatistic.ofFinset_empty` `FieldStatistic.ofFinset_singleton` `FieldStatistic.exchangeSign_symm` `FieldStatistic.ofFinset_union_disjoint` `FieldStatistic.mul_self`
`joinSignRightExtra_eq_i_j_finset_eq_if` 📖	mathematical	`FieldSpecification.FieldOp`	`joinSignRightExtra` `uncontractedListGet` `singleton` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `sndFieldOfContract` `FieldStatistic.ofFinset` `uncontractedListEmd` `fstFieldOfContract`	—	`joinSignRightExtra.eq_1` `signFinset.eq_1` `mem_uncontracted_iff_not_contracted` `singleton_uncontractedEmd_neq_right` `singleton_uncontractedEmd_neq_left` `join_singleton_getDual?_right` `join_singleton_getDual?_left`
`join_sign` 📖	mathematical	`GradingCompliant`	`sign` `join` `uncontractedListGet`	—	`join_sign_induction`
`join_sign_induction` 📖	mathematical	`GradingCompliant` `FieldSpecification.FieldOp`	`sign` `join` `uncontractedListGet`	—	`uncontractedListGet_empty` `empty_join` `sign_empty` `sign_congr` `card_zero_iff_empty` `exists_join_singleton_of_card_ge_zero` `join_uncontractedListGet` `join_assoc` `join_sign_singleton`
`join_sign_singleton` 📖	mathematical	`FieldSpecification.FieldOp` `FieldSpecification.fieldOpStatistic`	`sign` `join` `singleton` `uncontractedListGet`	—	`join_singleton_sign_right` `join_singleton_sign_left` `joinSignLeftExtra_eq_joinSignRightExtra` `FieldStatistic.exchangeSign_mul_self` `sign.eq_1` `prod_join` `mem_singleton` `singleton_prod` `join_sndFieldOfContract_joinLift` `singleton_sndFieldOfContract` `join_fstFieldOfContract_joinLiftLeft` `singleton_fstFieldOfContract` `join_sndFieldOfContract_joinLiftRight` `getElem_uncontractedListEmd` `join_fstFieldOfContract_joinLiftRight`
`join_sign_timeContract` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `sign` `join` `timeContract` `uncontractedListGet`	—	`join_timeContract` `join_sign` `timeContract_of_not_gradingCompliant`
`join_singleton_left_signFinset_eq_filter` 📖	mathematical	`FieldSpecification.FieldOp`	`FieldStatistic.ofFinset` `FieldSpecification.fieldOpStatistic` `signFinset` `singleton` `FieldStatistic` `FieldStatistic.instCommGroup` `join` `getDual?`	—	`join_singleton_signFinset_eq_filter` `FieldStatistic.ofFinset_filter_mul_neg`
`join_singleton_signFinset_eq_filter` 📖	mathematical	`FieldSpecification.FieldOp`	`signFinset` `join` `singleton` `getDual?`	—	`singleton_getDual?_eq_none_iff_neq` `getDual?_eq_some_iff_mem` `getDual?_getDual?_get_get`
`join_singleton_sign_left` 📖	mathematical	`FieldSpecification.FieldOp`	`sign` `singleton` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `FieldStatistic.ofFinset` `signFinset` `join` `joinSignLeftExtra`	—	`singleton_sign_expand` `join_singleton_left_signFinset_eq_filter`
`join_singleton_sign_right` 📖	mathematical	`FieldSpecification.FieldOp`	`sign` `uncontractedListGet` `singleton` `joinSignRightExtra` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `sndFieldOfContract` `FieldStatistic.ofFinset` `signFinset` `join` `uncontractedListEmd` `fstFieldOfContract`	—	`sign_right_eq_prod_mul_prod`
`signFinset_right_map_uncontractedListEmd_eq_filter` 📖	mathematical	—	`FieldSpecification.FieldOp` `uncontractedListGet` `uncontractedListEmd` `signFinset` `uncontracted` `join`	—	`join_getDual?_apply_uncontractedListEmb` `uncontractedListEmd_strictMono` `uncontractedListEmd_mem_uncontracted` `uncontractedListEmd_surjective_mem_uncontracted`
`sign_right_eq_prod_mul_prod` 📖	mathematical	—	`sign` `uncontractedListGet` `FieldSpecification.FieldOp` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `sndFieldOfContract` `FieldStatistic.ofFinset` `uncontracted` `signFinset` `join` `uncontractedListEmd` `fstFieldOfContract`	—	`sign.eq_1` `stat_signFinset_right` `signFinset_right_map_uncontractedListEmd_eq_filter` `FieldStatistic.ofFinset_filter`
`stat_signFinset_right` 📖	mathematical	—	`FieldStatistic.ofFinset` `FieldSpecification.FieldOp` `uncontractedListGet` `FieldSpecification.fieldOpStatistic` `signFinset` `uncontractedListEmd`	—	`fin_finset_sort_map_monotone` `uncontractedListEmd_strictMono` `getElem_uncontractedListEmd`

---

← Back to Index