structure
definition
T11Cert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.CKMGeometry on GitHub at line 187.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
184/-! ## Certificate -/
185
186/-- T11 Certificate: V_cb from cube edge geometry. -/
187structure T11Cert where
188 /-- V_cb = 1/(2*12) = 1/24 from cube edges. -/
189 geometric_origin : V_cb_geom = 1 / (2 * cube_edges 3)
190 /-- The prediction matches experiment within uncertainty. -/
191 matches_pdg : abs (V_cb_pred - V_cb_exp) < V_cb_err
192
193/-- The T11 certificate (for V_cb) is verified. -/
194def t11_V_cb_verified : T11Cert where
195 geometric_origin := V_cb_from_cube_edges
196 matches_pdg := V_cb_match
197
198end CKMGeometry
199end Physics
200end IndisputableMonolith