Basic

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

Statistics

Metric	Count
Definitions `CKMMatrix`, `Rcdcb`, `Rcscb`, `Rubud`, `Rubus`, `Rudus`, `Rusud`, `cb_element`, `cd_cb_ratio`, `cd_element`, `cs_cb_ratio`, `cs_element`, `tb_element`, `td_element`, `ts_element`, `ub_element`, `ub_ud_ratio`, `ub_us_ratio`, `ud_element`, `ud_us_ratio`, `us_element`, `us_ud_ratio`, `CKMMatrixSetoid`, `PhaseShiftRelation`, `VAbs`, `VAbs'`, `VcbAbs`, `VcdAbs`, `VcsAbs`, `VtbAbs`, `VtdAbs`, `VtsAbs`, `VubAbs`, `VudAbs`, `VusAbs`, `phaseShift`, `phaseShiftApply`, `phaseShiftMatrix`	38
Theorems `Rcdcb_mul_cb`, `Rcscb_mul_cb`, `CKMMatrix_ext`, `VAbs'_equiv`, `cb`, `cd`, `cs`, `equiv`, `tb`, `td`, `ts`, `ub`, `ud`, `us`, `phaseShiftApply_coe`, `phaseShiftMatrix_mul`, `phaseShiftMatrix_one`, `phaseShiftMatrix_star`, `phaseShiftRelation_equiv`, `phaseShiftRelation_refl`, `phaseShiftRelation_symm`, `phaseShiftRelation_trans`, `phaseShift_coe`, `phaseShift_coe_matrix`	24
Total	62

CKMMatrix

Definitions

