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)
84def V_cb_from_bridge (B : RSBridge L) : ℚ := 1 / B.edgeDual
proof body
Definition body.
85
86/-- V_cb = 1/24 for canonical bridge -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (10)
Lean names referenced from this declaration's body.
-
bridge
in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
decl_use
-
canonical
in IndisputableMonolith.Foundation.ArithmeticOf
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
canonical
in IndisputableMonolith.Gap45.Beat
decl_use
-
canonical
in IndisputableMonolith.NavierStokes.RM2U.NonParasitism
decl_use
-
V_cb
in IndisputableMonolith.Physics.CKM
decl_use
-
L
in IndisputableMonolith.Recognition
decl_use
-
L
in IndisputableMonolith.Recognition.Cycle3
decl_use
-
RSBridge
in IndisputableMonolith.RecogSpec.RSBridge
decl_use
-
V_cb
in IndisputableMonolith.StandardModel.CKMMatrix
decl_use