`IndisputableMonolith.Experimental.BMesonAnomaliesStructure`

IndisputableMonolith/Experimental/BMesonAnomaliesStructure.lean · 22 lines · 3 declarations

Explainer status: ready · generated 2026-05-15 23:25:14.270702+00:00

   1import Mathlib
   2import IndisputableMonolith.Experimental.MuonGMinusTwoStructure
   3
   4namespace IndisputableMonolith
   5namespace Experimental
   6namespace BMesonAnomaliesStructure
   7
   8open MuonGMinusTwoStructure
   9
  10def b_meson_anomalies_from_ledger : Prop := muon_g_minus_two_from_ledger
  11
  12theorem b_meson_anomalies_structure : b_meson_anomalies_from_ledger := muon_g_minus_two_structure
  13
  14/-- B-meson anomaly structure implies the muon g-2 structural input. -/
  15theorem b_meson_implies_muon_g_minus_two (h : b_meson_anomalies_from_ledger) :
  16    muon_g_minus_two_from_ledger :=
  17  h
  18
  19end BMesonAnomaliesStructure
  20end Experimental
  21end IndisputableMonolith
  22

source mirrored from github.com/jonwashburn/shape-of-logic