Name	Category	Theorems
`Rcdcb` 📖	CompOp	1 math math: `Rcdcb_mul_cb`
`Rcscb` 📖	CompOp	1 math math: `Rcscb_mul_cb`
`Rubud` 📖	CompOp	—
`Rubus` 📖	CompOp	—
`Rudus` 📖	CompOp	—
`Rusud` 📖	CompOp	—
`cb_element` 📖	CompOp	—
`cd_cb_ratio` 📖	CompOp	—
`cd_element` 📖	CompOp	—
`cs_cb_ratio` 📖	CompOp	—
`cs_element` 📖	CompOp	—
`tb_element` 📖	CompOp	—
`td_element` 📖	CompOp	—
`ts_element` 📖	CompOp	—
`ub_element` 📖	CompOp	—
`ub_ud_ratio` 📖	CompOp	—
`ub_us_ratio` 📖	CompOp	—
`ud_element` 📖	CompOp	—
`ud_us_ratio` 📖	CompOp	—
`us_element` 📖	CompOp	—
`us_ud_ratio` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Rcdcb_mul_cb` 📖	mathematical	—	`Rcdcb`	—	`Rcdcb.eq_1`
`Rcscb_mul_cb` 📖	mathematical	—	`Rcscb`	—	`Rcscb.eq_1`

(root)

Definitions

Name	Category	Theorems
`CKMMatrix` 📖	CompOp	25 math math: `CKMMatrix.ubOnePhaseCond_hold_up_to_equiv_of_ub_one`, `CKMMatrix.cd_of_fstRowThdColRealCond`, `standParam.mulExpδ₁₃_on_param_abs`, `CKMMatrix.shift_ub_phase_zero`, `Vs_zero_iff_cos_sin_zero`, `standParam.mulExpδ₁₃_on_param_neq_zero_arg`, `CKMMatrix.cs_of_fstRowThdColRealCond`, `CKMMatrix.shift_ud_phase_zero`, `CKMMatrix.shift_us_phase_zero`, `standParam.VusVubVcdSq_eq`, `standParam.exists_for_CKMatrix`, `standParam.mulExpδ₁₃_eq`, `CKMMatrix.shift_cd_phase_pi`, `standParam.mulExpδ₁₃_on_param_eq_zero_iff`, `standParam.eq_standardParameterization_δ₃`, `CKMMatrix.shift_tb_phase_zero`, `standParam.eq_standParam_of_fstRowThdColRealCond`, `standParam.eq_standParam_of_ubOnePhaseCond`, `CKMMatrix.fstRowThdColRealCond_holds_up_to_equiv`, `CKMMatrix.cs_of_ud_us_zero`, `CKMMatrix.shift_cs_phase_zero`, `phaseShiftApply.equiv`, `standParam.exists_δ₁₃`, `CKMMatrix.shift_cb_phase_zero`, `standParam.mulExpδ₁₃_on_param_δ₁₃`
`CKMMatrixSetoid` 📖	CompOp	25 math math: `CKMMatrix.ubOnePhaseCond_hold_up_to_equiv_of_ub_one`, `CKMMatrix.cd_of_fstRowThdColRealCond`, `standParam.mulExpδ₁₃_on_param_abs`, `CKMMatrix.shift_ub_phase_zero`, `Vs_zero_iff_cos_sin_zero`, `standParam.mulExpδ₁₃_on_param_neq_zero_arg`, `CKMMatrix.cs_of_fstRowThdColRealCond`, `CKMMatrix.shift_ud_phase_zero`, `CKMMatrix.shift_us_phase_zero`, `standParam.VusVubVcdSq_eq`, `standParam.exists_for_CKMatrix`, `standParam.mulExpδ₁₃_eq`, `CKMMatrix.shift_cd_phase_pi`, `standParam.mulExpδ₁₃_on_param_eq_zero_iff`, `standParam.eq_standardParameterization_δ₃`, `CKMMatrix.shift_tb_phase_zero`, `standParam.eq_standParam_of_fstRowThdColRealCond`, `standParam.eq_standParam_of_ubOnePhaseCond`, `CKMMatrix.fstRowThdColRealCond_holds_up_to_equiv`, `CKMMatrix.cs_of_ud_us_zero`, `CKMMatrix.shift_cs_phase_zero`, `phaseShiftApply.equiv`, `standParam.exists_δ₁₃`, `CKMMatrix.shift_cb_phase_zero`, `standParam.mulExpδ₁₃_on_param_δ₁₃`
`PhaseShiftRelation` 📖	MathDef	2 math math: `phaseShiftRelation_refl`, `phaseShiftRelation_equiv`
`VAbs` 📖	CompOp	4 math math: `CKMMatrix.VAbs_sum_sq_row_eq_one`, `CKMMatrix.VAbs_leq_one`, `CKMMatrix.VAbs_ge_zero`, `CKMMatrix.VAbs_sum_sq_col_eq_one`
`VAbs'` 📖	CompOp	1 math math: `VAbs'_equiv`
`VcbAbs` 📖	CompOp	8 math math: `CKMMatrix.cd_of_fstRowThdColRealCond`, `Vs_zero_iff_cos_sin_zero`, `CKMMatrix.cs_of_fstRowThdColRealCond`, `CKMMatrix.VcbAbs_sq_add_VtbAbs_sq`, `VcbAbs_eq_S₂₃_mul_C₁₃`, `standParam.mulExpδ₁₃_on_param_eq_zero_iff`, `CKMMatrix.shift_cb_phase_zero`, `S₂₃_of_Vub_neq_one`
`VcdAbs` 📖	CompOp	3 math math: `CKMMatrix.shift_cd_phase_pi`, `CKMMatrix.cs_of_ud_us_zero`, `S₂₃_of_Vub_eq_one`
`VcsAbs` 📖	CompOp	2 math math: `CKMMatrix.cs_of_ud_us_zero`, `CKMMatrix.shift_cs_phase_zero`
`VtbAbs` 📖	CompOp	8 math math: `CKMMatrix.cd_of_fstRowThdColRealCond`, `Vs_zero_iff_cos_sin_zero`, `CKMMatrix.cs_of_fstRowThdColRealCond`, `VtbAbs_eq_C₂₃_mul_C₁₃`, `CKMMatrix.VcbAbs_sq_add_VtbAbs_sq`, `C₂₃_of_Vub_neq_one`, `standParam.mulExpδ₁₃_on_param_eq_zero_iff`, `CKMMatrix.shift_tb_phase_zero`
`VtdAbs` 📖	CompOp	—
`VtsAbs` 📖	CompOp	—
`VubAbs` 📖	CompOp	9 math math: `CKMMatrix.cd_of_fstRowThdColRealCond`, `CKMMatrix.shift_ub_phase_zero`, `Vs_zero_iff_cos_sin_zero`, `CKMMatrix.cs_of_fstRowThdColRealCond`, `VubAbs_eq_S₁₃`, `CKMMatrix.VcbAbs_sq_add_VtbAbs_sq`, `standParam.mulExpδ₁₃_on_param_eq_zero_iff`, `CKMMatrix.VudAbs_sq_add_VusAbs_sq`, `VubAbs_of_cos_θ₁₃_zero`
`VudAbs` 📖	CompOp	11 math math: `C₁₃_eq_add_sq`, `CKMMatrix.cd_of_fstRowThdColRealCond`, `Vs_zero_iff_cos_sin_zero`, `CKMMatrix.cs_of_fstRowThdColRealCond`, `CKMMatrix.shift_ud_phase_zero`, `C₂₃_of_Vub_neq_one`, `VudAbs_eq_C₁₂_mul_C₁₃`, `standParam.mulExpδ₁₃_on_param_eq_zero_iff`, `CKMMatrix.VudAbs_sq_add_VusAbs_sq`, `C₁₂_eq_Vud_div_sqrt`, `S₂₃_of_Vub_neq_one`
`VusAbs` 📖	CompOp	11 math math: `C₁₃_eq_add_sq`, `CKMMatrix.cd_of_fstRowThdColRealCond`, `Vs_zero_iff_cos_sin_zero`, `CKMMatrix.cs_of_fstRowThdColRealCond`, `CKMMatrix.shift_us_phase_zero`, `C₂₃_of_Vub_neq_one`, `standParam.mulExpδ₁₃_on_param_eq_zero_iff`, `CKMMatrix.VudAbs_sq_add_VusAbs_sq`, `C₁₂_eq_Vud_div_sqrt`, `VusAbs_eq_S₁₂_mul_C₁₃`, `S₂₃_of_Vub_neq_one`
`phaseShift` 📖	CompOp	2 math math: `phaseShift_coe`, `phaseShift_coe_matrix`
`phaseShiftApply` 📖	CompOp	22 math math: `phaseShiftApply.td`, `CKMMatrix.shift_ub_phase_zero`, `phaseShiftApply.uRow_mul`, `CKMMatrix.shift_ud_phase_zero`, `CKMMatrix.shift_us_phase_zero`, `phaseShiftApply.cRow_mul`, `phaseShiftApply.us`, `phaseShiftApply.cs`, `phaseShiftApply.ub`, `phaseShiftApply.ts`, `CKMMatrix.shift_cd_phase_pi`, `phaseShiftApply_coe`, `phaseShiftApply.tb`, `phaseShiftApply.cb`, `CKMMatrix.shift_tb_phase_zero`, `phaseShiftApply.tRow_mul`, `CKMMatrix.shift_cross_product_phase_zero`, `phaseShiftApply.ud`, `CKMMatrix.shift_cs_phase_zero`, `phaseShiftApply.equiv`, `CKMMatrix.shift_cb_phase_zero`, `phaseShiftApply.cd`
`phaseShiftMatrix` 📖	CompOp	4 math math: `phaseShiftMatrix_one`, `phaseShiftMatrix_star`, `phaseShiftMatrix_mul`, `phaseShift_coe_matrix`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`CKMMatrix_ext` 📖	—	—	—	—	—
`VAbs'_equiv` 📖	mathematical	`CKMMatrix` `CKMMatrixSetoid`	`VAbs'`	—	—
`phaseShiftApply_coe` 📖	mathematical	—	`phaseShiftApply`	—	—
`phaseShiftMatrix_mul` 📖	mathematical	—	`phaseShiftMatrix`	—	—
`phaseShiftMatrix_one` 📖	mathematical	—	`phaseShiftMatrix`	—	—
`phaseShiftMatrix_star` 📖	mathematical	—	`phaseShiftMatrix`	—	—
`phaseShiftRelation_equiv` 📖	mathematical	—	`PhaseShiftRelation`	—	`phaseShiftRelation_refl` `phaseShiftRelation_symm` `phaseShiftRelation_trans`
`phaseShiftRelation_refl` 📖	mathematical	—	`PhaseShiftRelation`	—	`phaseShiftMatrix_one`
`phaseShiftRelation_symm` 📖	—	`PhaseShiftRelation`	—	—	`phaseShiftMatrix_mul` `phaseShiftMatrix_one`
`phaseShiftRelation_trans` 📖	—	`PhaseShiftRelation`	—	—	`phaseShiftMatrix_mul`
`phaseShift_coe` 📖	mathematical	—	`phaseShift`	—	—
`phaseShift_coe_matrix` 📖	mathematical	—	`phaseShift` `phaseShiftMatrix`	—	—

phaseShiftApply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cb` 📖	mathematical	—	`phaseShiftApply`	—	—
`cd` 📖	mathematical	—	`phaseShiftApply`	—	—
`cs` 📖	mathematical	—	`phaseShiftApply`	—	—
`equiv` 📖	mathematical	—	`CKMMatrix` `CKMMatrixSetoid` `phaseShiftApply`	—	—
`tb` 📖	mathematical	—	`phaseShiftApply`	—	—
`td` 📖	mathematical	—	`phaseShiftApply`	—	—
`ts` 📖	mathematical	—	`phaseShiftApply`	—	—
`ub` 📖	mathematical	—	`phaseShiftApply`	—	—
`ud` 📖	mathematical	—	`phaseShiftApply`	—	—
`us` 📖	mathematical	—	`phaseShiftApply`	—	—

---

← Back to Index