Documentation Verification Report

StaticContract

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

Statistics

Metric	Count
Definitions `staticContract`	1
Theorems `staticContract_insert_none`, `staticContract_insert_some`, `staticContract_insert_some_of_lt`, `staticContract_of_not_gradingCompliant`	4
Total	5

WickContraction

Definitions

Name	Category	Theorems
`staticContract` 📖	CompOp	10 math math: `staticContract_insert_some_of_lt`, `staticWickTerm_insert_zero_some`, `EqTimeOnly.timeOrder_staticContract_of_not_mem`, `join_staticContract`, `staticContract_of_not_gradingCompliant`, `staticContract_insert_some`, `EqTimeOnly.staticContract_eq_timeContract_of_eqTimeOnly`, `staticContract_insert_none`, `staticWickTerm_insert_zero_none`, `singleton_staticContract`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`staticContract_insert_none` 📖	mathematical	—	`staticContract` `FieldSpecification.FieldOp` `insertAndContract` `uncontracted`	—	`staticContract.eq_1` `PhysLean.List.insertIdx_length_fin` `insertAndContract_none_prod_contractions` `insertAndContract_fstFieldOfContract` `PhysLean.List.insertIdx_getElem_fin` `insertAndContract_sndFieldOfContract`
`staticContract_insert_some` 📖	mathematical	—	`staticContract` `FieldSpecification.FieldOp` `insertAndContract` `uncontracted` `FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `FieldSpecification.WickAlgebra.superCommute` `FieldSpecification.WickAlgebra.anPart` `FieldSpecification.WickAlgebra.ofFieldOp` `FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOp_mem_center`	—	`FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOp_mem_center` `staticContract.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`
`staticContract_insert_some_of_lt` 📖	mathematical	`FieldSpecification.FieldOp` `uncontracted`	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `staticContract` `insertAndContract` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `FieldStatistic.ofFinset` `FieldSpecification.WickAlgebra.contractStateAtIndex` `uncontractedListGet` `uncontractedFieldOpEquiv`	—	`FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOp_mem_center` `staticContract_insert_some` `uncontractedList_getElem_uncontractedIndexEquiv_symm` `take_uncontractedIndexEquiv_symm` `filter_uncontractedList` `FieldStatistic.exchangeSign_mul_self`
`staticContract_of_not_gradingCompliant` 📖	mathematical	`GradingCompliant`	`staticContract` `FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet`	—	`staticContract.eq_1` `FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOpF_diff_grade_zero`

---

← Back to Index