def definition def or abbrev

`mixingFromCycles`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  39def mixingFromCycles (B : RSBridge L) (φ : ℝ) : CkmMixingAngles :=

proof body

Definition body.

  40  ⟨ V_us_from_bridge B φ,
  41    V_cb_real B,
  42    V_ub_from_bridge B ⟩
  43
  44/-- g-2 muon derived from bridge loop structure.
  45
  46The bridge carries a structural `loopOrder` (default 5).
  47g-2 = 1/φ^{loopOrder} for the canonical bridge. -/

depends on (15)

Lean names referenced from this declaration's body.

default in IndisputableMonolith.Chemistry.PeriodicTable decl_use
bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
default in IndisputableMonolith.Config.Flags decl_use
canonical in IndisputableMonolith.Foundation.ArithmeticOf decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
canonical in IndisputableMonolith.Gap45.Beat decl_use
canonical in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use
CkmMixingAngles in IndisputableMonolith.RecogSpec.ObservablePayloads decl_use
RSBridge in IndisputableMonolith.RecogSpec.RSBridge decl_use
V_cb_real in IndisputableMonolith.RecogSpec.RSBridge decl_use
V_ub_from_bridge in IndisputableMonolith.RecogSpec.RSBridge decl_use
V_us_from_bridge in IndisputableMonolith.RecogSpec.RSBridge decl_use