No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
33noncomputable def V_ub : ℝ := V_ub_pred
proof body
Definition body.
34
35-- Derived diagonal elements (approximate unitarity)
used by (17)
From the project-wide theorem graph. These declarations reference this one in their body.
-
torsion_differences
in IndisputableMonolith.Particles.CKMDerivation
decl_use
-
jarlskog_witness_pos
in IndisputableMonolith.Physics.CKM
decl_use
-
s13_w
in IndisputableMonolith.Physics.CKM
decl_use
-
alpha_upper_bound
in IndisputableMonolith.Physics.CKMGeometry
decl_use
-
V_ub_err
in IndisputableMonolith.Physics.CKMGeometry
decl_use
-
vcb_derived
in IndisputableMonolith.Physics.MixingDerivation
decl_use
-
mk_toList
in IndisputableMonolith.RecogSpec.ObservablePayloads
decl_use
-
canonical_V_cb
in IndisputableMonolith.RecogSpec.RSBridge
decl_use
-
canonical_V_us
in IndisputableMonolith.RecogSpec.RSBridge
decl_use
-
RSBridge
in IndisputableMonolith.RecogSpec.RSBridge
decl_use
-
V_cb_real
in IndisputableMonolith.RecogSpec.RSBridge
decl_use
-
cp_violation_small
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
experimentalValues
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
gen12_mixing_largest
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
predictions
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
unitarity_triangle_valid
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
-
V_ub
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use
depends on (2)
Lean names referenced from this declaration's body.
-
V_ub_pred
in IndisputableMonolith.Physics.CKMGeometry
decl_use
-
V_ub
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use