`edgeDualCount`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogSpec.RSBridge
domain: RecogSpec
line: 45 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogSpec.RSBridge on GitHub at line 45.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  42def cubeEdges : ℕ := 12
  43
  44/-- The edge-dual count (2 × cube edges = 24) -/
  45def edgeDualCount : ℕ := 2 * cubeEdges
  46
  47theorem edgeDualCount_eq : edgeDualCount = 24 := rfl
  48
  49/-- The golden projection exponent for Cabibbo angle -/
  50def cabibboProjection : ℤ := -3
  51
  52/-- The radiative correction coefficient -/
  53def radiativeCoeff : ℚ := 3/2
  54
  55/-! ## RSBridge Structure -/
  56
  57/-- A bridge with geometric coupling structure for mixing angles.
  58
  59This extends the minimal `Bridge` with fields that determine the CKM matrix
  60from geometric structure rather than arbitrary parameters.
  61-/
  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
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.