Documentation Verification Report

Metric

📁 Source: PhysLean/Relativity/Tensors/ComplexTensor/Weyl/Metric.lean

Statistics

Metric	Count
Definitions `altLeftMetric`, `altLeftMetricVal`, `altRightMetric`, `altRightMetricVal`, `leftMetric`, `leftMetricVal`, `metricRaw`, `rightMetric`, `rightMetricVal`	9
Theorems `altLeftContraction_apply_metric`, `altLeftMetricVal_expand_tmul`, `altLeftMetric_apply_one`, `altRightContraction_apply_metric`, `altRightMetricVal_expand_tmul`, `altRightMetric_apply_one`, `comm_metricRaw`, `leftAltContraction_apply_metric`, `leftMetricVal_expand_tmul`, `leftMetric_apply_one`, `metricRaw_comm`, `metricRaw_comm_star`, `rightAltContraction_apply_metric`, `rightMetricVal_expand_tmul`, `rightMetric_apply_one`, `star_comm_metricRaw`	16
Total	25

Fermion

Definitions

Name	Category	Theorems
`altLeftMetric` 📖	CompOp	4 math math: `altLeftMetric_apply_one`, `complexLorentzTensor.altLeftMetric_eq_fromConstPair`, `altLeftContraction_apply_metric`, `leftAltContraction_apply_metric`
`altLeftMetricVal` 📖	CompOp	3 math math: `altLeftMetric_apply_one`, `complexLorentzTensor.altLeftMetric_eq_fromPairT`, `altLeftMetricVal_expand_tmul`
`altRightMetric` 📖	CompOp	4 math math: `complexLorentzTensor.altRightMetric_eq_fromConstPair`, `altRightMetric_apply_one`, `rightAltContraction_apply_metric`, `altRightContraction_apply_metric`
`altRightMetricVal` 📖	CompOp	3 math math: `altRightMetricVal_expand_tmul`, `altRightMetric_apply_one`, `complexLorentzTensor.altRightMetric_eq_fromPairT`
`leftMetric` 📖	CompOp	4 math math: `leftMetric_apply_one`, `altLeftContraction_apply_metric`, `complexLorentzTensor.leftMetric_eq_fromConstPair`, `leftAltContraction_apply_metric`
`leftMetricVal` 📖	CompOp	3 math math: `leftMetric_apply_one`, `leftMetricVal_expand_tmul`, `complexLorentzTensor.leftMetric_eq_fromPairT`
`metricRaw` 📖	CompOp	4 math math: `metricRaw_comm_star`, `star_comm_metricRaw`, `metricRaw_comm`, `comm_metricRaw`
`rightMetric` 📖	CompOp	4 math math: `rightAltContraction_apply_metric`, `complexLorentzTensor.rightMetric_eq_fromConstPair`, `altRightContraction_apply_metric`, `rightMetric_apply_one`
`rightMetricVal` 📖	CompOp	3 math math: `rightMetricVal_expand_tmul`, `complexLorentzTensor.rightMetric_eq_fromPairT`, `rightMetric_apply_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`altLeftContraction_apply_metric` 📖	mathematical	—	`altLeftHanded` `leftHanded` `altLeftContraction` `altLeftMetric` `leftMetric` `leftAltLeftUnit`	—	`leftMetric_apply_one` `altLeftMetric_apply_one` `leftMetricVal_expand_tmul` `altLeftMetricVal_expand_tmul` `altLeftContraction_basis` `leftAltLeftUnit_apply_one` `leftAltLeftUnitVal_expand_tmul`
`altLeftMetricVal_expand_tmul` 📖	mathematical	—	`altLeftMetricVal` `altLeftHanded` `altLeftBasis`	—	`altLeftaltLeftToMatrix_symm_expand_tmul`
`altLeftMetric_apply_one` 📖	mathematical	—	`altLeftHanded` `altLeftMetric` `altLeftMetricVal`	—	—
`altRightContraction_apply_metric` 📖	mathematical	—	`altRightHanded` `rightHanded` `altRightContraction` `altRightMetric` `rightMetric` `rightAltRightUnit`	—	`rightMetric_apply_one` `altRightMetric_apply_one` `rightMetricVal_expand_tmul` `altRightMetricVal_expand_tmul` `altRightContraction_basis` `rightAltRightUnit_apply_one` `rightAltRightUnitVal_expand_tmul`
`altRightMetricVal_expand_tmul` 📖	mathematical	—	`altRightMetricVal` `altRightHanded` `altRightBasis`	—	`altRightAltRightToMatrix_symm_expand_tmul`
`altRightMetric_apply_one` 📖	mathematical	—	`altRightHanded` `altRightMetric` `altRightMetricVal`	—	—
`comm_metricRaw` 📖	mathematical	—	`metricRaw`	—	`metricRaw.eq_1` `Lorentz.SL2C.inverse_coe`
`leftAltContraction_apply_metric` 📖	mathematical	—	`leftHanded` `altLeftHanded` `leftAltContraction` `leftMetric` `altLeftMetric` `altLeftLeftUnit`	—	`leftMetric_apply_one` `altLeftMetric_apply_one` `leftMetricVal_expand_tmul` `altLeftMetricVal_expand_tmul` `leftAltContraction_basis` `altLeftLeftUnit_apply_one` `altLeftLeftUnitVal_expand_tmul`
`leftMetricVal_expand_tmul` 📖	mathematical	—	`leftMetricVal` `leftHanded` `leftBasis`	—	`leftLeftToMatrix_symm_expand_tmul`
`leftMetric_apply_one` 📖	mathematical	—	`leftHanded` `leftMetric` `leftMetricVal`	—	—
`metricRaw_comm` 📖	mathematical	—	`metricRaw`	—	`metricRaw.eq_1` `Lorentz.SL2C.inverse_coe`
`metricRaw_comm_star` 📖	mathematical	—	`metricRaw`	—	`metricRaw.eq_1` `Lorentz.SL2C.inverse_coe`
`rightAltContraction_apply_metric` 📖	mathematical	—	`rightHanded` `altRightHanded` `rightAltContraction` `rightMetric` `altRightMetric` `altRightRightUnit`	—	`rightMetric_apply_one` `altRightMetric_apply_one` `rightMetricVal_expand_tmul` `altRightMetricVal_expand_tmul` `rightAltContraction_basis` `altRightRightUnit_apply_one` `altRightRightUnitVal_expand_tmul`
`rightMetricVal_expand_tmul` 📖	mathematical	—	`rightMetricVal` `rightHanded` `rightBasis`	—	`rightRightToMatrix_symm_expand_tmul`
`rightMetric_apply_one` 📖	mathematical	—	`rightHanded` `rightMetric` `rightMetricVal`	—	—
`star_comm_metricRaw` 📖	mathematical	—	`metricRaw`	—	`metricRaw.eq_1` `Lorentz.SL2C.inverse_coe`

---

← Back to Index