Documentation Verification Report

Basic

📁 Source: PhysLean/Particles/NeutrinoPhysics/Basic.lean

Statistics

Metric	Count
Definitions `PMNS_dirac_equivalence`, `diagPhase`, `diagPhase_unitary`, `leptonPhaseShift`, `majoranaPhaseMatrix`, `neutrinoPhaseShift`	6
Theorems `PMNS_dirac_equivalence_refl`, `PMNS_dirac_equivalence_symm`, `PMNS_dirac_equivalence_trans`, `diagPhaseShift_coe_matrix`, `diagPhase_mul`, `diagPhase_star`, `diagPhase_zero`, `diagPhase_zero_eq`	8
Total	14

(root)

Definitions

Name	Category	Theorems
`PMNS_dirac_equivalence` 📖	MathDef	1 math math: `PMNS_dirac_equivalence_refl`
`diagPhase` 📖	CompOp	5 math math: `diagPhase_zero_eq`, `diagPhase_zero`, `diagPhase_star`, `diagPhase_mul`, `diagPhaseShift_coe_matrix`
`diagPhase_unitary` 📖	CompOp	1 math math: `diagPhaseShift_coe_matrix`
`leptonPhaseShift` 📖	CompOp	—
`majoranaPhaseMatrix` 📖	CompOp	—
`neutrinoPhaseShift` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`PMNS_dirac_equivalence_refl` 📖	mathematical	—	`PMNS_dirac_equivalence`	—	`diagPhase_zero`
`PMNS_dirac_equivalence_symm` 📖	—	`PMNS_dirac_equivalence`	—	—	`diagPhase_mul` `diagPhase_zero_eq` `diagPhase_zero`
`PMNS_dirac_equivalence_trans` 📖	—	`PMNS_dirac_equivalence`	—	—	`diagPhase_mul`
`diagPhaseShift_coe_matrix` 📖	mathematical	—	`diagPhase_unitary` `diagPhase`	—	—
`diagPhase_mul` 📖	mathematical	—	`diagPhase`	—	—
`diagPhase_star` 📖	mathematical	—	`diagPhase`	—	—
`diagPhase_zero` 📖	mathematical	—	`diagPhase`	—	—
`diagPhase_zero_eq` 📖	mathematical	—	`diagPhase`	—	—

---

← Back to Index