def
definition
g2FromLoops
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RecogSpec.BridgeDerivation on GitHub at line 48.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
45
46The bridge carries a structural `loopOrder` (default 5).
47g-2 = 1/φ^{loopOrder} for the canonical bridge. -/
48def g2FromLoops (B : RSBridge L) (φ : ℝ) : ℝ :=
49 1 / (φ ^ B.loopOrder)
50
51/-- For the canonical bridge, V_cb = 1/24. -/
52theorem mixingFromCycles_Vcb_canonical (B : RSBridge L) (hB : B.edgeDual = 24) :
53 V_cb_from_bridge B = 1 / 24 := by
54 simp [V_cb_from_bridge, hB]
55
56/-- Canonical bridge g-2 equals 1/φ^5. -/
57theorem g2FromLoops_canonical (B : RSBridge L) (φ : ℝ)
58 (hLoop : B.loopOrder = 5) :
59 g2FromLoops B φ = 1 / (φ ^ 5) := by
60 simp only [g2FromLoops, hLoop]
61
62/-- The canonical bridge yields g-2 = 1/φ^5. -/
63theorem canonical_g2FromLoops (φ : ℝ) :
64 g2FromLoops (canonicalRSBridge L) φ = 1 / (φ ^ 5) := by
65 simp [g2FromLoops, canonicalRSBridge]
66
67end
68
69end RecogSpec
70end IndisputableMonolith