pith. machine review for the scientific record. sign in
structure definition def or abbrev

RSBridge

show as:
view Lean formalization →

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)

  62structure RSBridge (L : RSLedger) where
  63  /-- The underlying bridge -/
  64  toBridge : Bridge L.toLedger
  65  /-- Edge count of dual structure (default: 24) -/
  66  edgeDual : ℕ := edgeDualCount

proof body

Definition body.

  67  /-- Fine structure exponent for V_ub -/
  68  alphaExponent : ℝ
  69  /-- Golden projection exponent for Cabibbo (default: -3) -/
  70  phiProj : ℤ := cabibboProjection
  71  /-- Radiative correction coefficient (default: 3/2) -/
  72  radCoeff : ℚ := radiativeCoeff
  73  /-- Loop order exponent for g-2 derivation (default: 5) -/
  74  loopOrder : ℕ := 5
  75
  76/-! ## Mixing Angles from Bridge Structure -/
  77
  78variable {L : RSLedger}
  79
  80/-- V_cb from edge-dual geometry: 1/24
  81
  82This is EXACT — the mixing is the inverse of the dual edge count.
  83-/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (26)

Lean names referenced from this declaration's body.