Documentation Verification Report

PhaseFreedom

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

Statistics

Metric	Count
Definitions `FstRowThdColRealCond`, `ubOnePhaseCond`	2
Theorems `cd_of_fstRowThdColRealCond`, `cs_of_fstRowThdColRealCond`, `fstRowThdColRealCond_holds_up_to_equiv`, `fstRowThdColRealCond_shift_solution`, `shift_cb_phase_zero`, `shift_cd_phase_pi`, `shift_cross_product_phase_zero`, `shift_cs_phase_zero`, `shift_tb_phase_zero`, `shift_ub_phase_zero`, `shift_ud_phase_zero`, `shift_us_phase_zero`, `ubOnePhaseCond_hold_up_to_equiv_of_ub_one`, `ubOnePhaseCond_shift_solution`	14
Total	16

CKMMatrix

Definitions

Name	Category	Theorems
`FstRowThdColRealCond` 📖	MathDef	1 math math: `fstRowThdColRealCond_holds_up_to_equiv`
`ubOnePhaseCond` 📖	MathDef	1 math math: `ubOnePhaseCond_hold_up_to_equiv_of_ub_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cd_of_fstRowThdColRealCond` 📖	mathematical	`FstRowThdColRealCond`	`VtbAbs` `CKMMatrix` `CKMMatrixSetoid` `VusAbs` `VudAbs` `VubAbs` `VcbAbs`	—	`cd_of_ud_us_ub_cb_tb` `Vabs_sq_add_neq_zero`
`cs_of_fstRowThdColRealCond` 📖	mathematical	`FstRowThdColRealCond`	`VtbAbs` `CKMMatrix` `CKMMatrixSetoid` `VudAbs` `VusAbs` `VubAbs` `VcbAbs`	—	`cs_of_ud_us_ub_cb_tb` `Vabs_sq_add_neq_zero`
`fstRowThdColRealCond_holds_up_to_equiv` 📖	mathematical	—	`CKMMatrix` `CKMMatrixSetoid` `FstRowThdColRealCond`	—	`uRow_cross_cRow_eq_tRow` `phaseShiftApply.equiv` `shift_ud_phase_zero` `shift_us_phase_zero` `shift_cb_phase_zero` `shift_tb_phase_zero` `shift_cross_product_phase_zero`
`fstRowThdColRealCond_shift_solution` 📖	—	—	—	—	—
`shift_cb_phase_zero` 📖	mathematical	—	`phaseShiftApply` `VcbAbs` `CKMMatrix` `CKMMatrixSetoid`	—	`phaseShiftApply.cb`
`shift_cd_phase_pi` 📖	mathematical	—	`phaseShiftApply` `VcdAbs` `CKMMatrix` `CKMMatrixSetoid`	—	`phaseShiftApply.cd`
`shift_cross_product_phase_zero` 📖	mathematical	`uRow` `cRow` `tRow`	`phaseShiftApply`	—	`phaseShiftApply.ucCross_fst` `phaseShiftApply.td` `phaseShiftApply.ucCross_snd` `phaseShiftApply.ts` `phaseShiftApply.ucCross_thd` `phaseShiftApply.tb`
`shift_cs_phase_zero` 📖	mathematical	—	`phaseShiftApply` `VcsAbs` `CKMMatrix` `CKMMatrixSetoid`	—	`phaseShiftApply.cs`
`shift_tb_phase_zero` 📖	mathematical	—	`phaseShiftApply` `VtbAbs` `CKMMatrix` `CKMMatrixSetoid`	—	`phaseShiftApply.tb`
`shift_ub_phase_zero` 📖	mathematical	—	`phaseShiftApply` `VubAbs` `CKMMatrix` `CKMMatrixSetoid`	—	`phaseShiftApply.ub`
`shift_ud_phase_zero` 📖	mathematical	—	`phaseShiftApply` `VudAbs` `CKMMatrix` `CKMMatrixSetoid`	—	`phaseShiftApply.ud`
`shift_us_phase_zero` 📖	mathematical	—	`phaseShiftApply` `VusAbs` `CKMMatrix` `CKMMatrixSetoid`	—	`phaseShiftApply.us`
`ubOnePhaseCond_hold_up_to_equiv_of_ub_one` 📖	mathematical	`FstRowThdColRealCond`	`CKMMatrix` `CKMMatrixSetoid` `ubOnePhaseCond`	—	`phaseShiftApply.equiv` `cb_eq_zero_of_ud_us_zero` `shift_ub_phase_zero` `ud_us_neq_zero_iff_ub_neq_one` `shift_cross_product_phase_zero` `shift_cd_phase_pi` `shift_cs_phase_zero` `cs_of_ud_us_zero`
`ubOnePhaseCond_shift_solution` 📖	—	—	—	—	—

---

← Back to Index