Documentation Verification Report

Invariants

📁 Source: PhysLean/Particles/FlavorPhysics/CKMMatrix/Invariants.lean

Statistics

Metric	Count
Definitions `VusVubVcdSq`, `jarlskogℂ`, `jarlskogℂCKM`, `mulExpδ₁₃`	4
Theorems `jarlskogℂCKM_equiv`, `jarlskogℂCKM_im`, `jarlskogℂCKM_re`	3
Total	7

Invariant

Definitions

Name	Category	Theorems
`VusVubVcdSq` 📖	CompOp	1 math math: `standParam.VusVubVcdSq_eq`
`jarlskogℂ` 📖	CompOp	—
`jarlskogℂCKM` 📖	CompOp	3 math math: `jarlskogℂCKM_re`, `jarlskogℂCKM_equiv`, `jarlskogℂCKM_im`
`mulExpδ₁₃` 📖	CompOp	5 math math: `standParam.mulExpδ₁₃_on_param_abs`, `standParam.mulExpδ₁₃_on_param_neq_zero_arg`, `standParam.mulExpδ₁₃_eq`, `standParam.mulExpδ₁₃_on_param_eq_zero_iff`, `standParam.mulExpδ₁₃_on_param_δ₁₃`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`jarlskogℂCKM_equiv` 📖	mathematical	`CKMMatrix` `CKMMatrixSetoid`	`jarlskogℂCKM`	—	`phaseShiftApply.us` `phaseShiftApply.cb` `phaseShiftApply.ub` `phaseShiftApply.cs`
`jarlskogℂCKM_im` 📖	mathematical	—	`jarlskogℂCKM`	—	—
`jarlskogℂCKM_re` 📖	mathematical	—	`jarlskogℂCKM`	—	—

---

← Back to Index