`IndisputableMonolith.Experimental.MuonGMinusTwoStructure`

IndisputableMonolith/Experimental/MuonGMinusTwoStructure.lean · 21 lines · 3 declarations

Explainer status: ready · generated 2026-05-13 13:24:33.407472+00:00

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace Experimental
   6namespace MuonGMinusTwoStructure
   7
   8open Constants
   9
  10def muon_g_minus_two_from_ledger : Prop := 0 < phi
  11
  12theorem muon_g_minus_two_structure : muon_g_minus_two_from_ledger := phi_pos
  13
  14/-- Muon g-2 structure implies positivity of `phi`. -/
  15theorem muon_g_minus_two_implies_phi_pos (h : muon_g_minus_two_from_ledger) : 0 < phi :=
  16  h
  17
  18end MuonGMinusTwoStructure
  19end Experimental
  20end IndisputableMonolith
  21

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