`IndisputableMonolith.Experimental.MiniBooNELSNDStructure`

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

Explainer status: ready · generated 2026-06-07 12:22:14.580910+00:00

   1import Mathlib
   2import IndisputableMonolith.Experimental.FlybyAnomalyStructure
   3
   4namespace IndisputableMonolith
   5namespace Experimental
   6namespace MiniBooNELSNDStructure
   7
   8open FlybyAnomalyStructure
   9
  10def miniboone_lsnd_from_ledger : Prop := flyby_anomaly_from_ledger
  11
  12theorem miniboone_lsnd_structure : miniboone_lsnd_from_ledger := flyby_anomaly_structure
  13
  14/-- MiniBooNE/LSND structure implies flyby-anomaly structural input. -/
  15theorem miniboone_lsnd_implies_flyby (h : miniboone_lsnd_from_ledger) :
  16    flyby_anomaly_from_ledger :=
  17  h
  18
  19end MiniBooNELSNDStructure
  20end Experimental
  21end IndisputableMonolith
  22

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