Documentation Verification Report

TimeContract

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

Statistics

Metric	Count
Definitions `timeContract`	1
Theorems `timeContract_empty`, `timeContract_insertAndContract_some`, `timeContract_insert_none`, `timeContract_insert_some_of_lt`, `timeContract_insert_some_of_not_lt`, `timeContract_of_not_gradingCompliant`	6
Total	7

WickContraction

Definitions

Name	Category	Theorems
`timeContract` 📖	CompOp	21 math math: `wickTerm_insert_some`, `join_sign_timeContract`, `EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_mid`, `wickTerm_insert_none`, `EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction`, `timeContract_insert_none`, `timeContract_insert_some_of_not_lt`, `join_timeContract`, `timeContract_insert_some_of_lt`, `timeContract_empty`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `EqTimeOnly.staticContract_eq_timeContract_of_eqTimeOnly`, `EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_left`, `timeContract_of_not_gradingCompliant`, `EqTimeOnly.timeOrder_timeContract_of_not_eqTimeOnly`, `FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive`, `timeContract_insertAndContract_some`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`, `singleton_timeContract`, `FieldSpecification.WickAlgebra.timeOrder_haveEqTime_split`, `FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eqTimeOnly`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`timeContract_empty` 📖	mathematical	—	`timeContract` `empty` `FieldSpecification.FieldOp` `FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet`	—	`timeContract.eq_1` `empty.eq_1`
`timeContract_insertAndContract_some` 📖	mathematical	—	`timeContract` `FieldSpecification.FieldOp` `insertAndContract` `uncontracted` `FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `FieldSpecification.WickAlgebra.timeContract` `FieldSpecification.WickAlgebra.timeContract_mem_center`	—	`FieldSpecification.WickAlgebra.timeContract_mem_center` `timeContract.eq_1` `PhysLean.List.insertIdx_length_fin` `insertAndContract_some_prod_contractions` `insertAndContract_fstFieldOfContract_some_incl` `insertAndContract_sndFieldOfContract_some_incl` `PhysLean.List.insertIdx_getElem_fin` `insertAndContract_fstFieldOfContract` `insertAndContract_sndFieldOfContract`
`timeContract_insert_none` 📖	mathematical	—	`timeContract` `FieldSpecification.FieldOp` `insertAndContract` `uncontracted`	—	`timeContract.eq_1` `PhysLean.List.insertIdx_length_fin` `insertAndContract_none_prod_contractions` `insertAndContract_fstFieldOfContract` `PhysLean.List.insertIdx_getElem_fin` `insertAndContract_sndFieldOfContract`
`timeContract_insert_some_of_lt` 📖	mathematical	`FieldSpecification.timeOrderRel` `FieldSpecification.FieldOp` `uncontracted`	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `timeContract` `insertAndContract` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `FieldStatistic.ofFinset` `FieldSpecification.WickAlgebra.contractStateAtIndex` `uncontractedListGet` `uncontractedFieldOpEquiv`	—	`FieldSpecification.WickAlgebra.timeContract_mem_center` `timeContract_insertAndContract_some` `uncontractedList_getElem_uncontractedIndexEquiv_symm` `FieldSpecification.WickAlgebra.timeContract_of_timeOrderRel` `take_uncontractedIndexEquiv_symm` `filter_uncontractedList` `FieldStatistic.exchangeSign_mul_self`
`timeContract_insert_some_of_not_lt` 📖	mathematical	`FieldSpecification.timeOrderRel` `FieldSpecification.FieldOp` `uncontracted`	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `timeContract` `insertAndContract` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `FieldStatistic.ofFinset` `FieldSpecification.WickAlgebra.contractStateAtIndex` `uncontractedListGet` `uncontractedFieldOpEquiv`	—	`FieldSpecification.WickAlgebra.timeContract_mem_center` `timeContract_insertAndContract_some` `uncontractedList_getElem_uncontractedIndexEquiv_symm` `FieldSpecification.WickAlgebra.timeContract_of_not_timeOrderRel` `FieldSpecification.WickAlgebra.timeContract_of_timeOrderRel` `FieldSpecification.instIsTotalFieldOpTimeOrderRel` `take_uncontractedIndexEquiv_symm` `filter_uncontractedList` `FieldStatistic.exchangeSign_symm` `FieldStatistic.ofFinset_singleton` `FieldStatistic.ofFinset_union`
`timeContract_of_not_gradingCompliant` 📖	mathematical	`GradingCompliant`	`timeContract` `FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet`	—	`timeContract.eq_1` `FieldSpecification.WickAlgebra.timeContract_zero_of_diff_grade`

---

← Back to Index